Theory Lemmas_Regular_Variation
section ‹Lemmas›
theory Lemmas_Regular_Variation
imports
"HOL-Probability.Probability"
"Standard_Borel_Spaces.StandardBorel"
begin
subsection ‹ General Lemmas›
lemma image_mono_on_continuous_on_Icc:
fixes f :: "'a::linear_continuum_topology ⇒ 'b :: linorder_topology"
assumes ab:"a ≤ b" and mono:"mono_on {a..b} f"
and cont:"continuous_on {a..b} f"
shows "f ` {a..b} = {f a..f b}"
using IVT'[OF _ _ ab cont] mono_onD[OF mono] by fastforce
lemma image_mono_on_continuous_on_Ic:
fixes f :: "'a::linear_continuum_topology ⇒ 'b :: linorder_topology"
assumes mono:"mono_on {a..} f"
and cont:"continuous_on {a..} f"
and lim:"filterlim f at_top at_top"
shows "f ` {a..} = {f a..}"
proof -
have "f ` {a..} = f ` (⋃b∈{a..}. {a..b})"
by fastforce
also have "... = (⋃b∈{a..}. f ` {a..b})"
by blast
also have "... = (⋃b∈{a..}. {f a..f b})"
proof -
have "⋀b. a ≤ b ⟹ f ` {a..b} = {f a.. f b}"
by(intro image_mono_on_continuous_on_Icc mono_on_subset[OF mono]
continuous_on_subset[OF cont]) auto
thus ?thesis
by fast
qed
also have "... = {f a..}"
proof safe
fix y
assume y:"f a ≤ y"
obtain b where b: "a ≤ b" "y ≤ f b"
by (metis eventually_at_top_linorder filterlim_at_top lim nle_le)
thus "y ∈ (⋃b∈{a..}. {f a..f b})"
using y by fastforce
qed auto
finally show ?thesis .
qed
lemma image_mono_on_continuous_on_Ioo:
fixes f :: "'a::{linear_continuum_topology} ⇒ 'b :: linorder_topology"
assumes ab:"a ≤ b" and mono:"strict_mono_on {a..b} f"
and cont:"continuous_on {a..b} f"
shows "f ` {a<..<b} = {f a<..<f b}"
proof -
have "f ` {a<..<b} = f ` {a..b} - {f a, f b}"
apply safe
apply fastforce
apply (metis ab mono atLeastAtMost_iff greaterThanLessThan_iff le_less less_le
strict_mono_on_less)
apply (metis (mono_tags, opaque_lifting) ab mono
atLeastAtMost_iff greaterThanLessThan_iff less_le
monotone_onD order.refl)
apply (metis atLeastAtMost_iff greaterThanLessThan_iff imageI less_le)
done
also have "... = {f a..f b} - {f a, f b}"
by(simp add: image_mono_on_continuous_on_Icc
[OF ab strict_mono_on_imp_mono_on[OF mono] cont])
also have "... = {f a<..<f b}"
by fastforce
finally show ?thesis .
qed
lemma image_mono_on_continuous_on_Ioc:
fixes f :: "'a::{linear_continuum_topology} ⇒ 'b :: linorder_topology"
assumes ab:"a ≤ b" and mono:"strict_mono_on {a..b} f"
and cont:"continuous_on {a..b} f"
shows "f ` {a<..b} = {f a<..f b}"
proof -
have "f ` {a<..b} = f ` {a..b} - {f a}"
apply safe
apply fastforce
apply (metis ab mono atLeastAtMost_iff greaterThanAtMost_iff less_le order.refl
strict_mono_on_eqD)
apply (metis atLeastAtMost_iff greaterThanAtMost_iff image_eqI less_le)
done
also have "... = {f a..f b} - {f a}"
by(simp add: image_mono_on_continuous_on_Icc
[OF ab strict_mono_on_imp_mono_on[OF mono] cont])
also have "... = {f a<..f b}"
by fastforce
finally show ?thesis .
qed
lemma image_mono_on_continuous_on_greaterThan:
fixes f :: "'a::{linear_continuum_topology} ⇒ 'b :: linorder_topology"
assumes mono:"strict_mono_on {a..} f"
and cont:"continuous_on {a..} f"
and lim:"filterlim f at_top at_top"
shows "f ` {a<..} = {f a<..}"
proof -
have "f ` {a<..} = f ` {a..} - {f a}"
apply safe
apply fastforce
apply (metis mono atLeast_iff less_le nle_le strict_mono_on_eq)
apply (metis greaterThan_iff imageI less_le)
done
also have "... = {f a..} - {f a}"
by(simp add: image_mono_on_continuous_on_Ic
[OF strict_mono_on_imp_mono_on[OF mono] cont lim])
also have "... = {f a<..}"
by fastforce
finally show ?thesis .
qed
lemma image_antimono_on_continuous_on_Icc:
fixes f :: "'a::linear_continuum_topology ⇒ 'b :: linorder_topology"
assumes ab:"a ≤ b" and mono:"antimono_on {a..b} f"
and cont:"continuous_on {a..b} f"
shows "f ` {a..b} = {f b..f a}"
using IVT2'[OF _ _ ab cont] monotone_onD[OF mono] by fastforce
lemma image_antimono_on_continuous_on_Ioc:
fixes f :: "'a::{linear_continuum_topology} ⇒ 'b :: linorder_topology"
assumes ab:"a ≤ b" and mono:"strict_antimono_on {a..b} f"
and cont:"continuous_on {a..b} f"
shows "f ` {a<..b} = {f b..<f a}"
proof -
have "f ` {a<..b} = f ` {a..b} - {f a}"
apply safe
apply fastforce
apply (metis (mono_tags, lifting) assms(1,2) atLeastAtMost_iff
greaterThanAtMost_iff less_le monotone_onD order.refl)
apply (metis atLeastAtMost_iff greaterThanAtMost_iff imageI less_le)
done
also have "... = {f b..f a} - {f a}"
using mono
by(subst image_antimono_on_continuous_on_Icc[OF ab _ cont])
(auto simp: monotone_on_def le_less)
also have "... = {f b..<f a}"
by fastforce
finally show ?thesis .
qed
lemma image_mult_greaterThanLessThan[simp]:
fixes c :: real
assumes "0 < c"
shows "(*) c ` {a<..<b} = {c * a<..<c * b}"
proof -
have "(*) c ` {a<..<b} = (*) c ` ball ((b + a) / 2) ((b - a) / 2)"
by(rule arg_cong[where f="image (λx. c * x)"])
(simp add: ball_eq_greaterThanLessThan add_divide_distrib[symmetric]
diff_divide_distrib[symmetric])
also have "... = ball (c * (b + a) / 2) (c * (b - a) / 2)"
using ball_scale[of c "(b + a) / 2" "(b - a) / 2"] assms by simp
also have "... = {c * a<..<c * b}"
by(simp add: ball_eq_greaterThanLessThan add_divide_distrib[symmetric]
distrib_left[symmetric] diff_divide_distrib[symmetric] right_diff_distrib[symmetric])
finally show ?thesis .
qed
lemma image_times_atLeastLessThan[simp]:
fixes c :: real
assumes "0 < c"
shows "(*) c ` {a<..b} = {c * a<..c * b}"
proof -
have "(*) c ` {a<..b} = (*) c ` ({a<..<b+1} ∩ {a-1..b})"
by(rule arg_cong[where f="image (λx. c * x)"]) auto
also have "... = (*) c ` {a<..<b+1} ∩ (*) c ` {a-1..b}"
by(subst image_Int) (use assms in auto)
also have "... = {c * a<..<c * (b + 1)} ∩ {c * (a - 1)..c * b}"
using assms by simp
also have "... = {c * a<..c * b}"
unfolding set_eq_iff greaterThanLessThan_iff Int_iff atLeastAtMost_iff greaterThanAtMost_iff
by(intro allI iffI) (use assms in argo)+
finally show ?thesis .
qed
lemma image_power_Icc_pos:
assumes "0 ≤ ρ"
and "0 < a" and "a ≤ b"
shows "(λx::real. x powr ρ) ` {a..b} = {a powr ρ..b powr ρ}"
using assms
by(intro image_mono_on_continuous_on_Icc mono_onI powr_mono2 continuous_on_powr)
auto
lemma image_inverse_power_Icc_pos:
assumes "0 ≤ ρ"
and "0 < a" and "a ≤ b"
shows "(λx::real. 1 / x powr ρ) ` {a..b} = {1 / b powr ρ..1 / a powr ρ}"
using assms
by(intro image_antimono_on_continuous_on_Icc monotone_onI divide_left_mono powr_mono2
continuous_on_divide continuous_on_powr)
auto
lemma image_power_Icc_neg:
assumes "ρ ≤ 0"
and "0 < a" and "a ≤ b"
shows "(λx::real. x powr ρ) ` {a..b} = {b powr ρ..a powr ρ}"
using assms
by(intro image_antimono_on_continuous_on_Icc monotone_onI powr_mono2' continuous_on_powr)
auto
lemma image_inverse_power_Icc_neg:
assumes "ρ ≤ 0"
and "0 < a" and "a ≤ b"
shows "(λx::real. 1 / x powr ρ) ` {a..b} = {1 / a powr ρ..1 / b powr ρ}"
using assms
by(intro image_mono_on_continuous_on_Icc continuous_on_divide
divide_left_mono mono_onI powr_mono2' continuous_on_powr)
auto
lemma image_times_atLeastLessThan'[simp]:
fixes c :: real
assumes "0 < c"
shows "(λx. x * c) ` {a<..b} = {c * a<..c * b}"
using assms by(simp add: mult.commute[of _ c])
lemma bounded_times_comp:
fixes f g::"'a ⇒ 'b::real_normed_field"
assumes "bounded (f ` S)"
and "bounded (g ` S)"
shows "bounded ((λx. f x * g x) ` S)"
proof -
obtain a b where "⋀x. x ∈ S ⟹ norm (f x) ≤ a" "⋀x. x ∈ S ⟹ norm (g x) ≤ b"
"⋀x. x ∈ S ⟹ 0 ≤ a"
using assms by (metis bounded_pos less_eq_real_def rev_image_eqI)
thus ?thesis
by(auto simp: bounded_iff norm_mult intro!: exI[where x="a * b"] mult_mono)
qed
lemma antimono_on_iff_uminus_mono_on:
fixes f :: "_ ⇒ _ :: ordered_ab_group_add"
shows "antimono_on A f ⟷ mono_on A (λx. -f x)"
by(auto simp: monotone_on_def)
lemma filterlim_Pair_component:
"LIM x F. f x :> G ⟹ LIM x H. g x :> I ⟹ LIM (x, y) F ×⇩F H. (f x, g y) :> G ×⇩F I"
by (metis filterlim_def filtermap_prod_filter map_prod_def prod_filter_mono)
lemma eventually_eventually_prod_filter_principal1:
"eventually P (F ×⇩F principal A) ⟷ eventually (λx. ∀y∈A. P (x, y)) F"
proof
assume h:"∀⇩F x in F. ∀y∈A. P (x, y)"
show "eventually P (F ×⇩F principal A)"
unfolding eventually_prod_filter
by(intro exI[where x="λx. ∀y∈A. P (x, y)"] exI[where x="λy. y ∈ A"])
(use h in "auto simp: eventually_principal")
qed(auto dest: eventually_eventually_prod_filter1 simp: eventually_principal)
lemma eventually_eventually_prod_filter_principal2:
"eventually P (principal A ×⇩F G) ⟷ eventually (λy. ∀x∈A. P (x, y)) G"
proof
assume h:"∀⇩F y in G. ∀x∈A. P (x, y)"
show "eventually P (principal A ×⇩F G)"
unfolding eventually_prod_filter
by(intro exI[where x="λy. ∀x∈A. P (x, y)"] exI[where x="λx. x ∈ A"])
(use h in "auto simp: eventually_principal")
qed(auto dest: eventually_eventually_prod_filter2 simp: eventually_principal)
lemma prod_filter_distrib_right:
"F ×⇩F (G ⊔ H) = F ×⇩F G ⊔ F ×⇩F H"
proof(rule filter_eqI)
fix P
show "eventually P (F ×⇩F (G ⊔ H)) =
eventually P (F ×⇩F G ⊔ F ×⇩F H)"
proof
assume "eventually P (F ×⇩F (G ⊔ H))"
then obtain Pf Pg where "eventually Pf F" "eventually Pg G" "eventually Pg H"
"∀x y. Pf x ⟶ Pg y ⟶ P (x, y)"
by(auto simp: eventually_prod_filter eventually_sup)
thus "eventually P (F ×⇩F G ⊔ F ×⇩F H)"
by(auto simp: eventually_sup eventually_prod_filter)
next
assume "eventually P (F ×⇩F G ⊔ F ×⇩F H)"
then obtain Pf Pg Pf' Ph where h:
"eventually Pf F" "eventually Pg G" "∀x y. Pf x ⟶ Pg y ⟶ P (x, y)"
"eventually Pf' F" "eventually Ph H" "∀x y. Pf' x ⟶ Ph y ⟶ P (x, y)"
by(auto simp: eventually_sup eventually_prod_filter)
thus "eventually P (F ×⇩F (G ⊔ H))"
unfolding eventually_prod_filter
by(intro exI[where x="λx. Pf x ∧ Pf' x"] exI[where x="λy. Pg y ∨ Ph y"])
(auto simp: eventually_sup eventually_conj eventually_mono)
qed
qed
lemma suminf_const_infinity:
fixes a :: ennreal
assumes a:"0 < a"
shows "(∑n. a) = ⊤"
proof -
have *:"(⋃n. {real_of_int (from_nat_into UNIV n)..<real_of_int (from_nat_into UNIV n + 1)})
= UNIV"
proof safe
fix x :: real
have "∃n. real_of_int (from_nat_into UNIV n) ≤ x
∧ x < real_of_int (from_nat_into UNIV n + 1)"
by (metis UNIV_I countableI_type floor_correct from_nat_into_to_nat_on)
thm from_nat_into_to_nat_on
thus "x ∈ (⋃n. {real_of_int (from_nat_into UNIV n)..<real_of_int (from_nat_into UNIV n + 1)})"
by auto
qed auto
have **:"disjoint_family
(λn. {real_of_int (from_nat_into UNIV n)..<real_of_int (from_nat_into UNIV n + 1)})"
proof -
have "⋀n m. n ≠ m ⟹ from_nat_into UNIV n ≠ (from_nat_into UNIV m :: int)"
by simp
thus ?thesis
unfolding disjoint_family_on_def
by (metis Int_emptyI atLeastLessThan_iff floor_exists1)
qed
have "(∑n. a) = (∑n.
(∫⇧+ x∈{real_of_int (from_nat_into UNIV n)..<real_of_int (from_nat_into UNIV n + 1)}.
a ∂lborel))"
by(auto intro!: suminf_cong simp: nn_integral_cmult_indicator)
also have "... = (∫⇧+ x∈⋃n.
{real_of_int (from_nat_into UNIV n)..<real_of_int (from_nat_into UNIV n + 1)}.
a ∂lborel)"
by(rule nn_integral_disjoint_family[symmetric])
(use ** in auto)
also have "... = (∫⇧+ x∈UNIV. a ∂lborel)"
unfolding * by fastforce
also have "(∫⇧+ x∈UNIV. a ∂lborel) = a * emeasure lborel UNIV"
by(simp add: nn_integral_cmult_indicator)
also have "... = ⊤"
using a by force
finally show ?thesis
by simp
qed
subsection ‹Limit›
lemma tendsto_sandwich_mult_const:
fixes c :: real
assumes ev: "⋀e::real. 0 < e ⟹ eventually (λn. f e ≤ g n / c ∧ g n / c ≤ h e) net"
and limf:"(f ⤏ 1) (at_right 0)" and limh:"(h ⤏ 1) (at_right 0)"
shows "(g ⤏ c) net"
proof -
have "((λn. g n / c) ⤏ 1) net"
unfolding tendsto_iff dist_real_def
proof safe
fix e :: real
assume e:"0 < e"
obtain a where a_pos:"0 < a" and a:"⋀a'. 0 < a' ⟹ a' < a ⟹ ¦f a' - 1¦ < e"
using limf e unfolding tendsto_iff eventually_at_right[OF e]
by(auto simp: dist_real_def)
obtain b where b_pos:"0 < b" and b:"⋀b'. 0 < b' ⟹ b' < b ⟹ ¦h b' - 1¦ < e"
using limh e unfolding tendsto_iff eventually_at_right[OF e]
by(auto simp: dist_real_def)
show " ∀⇩F x in net. ¦g x / c - 1¦ < e"
proof(safe intro!: eventually_mono[OF ev[of "min a b / 2"]])
fix x
assume le1:"f (min a b / 2) ≤ g x / c"
and le2:"g x / c ≤ h (min a b / 2)"
have "1 - e < f (min a b / 2)"
using a[of "min a b / 2"] a_pos b_pos by argo
also have "... ≤ g x / c"
by fact
finally have *:"1 - e < g x / c" .
have "g x / c ≤ h (min a b / 2)"
by fact
also have "... < e + 1"
using b[of "min a b / 2"] a_pos b_pos by argo
finally show "¦g x / c - 1¦ < e"
using * by auto
qed(use a_pos b_pos in argo)
qed
from asymp_equivI'[OF this]
show ?thesis
by(auto simp: asymp_equivD_const)
qed
lemma asymp_equiv_Limsup_cong_ereal:
assumes equiv:"f ∼[F] g"
and nonneg1:"∀⇩F x in F. 0 ≤ f x"
and nonneg2:"∀⇩F x in F. 0 ≤ g x"
shows "Limsup F (λx. ereal (f x)) = Limsup F (λx. ereal (g x))"
proof(cases "F = ⊥")
assume F:"F ≠ ⊥"
have *:"Limsup F (λx. ereal (f x)) ≤ Limsup F (λx. ereal (g x))"
if equiv:"f ∼[F] g"
and nonneg1:"∀⇩F x in F. 0 ≤ f x"
and nonneg2:"∀⇩F x in F. 0 ≤ g x" for f g
proof -
have Limsup1:"0 ≤ Limsup F (λx. ereal (f x))"
by(auto intro!: le_Limsup nonneg1 F)
have Limsup2:"0 ≤ Limsup F (λx. ereal (g x))"
by(auto intro!: le_Limsup nonneg2 F)
have le:"Limsup F (λx. ereal (f x))
≤ ereal c * Limsup F (λx. ereal (g x))" if c:"1 < c" for c :: real
proof -
have "Limsup F (λx. ereal (f x)) ≤ Limsup F (λx. ereal c * ereal (g x))"
by(intro Limsup_mono eventually_mono[OF
eventually_conj[OF eventually_conj[OF nonneg1 nonneg2]
asymp_equiv_imp_eventually_le[OF equiv c]]])
auto
also have "... = ereal c * Limsup F (λx. ereal (g x))"
by(subst Limsup_ereal_mult_left) (use F c in auto)
finally show ?thesis .
qed
have *:"((λc. ereal c * Limsup F (λx. ereal (g x)))
⤏ Limsup F (λx. ereal (g x))) (at_right 1)"
proof -
have "((λc. ereal c) ⤏ ereal 1) (at_right 1)"
by simp
from tendsto_mult_ereal[OF this tendsto_const[of "Limsup F (λx. ereal (g x))"]]
show ?thesis
by simp
qed
show ?thesis
using le
by(intro tendsto_lowerbound[OF *] eventually_at_rightI[where b=2]) auto
qed
show ?thesis
by(intro antisym * assms asymp_equiv_symI)
qed simp
lemma asymp_equiv_Liminf_cong_ereal:
assumes equiv:"f ∼[F] g"
and nonneg1:"∀⇩F x in F. 0 ≤ f x"
and nonneg2:"∀⇩F x in F. 0 ≤ g x"
shows "Liminf F (λx. ereal (f x)) = Liminf F (λx. ereal (g x))"
proof(cases "F = ⊥")
assume F:"F ≠ ⊥"
have *:"Liminf F (λx. ereal (f x)) ≤ Liminf F (λx. ereal (g x))"
if equiv:"f ∼[F] g"
and nonneg1:"∀⇩F x in F. 0 ≤ f x"
and nonneg2:"∀⇩F x in F. 0 ≤ g x" for f g
proof -
have le:"Liminf F (λx. ereal (f x))
≤ ereal c * Liminf F (λx. ereal (g x))" if c:"1 < c" for c :: real
proof -
have "Liminf F (λx. ereal (f x)) ≤ Liminf F (λx. ereal c * ereal (g x))"
by(intro Liminf_mono eventually_mono[OF
eventually_conj[OF eventually_conj[OF nonneg1 nonneg2]
asymp_equiv_imp_eventually_le[OF equiv c]]])
auto
also have "... = ereal c * Liminf F (λx. ereal (g x))"
by(subst Liminf_ereal_mult_left) (use F c in auto)
finally show ?thesis .
qed
have *:"((λc. ereal c * Liminf F (λx. ereal (g x)))
⤏ Liminf F (λx. ereal (g x))) (at_right 1)"
proof -
have "((λc. ereal c) ⤏ ereal 1) (at_right 1)"
by simp
from tendsto_mult_ereal[OF this tendsto_const[of "Liminf F (λx. ereal (g x))"]]
show ?thesis
by simp
qed
show ?thesis
using le
by(intro tendsto_lowerbound[OF *] eventually_at_rightI[where b=2]) auto
qed
show ?thesis
by(intro antisym * assms asymp_equiv_symI)
qed simp
lemma tendsto_at_topI_sequentially_real':
fixes f :: "real ⇒ real"
assumes mono: "mono_on {K..} f"
and limseq: "(λn. f (real n)) ⇢ y"
shows "(f ⤏ y) at_top"
proof -
have mono2:"mono (λx. if x < K then f K else f x)"
using mono_onD[OF mono] by(auto intro!: monoI)
obtain N where "K < real N"
using reals_Archimedean2 by blast
hence "(λn. (λx. if x < K then f K else f x) (real n)) ⇢ y"
by(auto intro!: tendsto_cong[THEN iffD1,OF _ limseq]
eventually_at_top_linorderI[where c=N])
hence lim:"((λx. if x < K then f K else f x) ⤏ y) at_top"
by(auto intro!: tendsto_at_topI_sequentially_real mono2)
show ?thesis
by(auto intro!: tendsto_cong[THEN iffD1,OF _ lim]
eventually_at_top_linorderI[where c=K])
qed
lemma mono_convergent_real_le:
fixes f :: "real ⇒ real"
assumes mono:"mono_on {K..} f"
and le:"⋀r. K ≤ r ⟹ f r ≤ A"
shows "∃l. (f ⤏ l) at_top ∧ (∀r≥K. f r ≤ l)"
proof -
have inc:" incseq (λn. f (K + real n))"
by(auto intro!: monoI mono_onD[OF mono])
obtain L where L:"(λn. f (K + real n)) ⇢ L" "⋀i. f (K + real i) ≤ L"
using incseq_convergent[OF inc,of A] le by auto
hence "((λr. f (K + r)) ⤏ L) at_top"
using mono_onD[OF mono]
by(auto intro!: tendsto_at_topI_sequentially_real'[of 0 "λr. f (K + r)"]
mono_onI)
moreover have "LIM r at_top. r - K :> at_top"
using filterlim_tendsto_add_at_top_iff[where f="λx. - K",THEN iffD2]
filterlim_ident by auto
ultimately have 1:"(f ⤏ L) at_top"
using filterlim_compose[of "λr. f (K + r)" "nhds L" at_top "λr. -K + r" at_top]
by simp
moreover have "f r ≤ L" if r:"K ≤ r" for r
proof(rule ccontr)
assume "¬ f r ≤ L"
hence "∀⇩F x in at_top. f x < f r"
using order_topology_class.order_tendstoD[OF 1] by simp
moreover have "∀⇩F x in at_top. f r ≤ f x"
using mono_onD[OF mono,of r] r
by(auto intro!: eventually_at_top_linorderI[where c=r])
ultimately show False
unfolding eventually_at_top_linorder
by (metis nle_le not_less)
qed
ultimately show ?thesis
by blast
qed
lemma mono_convergent_real_less:
fixes f :: "real ⇒ real"
assumes mono:"mono_on {K<..} f"
and less:"⋀r. K < r ⟹ f r ≤ A"
shows "∃l. (f ⤏ l) at_top ∧ (∀r>K. f r ≤ l)"
proof -
have "∃l. (f ⤏ l) at_top ∧ (∀r≥K + 1. f r ≤ l)"
by(auto intro!: mono_convergent_real_le less mono_onI mono_onD[OF mono])
then obtain L where L:"(f ⤏ L) at_top"
by blast
have "0 < e ⟹ ∃l. (f ⤏ l) at_top ∧ (∀r≥K+e. f r ≤ l)" for e :: real
by(auto intro!: mono_convergent_real_le less mono_onI mono_onD[OF mono])
then obtain l where l':"⋀e. 0 < e ⟹ (f ⤏ l e) at_top ∧ (∀r≥K+e. f r ≤ l e)"
by metis
hence "⋀e. 0 < e ⟹ l e = L"
by(auto intro!: tendsto_unique[OF _ _ L])
hence l:"⋀e r. 0 < e ⟹ K + e ≤ r ⟹ f r ≤ L"
using l' by fast
hence "⋀r. K < r ⟹ f r ≤ L"
by (metis not_le field_le_epsilon nle_le)
with L show ?thesis by blast
qed
lemma at_top_real_iff_all_sequentially:
fixes f :: "real ⇒ 'b :: topological_space"
shows "(f ⤏ l) at_top
⟷ (∀a. filterlim a at_top sequentially ⟶ incseq a
⟶ (λn. (f (a n))) ⇢ l)"
proof
assume h:"∀a. filterlim a at_top sequentially ⟶ (incseq a) ⟶ (λn. f (a n)) ⇢ l"
show "(f ⤏ l) at_top"
proof (rule ccontr)
assume c:"¬ (f ⤏ l) at_top"
then obtain S where S:"open S" "l ∈ S""⋀R. ∃r ≥ R. f r ∉ S"
by(fastforce simp: tendsto_def eventually_at_top_linorder)
define a where "a ≡ rec_nat (SOME r. r ≥ 0 ∧ f r ∉ S)
(λn an. SOME r. r > max an (real (Suc n)) ∧ f r ∉ S)"
have a_inc:"incseq a"
proof(rule incseq_SucI)
fix n
have aSn:"a (Suc n) = (SOME r. r > max (a n) (real (Suc n)) ∧ f r ∉ S)"
by(simp add: a_def)
obtain r where r:"r ≥ max (a n + 1) (Suc (Suc n))" "f r ∉ S"
using S by blast
show "a n ≤ a (Suc n)"
unfolding aSn
by(rule someI2[where a=r]) (use r in auto)
qed
have a_ge_n:"a n ≥ real n ∧ f (a n) ∉ S" for n
proof(cases n)
case 0
obtain r where r:"r ≥ 0" "f r ∉ S"
using S by blast
show ?thesis
unfolding a_def 0 nat.rec
by(rule someI2[where a=r]) (use r in auto)
next
case n':(Suc n')
then have aSn':"a (Suc n') = (SOME r. r > max (a n') (real (Suc n')) ∧ f r ∉ S)"
by(simp add: a_def)
obtain r where r:"r ≥ max (a n' + 1) (Suc (Suc n'))" "f r ∉ S"
using S by blast
show ?thesis
unfolding n' aSn'
by(rule someI2[where a=r]) (use r in auto)
qed
hence a_ge_n:"a n ≥ real n" and fan_nin_S:"f (a n) ∉ S" for n
by auto
hence "filterlim a at_top sequentially"
unfolding filterlim_at_top
by (metis order.trans eventually_sequentially of_nat_mono real_arch_simple)
hence "(λn. f (a n)) ⇢ l"
using h a_inc by simp
thus False
using S fan_nin_S
by (meson lim_explicit order.refl)
qed
qed(use filterlim_compose in blast)
lemma at_top_real_iff_all_sequentially':
fixes f :: "real ⇒ 'b :: topological_space"
shows "(f ⤏ l) at_top
⟷ (∀a. filterlim a at_top sequentially ⟶ (∀n. a n ≥ K)
⟶ incseq a ⟶ (λn. (f (a n))) ⇢ l)"
unfolding at_top_real_iff_all_sequentially
proof safe
fix a :: "nat ⇒ real"
assume h:"∀a. filterlim a at_top sequentially ⟶ (∀n. K ≤ a n)
⟶ incseq a⟶ (λn. f (a n)) ⇢ l"
and a:"filterlim a at_top sequentially" "incseq a"
then obtain N where N:"⋀n. n ≥ N ⟹ a n ≥ K"
by (metis eventually_at_top_linorder filterlim_at_top)
have a':"filterlim (λn. a (n + N)) at_top sequentially" "incseq (λn. a (n + N))"
using a filterlim_compose[OF _ filterlim_add_const_nat_at_top]
by(auto simp: incseq_Suc_iff)
show "(λn. f (a n)) ⇢ l"
by(rule LIMSEQ_offset[where k=N]) (use h N a' in fastforce)
qed simp
subsection ‹Integrals on Sets›
lemma set_borel_measurable_iff_restrict_space:
fixes f :: "'a ⇒ 'b::real_normed_vector"
assumes [measurable]:"A ∈ sets M"
shows "set_borel_measurable M A f ⟷ f ∈ borel_measurable (restrict_space M A)"
by (simp add: borel_measurable_restrict_space_iff set_borel_measurable_def)
lemma set_borel_measurable_add:
fixes f :: "_ ⇒ _ :: {second_countable_topology, topological_monoid_add, real_vector}"
assumes "set_borel_measurable M A f"
and "set_borel_measurable M A g"
shows "set_borel_measurable M A (λx. f x + g x)"
using assms by(simp add: set_borel_measurable_def scaleR_add_right)
lemma set_borel_measurable_scaleR:
fixes g :: "_ ⇒ _ :: {second_countable_topology, real_normed_vector}"
assumes "set_borel_measurable M A f"
and "set_borel_measurable M A g"
shows "set_borel_measurable M A (λx. f x *⇩R g x)"
proof -
have *:"(λx. indicat_real A x *⇩R f x *⇩R g x)
= (λx. (indicat_real A x * f x) *⇩R (indicat_real A x *⇩R g x))"
by(auto simp: indicator_def)
show ?thesis
unfolding set_borel_measurable_def *
by(rule borel_measurable_scaleR) (use assms in "auto simp: set_borel_measurable_def")
qed
lemma set_borel_measurable_times:
fixes f :: "'a ⇒ 'b::{second_countable_topology, real_normed_algebra}"
assumes "set_borel_measurable M A f"
and "set_borel_measurable M A g"
shows "set_borel_measurable M A (λx. f x * g x)"
proof -
have *:"(λx. indicat_real A x *⇩R (f x * g x))
= (λx. (indicat_real A x *⇩R f x) * (indicat_real A x *⇩R g x))"
by(auto simp: indicator_def)
show ?thesis
unfolding set_borel_measurable_def *
by(rule borel_measurable_times) (use assms in "auto simp: set_borel_measurable_def")
qed
lemma set_borel_measurable_restrict_space_iff:
fixes f :: "'a ⇒ 'b::real_normed_vector"
assumes [measurable]:"A ∈ sets M"
shows "set_borel_measurable (restrict_space M A) A f ⟷ set_borel_measurable M A f"
proof
assume "set_borel_measurable (restrict_space M A) A f"
moreover have "(λx. indicat_real A x *⇩R f x)
= (λx. if x ∈ A then indicat_real A x *⇩R f x else 0)"
by auto
ultimately show "set_borel_measurable M A f"
by(auto simp: set_borel_measurable_def measurable_restrict_space_iff[symmetric])
qed(auto simp: set_borel_measurable_def measurable_restrict_space1)
lemma set_borel_measurable_comp':
fixes f :: "'a ⇒ 'b::real_normed_vector"
assumes [measurable]: "A ∈ sets M"
and "set_borel_measurable N (g ` A) f"
and [measurable]: "g ∈ measurable M N"
shows "set_borel_measurable M A (λx. f (g x))"
proof -
have "x ∈ space (restrict_space M A) ⟹
f (g x) = ((λx. indicat_real (g ` A) x *⇩R (f x)) ∘ g) x" for x
by simp
moreover have "... ∈ borel_measurable (restrict_space M A)"
by(rule measurable_comp[where N=N])
(use assms in "auto simp: measurable_restrict_space1 set_borel_measurable_def")
ultimately show ?thesis
by(simp del: comp_apply space_restrict_space2
add: set_borel_measurable_iff_restrict_space
cong: measurable_cong)
qed
lemma set_borel_measurable_comp:
fixes f :: "_ ⇒ _ ::real_normed_vector" and g :: "_ ⇒ _::real_vector"
assumes [measurable]: "A ∈ sets M"
and "set_borel_measurable borel (g ` A) f"
and "set_borel_measurable M A g"
shows "set_borel_measurable M A (λx. f (g x))"
proof -
have "x ∈ space (restrict_space M A) ⟹
f (g x) = ((λx. indicat_real (g ` A) x *⇩R (f x))
∘ (λx. indicat_real A x *⇩R (g x))) x" for x
by simp
moreover have "... ∈ borel_measurable (restrict_space M A)"
by(rule measurable_comp[where N="restrict_space borel (g ` A)"])
(use assms in "auto simp: set_borel_measurable_def
measurable_restrict_space2_iff measurable_restrict_space1")
ultimately show ?thesis
by(simp del: comp_apply space_restrict_space2
add: set_borel_measurable_iff_restrict_space
cong: measurable_cong)
qed
lemma set_integrable_set_borel_measurable:
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
assumes "set_integrable M S f"
shows "set_borel_measurable M S f"
using assms integrable_iff_bounded set_borel_measurable_def set_integrable_def
by blast
lemma set_integrable_uminus:
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
shows "set_integrable M S (λx. - f x) ⟷ set_integrable M S f"
by(auto simp: set_integrable_def)
lemma set_integrable_const:
fixes a :: "'b::{banach, second_countable_topology}"
assumes "emeasure M S < ⊤" "S ∈ sets M"
shows "set_integrable M S (λx. a)"
using assms by(auto simp: set_integrable_def)
lemma set_integrable_zero[simp]: "set_integrable M S (λx. 0)"
by(auto simp: set_integrable_def)
lemma set_integral_cong:
assumes "⋀x. x ∈ A ⟹ f x = g x"
shows "(∫x∈A. f x ∂M) = (∫x∈A. g x ∂M)"
unfolding set_lebesgue_integral_def
by(auto intro!: Bochner_Integration.integral_cong assms simp: indicator_def)
lemma set_integrable_bounded:
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
assumes "set_borel_measurable M S f"
and S:"emeasure M S < ⊤" "S ∈ sets M"
and le:"⋀x. x ∈ S ⟹ norm (f x) ≤ K"
shows "set_integrable M S f"
unfolding set_integrable_def integrable_iff_bounded
proof
have "(∫⇧+ x. ennreal (norm (indicat_real S x *⇩R f x)) ∂M)
≤ (∫⇧+ x. ennreal (norm (indicat_real S x *⇩R K)) ∂M)"
using assms by(fastforce intro!: nn_integral_mono simp: indicator_def)
also have "... = (∫⇧+x∈S. ennreal K ∂M)"
using order.trans[OF norm_ge_zero le]
by(auto intro!: nn_integral_cong ennreal_inj[THEN iffD2] simp: indicator_def)
also have "... < ∞"
using S ennreal_less_top ennreal_mult_less_top
by(simp add: nn_integral_cmult_indicator)
finally show "(∫⇧+ x. ennreal (norm (indicat_real S x *⇩R f x)) ∂M) < ∞" .
qed(use assms in "simp add: set_borel_measurable_def")
lemma set_integral_subset_AE:
fixes f :: "_ ⇒ real"
assumes integ:"set_integrable M B f"
and AB:"A ∈ sets M" "A ⊆ B"
and nonneg:"AE x∈ B - A in M. 0 ≤ f x"
shows "(∫x∈A. f x ∂M) ≤ (∫x∈B. f x ∂M)"
using set_integrable_subset[OF integ AB] assms
unfolding set_lebesgue_integral_def set_integrable_def
by(intro Bochner_Integration.integral_mono_AE eventually_mono[OF nonneg])
(auto simp: indicator_def)
lemma set_integral_subset:
fixes f :: "_ ⇒ real"
assumes integ:"set_integrable M B f"
and AB:"A ∈ sets M" "A ⊆ B"
and nonneg:"⋀x. x∈ B - A ⟹ 0 ≤ f x"
shows "(∫x∈A. f x ∂M) ≤ (∫x∈B. f x ∂M)"
by(auto intro!: set_integral_subset_AE assms)
lemma set_integral_empty[simp]:"(∫x∈{}. f x ∂M) = 0"
by(simp add: set_lebesgue_integral_def)
lemma set_integral_null_sets:
assumes "N ∈ null_sets M"
shows "(∫x∈N. f x ∂M) = 0"
by(auto simp: set_lebesgue_integral_def indicator_def
intro!: integral_eq_zero_AE AE_I'[OF assms])
corollary LBINT_singleton[simp]:"(∫x∈{a}. f x ∂lborel) = 0"
by(auto intro!: set_integral_null_sets)
lemma not_set_integrable_integral_eq:
assumes "¬ set_integrable M A f"
shows "(∫x∈A. f x ∂M) = 0"
using assms
by(simp add: set_integrable_def set_lebesgue_integral_def not_integrable_integral_eq)
text ‹ The following is more general than @{thm set_borel_integrable_singleton}.›
lemma set_borel_integrable_singleton'[simp]: "set_integrable lborel {a} f"
unfolding set_integrable_def
by(rule integrable_cong_AE[where f="λx. 0",THEN iffD1
,OF _ measurable_cong[where f="λx. if x = a then f a else 0",THEN iffD1]])
(auto intro!: AE_I'[where N="{a}"])
lemma set_integrable_Ioc_eq_Icc:
fixes a :: "_ :: linorder_topology"
fixes f :: "_ ⇒ _ :: {banach, second_countable_topology}"
shows "set_integrable lborel {a<..b} f ⟷ set_integrable lborel {a..b} f"
proof
assume "set_integrable lborel {a<..b} f"
from set_integrable_Un[OF set_borel_integrable_singleton'[of a f] this]
have *:"set_integrable lborel ({a} ∪ {a<..b}) f"
by simp
show "set_integrable lborel {a..b} f"
by(auto intro!: set_integrable_subset[OF *])
next
assume *:"set_integrable lborel {a..b} f"
show "set_integrable lborel {a<..b} f"
by(auto intro!: set_integrable_subset[OF *])
qed
lemma LBINT_Ioc_eq_Icc:
fixes f :: "_ :: linorder_topology ⇒ _ :: {banach, second_countable_topology}"
shows "(∫x∈{a<..b}. f x ∂lborel) = (∫x∈{a..b}. f x ∂lborel)"
proof(cases "set_integrable lborel {a<..b} f ∧ a ≤ b")
assume [simp]:"set_integrable lborel {a<..b} f ∧ a ≤ b"
have "(∫x∈{a<..b}. f x ∂lborel) = (∫x∈{a<..b}. f x ∂lborel) + (∫x∈{a}. f x ∂lborel)"
by simp
also have "... = (∫x∈{a<..b} ∪ {a}. f x ∂lborel)"
by(subst set_integral_Un) auto
also have "... = (∫x∈{a..b}. f x ∂lborel)"
by(auto intro!: arg_cong[where f="λB. (∫x∈B. f x ∂lborel)"])
finally show ?thesis .
qed (auto simp: set_integrable_Ioc_eq_Icc not_set_integrable_integral_eq)
lemma set_integrable_atLeast_eq:
fixes a :: "_ :: linorder_topology"
fixes f :: "_ ⇒ _ :: {banach, second_countable_topology}"
shows "set_integrable lborel {a<..} f ⟷ set_integrable lborel {a..} f"
proof
assume "set_integrable lborel {a<..} f"
from set_integrable_Un[OF set_borel_integrable_singleton'[of a f] this]
have *:"set_integrable lborel ({a} ∪ {a<..}) f"
by simp
show "set_integrable lborel {a..} f"
by(auto intro!: set_integrable_subset[OF *])
next
assume *:"set_integrable lborel {a..} f"
show "set_integrable lborel {a<..} f"
by(auto intro!: set_integrable_subset[OF *])
qed
lemma set_integral_atLeast_eq:
fixes f :: "real ⇒ _ :: {banach, second_countable_topology}"
shows "(∫x∈{a<..}. f x ∂lborel) = (∫x∈{a..}. f x ∂lborel)"
proof(cases "set_integrable lborel {a<..} f")
assume [simp]:"set_integrable lborel {a<..} f"
have "(∫x∈{a<..}. f x ∂lborel) = (∫x∈{a<..}. f x ∂lborel) + (∫x∈{a}. f x ∂lborel)"
by simp
also have "... = (∫x∈{a<..} ∪ {a}. f x ∂lborel)"
by(subst set_integral_Un) auto
also have "... = (∫x∈{a..}. f x ∂lborel)"
by(auto intro!: arg_cong[where f="λB. (∫x∈B. f x ∂lborel)"])
finally show ?thesis .
qed (auto simp: set_integrable_atLeast_eq not_set_integrable_integral_eq)
lemma set_nn_integral_atLeast_eq:
fixes a :: "_ :: linorder_topology"
shows "(∫⇧+x∈{a<..}. f x ∂lborel) = (∫⇧+x∈{a..}. f x ∂lborel)"
apply(safe intro!: nn_integral_cong_AE AE_I'[where N="{a}"])
apply (simp add: countable_imp_null_set_lborel)
apply (metis atLeast_iff greaterThan_iff indicator_simps order_less_le)
done
lemma set_integrable_atMost_eq:
fixes b :: "_ :: linorder_topology"
fixes f :: "_ ⇒ _ :: {banach, second_countable_topology}"
shows "set_integrable lborel {..<b} f ⟷ set_integrable lborel {..b} f"
proof
assume "set_integrable lborel {..<b} f"
from set_integrable_Un[OF set_borel_integrable_singleton'[of b f] this]
have *:"set_integrable lborel ({b} ∪ {..<b}) f"
by simp
show "set_integrable lborel {..b} f"
by(auto intro!: set_integrable_subset[OF *])
next
assume *:"set_integrable lborel {..b} f"
then show "set_integrable lborel {..<b} f"
by(rule set_integrable_subset) auto
qed
lemma set_integral_atMost_eq:
fixes f :: "real ⇒ _ :: {banach, second_countable_topology}"
shows "(∫x∈{..<b}. f x ∂lborel) = (∫x∈{..b}. f x ∂lborel)"
proof(cases "set_integrable lborel {..<b} f")
assume [simp]:"set_integrable lborel {..<b} f"
have "(∫x∈{..<b}. f x ∂lborel) = (∫x∈{..<b}. f x ∂lborel) + (∫x∈{b}. f x ∂lborel)"
by simp
also have "... = (∫x∈{..<b} ∪ {b}. f x ∂lborel)"
by(subst set_integral_Un) auto
also have "... = (∫x∈{..b}. f x ∂lborel)"
by(auto intro!: arg_cong[where f="λB. (∫x∈B. f x ∂lborel)"])
finally show ?thesis .
qed (auto simp: set_integrable_atMost_eq not_set_integrable_integral_eq)
lemma set_nn_integral_atMost_eq:
fixes b :: "_ :: linorder_topology"
shows "(∫⇧+x∈{..<b}. f x ∂lborel) = (∫⇧+x∈{..b}. f x ∂lborel)"
apply(safe intro!: nn_integral_cong_AE AE_I'[where N="{b}"])
apply (simp add: countable_imp_null_set_lborel)
apply (metis atMost_iff indicator_simps lessThan_iff less_le)
done
lemma AE_False_iff_False:
assumes "0 < emeasure M A"
shows "(AE x∈A in M. False) ⟷ False"
proof
assume "AE x∈A in M. False"
thus False
using AE_iff_null_sets assms emeasure_notin_sets less_irrefl null_setsD1
by metis
qed simp
lemma nn_integral_less':
assumes [measurable]: "f ∈ borel_measurable M" "g ∈ borel_measurable M"
assumes f: "(∫⇧+x. f x ∂M) ≠ ∞"
and ord1: "AE x ∈ A in M. f x < g x" and ord2:"AE x in M. f x ≤ g x"
and pos:"0 < emeasure M A"
shows "(∫⇧+x. f x ∂M) < (∫⇧+x. g x ∂M)"
proof(rule nn_integral_less)
have A:"A ∈ sets M"
using pos emeasure_notin_sets by fastforce
show "¬ (AE x in M. g x ≤ f x)"
proof
assume h:"AE x in M. g x ≤ f x"
have "AE x∈A in M. False"
by(rule eventually_mono[OF eventually_conj[OF h ord1]]) auto
thus False
using pos AE_False_iff_False by blast
qed
qed(use assms in auto)
lemma set_nn_integral_less':
fixes f :: "_ ⇒ ennreal"
assumes "(λx. f x * indicator A x) ∈ borel_measurable M"
and "(λx. g x * indicator A x) ∈ borel_measurable M"
and "A ∈ sets M"
and "B ⊆ A"
and le:"AE x∈B in M. f x < g x" "AE x∈A in M. f x ≤ g x"
and "(∫⇧+x∈A. f x ∂M) ≠ ∞"
and "0 < emeasure M B"
shows "(∫⇧+x∈A. f x ∂M) < (∫⇧+x∈A. g x ∂M)"
using assms
by(intro nn_integral_less'[where A=B] eventually_mono[OF AE_conjI[OF le]])
(auto simp: indicator_def)
lemma set_nn_integral_less:
fixes f :: "_ ⇒ ennreal"
assumes "(λx. f x * indicator A x) ∈ borel_measurable M"
and "(λx. g x * indicator A x) ∈ borel_measurable M"
and "AE x∈A in M. f x < g x"
and "(∫⇧+x∈A. f x ∂M) ≠ ∞"
and "0 < emeasure M A"
shows "(∫⇧+x∈A. f x ∂M) < (∫⇧+x∈A. g x ∂M)"
using emeasure_neq_0_sets[of M A] assms
by(auto intro!: set_nn_integral_less'[of f A M g A])
lemma set_nn_integral_zero_less:
assumes [measurable]:"(λx. g x * indicator A x) ∈ borel_measurable M"
and pos:"AE x∈A in M. 0 < g x"
and meas:"0 < emeasure M A"
shows "0 < (∫⇧+x∈A. g x ∂M)"
using set_nn_integral_less[where f="λx. 0" and g=g and A=A] assms
by fastforce
lemma set_integral_zero_less:
fixes f :: "_ ⇒ real"
assumes integ:"set_integrable M A f"
and le:"AE x∈A in M. 0 < f x"
and meas:"0 < emeasure M A"
shows "0 < (∫x∈A. f x ∂M)"
proof -
have *:"enn2real (∫⇧+x∈A. ennreal (f x) ∂M) = (∫x∈A. f x ∂M)"
proof -
have "enn2real (∫⇧+x∈A. ennreal (f x) ∂M)
= enn2real (∫⇧+x. ennreal (indicator A x * f x) ∂M)"
by(auto intro!: arg_cong[where f=enn2real] nn_integral_cong simp: indicator_def)
also have "... = enn2real (ennreal (∫x. indicator A x * f x ∂M))"
using integ le
by(subst nn_integral_eq_integral) (auto simp: set_integrable_def)
also have "... = (∫x∈A. f x ∂M)"
using le
by(subst enn2real_ennreal)
(auto simp: set_lebesgue_integral_def intro!: integral_nonneg_AE)
finally show ?thesis .
qed
have [measurable]:"(λx. ennreal (f x) * indicator A x) ∈ borel_measurable M"
by (smt (verit, ccfv_threshold) integ mult.commute indicator_mult_ennreal
integrable_iff_bounded measurable_compose measurable_cong measurable_ennreal
real_scaleR_def set_integrable_def)
have "0 < (∫⇧+x∈A. ennreal (f x) ∂M)"
using assms
by(auto intro!: set_nn_integral_zero_less simp: set_integrable_def)
hence "0 < enn2real (∫⇧+x∈A. ennreal (f x) ∂M)"
unfolding enn2real_positive_iff
by (smt (verit, best) integ ennreal_0 ennreal_less_zero_iff ennreal_mult_top
ennreal_zero_less_mult_iff indicator_def indicator_def indicator_def indicator_def
indicator_eq_0_iff indicator_eq_0_iff indicator_simps indicator_times_eq_if
integrable_iff_bounded less_top measurable_ennreal mult.right_neutral
mult_eq_0_iff mult_eq_0_iff mult_zero_right nless_le nn_integral_mono not_le
real_norm_def real_scaleR_def set_integrable_def)
also have "... = (∫x∈A. f x ∂M)"
unfolding * ..
finally show ?thesis .
qed
lemma set_integral_zero_less':
fixes f :: "_ ⇒ real"
assumes integ:"set_integrable M A f"
and le:"AE x∈B in M. 0 < f x"
and le2:"AE x∈A in M. 0 ≤ f x"
and [measurable]:"A ∈ sets M"
and AB:"B ⊆ A"
and meas:"0 < emeasure M B"
shows "0 < (∫x∈A. f x ∂M)"
proof -
have [measurable]:"B ∈ sets M"
using meas emeasure_notin_sets by fastforce
have "0 < (∫x∈B. f x ∂M)"
by(auto intro!: set_integral_zero_less set_integrable_subset[OF integ] assms)
also have "... ≤ (∫x∈A. f x ∂M)"
using AB
by(auto intro!: set_integral_subset_AE integ eventually_mono[OF le2])
finally show ?thesis .
qed
lemma set_integral_less':
fixes f :: "_ ⇒ real"
assumes f:"set_integrable M A f"
and g:"set_integrable M A g"
and [measurable]:"A ∈ sets M"
and AB:"B ⊆ A"
and le:"AE x∈B in M. f x < g x" and le2:"AE x∈A in M. f x ≤ g x"
and meas:"0 < emeasure M B"
shows "(∫x∈A. f x ∂M) < (∫x∈A. g x ∂M)"
proof -
have "0 < (∫x∈A. g x - f x ∂M)"
using assms
by(intro set_integral_zero_less'[where B=B] set_integral_diff) auto
also have "... = (∫x∈A. g x ∂M) - (∫x∈A. f x ∂M)"
using assms by auto
finally show ?thesis
by simp
qed
lemma set_integral_less:
fixes f :: "_ ⇒ real"
assumes f:"set_integrable M A f"
and g:"set_integrable M A g"
and le:"AE x∈A in M. f x < g x"
and meas:"0 < emeasure M A"
shows "(∫x∈A. f x ∂M) < (∫x∈A. g x ∂M)"
using assms
by(intro set_integral_less'[where B=A])
(auto simp: emeasure_neq_0_sets)
corollary set_itegral_strict_mono_Icc:
fixes f :: "real ⇒ real"
fixes a b :: real
assumes integ:"set_integrable lborel {a..b} f"
and le:"AE x∈{a<..b} in lborel. 0 < f x"
shows "strict_mono_on {a..b} (λx. (∫t∈{a<..x}. f t ∂lborel))"
proof(safe intro!: strict_mono_onI)
fix r s
assume "r ∈ {a..b}" "s ∈ {a..b}" and rs[arith]:"r < s"
then have rab[arith]:"a ≤ r" "r ≤ b" and sab[arith]:"a ≤ s" "s ≤ b"
by simp_all
with rs have "(∫t∈{a<..r}. f t ∂lborel) < (∫t∈{a<..r}. f t ∂lborel) + (∫t∈{r<..s}. f t ∂lborel)"
by(auto intro!: set_integral_zero_less set_integrable_subset[OF integ] eventually_mono[OF le])
also have "... = (∫t∈{a<..s}. f t ∂lborel)"
by(subst set_integral_Un[symmetric])
(auto intro!: set_integrable_subset[OF integ] arg_cong[where f="λA. (∫t∈A. f t ∂lborel)"])
finally show "(∫t∈{a<..r}. f t ∂lborel) <(∫t∈{a<..s}. f t ∂lborel)" .
qed
corollary set_itegral_tail_strict_antimono:
fixes f :: "real ⇒ real"
assumes integ:"set_integrable lborel {a..} f"
and le:"AE x∈{a<..} in lborel. 0 < f x"
shows "strict_antimono_on {a..} (λx. (∫t∈{x<..}. f t ∂lborel))"
proof(safe intro!: monotone_onI)
fix x y
assume x[arith]:"a ≤ x" and y[arith]:"a ≤ y" and xy[arith]:"x < y"
have "(∫t∈{y<..}. f t ∂lborel) < (∫t∈{x<..y}. f t ∂lborel) + (∫t∈{y<..}. f t ∂lborel)"
by(auto intro!: set_integral_zero_less set_integrable_subset[OF integ] eventually_mono[OF le])
also have "... = (∫t∈{x<..}. f t ∂lborel)"
by(subst set_integral_Un[symmetric])
(auto intro!: set_integrable_subset[OF integ] arg_cong[where f="λA. (∫t∈A. f t ∂lborel)"])
finally show "(∫t∈{y<..}. f t ∂lborel) < (∫t∈{x<..}. f t ∂lborel)" .
qed
subsection ‹Integral of Composite Functions $g(\int_{t\in A_x} f (t)\, \mathrm{d}t)$›
lemma continuous_on_LBINT_Ioc:
fixes f :: "real ⇒ real"
assumes f: "⋀b. a ≤ b ⟹ set_integrable lborel {a..b} f"
shows "continuous_on UNIV (λb. LBINT x:{a<..b}. f x)"
by (simp add: LBINT_Ioc_eq_Icc continuous_on_LBINT f)
corollary continuous_on_LBINT_tail:
fixes f :: "real ⇒ real"
assumes f: "set_integrable lborel {a..} f"
shows "continuous_on {a..} (λb. LBINT x:{b<..}. f x)"
proof(subst continuous_on_cong)
fix b
assume b:"b ∈ {a..}"
then have "(LBINT x:{b<..}. f x) + (LBINT x:{a<..b}. f x) = (LBINT x:{a<..}. f x)"
by(subst set_integral_Un[symmetric])
(auto intro!: set_integrable_subset[OF f] arg_cong[where f="λB. (LBINT x:B. f x)"])
thus "(LBINT x:{b<..}. f x) = (LBINT x:{a<..}. f x) - (LBINT x:{a<..b}. f x)"
by argo
next
show "continuous_on {a..} (λb. (LBINT x:{a<..}. f x) - (LBINT x:{a<..b}. f x))"
by(auto intro!: continuous_on_diff continuous_on_subset[OF continuous_on_LBINT_Ioc]
set_integrable_subset[OF f])
qed simp
corollary continuous_on_LBINT_com:
fixes f :: "real ⇒ real"
assumes "integrable lborel f"
shows "isCont (λb. LBINT x:{..b}. f x) x"
proof(rule continuous_on_interior)
have f:"set_integrable lborel UNIV f"
using assms by(simp add: set_integrable_def)
show "continuous_on {x-1<..<x+1} (λb. LBINT x:{..b}. f x)"
thm continuous_on_eq_continuous_at[OF open_UNIV]
proof(subst continuous_on_cong)
fix b
assume "b ∈ {x - 1<..<x + 1}"
thus "(LBINT x:{..b}. f x) = (LBINT x:{..x-1}. f x) + (LBINT x:{x-1<..b}. f x)"
by(subst set_integral_Un[symmetric])
(auto intro!: set_integrable_subset[OF f] arg_cong[where f="λB. (LBINT x:B. f x)"])
next
show "continuous_on {x-1<..<x+1} (λb. (LBINT x:{..x-1}. f x) + (LBINT x:{x-1<..b}. f x))"
by(auto intro!: continuous_on_subset[OF continuous_on_LBINT_Ioc]
continuous_on_add set_integrable_subset[OF f])
qed simp
qed simp
lemma sets_restrict_space_sigma_sets:
assumes "sets M = sigma_sets Ω E"
and A:"A ∈ sets M" and Ao:"A ⊆ Ω"
shows "sets (restrict_space M A) = sigma_sets A ((∩) A ` E)"
by (metis assms sets_restrict_space sigma_sets_Int)
lemma Int_stable_image_inter:
assumes "Int_stable A"
shows "Int_stable ((∩) a ` A)"
proof(intro Int_stableI_image)
fix i j
assume "i ∈ A" "j ∈ A"
thus "∃k∈A. a ∩ i ∩ (a ∩ j) = a ∩ k"
using Int_stableD[OF assms]
by(auto intro!: bexI[where x="i ∩ j"])
qed
lemma
fixes f and g:: "real ⇒ real" and A B
defines "F ≡ λx::real. (∫t∈A x. f t ∂lborel)"
defines "M ≡ density (restrict_space lborel B) f"
assumes f_pos:"AE x ∈ B in lborel. 0 ≤ f x"
and f_int:"⋀x. x ∈ X ⟹ set_integrable lborel (A x) f"
and F_meas:"F ∈ (restrict_space lborel B) →⇩M restrict_space borel C"
and B:"F `B = C" and [measurable]:"B ∈ sets borel" "C ∈ sets borel" "⋀x. A x ∈ sets borel"
and AB:"B ⊆ A a" and a:"a ∈ X"
and meq:"restrict_space lborel C = distr M (restrict_space borel C) F"
shows set_integral_compose_integral:
"g ∈ borel_measurable (restrict_space borel C)
⟹ (∫t∈B. g (F t) * f t ∂lborel) = (∫t∈C. g t ∂lborel)"
and set_integrable_compose_integral:
"set_integrable lborel C g
⟹ set_integrable lborel B (λt. g (F t) * f t)"
proof -
have [simp]:"AE x in restrict_space lborel B. 0 ≤ f x"
by (simp add: AE_restrict_space_iff f_pos)
have space_M:"space M = B"
by(simp add: M_def)
have indicat_eq:"x ∈ B ⟹ indicat_real B x = indicat_real C (F x)" for x
using B by auto
have F_meas1:"F ∈ M →⇩M restrict_space borel C"
using F_meas by(simp add: M_def)
have f_intbc[measurable]:"integrable (restrict_space lborel B) f"
using set_integrable_subset[OF f_int[OF a] _ AB]
by(simp add: set_integrable_eq)
show "(∫t∈B. g (F t) * f t ∂lborel) = (∫t∈C. g t ∂lborel)"
if g_meas:"g ∈ borel_measurable (restrict_space borel C)"
proof -
have [measurable]:"(λx. indicat_real B x * g (F x))
∈ borel_measurable (restrict_space lborel B)"
using measurable_compose[OF F_meas1 g_meas]
measurable_restrict_space1[of _ _ borel B,OF measurable_id]
by(auto simp add: M_def)
have [measurable]:"(λt. indicat_real C t * g t)
∈ borel_measurable (restrict_space borel C)"
by (simp add: borel_measurable_times g_meas measurable_restrict_space1)
have "(∫t∈B. g (F t) * f t ∂lborel) = (∫t∈B. g (F t) ∂M)"
unfolding set_lebesgue_integral_def M_def
by(subst integral_density)
(auto simp: integral_restrict_space indicator_times_eq_if
intro!: f_pos Bochner_Integration.integral_cong[OF refl])
also have "... = (∫t. indicat_real C t * g t ∂distr M (restrict_space borel C) F)"
unfolding set_lebesgue_integral_def using F_meas1
by(subst integral_distr)
(auto intro!: Bochner_Integration.integral_cong simp: space_M indicat_eq[symmetric])
thm meq
also have "... = (∫t∈C. g t ∂(restrict_space lborel C))"
by(simp add: meq[symmetric] set_lebesgue_integral_def)
also have "... = (∫t∈C. g t ∂lborel)"
unfolding set_lebesgue_integral_def
by(subst integral_restrict_space)
(auto intro!: Bochner_Integration.integral_cong simp: indicator_def)
finally show "(∫t∈B. g (F t) * f t ∂lborel) = (∫t∈C. g t ∂lborel)" .
qed
assume g_integ:"set_integrable lborel C g"
have g_meas:"g ∈ borel_measurable (restrict_space borel C)"
using g_integ by(simp add: set_integrable_eq)
have [measurable]:"(λx. indicat_real B x * g (F x))
∈ borel_measurable (restrict_space lborel B)"
using measurable_compose[OF F_meas1 g_meas]
measurable_restrict_space1[of _ _ borel B,OF measurable_id]
by(auto simp add: M_def)
have [measurable]:"(λt. indicat_real C t * g t)
∈ borel_measurable (restrict_space borel C)"
by (simp add: borel_measurable_times g_meas measurable_restrict_space1)
have "set_integrable (restrict_space lborel C) C g"
unfolding set_integrable_def
by(rule Bochner_Integration.integrable_cong[where f=g,OF refl,THEN iffD1])
(use g_integ in "simp_all add: set_integrable_eq")
hence 1:"integrable (distr M (restrict_space borel C) F) (λt. indicat_real C t * g t)"
by(simp add: meq[symmetric] set_integrable_def)
have "set_integrable M B (λt. g (F t))"
using F_meas1
by(auto intro!:
Bochner_Integration.integrable_cong[THEN iffD2,OF refl _ integrable_distr[OF _ 1]]
simp: set_integrable_def indicat_eq[symmetric] space_M)
hence "integrable (restrict_space lborel B)
(λt. f t *⇩R (indicat_real B t * g (F t)))"
by(intro integrable_density[THEN iffD1])
(auto simp: set_integrable_def M_def intro!: f_pos)
hence 2:"integrable lborel
(λt. indicat_real B t *⇩R f t *⇩R (indicat_real B t * g (F t)))"
by(subst integrable_restrict_space[symmetric]) auto
show "set_integrable lborel B (λt. g (F t) * f t)"
unfolding set_integrable_def
by(auto intro!: Bochner_Integration.integrable_cong[THEN iffD1,OF refl _ 2]
simp : indicator_def)
qed
lemma
fixes f and g:: "real ⇒ real" and a b c::real
defines "F ≡ λx. (∫t∈{a<..x}. f t ∂lborel)"
assumes f_pos:"⋀x. a < x ⟹ 0 < f x"
and f_int:"⋀d. a ≤ d ⟹ set_integrable lborel {a..d} f"
and ab[arith]:"a ≤ b" and bc[arith]:"b ≤ c"
shows set_integral_compose_integral_Ioc:
"g ∈ borel_measurable (restrict_space borel {F b<..F c})
⟹ (∫t∈{b<..c}. g (F t) * f t ∂lborel) = (∫t∈{F b<..F c}. g t ∂lborel)"
and set_integrable_compose_integral_Ioc:
"set_integrable lborel {F b<..F c} g
⟹ set_integrable lborel {b<..c} (λt. g (F t) * f t)"
proof -
define M where "M ≡ density (restrict_space lborel {b<..c}) f"
have space_M:"space M = {b<..c}"
by(simp add: M_def)
have F_strict_mono:"⋀d. a ≤ d ⟹ strict_mono_on {a..d} F"
using f_pos unfolding F_def
by(intro set_itegral_strict_mono_Icc f_int) auto
have F_0:"⋀d. d ≤ a ⟹ F d = 0"
by(simp add: F_def)
have F_pos:"a < d ⟹ 0 < F d" for d
unfolding F_def using f_pos
by(intro set_integral_zero_less set_integrable_subset[OF f_int[of d]]) auto
have F_cont:"continuous_on UNIV F"
unfolding F_def
by(intro continuous_on_LBINT_Ioc f_int)
have im_F:"b ≤ d ⟹ F ` {b<..d} = {F b<..F d}" for d
by(intro image_mono_on_continuous_on_Ioc monotone_on_subset[OF F_strict_mono[of d]]
continuous_on_subset[OF F_cont])
auto
have im_F2:"b ≤ d ⟹ F ` {b..d} = {F b..F d}" for d
by(intro image_mono_on_continuous_on_Icc
strict_mono_on_imp_mono_on monotone_on_subset[OF F_strict_mono[of d]]
continuous_on_subset[OF F_cont])
auto
have F_meas1:"F ∈ M →⇩M restrict_space borel {F b<..F c}"
using im_F[OF bc] borel_measurable_continuous_onI[OF F_cont]
by(auto simp add: M_def intro!: measurable_restrict_space3)
have F_meas2:"F ∈ restrict_space borel {b<..c} →⇩M restrict_space borel {F b<..F c}"
using F_meas1 by(simp add: M_def)
have f_intbc[measurable]:"integrable (restrict_space lborel {b<..c}) f"
using set_integrable_subset[where B="{b<..c}",OF f_int[of c]]
by(fastforce simp: set_integrable_eq)
have bij:"bij_betw F {b<..c} {F b<..F c}"
proof -
have "inj_on F {b<..c}"
by(subst injective_eq_monotone_map)
(auto intro!: disjI1 monotone_on_subset[OF F_strict_mono[of c]]
continuous_on_subset[OF F_cont])
from inj_on_imp_bij_betw[OF this]
show ?thesis
unfolding im_F[OF bc] by simp
qed
have inv_mono:"x' ≤ y'"
if mono:"F x' ≤ F y'"
and x'[arith]:"b ≤ x'" "x' ≤ c"
and y'[arith]: "b ≤ y'" "y' ≤ c" for x' y'
proof(rule ccontr)
assume "¬ x' ≤ y'"
then have "F y' < F x'"
using strict_mono_onD[OF F_strict_mono[of c],of y' x']
by simp
thus False
using mono by simp
qed
have inv_strict_mono:"x' < y'"
if mono:"F x' < F y'"
and x'[arith]:"b ≤ x'" "x' ≤ c"
and y'[arith]: "b ≤ y'" "y' ≤ c" for x' y'
by (metis inv_mono leD le_less that)
have eq_indicat:"b < x ⟹ x ≤ c ⟹
indicat_real {F b<..F c} (F x) = indicat_real {b<..c} x" for x
by (auto simp: indicator_def
intro!: strict_mono_onD[OF F_strict_mono[of c]]
mono_onD[OF strict_mono_on_imp_mono_on[OF F_strict_mono[of c]]])
have ex_inv:"F b ≤ x ⟹ x ≤ F c ⟹ ∃x'. b ≤ x' ∧ x' ≤ c ∧ F x' = x" for x
by (metis (mono_tags, lifting) bc atLeastAtMost_iff im_F2 image_iff)
have eq:"emeasure (distr M (restrict_space borel {F b<..F c}) F) {x<..y} = ennreal (y - x)"
if xy[arith]:"x ≤ y" "F b ≤ x" "y ≤ F c" for x y
proof -
obtain x' y' where x'[arith]:"b ≤ x'" "x' ≤ c" and y'[arith]:"b ≤ y'" "y' ≤ c"
and x'_eq:"F x' = x" and y'_eq:"F y' = y"
using ex_inv[of x] ex_inv[of y] by auto
have [arith]:"x' ≤ y'"
by(auto intro!: inv_mono[of x' y'] simp: x'_eq y'_eq)
have [measurable]:"{x<..y} ∈ sets (restrict_space borel {F b<..F c})"
by(subst sets_restrict_space_iff) auto
have [measurable]:"{x'<..y'} ∈ sets (restrict_space borel {b<..c})"
by(subst sets_restrict_space_iff) auto
have eq_set:"F -` {x<..y} ∩ {b<..c} = {x'<..y'}"
using x'_eq y'_eq inv_mono[of _ y'] inv_strict_mono[of x']
by(auto intro!: strict_mono_onD[OF F_strict_mono[of c]]
mono_onD[OF strict_mono_on_imp_mono_on[OF F_strict_mono[of c]]])
have "emeasure (distr M (restrict_space borel {F b<..F c}) F) {x<..y}
= emeasure M (F -` {x<..y} ∩ space M)"
by(intro emeasure_distr F_meas1) simp
also have "... = emeasure M {x'<..y'}"
by(simp add: M_def eq_set)
also have "... = (∫⇧+x∈{x'<..y'}. ennreal (f x) ∂restrict_space lborel {b<..c})"
unfolding M_def
by(subst emeasure_density) auto
also have "... = ennreal (∫x∈{x'<..y'}. f x∂restrict_space lborel {b<..c})"
by(intro nn_set_integral_eq_set_integral f_intbc)
(auto intro!: less_imp_le[OF f_pos])
also have "... = ennreal (∫x∈{x'<..y'}. f x∂lborel)"
by(subst set_integral_restrict_space)
(auto intro!: arg_cong[where f=ennreal] Bochner_Integration.integral_cong
simp: set_lebesgue_integral_def indicator_def)
also have "... = ennreal (∫x. indicator {a<..y'} x * f x - indicator {a<..x'} x * f x∂lborel)"
by(auto intro!: arg_cong[where f=ennreal] Bochner_Integration.integral_cong
simp: set_lebesgue_integral_def indicator_def)
also have "... = ennreal (F y' - F x')"
using set_integrable_subset[where B="{a<..y'}",OF f_int[of c]]
set_integrable_subset[where B="{a<..x'}",OF f_int[of c]]
unfolding F_def set_lebesgue_integral_def real_scaleR_def set_integrable_def
by(fastforce intro!: arg_cong[where f=ennreal] Bochner_Integration.integral_diff)
finally show ?thesis
by(simp add: x'_eq y'_eq)
qed
have meq:"restrict_space lborel {F b<..F c} = distr M (restrict_space borel {F b<..F c}) F"
proof(rule measure_eqI_generator_eq_countable
[where Ω="{F b<..F c}" and E="(∩) {F b<..F c} ` (range (λ(a, b). {a <.. b::real}))"
and A="(∩) {F b<..F c} ` ((λ(a, b). {a <.. b::real}) ` (ℚ × ℚ))"])
show "Int_stable ((∩) {F b<..F c} ` range (λ(a, b). {a<..b}))"
by(intro Int_stable_image_inter) (fastforce intro!: Int_stableI)
next
have *:"sets (distr M (restrict_space borel {F b<..F c}) F) =
sets (restrict_space lborel {F b<..F c})"
by(simp add: M_def cong: sets_restrict_space_cong)
show "sets (restrict_space lborel {F b<..F c}) =
sigma_sets {F b<..F c} ((∩) {F b<..F c} ` range (λ(a, b). {a<..b}))"
by(intro sets_restrict_space_sigma_sets[where Ω=UNIV])
(auto simp: borel_sigma_sets_Ioc)
thus "sets (distr M (restrict_space borel {F b<..F c}) F) =
sigma_sets {F b<..F c} ((∩) {F b<..F c} ` range (λ(a, b). {a<..b}))"
unfolding * by meson
next
fix X
assume X:"X ∈ (∩) {F b<..F c} ` range (λ(a, b). {a<..b})"
then obtain x y where "X = {x<..y}" "F b ≤ x" "y ≤ F c"
by fastforce
thus "emeasure (restrict_space lborel {F b<..F c}) X =
emeasure (distr M (restrict_space borel {F b<..F c}) F) X"
by(cases "x ≤ y", subst emeasure_restrict_space)
(auto simp add: eq emeasure_restrict_space)
next
have "real_of_int ⌊F b⌋ ∈ ℚ" "real_of_int ⌈F c⌉ ∈ ℚ"
"{F b<..F c} ∩ {⌊F b⌋<..⌈F c⌉} = {F b<..F c}"
by auto
thus "⋃ ((∩) {F b<..F c} ` (λ(a, b). {a<..b}) ` (ℚ × ℚ)) = {F b<..F c}"
by blast
next
fix a
assume a:"a ∈ (∩) {F b<..F c} ` (λ(a, b). {a<..b}) ` (ℚ × ℚ)"
then have "bounded a"
using bounded_Ioc by blast
from emeasure_bounded_finite[OF this] a
show "emeasure (restrict_space lborel {F b<..F c}) a ≠ ∞"
by(subst emeasure_restrict_space) auto
qed(auto intro!: countable_rat)
have f_int':"⋀x. x ∈ {a..} ⟹ set_integrable lborel {a..x} f"
by (simp add: f_int)
have c_in:"c ∈ {a..}"
by simp
have f_nonneg:"AE x ∈ {b<..c} in lborel. 0 ≤ f x"
by(auto intro!: less_imp_le f_pos)
show "(∫t∈{b<..c}. g (F t) * f t ∂lborel) = (∫t∈{F b<..F c}. g t ∂lborel)"
if g_meas:"g ∈ borel_measurable (restrict_space borel {F b<..F c})"
using
set_integral_compose_integral[where A="λx. {a..x}" and B="{b<..c}"
and C="{F b<..F c}" and a=c and X="{a..}" and f=f and g=g
, OF f_nonneg f_int' _ _ _ _ _ _ c_in _ g_meas] meq F_meas2 im_F[of c]
by (simp add: LBINT_Ioc_eq_Icc greaterThanAtMost_subseteq_atLeastAtMost_iff F_def M_def)
show "set_integrable lborel {b<..c} (λt. g (F t) * f t)"
if g_integ:"set_integrable lborel {F b<..F c} g"
using
set_integrable_compose_integral[where A="λx. {a..x}" and B="{b<..c}"
and C="{F b<..F c}" and a=c and X="{a..}" and f=f and g=g
, OF f_nonneg f_int' _ _ _ _ _ _ c_in _ g_integ] meq F_meas2 im_F[of c]
by (simp add: LBINT_Ioc_eq_Icc greaterThanAtMost_subseteq_atLeastAtMost_iff F_def M_def)
qed
lemma
fixes f and g:: "real ⇒ real" and a b c::real
defines "F ≡ λx. (∫t∈{x<..}. f t ∂lborel)"
assumes f_pos:"⋀x. a < x ⟹ 0 < f x"
and f_int:"set_integrable lborel {a..} f"
and ab[arith]:"a ≤ b" and bc[arith]:"b ≤ c"
shows set_integral_compose_integral_tail:
"g ∈ borel_measurable (restrict_space borel {F c<..F b})
⟹ (∫t∈{b<..c}. g (F t) * f t ∂lborel) = (∫t∈{F c<..F b}. g t ∂lborel)"
and set_integrable_compose_integral_tail:
"set_integrable lborel {F c<..F b} g
⟹ set_integrable lborel {b<..c} (λt. g (F t) * f t)"
proof -
have g_meas':"g ∈ borel_measurable (restrict_space borel {F c..F b})"
if h:"g ∈ borel_measurable (restrict_space borel {F c<..F b})"
proof -
have *:"- {F c} ∩ {F c..F b} = {F c<..F b}"
by auto
have "g = (λx. if x ∈ -{F c} then g x else g (F c))"
by auto
also have "... ∈ borel_measurable (restrict_space borel {F c..F b})"
by(subst measurable_restrict_space_iff[symmetric])
(auto simp: Int_commute sets_restrict_space restrict_restrict_space * h)
finally show ?thesis .
qed
define M where "M ≡ density (restrict_space lborel {b..c}) f"
have space_M:"space M = {b..c}"
by(simp add: M_def)
have F_strict_mono:"strict_antimono_on {a..} F"
using f_pos unfolding F_def
by(intro set_itegral_tail_strict_antimono f_int) auto
hence F_mono:"antimono_on {a..} F"
using strict_antimono_iff_antimono by blast
have F_pos:"a < d ⟹ 0 < F d" for d
unfolding F_def using f_pos
by(intro set_integral_zero_less set_integrable_subset[OF f_int]
order.strict_trans2[of _ "emeasure lborel {d<..d + 1}"
"emeasure lborel {d<..}",OF _ emeasure_mono])
auto
have F_cont:"continuous_on {a..} F"
unfolding F_def
by(intro continuous_on_LBINT_tail f_int)
have im_F:"b ≤ d ⟹ F ` {b..d} = {F d..F b}" for d
using monotone_on_subset[OF F_strict_mono]
by(intro image_antimono_on_continuous_on_Icc
continuous_on_subset[OF F_cont])
(auto simp: strict_antimono_iff_antimono)
have F_meas1:"F ∈ M →⇩M restrict_space borel {F c..F b}"
using im_F[OF bc]
borel_measurable_continuous_on_restrict[OF continuous_on_subset[where t="{b..c}",OF F_cont]]
by(fastforce simp add: M_def intro!: measurable_restrict_space2)
hence F_meas2:"F ∈ restrict_space borel {b..c} →⇩M restrict_space borel {F c..F b}"
by(simp add: M_def)
have f_intbc[measurable]:"integrable (restrict_space lborel {b..c}) f"
using set_integrable_subset[where B="{b..c}",OF f_int]
by(fastforce simp: set_integrable_eq)
have inv_mono:"y' ≤ x'"
if mono:"F x' ≤ F y'"
and x'[arith]:"b ≤ x'" "x' ≤ c"
and y'[arith]: "b ≤ y'" "y' ≤ c" for x' y'
proof(rule ccontr)
assume "¬ y' ≤ x'"
thus False
using monotone_onD[OF F_strict_mono,of x' y'] mono
by simp
qed
have inv_strict_mono:"y' < x'"
if mono:"F x' < F y'"
and x'[arith]:"b ≤ x'" "x' ≤ c"
and y'[arith]: "b ≤ y'" "y' ≤ c" for x' y'
by (metis inv_mono leD le_less that)
have ex_inv:"F c ≤ x ⟹ x ≤ F b ⟹ ∃x'. b ≤ x' ∧ x' ≤ c ∧ F x' = x" for x
by (metis (mono_tags, lifting) im_F[OF bc] atLeastAtMost_iff image_iff)
have eq:"emeasure (distr M (restrict_space borel {F c..F b}) F) {x..y} = ennreal (y - x)"
if xy[arith]:"x ≤ y" "F c ≤ x" "y ≤ F b" for x y
proof -
obtain x' y' where x'[arith]:"b ≤ x'" "x' ≤ c" and y'[arith]:"b ≤ y'" "y' ≤ c"
and x'_eq:"F x' = x" and y'_eq:"F y' = y"
using ex_inv[of x] ex_inv[of y] by auto
have [arith]:"y' ≤ x'"
by(auto intro!: inv_mono[of x' y'] simp: x'_eq y'_eq)
have [measurable]:"{x..y} ∈ sets (restrict_space borel {F c..F b})"
by(subst sets_restrict_space_iff) simp_all
have [measurable]:"{y'..x'} ∈ sets (restrict_space borel {b..c})"
by(subst sets_restrict_space_iff) auto
have eq_set:"F -` {x..y} ∩ {b..c} = {y'..x'}"
using x'_eq y'_eq inv_mono[of _ y'] inv_mono[of x']
by(fastforce intro!: monotone_onD[OF F_mono])
have "emeasure (distr M (restrict_space borel {F c..F b}) F) {x..y}
= emeasure M (F -` {x..y} ∩ space M)"
by(intro emeasure_distr F_meas1) simp
also have "... = emeasure M {y'..x'}"
by(simp add: M_def eq_set)
also have "... = (∫⇧+x∈{y'..x'}. ennreal (f x) ∂restrict_space lborel {b..c})"
unfolding M_def
by(subst emeasure_density) auto
also have "... = ennreal (∫x∈{y'..x'}. f x∂restrict_space lborel {b..c})"
by(intro nn_set_integral_eq_set_integral f_intbc)
(auto intro!: AE_I'[where N="{b}"] less_imp_le[OF f_pos]
simp: countable_imp_null_set_lborel null_sets_restrict_space)
also have "... = ennreal (∫x∈{y'..x'}. f x∂lborel)"
by(subst set_integral_restrict_space)
(auto intro!: arg_cong[where f=ennreal] Bochner_Integration.integral_cong
simp: set_lebesgue_integral_def indicator_def)
also have "... = ennreal (∫x. indicator {y'..} x * f x - indicator {x'<..} x * f x∂lborel)"
by(auto intro!: arg_cong[where f=ennreal] Bochner_Integration.integral_cong
simp: set_lebesgue_integral_def indicator_def)
also have "... = ennreal ((∫x. indicator {y'..} x * f x ∂lborel)
- (∫x. indicator {x'<..} x * f x∂lborel))"
using set_integrable_subset[where B="{y'..}",OF f_int]
set_integrable_subset[where B="{x'<..}",OF f_int]
by(fastforce intro!: arg_cong[where f=ennreal] Bochner_Integration.integral_diff
simp: set_integrable_def)
also have "... = ennreal (F y' - F x')"
unfolding F_def set_integral_atLeast_eq[of y']
by(simp add: set_lebesgue_integral_def)
finally show ?thesis
by(simp add: x'_eq y'_eq)
qed
have meq:"restrict_space lborel {F c..F b} = distr M (restrict_space borel {F c..F b}) F"
proof(rule measure_eqI_generator_eq_countable
[where Ω="{F c..F b}" and E="(∩) {F c..F b} ` (range (λ(a, b). {a .. b::real}))"
and A="(∩) {F c..F b} ` ((λ(a, b). {a .. b::real}) ` (ℚ × ℚ))"])
show "Int_stable ((∩) {F c..F b} ` range (λ(a, b). {a..b}))"
by(intro Int_stable_image_inter) (fastforce intro!: Int_stableI)
next
have *:"sets (distr M (restrict_space borel {F c..F b}) F) =
sets (restrict_space lborel {F c..F b})"
by(simp add: M_def cong: sets_restrict_space_cong)
show "sets (restrict_space lborel {F c..F b}) =
sigma_sets {F c..F b} ((∩) {F c..F b} ` range (λ(a, b). {a..b}))"
by(intro sets_restrict_space_sigma_sets[where Ω=UNIV])
(auto simp: borel_eq_atLeastAtMost)
thus "sets (distr M (restrict_space borel {F c..F b}) F) =
sigma_sets {F c..F b} ((∩) {F c..F b} ` range (λ(a, b). {a..b}))"
unfolding * by meson
next
fix X
assume X:"X ∈ (∩) {F c..F b} ` range (λ(a, b). {a..b})"
then obtain x y where "X = {x..y}" "F c ≤ x" "y ≤ F b"
by fastforce
thus "emeasure (restrict_space lborel {F c..F b}) X =
emeasure (distr M (restrict_space borel {F c..F b}) F) X"
by(cases "x ≤ y", subst emeasure_restrict_space)
(auto simp add: eq emeasure_restrict_space)
next
have "real_of_int ⌊F c⌋ ∈ ℚ" "real_of_int ⌈F b⌉ ∈ ℚ"
"{F c..F b} ∩ {⌊F c⌋..⌈F b⌉} = {F c..F b}"
by auto
thus "⋃ ((∩) {F c..F b} ` (λ(a, b). {a..b}) ` (ℚ × ℚ)) = {F c..F b}"
by blast
next
fix a
assume a:"a ∈ (∩) {F c..F b} ` (λ(a, b). {a..b}) ` (ℚ × ℚ)"
then have "bounded a"
by auto
from emeasure_bounded_finite[OF this] a
show "emeasure (restrict_space lborel {F c..F b}) a ≠ ∞"
by(subst emeasure_restrict_space) auto
qed(auto intro!: countable_rat)
have f_int':"⋀x. x ∈ {a..} ⟹ set_integrable lborel {x..} f"
by (auto intro!: set_integrable_subset[OF f_int])
have a_in:"a ∈ {a..}"
by simp
have f_nonneg:"AE x∈{b..c} in lborel. 0 ≤ f x"
using less_imp_le[OF f_pos]
by(auto intro!: AE_I'[where N="{b}"])
show "(∫t∈{b<..c}. g (F t) * f t ∂lborel) = (∫t∈{F c<..F b}. g t ∂lborel)"
if g_meas:"g ∈ borel_measurable (restrict_space borel {F c<..F b})"
using set_integral_compose_integral[where A="λx. {x..}" and B="{b..c}"
and C="{F c..F b}" and a=a and X="{a..}" and f=f and g=g
,OF f_nonneg f_int' _ _ _ _ _ _ a_in _ g_meas'[OF g_meas]] meq F_meas2 im_F[of c]
by(simp add: F_def M_def LBINT_Ioc_eq_Icc[symmetric] set_integral_atLeast_eq)
show "set_integrable lborel {b<..c} (λt. g (F t) * f t)"
if integ:"set_integrable lborel {F c<..F b} g"
using set_integrable_compose_integral[where A="λx. {x..}" and B="{b..c}"
and C="{F c..F b}" and a=a and X="{a..}" and f=f and g=g
,OF f_nonneg f_int' _ _ _ _ _ _ a_in _ ] meq F_meas2 im_F[of c] integ
by(simp add: F_def M_def LBINT_Ioc_eq_Icc[symmetric]
set_integral_atLeast_eq set_integrable_Ioc_eq_Icc)
qed
subsection ‹ Convergence Theorems with Real Index›
lemma borel_measurable_LIMSEQ_metric_at_top:
fixes f :: "real ⇒ 'a ⇒ 'b :: metric_space"
assumes [measurable]: "⋀r. K ≤ r ⟹ f r ∈ borel_measurable M"
assumes lim: "⋀x. x ∈ space M ⟹ ((λr. f r x) ⤏ g x) at_top"
shows "g ∈ borel_measurable M"
by(rule borel_measurable_LIMSEQ_metric[where f="λn. f (real n + K)"])
(use assms in "auto simp: at_top_real_iff_all_sequentially add.commute[of _ K]
intro!: filterlim_compose[OF _ filterlim_tendsto_add_at_top[OF tendsto_const[of K]
filterlim_real_sequentially]]")
lemma nn_integral_at_top_real:
assumes "mono_on {K..} f" "⋀r. r ≥ K ⟹ f r ∈ borel_measurable M"
and u: "⋀x. ((λr::real. f r x) ⤏ u x) at_top"
shows "((λr. integral⇧N M (f r)) ⤏ integral⇧N M u) at_top"
using assms
by(auto intro!: nn_integral_LIMSEQ
simp: at_top_real_iff_all_sequentially'[where K=K] monotone_on_def)
theorem nn_integral_dominated_convergence_at_top:
assumes
"⋀r::real. r ≥ K ⟹ u r ∈ borel_measurable M"
"u' ∈ borel_measurable M" "w ∈ borel_measurable M"
and "⋀r. r ≥ K ⟹ AE x in M. u r x ≤ w x"
and "(∫⇧+x. w x ∂M) < ∞"
and "AE x in M. ((λr. u r x) ⤏ u' x) at_top"
shows "((λr. (∫⇧+x. u r x ∂M)) ⤏ (∫⇧+x. u' x ∂M)) at_top"
using assms
by(force intro!: nn_integral_dominated_convergence
simp: at_top_real_iff_all_sequentially'[where K=K])
lemma
fixes f :: "real ⇒ 'a ⇒ real"
assumes "⋀r. K ≤ r ⟹ integrable M (f r)" and mono: "AE x in M. mono_on {K..} (λr. f r x)"
and "AE x in M. ((λr. f r x) ⤏ u x) at_top"
and "((λr. integral⇧L M (f r)) ⤏ x) at_top"
and u:"u ∈ borel_measurable M"
shows integrable_monotone_convergence_real: "integrable M u" (is ?g1)
and integral_monotone_convergence_real: "integral⇧L M u = x" (is ?g2)
and has_bochner_integral_monotone_convergence_real: "has_bochner_integral M u x" (is ?g3)
proof -
have fl:"filterlim (λn. K + real n) at_top sequentially"
by(rule filterlim_tendsto_add_at_top) (use filterlim_real_sequentially in auto)
have inc: "incseq (λn. K + real n)"
by(auto intro!: monoI)
have "⋀n. integrable M (f (K + real n))" "AE x in M. incseq (λn. f (K + real n) x)"
"AE x in M. (λn. f (K + real n) x) ⇢ u x"
"(λn. integral⇧L M (f (K + real n))) ⇢ x"
using assms fl inc by(auto simp: at_top_real_iff_all_sequentially mono_on_def)
thus ?g1 ?g2 ?g3
using u integrable_monotone_convergence[where f="λn. f (K + real n)"]
integral_monotone_convergence[where f="λn. f (K + real n)"]
has_bochner_integral_monotone_convergence [where f="λn. f (K + real n)"]
by blast+
qed
lemma
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}" and w :: "'a ⇒ real"
assumes "f ∈ borel_measurable M" "⋀r::real. K ≤ r ⟹ s r ∈ borel_measurable M"
"integrable M w"
assumes lim: "AE x in M. ((λr. s r x) ⤏ f x) at_top"
assumes bound: "⋀r. K ≤ r ⟹ AE x in M. norm (s r x) ≤ w x"
shows integrable_dominated_convergence_real: "integrable M f"
and integrable_dominated_convergence_real2: "⋀r. K ≤ r ⟹ integrable M (s r)"
and integral_dominated_convergence_real: "((λr. integral⇧L M (s r)) ⤏ integral⇧L M f) at_top"
proof -
have fl:"filterlim (λn. r + real n) at_top sequentially" for r
by(rule filterlim_tendsto_add_at_top) (use filterlim_real_sequentially in auto)
have inc: "incseq (λn. r + real n)" for r
by(auto intro!: monoI)
show "integrable M f"
by(rule integrable_dominated_convergence[where s="λn. s (K + real n)" and w=w])
(use assms fl[of K] inc[of K] bound[of "K + real _"]
in "auto simp: at_top_real_iff_all_sequentially")
have dct:"f ∈ borel_measurable M ⟹ (⋀i. s (r + real i) ∈ borel_measurable M)
⟹ integrable M w ⟹ AE x in M. (λi. s (r + real i) x) ⇢ f x
⟹ (⋀i. AE x in M. norm (s (r + real i) x) ≤ w x) ⟹ integrable M (s r)" for r
using integrable_dominated_convergence2[where s="λn. s (r + real n)" and i=0]
by simp
show "K ≤ r ⟹ integrable M (s r)" for r
by(rule dct) (use assms fl[of r] inc[of r]
in "auto simp: at_top_real_iff_all_sequentially")
show "((λr. integral⇧L M (s r)) ⤏ integral⇧L M f) at_top"
unfolding at_top_real_iff_all_sequentially'[where K=K]
by(intro allI impI integral_dominated_convergence[where w=w])
(use assms in "auto simp: at_top_real_iff_all_sequentially")
qed
corollary
fixes f :: "real ⇒ real"
assumes f_nonneg: "⋀x. K < x ⟹ 0 ≤ f x"
and integrable: "⋀r. K < r ⟹ set_integrable M {K<..r} f"
and le:"⋀r. K < r ⟹ (∫x∈{K<..r}. f x ∂M) ≤ G"
shows interval_integral_inf:
"((λr. (∫x∈{K<..r}. f x ∂M)) ⤏ (∫x∈{K<..}. f x ∂M)) at_top"
and interval_integral_inf_integrable:
"set_integrable M {K<..} f"
and measurable_integral_inf:
"set_borel_measurable M {K<..} f"
proof -
have 1:"⋀r. K + 1 ≤ r ⟹ integrable M (λx. indicat_real {K<..r} x * f x)"
using integrable by(auto simp: set_integrable_def)
have 2: "AE x in M. mono_on {K + 1..} (λr. indicat_real {K<..r} x * f x)"
by(auto intro!: mono_onI f_nonneg simp: indicator_def)
have 3: "AE x in M.
((λr. indicat_real {K<..r} x * f x) ⤏ indicator {K<..} x * f x) at_top"
proof(rule AE_I2)
fix x
show "((λr. indicat_real {K<..r} x * f x) ⤏ indicat_real {K<..} x * f x) at_top"
by(auto intro!: tendstoI eventually_at_top_linorderI[where c=x]
simp: dist_real_def indicator_def)
qed
have "mono_on {K<..} (λr. (∫x∈{K<..r}. f x ∂M))"
using integrable f_nonneg
by(auto intro!: mono_onI Bochner_Integration.integral_mono
simp: set_lebesgue_integral_def set_integrable_def indicator_def)
from mono_convergent_real_less[OF this le]
obtain l where l:"((λr. (∫x∈{K<..r}. f x ∂M)) ⤏ l) at_top"
by blast
show "set_borel_measurable M {K<..} f"
unfolding set_borel_measurable_def
proof(rule borel_measurable_LIMSEQ_metric)
fix x
obtain n where "x ≤ K + real n"
by (meson abs_diff_le_iff real_arch_simple)
thus " (λi. indicat_real {K<..K + real i + 1} x * f x)
⇢ indicat_real {K<..} x *⇩R f x"
by(auto intro!:LIMSEQ_I exI[where x=n] simp: indicator_def)
qed(use integrable in "auto simp: set_integrable_def")
thus "((λr. (∫x∈{K<..r}. f x ∂M)) ⤏ (∫x∈{K<..}. f x ∂M)) at_top"
and "set_integrable M {K<..} f"
using integrable_monotone_convergence_real[OF 1 2 3,of l] l
integral_monotone_convergence_real[OF 1 2 3,of l ]
unfolding set_lebesgue_integral_def set_borel_measurable_def set_integrable_def
by auto
qed
corollary interval_integral_inf2:
fixes f :: "real ⇒ real"
assumes f_nonneg: "⋀x. K < x ⟹ 0 ≤ f x"
and integrable: "⋀r. K < r ⟹ set_integrable M {K<..r} f"
and integrable2:"set_integrable M {K<..} f"
shows "((λr. (∫x∈{K<..r}. f x ∂M)) ⤏ (∫x∈{K<..}. f x ∂M)) at_top"
proof(rule interval_integral_inf)
fix r
assume r:"K < r"
show "(∫x∈{K<..r}. f x ∂M) ≤ (∫x∈{K<..}. f x ∂M)"
using integrable[OF r] integrable2 f_nonneg
by(auto intro!: Bochner_Integration.integral_mono
simp: set_integrable_def set_lebesgue_integral_def indicator_def)
qed(use assms in auto)
subsection ‹ Change of Variables w.r.t. Lebesgue Integration on a Set›
lemma lebesgue_integral_change_of_variables_real1:
fixes f :: "real ⇒ real" and g :: "real⇒ real"
assumes S[measurable]: "S ∈ sets borel"
and g[measurable]:"g ∈ borel_measurable (restrict_space borel S)"
and g'[measurable]:"g' ∈ borel_measurable (restrict_space borel S)"
and der_g: "⋀x. x ∈ S ⟹ (g has_field_derivative g' x) (at x within S)"
and inj: "inj_on g S"
and integrable: "set_integrable lborel (g ` S) f"
shows "(∫x∈ g ` S. f x ∂lborel) = (∫x∈S. ¦g' x¦ * f (g x) ∂lborel)"
proof -
have *:"set_borel_measurable borel S (λx. f (g x))"
using set_borel_measurable_comp[of S borel g f]
set_integrable_set_borel_measurable[OF integrable] g
by (simp add: borel_measurable_restrict_space_iff set_borel_measurable_def)
hence [measurable]:"(λx. indicat_real S x * (¦g' x¦ * f (g x))) ∈ borel_measurable borel"
proof -
have "set_borel_measurable borel S (λx. ¦g' x¦)"
by(auto simp: set_borel_measurable_iff_restrict_space)
from set_borel_measurable_times[OF this *]
show ?thesis
by(simp add: set_borel_measurable_def)
qed
have S':"S ∈ sets lebesgue"
using S sets_lborel by blast
have h:"f absolutely_integrable_on g ` S"
using integrable by(auto simp: set_integrable_def integrable_completion)
hence h':"(λx. ¦g' x¦ * f (g x)) absolutely_integrable_on S"
using absolutely_integrable_change_of_variables_real[OF S' der_g inj]
by force
have "(∫x∈ g ` S. f x ∂lborel) = integral (g ` S) f"
by(intro set_borel_integral_eq_integral integrable)
also have "... = integral S (λx. ¦g' x¦ * f (g x))"
using has_absolute_integral_change_of_variables_1'[OF S' der_g inj] h' by blast
also have "... = (∫x∈S. ¦g' x¦ * f (g x) ∂lborel)"
by(subst set_borel_integral_eq_integral)
(use h' in"auto simp: set_integrable_def integrable_completion")
finally show ?thesis .
qed
lemma lebesgue_integral_change_of_variables_real2:
fixes f :: "real ⇒ real" and g :: "real⇒ real"
assumes S[measurable]: "S ∈ sets borel"
and f:"set_borel_measurable borel (g ` S) f"
and der_g: "⋀x. x ∈ S ⟹ (g has_field_derivative g' x) (at x within S)"
and inj: "inj_on g S"
and integrable:"set_integrable lborel S (λx. ¦g' x¦ * f (g x))"
shows "(∫x∈ g ` S. f x ∂lborel) = (∫x∈S. ¦g' x¦ * f (g x) ∂lborel)"
proof -
have S':"S ∈ sets lebesgue"
using S sets_lborel by blast
have [measurable]:"(λx. indicat_real (g ` S) x * f x) ∈ borel_measurable borel"
using f by(simp add: set_borel_measurable_def)
have h':"(λx. ¦g' x¦ * f (g x)) absolutely_integrable_on S"
using integrable by(auto simp: set_integrable_def integrable_completion)
hence h:"f absolutely_integrable_on g ` S"
using absolutely_integrable_change_of_variables_real[OF S' der_g inj]
by force
have "set_integrable lborel (g ` S) f"
using h by(auto simp: set_integrable_def integrable_completion)
hence "(∫x∈ g ` S. f x ∂lborel) = integral (g ` S) f"
by(intro set_borel_integral_eq_integral)
also have "... = integral S (λx. ¦g' x¦ * f (g x))"
using has_absolute_integral_change_of_variables_1'[OF S' der_g inj] h' by blast
also have "... = (∫x∈S. ¦g' x¦ * f (g x) ∂lborel)"
by(simp add: integrable set_borel_integral_eq_integral)
finally show ?thesis .
qed
lemma lebesgue_integrable_change_of_variables_real:
fixes f :: "real ⇒ real" and g :: "real⇒ real"
assumes S[measurable]: "S ∈ sets borel"
and f:"set_borel_measurable borel (g ` S) f"
and g[measurable]:"g ∈ borel_measurable (restrict_space borel S)"
and g'[measurable]:"g' ∈ borel_measurable (restrict_space borel S)"
and der_g: "⋀x. x ∈ S ⟹ (g has_field_derivative g' x) (at x within S)"
and inj: "inj_on g S"
shows "set_integrable lborel (g ` S) f
⟷ set_integrable lborel S (λx. ¦g' x¦ * f (g x))"
proof -
have *:"set_borel_measurable borel S (λx. f (g x))"
using set_borel_measurable_comp[of S borel g f] f g
by (simp add: borel_measurable_restrict_space_iff set_borel_measurable_def)
have [measurable]:"(λx. indicat_real S x * (¦g' x¦ * f (g x))) ∈ borel_measurable borel"
proof -
have "set_borel_measurable borel S (λx. ¦g' x¦)"
by(auto simp: set_borel_measurable_iff_restrict_space)
from set_borel_measurable_times[OF this *]
show ?thesis
by(simp add: set_borel_measurable_def)
qed
have [measurable]:"(λx. indicat_real (g ` S) x * f x) ∈ borel_measurable borel"
using f by(simp add: set_borel_measurable_def)
show ?thesis
using absolutely_integrable_change_of_variables_real[OF _ der_g inj,of f] S
by(auto simp: set_integrable_def integrable_completion)
qed
lemma nn_integral_change_of_variables_real1:
fixes f :: "real ⇒ real" and g :: "real⇒ real"
assumes S[measurable]: "S ∈ sets borel"
and g[measurable]:"g ∈ borel_measurable (restrict_space borel S)"
and g'[measurable]:"g' ∈ borel_measurable (restrict_space borel S)"
and der_g: "⋀x. x ∈ S ⟹ (g has_field_derivative g' x) (at x within S)"
and inj: "inj_on g S"
and integrable: "set_integrable lborel (g ` S) f"
and nonneg:"AE x∈S in lborel. 0 ≤ f (g x)" "AE x∈g ` S in lborel. 0 ≤ f x"
shows "(∫⇧+x∈ g ` S. ennreal (f x) ∂lborel) = (∫⇧+x∈S. ennreal (¦g' x¦ * f (g x)) ∂lborel)"
proof -
have f:"set_borel_measurable borel (g ` S) f"
using integrable by(auto simp: set_integrable_def set_borel_measurable_def)
have integrable2:"set_integrable lborel S (λx. ¦g' x¦ * f (g x))"
using lebesgue_integrable_change_of_variables_real assms f by blast
have "(∫⇧+x∈ g ` S. ennreal (f x) ∂lborel)
= (∫⇧+ x. ennreal (indicat_real (g ` S) x * f x) ∂lborel)"
using mult.commute
by(auto simp: indicator_mult_ennreal[symmetric] intro!: nn_integral_cong)
also have "... = ennreal (∫x. indicat_real (g ` S) x * f x ∂lborel)"
by(rule nn_integral_eq_integral)
(use integrable nonneg in "auto simp: set_integrable_def")
also have "... = ennreal (∫x∈ g ` S. f x ∂lborel)"
by(simp add: set_lebesgue_integral_def)
also have "... = ennreal (∫x∈S. ¦g' x¦ * f (g x) ∂lborel)"
by(intro arg_cong[where f=ennreal] lebesgue_integral_change_of_variables_real1 assms)
also have "... = ennreal (∫x. indicat_real S x * (¦g' x¦ * f (g x)) ∂lborel)"
by(simp add: set_lebesgue_integral_def)
also have "... = (∫⇧+ x. ennreal (indicat_real S x * (¦g' x¦ * f (g x))) ∂lborel)"
by(rule nn_integral_eq_integral[symmetric])
(use integrable2 nonneg in "auto simp: set_integrable_def")
also have "... = (∫⇧+x∈S. ennreal (¦g' x¦ * f (g x)) ∂lborel)"
using mult.commute
by(auto simp: indicator_mult_ennreal[symmetric] intro!: nn_integral_cong)
finally show ?thesis .
qed
lemma nn_integral_change_of_variables_real1':
fixes f :: "real ⇒ real" and g :: "real⇒ real"
assumes "S ∈ sets borel"
and "g ∈ borel_measurable (restrict_space borel S)"
and "g' ∈ borel_measurable (restrict_space borel S)"
and "⋀x. x ∈ S ⟹ (g has_field_derivative g' x) (at x within S)"
and "inj_on g S"
and "set_integrable lborel (g ` S) f"
and nonneg:"⋀x. x ∈ S ⟹ 0 ≤ f (g x)"
shows "(∫⇧+x∈ g ` S. ennreal (f x) ∂lborel) = (∫⇧+x∈S. ennreal (¦g' x¦ * f (g x)) ∂lborel)"
by(auto intro!: nn_integral_change_of_variables_real1 assms)
lemma nn_integral_change_of_variables_real2:
fixes f :: "real ⇒ real" and g :: "real⇒ real"
assumes S[measurable]: "S ∈ sets borel"
and f:"set_borel_measurable borel (g ` S) f"
and g[measurable]:"g ∈ borel_measurable (restrict_space borel S)"
and g'[measurable]:"g' ∈ borel_measurable (restrict_space borel S)"
and der_g: "⋀x. x ∈ S ⟹ (g has_field_derivative g' x) (at x within S)"
and inj: "inj_on g S"
and integrable:"set_integrable lborel S (λx. ¦g' x¦ * f (g x))"
and nonneg:"AE x∈S in lborel. 0 ≤ f (g x)" "AE x∈g ` S in lborel. 0 ≤ f x"
shows "(∫⇧+x∈ g ` S. ennreal (f x) ∂lborel) = (∫⇧+x∈S. ennreal (¦g' x¦ * f (g x)) ∂lborel)"
by(auto intro!: nn_integral_change_of_variables_real1 assms
lebesgue_integrable_change_of_variables_real[THEN iffD2])
lemma nn_integral_change_of_variables_real2':
fixes f :: "real ⇒ real" and g :: "real⇒ real"
assumes S[measurable]: "S ∈ sets borel"
and f:"set_borel_measurable borel (g ` S) f"
and g[measurable]:"g ∈ borel_measurable (restrict_space borel S)"
and g'[measurable]:"g' ∈ borel_measurable (restrict_space borel S)"
and der_g: "⋀x. x ∈ S ⟹ (g has_field_derivative g' x) (at x within S)"
and inj: "inj_on g S"
and integrable:"set_integrable lborel S (λx. ¦g' x¦ * f (g x))"
and nonneg:"⋀x. x ∈ S ⟹ 0 ≤ f (g x)"
shows "(∫⇧+x∈ g ` S. ennreal (f x) ∂lborel) = (∫⇧+x∈S. ennreal (¦g' x¦ * f (g x)) ∂lborel)"
by(auto intro!: nn_integral_change_of_variables_real2 assms)
subsection ‹Integral of Power Functions›
lemma set_integrable_inverse:
fixes a b c :: real
assumes a_pos:"0 < a"
shows "set_integrable lborel {a..b} (λx. c / x)"
using a_pos
by(cases "a ≤ b")
(auto intro!: set_integrable_bounded[where K="(abs c) / a"] divide_mono
simp: lborel_eq_real set_borel_measurable_def emeasure_interval_measure_Icc)
lemma set_integrable_inverse':
fixes a b c :: real
assumes "0 < a"
shows "set_integrable lborel {a<..b} (λx. c / x)"
by(auto intro!: set_integrable_subset[OF set_integrable_inverse] assms)
corollary set_integral_inverse:
fixes a b c :: real
assumes a_pos:"0 < a"
and a_le_b:"a ≤ b"
shows "(∫x∈{a<..b}. c / x ∂lborel) = c * (ln b - ln a)"
proof -
have ln_im:"ln ` {a<..b} = {ln a<..ln b}"
using assms
by(intro image_mono_on_continuous_on_Ioc strict_mono_on_imp_inj_on
monotone_onI ln_strict_mono continuous_on_ln)
auto
have "(∫x∈{a<..b}. c / x ∂lborel) = (∫x∈{a<..b}. ¦1 / x¦ * c ∂lborel)"
using assms by(auto intro!: Bochner_Integration.integral_cong
simp: set_lebesgue_integral_def indicator_def)
also have "... = (∫x∈ln ` {a<..b}. c ∂lborel)"
using a_pos a_le_b
by(intro lebesgue_integral_change_of_variables_real2[symmetric]
has_field_derivative_at_within[OF DERIV_ln_divide]
strict_mono_on_imp_inj_on monotone_onI ln_strict_mono)
(fastforce intro!: integrableI_bounded_set[where A="{a<..b}" and B="¦c¦ / a"]
divide_mono simp: set_borel_measurable_def set_integrable_def ln_im)+
also have "... = c * (ln b - ln a)"
by(simp add: interval_integral_Ioc[symmetric] ln_mono[OF a_le_b a_pos] ln_im)
finally show ?thesis .
qed
lemma set_integrable_powr_Icc:
fixes c :: real
assumes c:"0 < c"
shows "set_integrable lborel {c..d} (λx. x powr a)"
proof(cases "c ≤ d")
assume cd:"c ≤ d"
thus "set_integrable lborel {c..d} (λx. x powr a)"
using c
by(cases "a = - 1")
(auto intro!: borel_integrable_atLeastAtMost isCont_divide continuous_powr
simp del: times_divide_eq_left simp add: set_integrable_def mult.commute)
qed simp
lemma set_integral_powr_Icc:
fixes c :: real
assumes a:"- 1 ≠ a"
and c:"0 < c"
and cd:"c ≤ d"
shows "(∫x∈{c..d}. x powr a ∂lborel) = d powr (a + 1) / (a + 1) - c powr (a + 1) / (a + 1)"
proof -
have "(∫x∈{c..d}. x powr a ∂lborel) = (∫x. x powr a * indicat_real {c..d} x ∂lborel)"
by(simp add: set_lebesgue_integral_def mult.commute)
also have "... = d powr (a + 1) / (a + 1) - c powr (a + 1) / (a + 1)"
proof(rule integral_FTC_Icc_nonneg)
fix x
assume "x ∈ {c..d}"
then show "((λy. (y powr (a + 1)) / (a + 1)) has_real_derivative x powr a) (at x)"
using has_real_derivative_powr[of x "a + 1"] c a
DERIV_cmult[OF has_real_derivative_powr[of x "a + 1"],where c="1 / (a + 1)"]
by auto
qed(use cd in auto)
finally show "(∫x∈{c..d}. x powr a ∂lborel)
= d powr (a + 1) / (a + 1) - c powr (a + 1) / (a + 1)" .
qed
corollary set_integrable_powr_Ioc:
fixes c :: real
assumes c:"0 < c"
shows "set_integrable lborel {c<..d} (λx. x powr a)"
by(auto intro!: set_integrable_subset[OF set_integrable_powr_Icc[OF c]])
corollary set_integral_powr_Ioc:
fixes c :: real
shows "a ≠ - 1 ⟹ 0 < c ⟹ c ≤ d ⟹
(∫x∈{c<..d}. x powr a ∂lborel) = d powr (a + 1) / (a + 1) - c powr (a + 1) / (a + 1)"
by(auto intro!: set_integrable_subset[OF set_integrable_powr_Icc[of a c]]
simp: interval_integral_Ioc[symmetric] interval_integral_Icc set_integral_powr_Icc)
lemma
fixes c :: real
assumes a:"- 1 < a"
shows set_integrable_powr_from_0:"set_integrable lborel {0<..c} (λx. x powr a)"
and set_integral_powr_from_0:"0 ≤ c ⟹
(∫x∈{0<..c}. x powr a ∂lborel) = c powr (a + 1) / (a + 1)"
proof -
have *:"set_integrable lborel {0<..c} (λx. x powr a)"
"(∫x∈{0<..c}. x powr a ∂lborel) = c powr (a + 1) / (a + 1)" if c:"0 < c"
proof -
obtain N where N:"0 < N" "1 / real N < c"
using c by (metis less_Suc_eq_0_disj nat_approx_posE)
hence cn0: "⋀n. 1 / real (n + N) < c"
by (metis basic_trans_rules(21) inverse_of_nat_le le_add2 not_gr0)
have cnle0:"⋀n. 1 / real (n + N) > 0"
using N by simp
have dec:"decseq (λn. 1 / real (n + N))"
using N by (metis (mono_tags, lifting) add_le_mono1
antimonoI inverse_of_nat_le not_add_less2)
have 1:"integrable lborel (λx. indicator {1 / real (n + N)..c} x * x powr a)" for n
using set_integrable_powr_Icc[of "1 / real (n + N)" c] N
by(auto simp: set_integrable_def)
have 2:"AE x in lborel. incseq (λn. indicator {1 / real (n + N)..c} x * x powr a)"
using decseq_SucD[OF dec]
by(intro AE_I2 incseq_SucI mult_mono order.refl indicator_pos_le powr_ge_zero indicator_leI)
(meson atLeastAtMost_iff order.trans)
have 3:"AE x in lborel. (λn. indicator {1 / real (n + N)..c} x * x powr a)
⇢ indicator {0<..c} x * x powr a"
proof(intro AE_I2 tendsto_mult_right)
fix x
consider "0 < x" "x ≤ c" | "x ≤ 0" | "c < x"
by linarith
then show "(λn. indicator {1 / real (n + N)..c} x) ⇢ indicator {0<..c} x"
proof cases
assume x:"0 < x" "x ≤ c"
then obtain N' where "1 / real (N' + N) ≤ x"
by (smt (verit) inverse_of_nat_le le_add1 less_Suc_eq nat_approx_posE not_gr0)
hence "⋀n. N' ≤ n ⟹ 1 / real (n + N) ≤ x"
using N
by (metis add_mono_thms_linordered_semiring(3) inverse_of_nat_le not_add_less2
order.trans)
with x have "∀⇩F n in sequentially. indicator {1 / real (n + N)..c} x = 1"
by(auto intro!: eventually_sequentiallyI[where c=N'] simp: indicator_def)
thus ?thesis
using x atLeastAtMost_iff greaterThanAtMost_iff tendsto_eventually by fastforce
next
assume x:"x ≤ 0"
then have *:"indicator {1 / real (n + N)..c} x = 0" for n
using cnle0[of n] c
by (meson atLeastAtMost_iff indicator_eq_0_iff not_less order.strict_trans1)
thus ?thesis
using x unfolding * by force
qed simp
qed
have 4:"(λn. (∫x. indicator {1 / real (n + N)..c} x * x powr a ∂lborel))
⇢ c powr (a + 1) / (a + 1)"
proof -
have "(∫x. indicator {1 / real (n + N)..c} x * x powr a ∂lborel)
= c powr (a + 1) / (a + 1) - (1 / real (n + N)) powr (a + 1) / (a + 1)" for n
using cn0 a cnle0
by(subst set_integral_powr_Icc[symmetric])
(auto simp: set_lebesgue_integral_def less_imp_le)
moreover have "(λn. c powr (a + 1) / (a + 1) - (1 / real (n + N)) powr (a + 1) / (a + 1))
⇢ c powr (a + 1) / (a + 1)"
by(rule LIM_zero_cancel)
(use a in "auto simp: tendsto_minus_cancel_left[symmetric]
simp del: of_nat_add intro!: lim_const_over_n tendsto_divide_zero
tendsto_zero_powrI LIMSEQ_ignore_initial_segment[where a=0]")
ultimately show ?thesis
by presburger
qed
show "set_integrable lborel {0<..c} (λx. x powr a)"
and "(∫x∈{0<..c}. x powr a ∂lborel) = c powr (a + 1) / (a + 1)"
using integral_monotone_convergence[OF 1 2 3 4]
integrable_monotone_convergence[OF 1 2 3 4]
unfolding set_integrable_def set_lebesgue_integral_def
by fastforce+
qed
show "set_integrable lborel {0<..c} (λx. x powr a)"
by(cases "0 < c") (use * in auto)
show "0 ≤ c ⟹
(∫x∈{0<..c}. x powr a ∂lborel) = c powr (a + 1) / (a + 1)"
by(cases "0 < c") (use * in auto)
qed
lemma
fixes c :: real
assumes a:"a < - 1"
and c:"0 < c"
shows set_integrable_powr_inf:"set_integrable lborel {c<..} (λx. x powr a)"
and set_integral_powr_inf:"(∫x∈{c<..}. x powr a ∂lborel) = - (c powr (a + 1) / (a + 1))"
proof -
show "set_integrable lborel {c<..} (λx. x powr a)"
using a c
by(intro interval_integral_inf_integrable[where G="- (c powr (a + 1) / (a + 1))"]
set_integrable_powr_Ioc)
(auto simp: set_integral_powr_Ioc[of a c] intro!: divide_nonneg_neg)
have "((λr. (∫x∈{c<..r}. x powr a ∂lborel)) ⤏ (∫x∈{c<..}. x powr a ∂lborel)) at_top"
using a c
by(intro interval_integral_inf[where G="- (c powr (a + 1) / (a + 1))"]
set_integrable_powr_Ioc)
(auto simp: set_integral_powr_Ioc[of a c] intro!: divide_nonneg_neg)
moreover have "((λr. (∫x∈{c<..r}. x powr a ∂lborel))
⤏ - (c powr (a + 1) / (a + 1))) at_top"
proof -
have "∀⇩F r in at_top. (∫x∈{c<..r}. x powr a ∂lborel)
= r powr (a + 1) / (a + 1) - c powr (a + 1) / (a + 1)"
unfolding eventually_at_top_linorder
using a c by(auto simp add: set_integral_powr_Ioc intro!: exI[where x=c])
moreover have "((λr::real. r powr (a + 1) / (a + 1) - c powr (a + 1) / (a + 1))
⤏ - (c powr (a + 1) / (a + 1))) at_top"
using a
by(intro LIM_zero_cancel[where l="- (c powr (a + 1) / (a + 1))"])
(auto intro!: tendsto_divide_zero tendsto_neg_powr filterlim_ident)
ultimately show ?thesis
by(simp cong: tendsto_cong)
qed
ultimately show "(∫x∈{c<..}. x powr a ∂lborel) = - (c powr (a + 1) / (a + 1))"
using tendsto_unique trivial_limit_at_top_linorder by blast
qed
subsection ‹Uniform Convergence›
corollary uniform_limit_uminus_iff:
fixes f :: "_ ⇒ _ :: real_normed_vector"
shows "uniform_limit A (λi x. - fi i x) (λx. - f x) F
⟷ uniform_limit A fi f F"
using uniform_limit_uminus by fastforce
lemma uniform_lim_mult_bdd1:
fixes f :: "_ ⇒ _ :: real_normed_field"
assumes ul:"uniform_limit A fi f F"
and bdd:"bounded (g ` A)"
shows "uniform_limit A (λi x. g x * fi i x) (λx. g x * f x) F"
unfolding uniform_limit_iff
proof safe
fix e :: real
assume e:"0 < e"
obtain K where K:"⋀x. x ∈ A ⟹ norm (g x) ≤ K" "0 < K"
by (metis bdd bounded_pos image_eqI)
hence eK:"0 < e / K"
using e by simp
show "∀⇩F i in F. ∀x∈A. dist (g x * fi i x) (g x * f x) < e"
by(intro eventually_mono[OF uniform_limitD[OF ul eK]] ballI)
(smt (verit, best) K(1) dist_mult_left e frac_le
nonzero_mult_div_cancel_left norm_ge_zero zero_less_mult_iff)
qed
lemma uconvergence_on_bdd_times2:
fixes f :: "_ ⇒ _ :: real_normed_field"
assumes "uniform_limit A fi f F"
and "bounded (g ` A)"
shows "uniform_limit A (λi x. fi i x * g x) (λx. f x * g x) F"
using uniform_lim_mult_bdd1[OF assms] by(simp add: mult.commute)
lemma uniform_limit_eventually_in:
assumes lim: "uniform_limit A g g' F"
and e:"0 < e"
and d: "⋀x y. x ∈ A ⟹ dist (g' x) y < e ⟹ y ∈ B"
shows "∀⇩F t in F. ∀y∈A. g t y ∈ B"
by(rule eventually_mono[OF uniform_limitD[OF lim e]])
(use d in "simp add: Met_TC.commute")
lemma mono_on_UCT:
fixes Ui :: "_ ⇒ real ⇒ real"
assumes ab:"a ≤ b"
and mono:"∀⇩F i in F. mono_on {a..b} (Ui i)" and monoU:"mono_on {a..b} U"
and U:"continuous_on {a..b} U"
and lim: "⋀x. a ≤ x ⟹ x ≤ b ⟹ ((λi. Ui i x) ⤏ U x) F"
shows "uniform_limit {a..b} Ui U F"
proof(intro uniform_limitI)
fix e :: real
assume e:"0 < e"
hence e':"0 < e / 2"
by simp
then obtain d' where d': "d' > 0"
"⋀x y. a ≤ x ⟹ x ≤ b ⟹ a ≤ y ⟹ y ≤ b
⟹ ¦x - y¦ < d' ⟹ ¦U x - U y¦ < e / 2"
using compact_uniformly_continuous[OF U compact_interval[of a b]]
unfolding uniformly_continuous_on_def
by (metis atLeastAtMost_iff dist_real_def)
define d where "d ≡ min d' (1 / 2)"
have d_less:"d < 1" and d_pos:"0 < d"
and d:"⋀x y. a ≤ x ⟹ x ≤ b ⟹ a ≤ y ⟹ y ≤ b
⟹ ¦x - y¦ < d ⟹ ¦U x - U y¦ < e / 2"
using d' by(auto simp: d_def)
have *:"{a..b} ⊆ (⋃ ((λx. {x - d / 4<..< x + d / 4}) ` {a..b}))"
using d_pos by fastforce
then obtain K where finK:"finite K" and K_sub:"K ⊆ {a..b}"
and K: "{a..b} ⊆ (⋃x∈K. {x - d / 4<..< x + d / 4})"
using compactE_image[OF compact_interval _ *] by force
hence K': "(⋃x∈K. {x - d / 4<..< x + d / 4} ∩ {a..b}) = {a..b}"
(is "(⋃x∈K. ?A x) = {a..b}")
by blast
have K_ne:"K ≠ {}"
using K ab by fastforce
have "⋀x. x ∈ K ⟹ a ≤ max (x - d / 4) a" "⋀x. x ∈ K ⟹ max (x - d / 4) a ≤ b"
"⋀x. x ∈ K ⟹ a ≤ (min (x + d / 4) b)" "⋀x. x ∈ K ⟹ (min (x + d / 4) b) ≤ b"
using ab K_sub d_pos by auto
hence "∀x∈K. ∀⇩F i in F. ¦Ui i (max (x - d / 4) a) - U (max (x - d / 4) a)¦ < e / 2"
and "∀x∈K. ∀⇩F i in F. ¦Ui i (min (x + d / 4) b) - U (min (x + d / 4) b)¦ < e / 2"
using e' lim
unfolding tendsto_iff dist_norm real_norm_def by fast+
hence "∀⇩F i in F. ∀x∈K. ¦Ui i (max (x - d / 4) a) - U (max (x - d / 4) a)¦ < e / 2"
and "∀⇩F i in F. ∀x∈K. ¦Ui i (min (x + d / 4) b) - U (min (x + d / 4) b)¦ < e / 2"
using finK by(auto simp: eventually_ball_finite)
hence *:"∀⇩F i in F. ∀x∈K. ¦Ui i (max (x - d / 4) a) - U (max (x - d / 4) a)¦ < e / 2
∧ ¦Ui i (min (x + d / 4) b) - U (min (x + d / 4) b)¦ < e / 2"
using eventually_elim2 by fastforce
show "∀⇩F i in F. ∀x∈{a..b}. dist (Ui i x) (U x) < e"
proof(safe intro!: eventually_mono[where Q="λi. ∀x∈{a..b}. dist (Ui i x) (U x) < e",
OF eventually_conj[OF * mono]])
fix i and x :: real
assume i:"∀y∈K. ¦Ui i (max (y - d / 4) a) - U (max (y - d / 4) a)¦ < e / 2
∧ ¦Ui i (min (y + d / 4) b) - U (min (y + d / 4) b)¦ < e / 2"
and x:"x ∈ {a..b}" and monoUi:"mono_on {a..b} (Ui i)"
then obtain y where y:"y ∈ K" "x ∈ {y - d / 4<..< y + d / 4} ∩ {a..b}"
using K' by blast
have "Ui i x - U x ≤ Ui i (min (y + d / 4) b) - U (max (y - d / 4) a)"
using mono_onD[OF monoUi] y mono_onD[OF monoU]
by(auto intro!: diff_mono)
also have "... ≤ ¦Ui i (min (y + d / 4) b) - U (min (y + d / 4) b)¦
+ ¦U (min (y + d / 4) b) - U (max (y - d / 4) a)¦"
by simp
also have "... < e / 2 + e / 2"
using d[of "min (y + d / 4) b" "max (y - d / 4) a"] y i K_sub d_less d_pos
by(intro add_strict_mono) auto
also have "... = e"
by simp
finally have 1:"Ui i x - U x < e" .
have "- e = - e / 2 - e / 2"
by simp
also have "... < - ¦Ui i (max (y - d / 4) a) - U (max (y - d / 4) a)¦
- ¦U (max (y - d / 4) a) - U (min (y + d / 4) b)¦"
using y i K_sub d_less d_pos
by(intro diff_strict_mono d) auto
also have "... ≤ Ui i (max (y - d / 4) a) - U (min (y + d / 4) b)"
by linarith
also have "... ≤ Ui i x - U x"
using mono_onD[OF monoUi] y mono_onD[OF monoU]
by(auto intro!: diff_mono)
finally have 2:"- e < Ui i x - U x" .
show "dist (Ui i x) (U x) < e"
using 1 2 by (simp add: dist_real_def)
qed
qed
lemma mono_on_UCT_atLeast:
fixes f :: "'a ⇒ real ⇒ real" and g :: "real ⇒ real" and F :: "'a filter"
assumes mono: "∀⇩F i in F. mono_on {a..} (f i)"
and bdd: "∀⇩F i in F. ∀x≥a. f i x ≤ B"
and gmono: "mono_on {a..} g"
and gcont: "continuous_on {a..} g"
and glim: "(g ⤏ B) at_top"
and lim: "⋀x. a ≤ x ⟹ ((λi. f i x) ⤏ g x) F"
shows "uniform_limit {a..} f g F"
proof(safe intro!: uniform_limitI)
fix e :: real
assume e[arith]:"0 < e"
have gB:"g x ≤ B" if x:"a ≤ x" for x
using mono_onD[OF gmono] x
by(auto intro!: tendsto_lowerbound[OF glim] eventually_at_top_linorderI[where c=x])
obtain b' where b':"⋀x. b' ≤ x ⟹ ¦g x - B¦ < e / 2"
using tendstoD[OF glim half_gt_zero[OF e]]
unfolding dist_real_def eventually_at_top_linorder
by blast
define b where "b ≡ max b' a"
have b:"⋀x. b ≤ x ⟹ B - g x < e / 2" and ab:"a ≤ b"
using gB b' by(fastforce simp: b_def simp del: less_divide_eq_numeral1)+
have "e / 2 - (B - g b) > 0"
using b[OF order.refl] by simp
from tendstoD[OF lim[OF ab] this]
have "∀⇩F i in F. ¦f i b - g b¦ < e / 2 - (B - g b)"
by(auto simp: dist_real_def)
hence *:"∀⇩F i in F. B - f i b < e / 2"
by eventually_elim argo
have 1:"∀⇩F i in F. ∀x∈{b..}. dist (f i x) (g x) < e"
proof(safe intro!: eventually_mono[OF eventually_conj[OF * eventually_conj[OF bdd mono]]])
fix i x
assume h:"B - f i b < e / 2"
and mono:"mono_on {a..} (f i)"
and bx:"b ≤ x" and bdd:"∀y≥a. f i y ≤ B"
have "dist (f i x) (g x) ≤ ¦B - g x¦ + ¦B - f i x¦"
by(simp add: dist_real_def)
also have "... = B - g x + (B - f i x)"
using bdd bx gB ab by simp
also have "... ≤ B - g x + (B - f i b)"
using mono_onD[OF mono] ab bx by simp
finally show "dist (f i x) (g x) < e"
using b[OF bx] h by linarith
qed
have "uniform_limit {a..b} f g F"
by(intro mono_on_UCT[OF ab eventually_mp[OF _ mono]
mono_on_subset[OF gmono] continuous_on_subset[OF gcont] lim] eventuallyI)
(auto simp: mono_on_subset)
hence 2:"∀⇩F i in F. ∀x∈{a..b}. dist (f i x) (g x) < e"
using uniform_limitD e by blast
show "∀⇩F i in F. ∀x∈{a..}. dist (f i x) (g x) < e"
using 1 2 by eventually_elim auto
qed
lemma antimono_on_UCT:
fixes Ui :: "_ ⇒ real ⇒ real"
assumes ab:"a ≤ b"
and mono:"∀⇩F i in F. antimono_on {a..b} (Ui i)" and monoU:"antimono_on {a..b} U"
and U:"continuous_on {a..b} U"
and lim: "⋀x. a ≤ x ⟹ x ≤ b ⟹ ((λi. Ui i x) ⤏ U x) F"
shows "uniform_limit {a..b} Ui U F"
using assms mono_on_UCT[where Ui="λi x. - Ui i x" and U="λx. - U x"]
by(auto simp: antimono_on_iff_uminus_mono_on uniform_limit_uminus_iff
tendsto_minus_cancel continuous_on_minus)
end