Theory Lerch_Lemma

section ‹Lerch Lemma›
theory Lerch_Lemma
  imports
     "HOL-Analysis.Analysis"
begin

text ‹The main tool to prove uniqueness of the Laplace transform.›

lemma lerch_lemma_real:
  fixes h::"real ⇒ real"
  assumes h_cont[continuous_intros]: "continuous_on {0 .. 1} h"
  assumes int_0: "⋀n. ((λu. u ^ n * h u) has_integral 0) {0 .. 1}"
  assumes u: "0 ≤ u" "u ≤ 1"
  shows "h u = 0"
proof -
  from Stone_Weierstrass_uniform_limit[OF compact_Icc h_cont]
  obtain g where g: "uniform_limit {0..1} g h sequentially" "polynomial_function (g n)" for n
    by blast
  then have rpf_g: "real_polynomial_function (g n)" for n
    by (simp add: real_polynomial_function_eq)

  let ?P = "λn x. h x * g n x"
  have continuous_on_g[continuous_intros]: "continuous_on s (g n)" for s n
    by (rule continuous_on_polymonial_function) fact
  have P_cont: "continuous_on {0 .. 1} (?P n)" for n
    by (auto intro!: continuous_intros)
  have "uniform_limit {0 .. 1} (λn x. h x * g n x) (λx. h x * h x) sequentially"
    by (auto intro!: uniform_limit_intros g assms compact_imp_bounded compact_continuous_image)

  from uniform_limit_integral[OF this P_cont]
  obtain I J where
    I: "(⋀n. (?P n has_integral I n) {0..1})"
    and J: "((λx. h x * h x) has_integral J) {0..1}"
    and IJ: "I ⇢ J"
    by auto

  have "(?P n has_integral 0) {0..1}" for n
  proof -
    from real_polynomial_function_imp_sum[OF rpf_g]
    obtain gn ga where "g n = (λx. ∑i≤gn. ga i * x ^ i)" by metis
    then have "?P n x = (∑i≤gn. x ^ i * h x * ga i)" for x
      by (auto simp: sum_distrib_left algebra_simps)
    moreover have "((λx. … x) has_integral 0) {0 .. 1}"
      by (auto intro!: has_integral_sum[THEN has_integral_eq_rhs] has_integral_mult_left assms)
    ultimately show ?thesis by simp
  qed
  with I have "I n = 0" for n
    using has_integral_unique by blast
  with IJ J have "((λx. h x * h x) has_integral 0) (cbox 0 1)"
    by (metis (full_types) LIMSEQ_le_const LIMSEQ_le_const2 box_real(2) dual_order.antisym order_refl)
  with _ _ have "h u * h u = 0"
    by (rule has_integral_0_cbox_imp_0) (auto intro!: continuous_intros u)
  then show "h u = 0"
    by simp
qed

lemma lerch_lemma:
  fixes h::"real ⇒ 'a::euclidean_space"
  assumes [continuous_intros]: "continuous_on {0 .. 1} h"
  assumes int_0: "⋀n. ((λu. u ^ n *⇩R h u) has_integral 0) {0 .. 1}"
  assumes u: "0 ≤ u" "u ≤ 1"
  shows "h u = 0"
proof (rule euclidean_eqI)
  fix b::'a assume "b ∈ Basis"
  have "continuous_on {0 .. 1} (λx. h x ∙ b)"
    by (auto intro!: continuous_intros)
  moreover
  from ‹b ∈ Basis› have "((λu. u ^ n * (h u ∙ b)) has_integral 0) {0 .. 1}" for n
    using int_0[of n] has_integral_componentwise_iff[of "λu. u ^ n *⇩R h u" 0 "{0 .. 1}"]
    by auto
  moreover note u
  ultimately show "h u ∙ b = 0 ∙ b"
    unfolding inner_zero_left
    by (rule lerch_lemma_real)
qed

end