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