section ‹Various preliminary material› theory Zeta_Library imports "HOL-Complex_Analysis.Complex_Analysis" "HOL-Real_Asymp.Real_Asymp" "Dirichlet_Series.Dirichlet_Series_Analysis" begin subsection ‹Facts about limits› lemma at_within_altdef: "at x within A = (INF S∈{S. open S ∧ x ∈ S}. principal (S ∩ (A - {x})))" unfolding at_within_def nhds_def inf_principal [symmetric] by (subst INF_inf_distrib [symmetric]) (auto simp: INF_constant) lemma tendsto_at_left_realI_sequentially: fixes f :: "real ⇒ 'b::first_countable_topology" assumes *: "⋀X. filterlim X (at_left c) sequentially ⟹ (λn. f (X n)) ⇢ y" shows "(f ⤏ y) (at_left c)" proof - obtain A where A: "decseq A" "open (A n)" "y ∈ A n" "nhds y = (INF n. principal (A n))" for n by (rule nhds_countable[of y]) (rule that) have "∀m. ∃d<c. ∀x∈{d<..<c}. f x ∈ A m" proof (rule ccontr) assume "¬ (∀m. ∃d<c. ∀x∈{d<..<c}. f x ∈ A m)" then obtain m where **: "⋀d. d < c ⟹ ∃x∈{d<..<c}. f x ∉ A m" by auto have "∃X. ∀n. (f (X n) ∉ A m ∧ X n < c) ∧ X (Suc n) > c - max 0 ((c - X n) / 2)" proof (intro dependent_nat_choice, goal_cases) case 1 from **[of "c - 1"] show ?case by auto next case (2 x n) with **[of "c - max 0 (c - x) / 2"] show ?case by force qed then obtain X where X: "⋀n. f (X n) ∉ A m" "⋀n. X n < c" "⋀n. X (Suc n) > c - max 0 ((c - X n) / 2)" by auto (metis diff_gt_0_iff_gt half_gt_zero_iff max.absorb3 max.commute) have X_ge: "X n ≥ c - (c - X 0) / 2 ^ n" for n proof (induction n) case (Suc n) have "c - (c - X 0) / 2 ^ Suc n = c - (c - (c - (c - X 0) / 2 ^ n)) / 2" by simp also have "c - (c - (c - (c - X 0) / 2 ^ n)) / 2 ≤ c - (c - X n) / 2" by (intro diff_left_mono divide_right_mono Suc diff_right_mono) auto also have "… = c - max 0 ((c - X n) / 2)" using X[of n] by (simp add: max_def) also have "… < X (Suc n)" using X[of n] by simp finally show ?case by linarith qed auto have "X ⇢ c" proof (rule tendsto_sandwich) show "eventually (λn. X n ≤ c) sequentially" using X by (intro always_eventually) (auto intro!: less_imp_le) show "eventually (λn. X n ≥ c - (c - X 0) / 2 ^ n) sequentially" using X_ge by (intro always_eventually) auto qed real_asymp+ hence "filterlim X (at_left c) sequentially" by (rule tendsto_imp_filterlim_at_left) (use X in ‹auto intro!: always_eventually less_imp_le›) from topological_tendstoD[OF *[OF this] A(2, 3), of m] X(1) show False by auto qed then obtain d where d: "d m < c" "x ∈ {d m<..<c} ⟹ f x ∈ A m" for m x by metis have ***: "at_left c = (INF S∈{S. open S ∧ c ∈ S}. principal (S ∩ {..<c}))" by (simp add: at_within_altdef) from d show ?thesis unfolding *** A using A(1,2) by (intro filterlim_base[of _ "λm. {d m<..}"]) auto qed lemma shows at_right_PInf [simp]: "at_right (∞ :: ereal) = bot" and at_left_MInf [simp]: "at_left (-∞ :: ereal) = bot" proof - have "{(∞::ereal)<..} = {}" "{..<-(∞::ereal)} = {}" by auto thus "at_right (∞ :: ereal) = bot" "at_left (-∞ :: ereal) = bot" by (simp_all add: at_within_def) qed lemma tendsto_at_left_erealI_sequentially: fixes f :: "ereal ⇒ 'b::first_countable_topology" assumes *: "⋀X. filterlim X (at_left c) sequentially ⟹ (λn. f (X n)) ⇢ y" shows "(f ⤏ y) (at_left c)" proof (cases c) case [simp]: PInf have "((λx. f (ereal x)) ⤏ y) at_top" using assms by (intro tendsto_at_topI_sequentially assms) (simp_all flip: ereal_tendsto_simps add: o_def filterlim_at) thus ?thesis by (simp add: at_left_PInf filterlim_filtermap) next case [simp]: MInf thus ?thesis by auto next case [simp]: (real c') have "((λx. f (ereal x)) ⤏ y) (at_left c')" proof (intro tendsto_at_left_realI_sequentially assms) fix X assume *: "filterlim X (at_left c') sequentially" show "filterlim (λn. ereal (X n)) (at_left c) sequentially" by (rule filterlim_compose[OF _ *]) (simp add: sequentially_imp_eventually_within tendsto_imp_filterlim_at_left) qed thus ?thesis by (simp add: at_left_ereal filterlim_filtermap) qed lemma tendsto_at_right_realI_sequentially: fixes f :: "real ⇒ 'b::first_countable_topology" assumes *: "⋀X. filterlim X (at_right c) sequentially ⟹ (λn. f (X n)) ⇢ y" shows "(f ⤏ y) (at_right c)" proof - obtain A where A: "decseq A" "open (A n)" "y ∈ A n" "nhds y = (INF n. principal (A n))" for n by (rule nhds_countable[of y]) (rule that) have "∀m. ∃d>c. ∀x∈{c<..<d}. f x ∈ A m" proof (rule ccontr) assume "¬ (∀m. ∃d>c. ∀x∈{c<..<d}. f x ∈ A m)" then obtain m where **: "⋀d. d > c ⟹ ∃x∈{c<..<d}. f x ∉ A m" by auto have "∃X. ∀n. (f (X n) ∉ A m ∧ X n > c) ∧ X (Suc n) < c + max 0 ((X n - c) / 2)" proof (intro dependent_nat_choice, goal_cases) case 1 from **[of "c + 1"] show ?case by auto next case (2 x n) with **[of "c + max 0 (x - c) / 2"] show ?case by force qed then obtain X where X: "⋀n. f (X n) ∉ A m" "⋀n. X n > c" "⋀n. X (Suc n) < c + max 0 ((X n - c) / 2)" by auto (metis add.left_neutral half_gt_zero_iff less_diff_eq max.absorb4) have X_le: "X n ≤ c + (X 0 - c) / 2 ^ n" for n proof (induction n) case (Suc n) have "X (Suc n) < c + max 0 ((X n - c) / 2)" by (intro X) also have "… = c + (X n - c) / 2" using X[of n] by (simp add: field_simps max_def) also have "… ≤ c + (c + (X 0 - c) / 2 ^ n - c) / 2" by (intro add_left_mono divide_right_mono Suc diff_right_mono) auto also have "… = c + (X 0 - c) / 2 ^ Suc n" by simp finally show ?case by linarith qed auto have "X ⇢ c" proof (rule tendsto_sandwich) show "eventually (λn. X n ≥ c) sequentially" using X by (intro always_eventually) (auto intro!: less_imp_le) show "eventually (λn. X n ≤ c + (X 0 - c) / 2 ^ n) sequentially" using X_le by (intro always_eventually) auto qed real_asymp+ hence "filterlim X (at_right c) sequentially" by (rule tendsto_imp_filterlim_at_right) (use X in ‹auto intro!: always_eventually less_imp_le›) from topological_tendstoD[OF *[OF this] A(2, 3), of m] X(1) show False by auto qed then obtain d where d: "d m > c" "x ∈ {c<..<d m} ⟹ f x ∈ A m" for m x by metis have ***: "at_right c = (INF S∈{S. open S ∧ c ∈ S}. principal (S ∩ {c<..}))" by (simp add: at_within_altdef) from d show ?thesis unfolding *** A using A(1,2) by (intro filterlim_base[of _ "λm. {..<d m}"]) auto qed lemma tendsto_at_right_erealI_sequentially: fixes f :: "ereal ⇒ 'b::first_countable_topology" assumes *: "⋀X. filterlim X (at_right c) sequentially ⟹ (λn. f (X n)) ⇢ y" shows "(f ⤏ y) (at_right c)" proof (cases c) case [simp]: MInf have "((λx. f (-ereal x)) ⤏ y) at_top" using assms by (intro tendsto_at_topI_sequentially assms) (simp_all flip: uminus_ereal.simps ereal_tendsto_simps add: o_def filterlim_at) thus ?thesis by (simp add: at_right_MInf filterlim_filtermap at_top_mirror) next case [simp]: PInf thus ?thesis by auto next case [simp]: (real c') have "((λx. f (ereal x)) ⤏ y) (at_right c')" proof (intro tendsto_at_right_realI_sequentially assms) fix X assume *: "filterlim X (at_right c') sequentially" show "filterlim (λn. ereal (X n)) (at_right c) sequentially" by (rule filterlim_compose[OF _ *]) (simp add: sequentially_imp_eventually_within tendsto_imp_filterlim_at_right) qed thus ?thesis by (simp add: at_right_ereal filterlim_filtermap) qed proposition analytic_continuation': assumes hol: "f holomorphic_on S" "g holomorphic_on S" and "open S" and "connected S" and "U ⊆ S" and "ξ ∈ S" and "ξ islimpt U" and fU0 [simp]: "⋀z. z ∈ U ⟹ f z = g z" and "w ∈ S" shows "f w = g w" using analytic_continuation[OF holomorphic_on_diff[OF hol] assms(3-7) _ assms(9)] assms(8) by simp subsection ‹Various facts about integrals› lemma continuous_on_imp_set_integrable_cbox: fixes h :: "'a :: euclidean_space ⇒ 'b :: euclidean_space" assumes "continuous_on (cbox a b) h" shows "set_integrable lborel (cbox a b) h" by (simp add: assms borel_integrable_compact set_integrable_def) subsection ‹Uniform convergence of integrals› lemma has_absolute_integral_change_of_variables_1': fixes f :: "real ⇒ real" and g :: "real ⇒ real" assumes S: "S ∈ sets lebesgue" and der_g: "⋀x. x ∈ S ⟹ (g has_field_derivative g' x) (at x within S)" and inj: "inj_on g S" shows "(λx. ¦g' x¦ *⇩R f(g x)) absolutely_integrable_on S ∧ integral S (λx. ¦g' x¦ *⇩R f(g x)) = b ⟷ f absolutely_integrable_on (g ` S) ∧ integral (g ` S) f = b" proof - have "(λx. ¦g' x¦ *⇩R vec (f(g x)) :: real ^ 1) absolutely_integrable_on S ∧ integral S (λx. ¦g' x¦ *⇩R vec (f(g x))) = (vec b :: real ^ 1) ⟷ (λx. vec (f x) :: real ^ 1) absolutely_integrable_on (g ` S) ∧ integral (g ` S) (λx. vec (f x)) = (vec b :: real ^ 1)" using assms unfolding has_real_derivative_iff_has_vector_derivative by (intro has_absolute_integral_change_of_variables_1 assms) auto thus ?thesis by (simp add: absolutely_integrable_on_1_iff integral_on_1_eq) qed lemma uniform_limit_set_lebesgue_integral: fixes f :: "'a ⇒ 'b :: euclidean_space ⇒ 'c :: {banach, second_countable_topology}" assumes "set_integrable lborel X' g" assumes [measurable]: "X' ∈ sets borel" assumes [measurable]: "⋀y. y ∈ Y ⟹ set_borel_measurable borel X' (f y)" assumes "⋀y. y ∈ Y ⟹ (AE t∈X' in lborel. norm (f y t) ≤ g t)" assumes "eventually (λx. X x ∈ sets borel ∧ X x ⊆ X') F" assumes "filterlim (λx. set_lebesgue_integral lborel (X x) g) (nhds (set_lebesgue_integral lborel X' g)) F" shows "uniform_limit Y (λx y. set_lebesgue_integral lborel (X x) (f y)) (λy. set_lebesgue_integral lborel X' (f y)) F" proof (rule uniform_limitI, goal_cases) case (1 ε) have integrable_g: "set_integrable lborel U g" if "U ∈ sets borel" "U ⊆ X'" for U by (rule set_integrable_subset[OF assms(1)]) (use that in auto) have "eventually (λx. dist (set_lebesgue_integral lborel (X x) g) (set_lebesgue_integral lborel X' g) < ε) F" using ‹ε > 0› assms by (auto simp: tendsto_iff) from this show ?case using ‹eventually (λ_. _ ∧ _) F› proof eventually_elim case (elim x) hence [measurable]:"X x ∈ sets borel" and "X x ⊆ X'" by auto have integrable: "set_integrable lborel U (f y)" if "y ∈ Y" "U ∈ sets borel" "U ⊆ X'" for y U apply (rule set_integrable_subset) apply (rule set_integrable_bound[OF assms(1)]) apply (use assms(3) that in ‹simp add: set_borel_measurable_def›) using assms(4)[OF ‹y ∈ Y›] apply eventually_elim apply force using that apply simp_all done show ?case proof fix y assume "y ∈ Y" have "dist (set_lebesgue_integral lborel (X x) (f y)) (set_lebesgue_integral lborel X' (f y)) = norm (set_lebesgue_integral lborel X' (f y) - set_lebesgue_integral lborel (X x) (f y))" by (simp add: dist_norm norm_minus_commute) also have "set_lebesgue_integral lborel X' (f y) - set_lebesgue_integral lborel (X x) (f y) = set_lebesgue_integral lborel (X' - X x) (f y)" unfolding set_lebesgue_integral_def apply (subst Bochner_Integration.integral_diff [symmetric]) unfolding set_integrable_def [symmetric] apply (rule integrable; (fact | simp)) apply (rule integrable; fact) apply (intro Bochner_Integration.integral_cong) apply (use ‹X x ⊆ X'› in ‹auto simp: indicator_def›) done also have "norm … ≤ (∫t∈X'-X x. norm (f y t) ∂lborel)" by (intro set_integral_norm_bound integrable) (fact | simp)+ also have "AE t∈X' - X x in lborel. norm (f y t) ≤ g t" using assms(4)[OF ‹y ∈ Y›] by eventually_elim auto with ‹y ∈ Y› have "(∫t∈X'-X x. norm (f y t) ∂lborel) ≤ (∫t∈X'-X x. g t ∂lborel)" by (intro set_integral_mono_AE set_integrable_norm integrable integrable_g) auto also have "… = (∫t∈X'. g t ∂lborel) - (∫t∈X x. g t ∂lborel)" unfolding set_lebesgue_integral_def apply (subst Bochner_Integration.integral_diff [symmetric]) unfolding set_integrable_def [symmetric] apply (rule integrable_g; (fact | simp)) apply (rule integrable_g; fact) apply (intro Bochner_Integration.integral_cong) apply (use ‹X x ⊆ X'› in ‹auto simp: indicator_def›) done also have "… ≤ dist (∫t∈X x. g t ∂lborel) (∫t∈X'. g t ∂lborel)" by (simp add: dist_norm) also have "… < ε" by fact finally show "dist (set_lebesgue_integral lborel (X x) (f y)) (set_lebesgue_integral lborel X' (f y)) < ε" . qed qed qed lemma integral_dominated_convergence_at_right: fixes s :: "real ⇒ 'a ⇒ 'b::{banach, second_countable_topology}" and w :: "'a ⇒ real" and f :: "'a ⇒ 'b" and M and c :: real assumes "f ∈ borel_measurable M" "⋀t. s t ∈ borel_measurable M" "integrable M w" assumes lim: "AE x in M. ((λi. s i x) ⤏ f x) (at_right c)" assumes bound: "∀⇩F i in at_right c. AE x in M. norm (s i x) ≤ w x" shows "((λt. integral⇧L M (s t)) ⤏ integral⇧L M f) (at_right c)" proof (rule tendsto_at_right_realI_sequentially) fix X :: "nat ⇒ real" assume X: "filterlim X (at_right c) sequentially" from filterlim_iff[THEN iffD1, OF this, rule_format, OF bound] obtain N where w: "⋀n. N ≤ n ⟹ AE x in M. norm (s (X n) x) ≤ w x" by (auto simp: eventually_sequentially) show "(λn. integral⇧L M (s (X n))) ⇢ integral⇧L M f" proof (rule LIMSEQ_offset, rule integral_dominated_convergence) show "AE x in M. norm (s (X (n + N)) x) ≤ w x" for n by (rule w) auto show "AE x in M. (λn. s (X (n + N)) x) ⇢ f x" using lim proof eventually_elim fix x assume "((λi. s i x) ⤏ f x) (at_right c)" then show "(λn. s (X (n + N)) x) ⇢ f x" by (intro LIMSEQ_ignore_initial_segment filterlim_compose[OF _ X]) qed qed fact+ qed lemma integral_dominated_convergence_at_left: fixes s :: "real ⇒ 'a ⇒ 'b::{banach, second_countable_topology}" and w :: "'a ⇒ real" and f :: "'a ⇒ 'b" and M and c :: real assumes "f ∈ borel_measurable M" "⋀t. s t ∈ borel_measurable M" "integrable M w" assumes lim: "AE x in M. ((λi. s i x) ⤏ f x) (at_left c)" assumes bound: "∀⇩F i in at_left c. AE x in M. norm (s i x) ≤ w x" shows "((λt. integral⇧L M (s t)) ⤏ integral⇧L M f) (at_left c)" proof (rule tendsto_at_left_realI_sequentially) fix X :: "nat ⇒ real" assume X: "filterlim X (at_left c) sequentially" from filterlim_iff[THEN iffD1, OF this, rule_format, OF bound] obtain N where w: "⋀n. N ≤ n ⟹ AE x in M. norm (s (X n) x) ≤ w x" by (auto simp: eventually_sequentially) show "(λn. integral⇧L M (s (X n))) ⇢ integral⇧L M f" proof (rule LIMSEQ_offset, rule integral_dominated_convergence) show "AE x in M. norm (s (X (n + N)) x) ≤ w x" for n by (rule w) auto show "AE x in M. (λn. s (X (n + N)) x) ⇢ f x" using lim proof eventually_elim fix x assume "((λi. s i x) ⤏ f x) (at_left c)" then show "(λn. s (X (n + N)) x) ⇢ f x" by (intro LIMSEQ_ignore_initial_segment filterlim_compose[OF _ X]) qed qed fact+ qed lemma uniform_limit_interval_integral_right: fixes f :: "'a ⇒ real ⇒ 'c :: {banach, second_countable_topology}" assumes "interval_lebesgue_integrable lborel a b g" assumes [measurable]: "⋀y. y ∈ Y ⟹ set_borel_measurable borel (einterval a b) (f y)" assumes "⋀y. y ∈ Y ⟹ (AE t∈einterval a b in lborel. norm (f y t) ≤ g t)" assumes "a < b" shows "uniform_limit Y (λb' y. LBINT t=a..b'. f y t) (λy. LBINT t=a..b. f y t) (at_left b)" proof (cases "Y = {}") case False have g_nonneg: "AE t∈einterval a b in lborel. g t ≥ 0" proof - from ‹Y ≠ {}› obtain y where "y ∈ Y" by auto from assms(3)[OF this] show ?thesis by eventually_elim (auto elim: order.trans[rotated]) qed have ev: "eventually (λb'. b' ∈ {a<..<b}) (at_left b)" using ‹a < b› by (intro eventually_at_leftI) with ‹a < b› have "?thesis ⟷ uniform_limit Y (λb' y. ∫t∈einterval a (min b b'). f y t ∂lborel) (λy. ∫t∈einterval a b. f y t ∂lborel) (at_left b)" by (intro filterlim_cong arg_cong2[where f = uniformly_on]) (auto simp: interval_lebesgue_integral_def fun_eq_iff min_def intro!: eventually_mono[OF ev]) also have … proof (rule uniform_limit_set_lebesgue_integral[where g = g], goal_cases) show "∀⇩F b' in at_left b. einterval a (min b b') ∈ sets borel ∧ einterval a (min b b') ⊆ einterval a b" using ev by eventually_elim (auto simp: einterval_def) next show "((λb'. set_lebesgue_integral lborel (einterval a (min b b')) g) ⤏ set_lebesgue_integral lborel (einterval a b) g) (at_left b)" unfolding set_lebesgue_integral_def proof (intro tendsto_at_left_erealI_sequentially integral_dominated_convergence) have *: "set_borel_measurable borel (einterval a b) g" using assms(1) less_imp_le[OF ‹a < b›] by (simp add: interval_lebesgue_integrable_def set_integrable_def set_borel_measurable_def) show "(λx. indicat_real (einterval a b) x *⇩R g x) ∈ borel_measurable lborel" using * by (simp add: set_borel_measurable_def) fix X :: "nat ⇒ ereal" and n :: nat have "set_borel_measurable borel (einterval a (min b (X n))) g" by (rule set_borel_measurable_subset[OF *]) (auto simp: einterval_def) thus "(λx. indicat_real (einterval a (min b (X n))) x *⇩R g x) ∈ borel_measurable lborel" by (simp add: set_borel_measurable_def) next fix X :: "nat ⇒ ereal" assume X: "filterlim X (at_left b) sequentially" show "AE x in lborel. (λn. indicat_real (einterval a (min b (X n))) x *⇩R g x) ⇢ indicat_real (einterval a b) x *⇩R g x" proof (rule AE_I2) fix x :: real have "(λt. indicator (einterval a (min b (X t))) x :: real) ⇢ indicator (einterval a b) x" proof (cases "x ∈ einterval a b") case False hence "x ∉ einterval a (min b (X t))"for t by (auto simp: einterval_def) with False show ?thesis by (simp add: indicator_def) next case True with ‹a < b› have "eventually (λt. t ∈ {max a x<..<b}) (at_left b)" by (intro eventually_at_leftI[of "ereal x"]) (auto simp: einterval_def min_def) from this and X have "eventually (λt. X t ∈ {max a x<..<b}) sequentially" by (rule eventually_compose_filterlim) hence "eventually (λt. indicator (einterval a (min b (X t))) x = (1 :: real)) sequentially" by eventually_elim (use True in ‹auto simp: indicator_def einterval_def›) from tendsto_eventually[OF this] and True show ?thesis by (simp add: indicator_def) qed thus "(λn. indicat_real (einterval a (min b (X n))) x *⇩R g x) ⇢ indicat_real (einterval a b) x *⇩R g x" by (intro tendsto_intros) qed next fix X :: "nat ⇒ ereal" and n :: nat show "AE x in lborel. norm (indicator (einterval a (min b (X n))) x *⇩R g x) ≤ indicator (einterval a b) x *⇩R g x" using g_nonneg by eventually_elim (auto simp: indicator_def einterval_def) qed (use assms less_imp_le[OF ‹a < b›] in ‹auto simp: interval_lebesgue_integrable_def set_integrable_def›) qed (use assms in ‹auto simp: interval_lebesgue_integrable_def›) finally show ?thesis . qed auto lemma uniform_limit_interval_integral_left: fixes f :: "'a ⇒ real ⇒ 'c :: {banach, second_countable_topology}" assumes "interval_lebesgue_integrable lborel a b g" assumes [measurable]: "⋀y. y ∈ Y ⟹ set_borel_measurable borel (einterval a b) (f y)" assumes "⋀y. y ∈ Y ⟹ (AE t∈einterval a b in lborel. norm (f y t) ≤ g t)" assumes "a < b" shows "uniform_limit Y (λa' y. LBINT t=a'..b. f y t) (λy. LBINT t=a..b. f y t) (at_right a)" proof (cases "Y = {}") case False have g_nonneg: "AE t∈einterval a b in lborel. g t ≥ 0" proof - from ‹Y ≠ {}› obtain y where "y ∈ Y" by auto from assms(3)[OF this] show ?thesis by eventually_elim (auto elim: order.trans[rotated]) qed have ev: "eventually (λb'. b' ∈ {a<..<b}) (at_right a)" using ‹a < b› by (intro eventually_at_rightI) with ‹a < b› have "?thesis ⟷ uniform_limit Y (λa' y. ∫t∈einterval (max a a') b. f y t ∂lborel) (λy. ∫t∈einterval a b. f y t ∂lborel) (at_right a)" by (intro filterlim_cong arg_cong2[where f = uniformly_on]) (auto simp: interval_lebesgue_integral_def fun_eq_iff max_def intro!: eventually_mono[OF ev]) also have … proof (rule uniform_limit_set_lebesgue_integral[where g = g], goal_cases) show "∀⇩F a' in at_right a. einterval (max a a') b ∈ sets borel ∧ einterval (max a a') b ⊆ einterval a b" using ev by eventually_elim (auto simp: einterval_def) next show "((λa'. set_lebesgue_integral lborel (einterval (max a a') b) g) ⤏ set_lebesgue_integral lborel (einterval a b) g) (at_right a)" unfolding set_lebesgue_integral_def proof (intro tendsto_at_right_erealI_sequentially integral_dominated_convergence) have *: "set_borel_measurable borel (einterval a b) g" using assms(1) less_imp_le[OF ‹a < b›] by (simp add: interval_lebesgue_integrable_def set_integrable_def set_borel_measurable_def) show "(λx. indicat_real (einterval a b) x *⇩R g x) ∈ borel_measurable lborel" using * by (simp add: set_borel_measurable_def) fix X :: "nat ⇒ ereal" and n :: nat have "set_borel_measurable borel (einterval (max a (X n)) b) g" by (rule set_borel_measurable_subset[OF *]) (auto simp: einterval_def) thus "(λx. indicat_real (einterval (max a (X n)) b) x *⇩R g x) ∈ borel_measurable lborel" by (simp add: set_borel_measurable_def) next fix X :: "nat ⇒ ereal" assume X: "filterlim X (at_right a) sequentially" show "AE x in lborel. (λn. indicat_real (einterval (max a (X n)) b) x *⇩R g x) ⇢ indicat_real (einterval a b) x *⇩R g x" proof (rule AE_I2) fix x :: real have "(λt. indicator (einterval (max a (X t)) b) x :: real) ⇢ indicator (einterval a b) x" proof (cases "x ∈ einterval a b") case False hence "x ∉ einterval (max a (X t)) b"for t by (auto simp: einterval_def) with False show ?thesis by (simp add: indicator_def) next case True with ‹a < b› have "eventually (λt. t ∈ {a<..<x}) (at_right a)" by (intro eventually_at_rightI[of _ "ereal x"]) (auto simp: einterval_def min_def) from this and X have "eventually (λt. X t ∈ {a<..<x}) sequentially" by (rule eventually_compose_filterlim) hence "eventually (λt. indicator (einterval (max a (X t)) b) x = (1 :: real)) sequentially" by eventually_elim (use True in ‹auto simp: indicator_def einterval_def›) from tendsto_eventually[OF this] and True show ?thesis by (simp add: indicator_def) qed thus "(λn. indicat_real (einterval (max a (X n)) b) x *⇩R g x) ⇢ indicat_real (einterval a b) x *⇩R g x" by (intro tendsto_intros) qed next fix X :: "nat ⇒ ereal" and n :: nat show "AE x in lborel. norm (indicator (einterval (max a (X n)) b) x *⇩R g x) ≤ indicator (einterval a b) x *⇩R g x" using g_nonneg by eventually_elim (auto simp: indicator_def einterval_def) qed (use assms less_imp_le[OF ‹a < b›] in ‹auto simp: interval_lebesgue_integrable_def set_integrable_def›) qed (use assms in ‹auto simp: interval_lebesgue_integrable_def›) finally show ?thesis . qed auto lemma uniform_limit_interval_integral_sequentially: fixes f :: "'a ⇒ real ⇒ 'c :: {banach, second_countable_topology}" assumes "interval_lebesgue_integrable lborel a b g" assumes [measurable]: "⋀y. y ∈ Y ⟹ set_borel_measurable borel (einterval a b) (f y)" assumes "⋀y. y ∈ Y ⟹ (AE t∈einterval a b in lborel. norm (f y t) ≤ g t)" assumes a': "filterlim a' (at_right a) sequentially" assumes b': "filterlim b' (at_left b) sequentially" assumes "a < b" shows "uniform_limit Y (λn y. LBINT t=a' n..b' n. f y t) (λy. LBINT t=a..b. f y t) sequentially" proof (cases "Y = {}") case False have g_nonneg: "AE t∈einterval a b in lborel. g t ≥ 0" proof - from ‹Y ≠ {}› obtain y where "y ∈ Y" by auto from assms(3)[OF this] show ?thesis by eventually_elim (auto elim: order.trans[rotated]) qed have ev: "eventually (λn. a < a' n ∧ a' n < b' n ∧ b' n < b) sequentially" proof - from ereal_dense2[OF ‹a < b›] obtain t where t: "a < ereal t" "ereal t < b" by blast from t have "eventually (λn. a' n ∈ {a<..<t}) sequentially" by (intro eventually_compose_filterlim[OF _ a'] eventually_at_rightI[of _ "ereal t"]) moreover from t have "eventually (λn. b' n ∈ {t<..<b}) sequentially" by (intro eventually_compose_filterlim[OF _ b'] eventually_at_leftI[of "ereal t"]) ultimately show "eventually (λn. a < a' n ∧ a' n < b' n ∧ b' n < b) sequentially" by eventually_elim auto qed have "?thesis ⟷ uniform_limit Y (λn y. ∫t∈einterval (max a (a' n)) (min b (b' n)). f y t ∂lborel) (λy. ∫t∈einterval a b. f y t ∂lborel) sequentially" using ‹a < b› by (intro filterlim_cong arg_cong2[where f = uniformly_on]) (auto simp: interval_lebesgue_integral_def fun_eq_iff min_def max_def intro!: eventually_mono[OF ev]) also have … proof (rule uniform_limit_set_lebesgue_integral[where g = g], goal_cases) show "∀⇩F n in sequentially. einterval (max a (a' n)) (min b (b' n)) ∈ sets borel ∧ einterval (max a (a' n)) (min b (b' n)) ⊆ einterval a b" using ev by eventually_elim (auto simp: einterval_def) next show "((λn. set_lebesgue_integral lborel (einterval (max a (a' n)) (min b (b' n))) g) ⤏ set_lebesgue_integral lborel (einterval a b) g) sequentially" unfolding set_lebesgue_integral_def proof (intro integral_dominated_convergence) have *: "set_borel_measurable borel (einterval a b) g" using assms(1) less_imp_le[OF ‹a < b›] by (simp add: interval_lebesgue_integrable_def set_integrable_def set_borel_measurable_def) show "(λx. indicat_real (einterval a b) x *⇩R g x) ∈ borel_measurable lborel" using * by (simp add: set_borel_measurable_def) fix n :: nat have "set_borel_measurable borel (einterval (max a (a' n)) (min b (b' n))) g" by (rule set_borel_measurable_subset[OF *]) (auto simp: einterval_def) thus "(λx. indicat_real (einterval (max a (a' n)) (min b (b' n))) x *⇩R g x) ∈ borel_measurable lborel" by (simp add: set_borel_measurable_def) next show "AE x in lborel. (λn. indicat_real (einterval (max a (a' n)) (min b (b' n))) x *⇩R g x) ⇢ indicat_real (einterval a b) x *⇩R g x" proof (rule AE_I2) fix x :: real have "(λt. indicator (einterval (max a (a' t)) (min b (b' t))) x :: real) ⇢ indicator (einterval a b) x" proof (cases "x ∈ einterval a b") case False hence "x ∉ einterval (max a (a' t)) (min b (b' t))"for t by (auto simp: einterval_def) with False show ?thesis by (simp add: indicator_def) next case True with ‹a < b› have "eventually (λt. t ∈ {a<..<x}) (at_right a)" by (intro eventually_at_rightI[of _ "ereal x"]) (auto simp: einterval_def min_def) have "eventually (λn. x ∈ {a' n<..<b' n}) sequentially" proof - have "eventually (λn. a' n ∈ {a<..<x}) sequentially" using True by (intro eventually_compose_filterlim[OF _ a'] eventually_at_rightI[of _ "ereal x"]) (auto simp: einterval_def) moreover have "eventually (λn. b' n ∈ {x<..<b}) sequentially" using True by (intro eventually_compose_filterlim[OF _ b'] eventually_at_leftI[of "ereal x"]) (auto simp: einterval_def) ultimately show "eventually (λn. x ∈ {a' n<..<b' n}) sequentially" by eventually_elim auto qed hence "eventually (λt. indicator (einterval (max a (a' t)) (min b (b' t))) x = (1 :: real)) sequentially" by eventually_elim (use True in ‹auto simp: indicator_def einterval_def›) from tendsto_eventually[OF this] and True show ?thesis by (simp add: indicator_def) qed thus "(λn. indicat_real (einterval (max a (a' n)) (min b (b' n))) x *⇩R g x) ⇢ indicat_real (einterval a b) x *⇩R g x" by (intro tendsto_intros) qed next fix X :: "nat ⇒ ereal" and n :: nat show "AE x in lborel. norm (indicator (einterval (max a (a' n)) (min b (b' n))) x *⇩R g x) ≤ indicator (einterval a b) x *⇩R g x" using g_nonneg by eventually_elim (auto simp: indicator_def einterval_def) qed (use assms less_imp_le[OF ‹a < b›] in ‹auto simp: interval_lebesgue_integrable_def set_integrable_def›) qed (use assms in ‹auto simp: interval_lebesgue_integrable_def›) finally show ?thesis . qed auto lemma interval_lebesgue_integrable_combine: assumes "interval_lebesgue_integrable lborel A B f" assumes "interval_lebesgue_integrable lborel B C f" assumes "set_borel_measurable borel (einterval A C) f" assumes "A ≤ B" "B ≤ C" shows "interval_lebesgue_integrable lborel A C f" proof - have meas: "set_borel_measurable borel (einterval A B ∪ einterval B C) f" by (rule set_borel_measurable_subset[OF assms(3)]) (use assms in ‹auto simp: einterval_def›) have "set_integrable lborel (einterval A B ∪ einterval B C) f" using assms by (intro set_integrable_Un) (auto simp: interval_lebesgue_integrable_def) also have "?this ⟷ set_integrable lborel (einterval A C) f" proof (cases "B ∈ {∞, -∞}") case True with assms have "einterval A B ∪ einterval B C = einterval A C" by (auto simp: einterval_def) thus ?thesis by simp next case False then obtain B' where [simp]: "B = ereal B'" by (cases B) auto have "indicator (einterval A C) x = (indicator (einterval A B ∪ einterval B C) x :: real)" if "x ≠ B'" for x using assms(4,5) that by (cases A; cases C) (auto simp: einterval_def indicator_def) hence "{x ∈ space lborel. indicat_real (einterval A B ∪ einterval B C) x *⇩R f x ≠ indicat_real (einterval A C) x *⇩R f x} ⊆ {B'}" by force thus ?thesis unfolding set_integrable_def using meas assms by (intro integrable_cong_AE AE_I[of _ _ "{B'}"]) (simp_all add: set_borel_measurable_def) qed also have "… ⟷ ?thesis" using order.trans[OF assms(4,5)] by (simp add: interval_lebesgue_integrable_def) finally show ?thesis . qed lemma interval_lebesgue_integrable_bigo_right: fixes A B :: real fixes f :: "real ⇒ real" assumes "f ∈ O[at_left B](g)" assumes cont: "continuous_on {A..<B} f" assumes meas: "set_borel_measurable borel {A<..<B} f" assumes "interval_lebesgue_integrable lborel A B g" assumes "A < B" shows "interval_lebesgue_integrable lborel A B f" proof - from assms(1) obtain c where c: "c > 0" "eventually (λx. norm (f x) ≤ c * norm (g x)) (at_left B)" by (elim landau_o.bigE) then obtain B' where B': "B' < B" "⋀x. x ∈ {B'<..<B} ⟹ norm (f x) ≤ c * norm (g x)" using ‹A < B› by (auto simp: Topological_Spaces.eventually_at_left[of A]) show ?thesis proof (rule interval_lebesgue_integrable_combine) show "interval_lebesgue_integrable lborel A (max A B') f" using B' assms by (intro interval_integrable_continuous_on continuous_on_subset[OF cont]) auto show "set_borel_measurable borel (einterval (ereal A) (ereal B)) f" using assms by simp have meas': "set_borel_measurable borel {max A B'<..<B} f" by (rule set_borel_measurable_subset[OF meas]) auto have "set_integrable lborel {max A B'<..<B} f" proof (rule set_integrable_bound[OF _ _ AE_I2[OF impI]]) have "set_integrable lborel {A<..<B} (λx. c * g x)" using assms by (simp add: interval_lebesgue_integrable_def) thus "set_integrable lborel {max A B'<..<B} (λx. c * g x)" by (rule set_integrable_subset) auto next fix x assume "x ∈ {max A B'<..<B}" hence "norm (f x) ≤ c * norm (g x)" by (intro B') auto also have "… ≤ norm (c * g x)" unfolding norm_mult by (intro mult_right_mono) auto finally show "norm (f x) ≤ norm (c * g x)" . qed (use meas' in ‹simp_all add: set_borel_measurable_def›) thus "interval_lebesgue_integrable lborel (ereal (max A B')) (ereal B) f" unfolding interval_lebesgue_integrable_def einterval_eq_Icc using ‹B' < B› assms by simp qed (use B' assms in auto) qed lemma interval_lebesgue_integrable_bigo_left: fixes A B :: real fixes f :: "real ⇒ real" assumes "f ∈ O[at_right A](g)" assumes cont: "continuous_on {A<..B} f" assumes meas: "set_borel_measurable borel {A<..<B} f" assumes "interval_lebesgue_integrable lborel A B g" assumes "A < B" shows "interval_lebesgue_integrable lborel A B f" proof - from assms(1) obtain c where c: "c > 0" "eventually (λx. norm (f x) ≤ c * norm (g x)) (at_right A)" by (elim landau_o.bigE) then obtain A' where A': "A' > A" "⋀x. x ∈ {A<..<A'} ⟹ norm (f x) ≤ c * norm (g x)" using ‹A < B› by (auto simp: Topological_Spaces.eventually_at_right[of A]) show ?thesis proof (rule interval_lebesgue_integrable_combine) show "interval_lebesgue_integrable lborel (min B A') B f" using A' assms by (intro interval_integrable_continuous_on continuous_on_subset[OF cont]) auto show "set_borel_measurable borel (einterval (ereal A) (ereal B)) f" using assms by simp have meas': "set_borel_measurable borel {A<..<min B A'} f" by (rule set_borel_measurable_subset[OF meas]) auto have "set_integrable lborel {A<..<min B A'} f" proof (rule set_integrable_bound[OF _ _ AE_I2[OF impI]]) have "set_integrable lborel {A<..<B} (λx. c * g x)" using assms by (simp add: interval_lebesgue_integrable_def) thus "set_integrable lborel {A<..<min B A'} (λx. c * g x)" by (rule set_integrable_subset) auto next fix x assume "x ∈ {A<..<min B A'}" hence "norm (f x) ≤ c * norm (g x)" by (intro A') auto also have "… ≤ norm (c * g x)" unfolding norm_mult by (intro mult_right_mono) auto finally show "norm (f x) ≤ norm (c * g x)" . qed (use meas' in ‹simp_all add: set_borel_measurable_def›) thus "interval_lebesgue_integrable lborel (ereal A) (ereal (min B A')) f" unfolding interval_lebesgue_integrable_def einterval_eq_Icc using ‹A' > A› assms by simp qed (use A' assms in auto) qed subsection ‹Other material› (* TODO: Library *) lemma summable_comparison_test_bigo: fixes f :: "nat ⇒ real" assumes "summable (λn. norm (g n))" "f ∈ O(g)" shows "summable f" proof - from ‹f ∈ O(g)› obtain C where C: "eventually (λx. norm (f x) ≤ C * norm (g x)) at_top" by (auto elim: landau_o.bigE) thus ?thesis by (rule summable_comparison_test_ev) (insert assms, auto intro: summable_mult) qed lemma fps_expansion_cong: assumes "eventually (λx. g x = h x) (nhds x)" shows "fps_expansion g x = fps_expansion h x" proof - have "(deriv ^^ n) g x = (deriv ^^ n) h x" for n by (intro higher_deriv_cong_ev assms refl) thus ?thesis by (simp add: fps_expansion_def) qed lemma fps_expansion_eq_zero_iff: assumes "g holomorphic_on ball z r" "r > 0" shows "fps_expansion g z = 0 ⟷ (∀z∈ball z r. g z = 0)" proof assume *: "∀z∈ball z r. g z = 0" have "eventually (λw. w ∈ ball z r) (nhds z)" using assms by (intro eventually_nhds_in_open) auto hence "eventually (λz. g z = 0) (nhds z)" by eventually_elim (use * in auto) hence "fps_expansion g z = fps_expansion (λ_. 0) z" by (intro fps_expansion_cong) thus "fps_expansion g z = 0" by (simp add: fps_expansion_def fps_zero_def) next assume *: "fps_expansion g z = 0" have "g w = 0" if "w ∈ ball z r" for w by (rule holomorphic_fun_eq_0_on_ball[OF assms(1) that]) (use * in ‹auto simp: fps_expansion_def fps_eq_iff›) thus "∀w∈ball z r. g w = 0" by blast qed lemma fds_nth_higher_deriv: "fds_nth ((fds_deriv ^^ k) F) = (λn. (-1) ^ k * of_real (ln n) ^ k * fds_nth F n)" by (induction k) (auto simp: fds_nth_deriv fun_eq_iff simp flip: scaleR_conv_of_real) lemma binomial_n_n_minus_one [simp]: "n > 0 ⟹ n choose (n - Suc 0) = n" by (cases n) auto lemma has_field_derivative_complex_powr_right: "w ≠ 0 ⟹ ((λz. w powr z) has_field_derivative Ln w * w powr z) (at z within A)" by (rule DERIV_subset, rule has_field_derivative_powr_right) auto lemmas has_field_derivative_complex_powr_right' = has_field_derivative_complex_powr_right[THEN DERIV_chain2] end