Theory Zeta_Function.Zeta_Library
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›
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