# 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

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
```