Theory Absolute_Continuity
theory Absolute_Continuity
imports Bounded_Variation Equivalence_Lebesgue_Henstock_Integration Equivalence_Measurable_On_Borel
begin
text ‹
Absolute continuity for functions @{typ "real ⇒ 'a::euclidean_space"},
and the fundamental theorem of calculus for absolutely continuous functions.
Taken from HOL Light.
›
lemma lebesgue_measure_eq_content:
assumes "d division_of S"
shows "measure lebesgue S = sum Henstock_Kurzweil_Integration.content d"
by (metis assms content_division division_ofD(4) fmeasurableD fmeasurable_cbox
measure_completion sum.cong)
lemma content_box_cases:
"measure lborel (box a b) = (if ∀i∈Basis. a∙i ≤ b∙i then prod (λi. b∙i - a∙i) Basis else 0)"
by (simp add: measure_lborel_box_eq inner_diff)
lemma content_box_cbox:
shows "measure lborel (box a b) = measure lborel (cbox a b)"
by (simp add: content_box_cases content_cbox_cases)
lemma content_eq_0: "measure lborel (box a b) = 0 ⟷ (∃i∈Basis. b∙i ≤ a∙i)"
by (auto simp: content_box_cases not_le intro: less_imp_le antisym eq_refl)
lemma box_subset_imp_measure_le: "cbox a b ⊆ box c d ⟹ measure lborel (cbox a b) ≤ measure lborel (box c d)"
unfolding measure_def
by (intro enn2real_mono emeasure_mono) (auto simp: emeasure_lborel_cbox_eq emeasure_lborel_box_eq)
section ‹Absolute set-continuity›
definition absolutely_setcontinuous_on ::
"('a::euclidean_space set ⇒ 'b::euclidean_space) ⇒ 'a set ⇒ bool" where
"absolutely_setcontinuous_on f S ≡
(∀ε>0. ∃δ>0. ∀d T. d division_of T ∧ T ⊆ S ∧ (∑k∈d. content k) < δ
⟶ (∑k∈d. norm (f k)) < ε)"
lemma absolutely_setcontinuous_on_subset:
assumes ‹absolutely_setcontinuous_on f S› ‹T ⊆ S›
shows ‹absolutely_setcontinuous_on f T›
using assms unfolding absolutely_setcontinuous_on_def by (meson order_trans)
lemma absolutely_setcontinuous_on_imp_has_bounded_setvariation_on:
fixes f :: "real set ⇒ 'a::euclidean_space"
assumes "operative (+) 0 f" "absolutely_setcontinuous_on f S" "bounded S"
shows "has_bounded_setvariation_on f S"
proof -
from assms
obtain r where r_pos: ‹r > 0›
and r_bound: ‹⋀d T. d division_of T ⟹ T ⊆ S ⟹ (∑k∈d. content k) < r ⟹ (∑k∈d. norm (f k)) < 1›
by (metis absolutely_setcontinuous_on_def zero_less_one)
from ‹bounded S› obtain a :: real where s_sub: ‹S ⊆ cbox (-a) a›
using bounded_subset_cbox_symmetric by blast
define δ where ‹δ = min r 1 / 3›
have δ_pos: ‹δ > 0› unfolding δ_def using r_pos by auto
obtain p where p_div: ‹p tagged_division_of {-a..a}› and p_fine: ‹(λx. ball x δ) fine p›
using fine_division_exists_real[OF gauge_ball[OF δ_pos]] by blast
define D where ‹D ≡ snd ` p›
have D_div: ‹D division_of {-a..a}›
unfolding D_def using division_of_tagged_division[OF p_div] by simp
have fin_D: ‹finite D› using division_ofD(1)[OF D_div] by auto
have f_empty: ‹f {} = 0› using operative.empty[OF assms(1)] .
have "(∑k∈d. norm (f k)) ≤ card D * 1"
if div: "d division_of T" and sub: "T ⊆ S" for d T
proof -
have t_sub: "T ⊆ cbox (-a) a"
using sub s_sub by auto
have step1: "(∑k∈d. norm (f k)) ≤ (∑k∈d. ∑l∈D. norm (f (k ∩ l)))"
proof (rule sum_mono)
fix k assume kd: "k ∈ d"
then obtain c' d' where k_eq: "k = cbox c' d'" and k_ne: "k ≠ {}" and k_sub: "k ⊆ cbox (-a) a"
by (metis cbox_division_memE div dual_order.trans t_sub)
have k_div_self: "{cbox c' d'} division_of cbox c' d'"
by (metis k_ne k_eq division_of_self)
have inter_div: "{k1 ∩ k2 |k1 k2. k1 ∈ {cbox c' d'} ∧ k2 ∈ D ∧ k1 ∩ k2 ≠ {}}
division_of (cbox c' d' ∩ cbox (-a) a)"
using division_inter[OF k_div_self D_div] by auto
have k_inter: "cbox c' d' ∩ cbox (-a) a = cbox c' d'"
using k_sub k_eq by blast
then have E_div: "{cbox c' d' ∩ l |l. l ∈ D ∧ cbox c' d' ∩ l ≠ {}}
division_of cbox c' d'"
using inter_div by force
have f_split: "sum f {cbox c' d' ∩ l |l. l ∈ D ∧ cbox c' d' ∩ l ≠ {}} = f (cbox c' d')"
using operative.division[OF assms(1) E_div] by (simp add: sum_def)
have step_eq: "norm (f k) = norm (sum f {cbox c' d' ∩ l |l. l ∈ D ∧ cbox c' d' ∩ l ≠ {}})"
by (metis f_split k_eq)
have step_ext: "(∑j∈{cbox c' d' ∩ l |l. l ∈ D ∧ cbox c' d' ∩ l ≠ {}}. norm (f j))
≤ (∑l∈D. norm (f (k ∩ l)))"
proof -
have eq: "(λl. cbox c' d' ∩ l) ` {l ∈ D. cbox c' d' ∩ l ≠ {}}
= {cbox c' d' ∩ l |l. l ∈ D ∧ cbox c' d' ∩ l ≠ {}}"
by auto
have "(∑j∈{cbox c' d' ∩ l |l. l ∈ D ∧ cbox c' d' ∩ l ≠ {}}. norm (f j))
≤ (∑l∈{l ∈ D. cbox c' d' ∩ l ≠ {}}. norm (f (cbox c' d' ∩ l)))"
unfolding eq[symmetric]
by (intro order_trans[OF sum_image_le]) (auto simp: fin_D o_def)
also have ‹… ≤ (∑l∈D. norm (f (k ∩ l)))›
by (auto intro!: sum_mono2[OF fin_D] simp: k_eq)
finally show ?thesis .
qed
show "norm (f k) ≤ (∑l∈D. norm (f (k ∩ l)))"
using step_eq norm_sum step_ext
by (metis (mono_tags, lifting) order_trans)
qed
also have "(∑k∈d. ∑l∈D. norm (f (k ∩ l))) = (∑l∈D. ∑k∈d. norm (f (k ∩ l)))"
by (rule sum.swap)
also have "… ≤ card D * 1"
proof -
have "(∑l∈D. ∑k∈d. norm (f (k ∩ l))) ≤ of_nat (card D) * 1"
proof (rule sum_bounded_above)
fix l assume lD: "l ∈ D"
then obtain u v where luv: ‹l = {u..v}› and ‹{u..v} ∈ D› ‹{u..v} ≠ {}›
by (metis D_div cbox_division_memE cbox_interval)
define d' where ‹d' ≡ (λk. k ∩ {u..v}) ` {k ∈ d. k ∩ {u..v} ≠ {}}›
have ‹d' division_of T ∩ {u..v}›
proof -
have ‹{u..v} = cbox u v› by (simp add: cbox_interval)
then have ‹{{u..v}} division_of {u..v}›
using ‹{u..v} ≠ {}› division_of_self by metis
from division_inter[OF div this] show ?thesis
by (simp add: setcompr_eq_image d'_def)
qed
moreover have ‹T ∩ {u..v} ⊆ S›
using sub by auto
moreover have ‹sum content d' < r›
proof -
have content_bound: ‹sum content d' ≤ content (cbox u v)›
using subadditive_content_division[OF ‹d' division_of T ∩ {u..v}›] by auto
obtain x where ‹(x, {u..v}) ∈ p›
using ‹{u..v} ∈ D› unfolding D_def by auto
then have ‹{u..v} ⊆ ball x δ›
using fineD[OF p_fine] by auto
then have uv_in: ‹u ∈ ball x δ› ‹v ∈ ball x δ›
using ‹{u..v} ≠ {}› by auto
have ‹u ≤ v› using ‹{u..v} ≠ {}› by auto
have ‹content (cbox u v) < r›
proof -
from uv_in have ‹dist x u < δ› ‹dist x v < δ› by auto
then have ‹v - u < 2 * δ›
by (auto simp: dist_real_def)
also have ‹… ≤ 2 * (r / 3)›
unfolding δ_def by (auto simp: min_def)
also have ‹… < r› using r_pos by auto
finally show ?thesis
using ‹u ≤ v› by (simp add: cbox_interval content_real)
qed
then show ?thesis using content_bound by linarith
qed
ultimately have less1: ‹(∑k∈d'. norm (f k)) < 1›
using r_bound by presburger
show "(∑k∈d. norm (f (k ∩ l))) ≤ 1"
proof -
have fin_d: ‹finite d› using division_ofD(1)[OF div] .
have collision: ‹norm (f (k1 ∩ {u..v})) = 0›
if k1d: ‹k1 ∈ d› and k2d: ‹k2 ∈ d› and neq: ‹k1 ≠ k2›
and coll: ‹k1 ∩ {u..v} = k2 ∩ {u..v}›
for k1 k2
proof -
have ‹interior k1 ∩ interior {u..v} = interior k2 ∩ interior {u..v}›
using arg_cong[OF coll, of interior] by simp
then have ‹interior (k1 ∩ {u..v}) ⊆ interior k1 ∩ interior k2›
by auto
then have ‹interior (k1 ∩ {u..v}) = {}›
using division_ofD(5)[OF div k1d k2d neq] by auto
obtain a1 b1 where k1_eq: ‹k1 = cbox a1 b1›
using division_ofD(4)[OF div k1d] by blast
have k1_uv: ‹k1 ∩ {u..v} = cbox (max a1 u) (min b1 v)›
by (simp add: k1_eq cbox_interval)
then have ‹box (max a1 u) (min b1 v) = {}›
using ‹interior (k1 ∩ {u..v}) = {}› by simp
then show ?thesis
using operative.box_empty_imp[OF assms(1)] k1_uv by auto
qed
have fin_A: ‹finite {k ∈ d. k ∩ {u..v} ≠ {}}› using fin_d by auto
have reindex: ‹sum (λk. norm (f k)) ((λk. k ∩ {u..v}) ` {k ∈ d. k ∩ {u..v} ≠ {}})
= sum ((λk. norm (f k)) ∘ (λk. k ∩ {u..v})) {k ∈ d. k ∩ {u..v} ≠ {}}›
by (smt (verit) collision fin_A mem_Collect_eq sum.reindex_nontrivial)
have ‹(∑k∈d. norm (f (k ∩ l)))
= (∑k∈{k ∈ d. k ∩ {u..v} ≠ {}}. norm (f (k ∩ {u..v})))›
by (auto intro!: sum.mono_neutral_right simp: luv f_empty fin_d)
also have ‹… = (∑k∈d'. norm (f k))›
using reindex unfolding d'_def comp_def by auto
also have ‹… < 1› using less1 .
finally show ?thesis by simp
qed
qed
then show ?thesis by simp
qed
finally show ?thesis .
qed
then show ?thesis
using has_bounded_setvariation_on_def by blast
qed
section ‹Absolute continuity for functions›
definition absolutely_continuous_on ::
"real set ⇒ (real ⇒ 'a::euclidean_space) ⇒ bool" where
"absolutely_continuous_on S f ≡
absolutely_setcontinuous_on (λk. f (Sup k) - f (Inf k)) S"
subsection ‹Basic properties›
lemma absolutely_continuous_on_eq:
assumes eq: "⋀x. x ∈ S ⟹ f x = g x"
and ac: "absolutely_continuous_on S f"
shows "absolutely_continuous_on S g"
proof -
have "g (Sup k) - g (Inf k) = f (Sup k) - f (Inf k)" if "k ∈ d" "d division_of T" "T ⊆ S"
for k d T
proof -
from that obtain a b where kb: "k = {a..b}" and "k ⊆ T" and "a ≤ b"
by (metis atLeastatMost_empty_iff box_real(2) cbox_division_memE)
then have "a ∈ S" "b ∈ S"
using ‹k ⊆ T› ‹T ⊆ S› kb by auto
then show "g (Sup k) - g (Inf k) = f (Sup k) - f (Inf k)"
using eq kb ‹a ≤ b› by auto
qed
then show ?thesis
using ac unfolding absolutely_continuous_on_def absolutely_setcontinuous_on_def
by (metis (no_types, lifting) sum.cong)
qed
lemma absolutely_continuous_on_subset:
"absolutely_continuous_on S f ⟹ T ⊆ S ⟹ absolutely_continuous_on T f"
unfolding absolutely_continuous_on_def absolutely_setcontinuous_on_def
by (meson order_trans)
lemma absolutely_continuous_on_const [continuous_intros]:
"absolutely_continuous_on S (λx. c)"
unfolding absolutely_continuous_on_def absolutely_setcontinuous_on_def
by simp
lemma absolutely_continuous_on_cmul [continuous_intros]:
assumes ac: "absolutely_continuous_on S f"
shows "absolutely_continuous_on S (λx. a *⇩R f x)"
proof (cases "a = 0")
case True then show ?thesis
by (simp add: absolutely_continuous_on_const)
next
case False
show ?thesis
unfolding absolutely_continuous_on_def absolutely_setcontinuous_on_def
proof (intro allI impI)
fix ε :: real assume "ε > 0"
then have "ε / ¦a¦ > 0" using False by simp
then obtain δ where "δ > 0" and δ: "⋀d T. d division_of T ⟹ T ⊆ S ⟹
(∑k∈d. content k) < δ ⟹ (∑k∈d. norm (f (Sup k) - f (Inf k))) < ε / ¦a¦"
using ac unfolding absolutely_continuous_on_def absolutely_setcontinuous_on_def
by (meson order.strict_trans2)
show "∃δ>0. ∀d T. d division_of T ∧ T ⊆ S ∧ (∑k∈d. content k) < δ ⟶
(∑k∈d. norm (a *⇩R f (Sup k) - a *⇩R f (Inf k))) < ε"
proof (intro exI conjI allI impI)
show "δ > 0" by fact
next
fix d T assume H: "d division_of T ∧ T ⊆ S ∧ (∑k∈d. content k) < δ"
then have "(∑k∈d. norm (f (Sup k) - f (Inf k))) < ε / ¦a¦"
using δ by auto
then have "¦a¦ * (∑k∈d. norm (f (Sup k) - f (Inf k))) < ε"
using False by (simp add: field_simps)
moreover have "(∑k∈d. norm (a *⇩R f (Sup k) - a *⇩R f (Inf k))) =
¦a¦ * (∑k∈d. norm (f (Sup k) - f (Inf k)))"
by (simp add: scaleR_diff_right[symmetric] sum_distrib_left)
ultimately show "(∑k∈d. norm (a *⇩R f (Sup k) - a *⇩R f (Inf k))) < ε"
by linarith
qed
qed
qed
lemma absolutely_continuous_on_neg [continuous_intros]:
"absolutely_continuous_on S f ⟹ absolutely_continuous_on S (λx. - f x)"
using absolutely_continuous_on_cmul[of S f "-1"] by simp
lemma absolutely_continuous_on_add [continuous_intros]:
assumes "absolutely_continuous_on S f" and g: "absolutely_continuous_on S g"
shows "absolutely_continuous_on S (λx. f x + g x)"
unfolding absolutely_continuous_on_def absolutely_setcontinuous_on_def
proof (intro allI impI)
fix ε :: real assume "ε > 0"
obtain δ1 δ2 where "δ1 > 0" and δ1: "∀d T. d division_of T ∧ T ⊆ S ∧ (∑k∈d. content k) < δ1 ⟶
(∑k∈d. norm (f (Sup k) - f (Inf k))) < ε/2"
and "δ2 > 0" and δ2: "∀d T. d division_of T ∧ T ⊆ S ∧ (∑k∈d. content k) < δ2 ⟶
(∑k∈d. norm (g (Sup k) - g (Inf k))) < ε/2"
using assms ‹ε > 0›
unfolding absolutely_continuous_on_def absolutely_setcontinuous_on_def
by (metis (lifting) less_divide_eq_numeral1(1) mult_zero_left)
show "∃δ>0. ∀d T. d division_of T ∧ T ⊆ S ∧ (∑k∈d. content k) < δ ⟶
(∑k∈d. norm (f (Sup k) + g (Sup k) - (f (Inf k) + g (Inf k)))) < ε"
proof (intro exI conjI allI impI)
show "min δ1 δ2 > 0" using ‹δ1 > 0› ‹δ2 > 0› by auto
next
fix d T assume H: "d division_of T ∧ T ⊆ S ∧ (∑k∈d. content k) < min δ1 δ2"
have f_bd: "(∑k∈d. norm (f (Sup k) - f (Inf k))) < ε/2" using δ1 H by auto
have g_bd: "(∑k∈d. norm (g (Sup k) - g (Inf k))) < ε/2" using δ2 H by auto
have "(∑k∈d. norm (f (Sup k) + g (Sup k) - (f (Inf k) + g (Inf k)))) ≤
(∑k∈d. norm (f (Sup k) - f (Inf k)) + norm (g (Sup k) - g (Inf k)))"
by (intro sum_mono norm_diff_triangle_ineq)
also have "… = (∑k∈d. norm (f (Sup k) - f (Inf k))) + (∑k∈d. norm (g (Sup k) - g (Inf k)))"
by (rule sum.distrib)
also have "… < ε" using f_bd g_bd by linarith
finally show "(∑k∈d. norm (f (Sup k) + g (Sup k) - (f (Inf k) + g (Inf k)))) < ε" .
qed
qed
lemma absolutely_continuous_on_sub [continuous_intros]:
"absolutely_continuous_on S f ⟹ absolutely_continuous_on S g ⟹
absolutely_continuous_on S (λx. f x - g x)"
using absolutely_continuous_on_add[of S f "λx. - g x"] absolutely_continuous_on_neg by auto
lemma absolutely_continuous_on_norm [continuous_intros]:
assumes ac: "absolutely_continuous_on S f"
shows "absolutely_continuous_on S (λx. norm (f x) *⇩R e)"
proof (cases "e = 0")
case True then show ?thesis by (simp add: absolutely_continuous_on_const)
next
case False
show ?thesis
unfolding absolutely_continuous_on_def absolutely_setcontinuous_on_def
proof (intro allI impI)
fix ε :: real assume "ε > 0"
then have "ε / norm e > 0" using False by simp
then obtain δ where "δ > 0" and δ: "⋀d T. d division_of T ⟹ T ⊆ S ⟹
(∑k∈d. content k) < δ ⟹ (∑k∈d. norm (f (Sup k) - f (Inf k))) < ε / norm e"
using ac unfolding absolutely_continuous_on_def absolutely_setcontinuous_on_def
by (meson order.strict_trans2)
show "∃δ>0. ∀d T. d division_of T ∧ T ⊆ S ∧ (∑k∈d. content k) < δ ⟶
(∑k∈d. norm (norm (f (Sup k)) *⇩R e - norm (f (Inf k)) *⇩R e)) < ε"
proof (intro exI conjI allI impI)
show "δ > 0" by fact
next
fix d T assume H: "d division_of T ∧ T ⊆ S ∧ (∑k∈d. content k) < δ"
have bd: "(∑k∈d. norm (f (Sup k) - f (Inf k))) < ε / norm e"
using δ H by auto
have "(∑k∈d. norm (norm (f (Sup k)) *⇩R e - norm (f (Inf k)) *⇩R e)) =
(∑k∈d. ¦norm (f (Sup k)) - norm (f (Inf k))¦ * norm e)"
by (simp add: scaleR_diff_left[symmetric] abs_real_def norm_scaleR)
also have "… ≤ (∑k∈d. norm (f (Sup k) - f (Inf k)) * norm e)"
by (intro sum_mono mult_right_mono norm_triangle_ineq3) auto
also have "… = (∑k∈d. norm (f (Sup k) - f (Inf k))) * norm e"
by (simp add: sum_distrib_right)
also have "… < (ε / norm e) * norm e"
using bd False by (intro mult_strict_right_mono) auto
also have "… = ε" using False by simp
finally show "(∑k∈d. norm (norm (f (Sup k)) *⇩R e - norm (f (Inf k)) *⇩R e)) < ε" .
qed
qed
qed
lemma absolutely_continuous_on_compose_linear [continuous_intros]:
assumes ac: "absolutely_continuous_on S f" and lin: "linear h"
shows "absolutely_continuous_on S (h ∘ f)"
proof -
obtain K where "K > 0" and K: "⋀x. norm (h x) ≤ norm x * K"
using lin linear_conv_bounded_linear bounded_linear.pos_bounded by blast
show ?thesis
unfolding absolutely_continuous_on_def absolutely_setcontinuous_on_def o_def
proof (intro allI impI)
fix ε :: real assume "ε > 0"
then have "ε / K > 0" using ‹K > 0› by simp
then obtain δ where "δ > 0" and δ: "⋀d T. d division_of T ⟹ T ⊆ S ⟹
(∑k∈d. content k) < δ ⟹ (∑k∈d. norm (f (Sup k) - f (Inf k))) < ε / K"
using ac unfolding absolutely_continuous_on_def absolutely_setcontinuous_on_def
by (meson order.strict_trans2)
show "∃δ>0. ∀d T. d division_of T ∧ T ⊆ S ∧ (∑k∈d. content k) < δ ⟶
(∑k∈d. norm (h (f (Sup k)) - h (f (Inf k)))) < ε"
proof (intro exI conjI allI impI)
show "δ > 0" by fact
next
fix d T assume H: "d division_of T ∧ T ⊆ S ∧ (∑k∈d. content k) < δ"
have "(∑k∈d. norm (h (f (Sup k)) - h (f (Inf k)))) =
(∑k∈d. norm (h (f (Sup k) - f (Inf k))))"
using lin by (simp add: linear_diff)
also have "… ≤ (∑k∈d. norm (f (Sup k) - f (Inf k)) * K)"
by (intro sum_mono K)
also have "… = (∑k∈d. norm (f (Sup k) - f (Inf k))) * K"
by (simp add: sum_distrib_right)
also have "… < (ε / K) * K"
using δ H ‹K > 0› by (intro mult_strict_right_mono) auto
also have "… = ε" using ‹K > 0› by simp
finally show "(∑k∈d. norm (h (f (Sup k)) - h (f (Inf k)))) < ε" .
qed
qed
qed
lemma absolutely_continuous_on_null:
assumes "content {a..b} = 0"
shows "absolutely_continuous_on {a..b} f"
unfolding absolutely_continuous_on_def absolutely_setcontinuous_on_def
proof (intro allI impI)
fix ε :: real assume "ε > 0"
show "∃δ>0. ∀d T. d division_of T ∧ T ⊆ {a..b} ∧ (∑k∈d. content k) < δ ⟶
(∑k∈d. norm (f (Sup k) - f (Inf k))) < ε"
proof (intro exI conjI allI impI)
fix d T assume H: "d division_of T ∧ T ⊆ {a..b} ∧ (∑k∈d. content k) < 1"
then have div: "d division_of T" and sub: "T ⊆ {a..b}" by auto
have "∀k∈d. f (Sup k) - f (Inf k) = 0"
proof
fix k assume kd: "k ∈ d"
then obtain u v where uv: "k = cbox u v" and kt: "k ⊆ T" and "u ≤ v" "k ⊆ {a..b}"
by (metis atLeastatMost_empty' box_real(2) cbox_division_memE div sub subset_trans)
then have "u = v"
using assms by auto
then show "f (Sup k) - f (Inf k) = 0"
using uv by simp
qed
then show "(∑k∈d. norm (f (Sup k) - f (Inf k))) < ε"
using ‹ε > 0› by simp
qed auto
qed
lemma absolutely_continuous_on_id: "absolutely_continuous_on {a..b} id"
unfolding absolutely_continuous_on_def absolutely_setcontinuous_on_def
proof (intro allI impI)
fix ε :: real assume "ε > 0"
show "∃δ>0. ∀d T. d division_of T ∧ T ⊆ {a..b} ∧ (∑k∈d. content k) < δ ⟶
(∑k∈d. norm (id (Sup k) - id (Inf k))) < ε"
proof (intro exI conjI allI impI)
show "ε > 0" by fact
next
fix d T assume H: "d division_of T ∧ T ⊆ {a..b} ∧ (∑k∈d. content k) < ε"
then have div: "d division_of T" by auto
have "(∑k∈d. norm (id (Sup k) - id (Inf k))) = (∑k∈d. content k)"
proof (rule sum.cong, simp)
fix k assume kd: "k ∈ d"
then obtain u v where uv: "k = cbox u v" and kt: "k ⊆ T" and "u ≤ v"
by (metis div atLeastatMost_empty_iff box_real(2) cbox_division_memE)
then show "norm (id (Sup k) - id (Inf k)) = content k"
using uv by (simp add: content_real)
qed
also have "… < ε" using H by auto
finally show "(∑k∈d. norm (id (Sup k) - id (Inf k))) < ε" .
qed
qed
subsection ‹Relationship to bounded variation and continuity›
lemma absolutely_continuous_on_imp_continuous:
assumes "absolutely_continuous_on S f" "is_interval S"
shows "continuous_on S f"
proof (rule continuous_on_iff[THEN iffD2], intro ballI allI impI)
fix x ε :: real assume xs: "x ∈ S" and "ε > 0"
then obtain δ where "δ > 0" and δ: "⋀d T. d division_of T ⟹ T ⊆ S ⟹
(∑k∈d. content k) < δ ⟹ (∑k∈d. norm (f (Sup k) - f (Inf k))) < ε"
using assms(1) unfolding absolutely_continuous_on_def absolutely_setcontinuous_on_def
by (meson order.strict_trans2)
show "∃δ>0. ∀x'∈S. dist x' x < δ ⟶ dist (f x') (f x) < ε"
proof (intro exI conjI ballI impI)
show "δ > 0" by fact
next
fix y assume ys: "y ∈ S" and dyx: "dist y x < δ"
show "dist (f y) (f x) < ε"
proof (cases "x = y")
case True then show ?thesis using ‹ε > 0› by simp
next
case False
define lo hi where "lo = min x y" and "hi = max x y"
then have lohi: "lo ≤ hi" and lox: "lo ≤ x" and hix: "x ≤ hi"
and loy: "lo ≤ y" and hiy: "y ≤ hi"
by (auto simp: min_def max_def)
have sub: "{lo..hi} ⊆ S"
by (metis assms(2) box_real(2) hi_def interval_subset_is_interval lo_def max_def min_def xs ys)
have ne: "cbox lo hi ≠ {}" using lohi by auto
have div: "{cbox lo hi} division_of cbox lo hi"
by (rule division_of_self[OF ne])
have "(∑k∈{cbox lo hi}. content k) = content {lo..hi}" by simp
also have "… = hi - lo" using content_real lohi by auto
also have "… = dist y x"
unfolding lo_def hi_def dist_real_def by (auto simp: min_def max_def)
also have "… < δ" by fact
finally have sm: "(∑k∈{cbox lo hi}. content k) < δ" .
have "(∑k∈{cbox lo hi}. norm (f (Sup k) - f (Inf k))) < ε"
using δ[OF div] sub sm by auto
then have "norm (f hi - f lo) < ε" using lohi by simp
then show "dist (f y) (f x) < ε"
using ‹norm (f hi - f lo) < ε› lo_def hi_def
by (cases "x ≤ y") (auto simp: dist_norm norm_minus_commute)
qed
qed
qed
lemma operative_function_endpoint_diff:
fixes f :: ‹real ⇒ 'a::real_normed_vector›
defines ‹h ≡ λS. if S = {} then 0 else f (Sup S) - f (Inf S)›
shows ‹operative (+) 0 h›
proof (rule operative.intro)
show ‹comm_monoid_set (+) (0::'a)›
using sum.comm_monoid_set_axioms .
next
show ‹operative_axioms (+) 0 h›
proof (rule operative_axioms.intro)
fix a b :: real
assume ‹box a b = {}›
then show ‹h (cbox a b) = 0›
by (cases ‹a = b›) (auto simp: h_def cbox_interval)
next
fix a b c :: real and k :: real
assume ‹k ∈ Basis›
then have k1: ‹k = 1› by (simp add: Basis_real_def)
have eq1: ‹cbox a b ∩ {x. x ∙ k ≤ c} = {a..min b c}› if ‹a ≤ b› for c
using k1 that by (auto simp: cbox_interval min_def)
have eq2: ‹cbox a b ∩ {x. c ≤ x ∙ k} = {max a c..b}› if ‹a ≤ b› for c
using k1 that by (auto simp: cbox_interval max_def)
show ‹h (cbox a b) = h (cbox a b ∩ {x. x ∙ k ≤ c}) + h (cbox a b ∩ {x. c ≤ x ∙ k})›
proof (cases ‹a ≤ b›)
case True
then show ?thesis
using eq1[OF True] eq2[OF True]
by (cases ‹c < a›; cases ‹b < c›) (auto simp: h_def cbox_interval min_def max_def)
next
case False
then have ‹cbox a b = {}› by (auto simp: cbox_interval)
then show ?thesis by (simp add: h_def)
qed
qed
qed
lemma operative_absolutely_setcontinuous_on:
fixes g :: ‹'a::euclidean_space set ⇒ 'b::euclidean_space›
assumes ‹operative (+) 0 g›
shows ‹operative (∧) True (absolutely_setcontinuous_on g)›
proof (intro operative.intro comm_monoid_set_and operative_axioms.intro iffI)
note null = operative.box_empty_imp[OF assms]
note split = operative.Basis_imp[OF assms, symmetric]
show ‹absolutely_setcontinuous_on g (cbox a b)› if ‹box a b = {}› for a b
proof -
have ‹g k = 0› if ‹k ∈ d› and ‹d division_of T› and ‹T ⊆ cbox a b› for k d T
by (metis ‹box a b = {}› cbox_division_memE negligible_interval(1) negligible_subset null
that)
then show ?thesis using that
unfolding absolutely_setcontinuous_on_def
by (intro iffI TrueI allI impI exI[of _ 1]) (auto simp: division_ofD(1))
qed
fix a b c and k::'a
assume ‹k ∈ Basis›
assume ac: ‹absolutely_setcontinuous_on g (cbox a b ∩ {x. x ∙ k ≤ c}) ∧
absolutely_setcontinuous_on g (cbox a b ∩ {x. c ≤ x ∙ k})›
show ‹absolutely_setcontinuous_on g (cbox a b)›
unfolding absolutely_setcontinuous_on_def
proof (intro allI impI)
fix e :: real assume ‹e > 0›
then have e2: ‹e / 2 > 0› by simp
from ac[unfolded absolutely_setcontinuous_on_def] e2
obtain r1 where r1: ‹r1 > 0›
and L: ‹⋀d T. d division_of T ⟹ T ⊆ cbox a b ∩ {x. x ∙ k ≤ c} ⟹
(∑k∈d. content k) < r1 ⟹ (∑k∈d. norm (g k)) < e / 2›
by metis
from ac[unfolded absolutely_setcontinuous_on_def] e2
obtain r2 where r2: ‹r2 > 0›
and R: ‹⋀d T. d division_of T ⟹ T ⊆ cbox a b ∩ {x. c ≤ x ∙ k} ⟹
(∑k∈d. content k) < r2 ⟹ (∑k∈d. norm (g k)) < e / 2›
by metis
show ‹∃δ>0. ∀d T. d division_of T ∧ T ⊆ cbox a b ∧
(∑k∈d. content k) < δ ⟶ (∑k∈d. norm (g k)) < e›
proof (intro exI[of _ ‹min r1 r2›] conjI allI impI)
show ‹min r1 r2 > 0› using r1 r2 by simp
next
fix d T
assume H: ‹d division_of T ∧ T ⊆ cbox a b ∧ (∑k∈d. content k) < min r1 r2›
then have div: ‹d division_of T› and sub: ‹T ⊆ cbox a b›
and content_bound: ‹(∑k∈d. content k) < r1› ‹(∑k∈d. content k) < r2›
by auto
define dL where ‹dL = (λl. l ∩ {x. x ∙ k ≤ c}) ` {l ∈ d. l ∩ {x. x ∙ k ≤ c} ≠ {}}›
define dR where ‹dR = (λl. l ∩ {x. c ≤ x ∙ k}) ` {l ∈ d. l ∩ {x. c ≤ x ∙ k} ≠ {}}›
have fin_d: ‹finite d› using division_of_finite[OF div] .
have g_empty: ‹g {} = 0› using operative.empty[OF assms] .
have ‹(∑K∈d. norm (g K))
≤ (∑K∈d. norm (g (K ∩ {x. x ∙ k ≤ c})) + norm (g (K ∩ {x. c ≤ x ∙ k})))›
proof (rule sum_mono)
fix K assume Kd: ‹K ∈ d›
then obtain aK bK where K_eq: ‹K = cbox aK bK› using division_ofD(4)[OF div] by blast
have ‹g K = g (K ∩ {x. x ∙ k ≤ c}) + g (K ∩ {x. c ≤ x ∙ k})›
using local.split[OF ‹k ∈ Basis›, of aK bK c] K_eq by simp
then show ‹norm (g K) ≤ norm (g (K ∩ {x. x ∙ k ≤ c})) + norm (g (K ∩ {x. c ≤ x ∙ k}))›
by (metis norm_triangle_ineq)
qed
then have step1: ‹(∑K∈d. norm (g K))
≤ (∑K∈d. norm (g (K ∩ {x. x ∙ k ≤ c}))) + (∑K∈d. norm (g (K ∩ {x. c ≤ x ∙ k})))›
by (metis (no_types, lifting) sum.distrib sum.cong)
have step2L: ‹(∑K∈d. norm (g (K ∩ {x. x ∙ k ≤ c})))
= (∑K∈{l ∈ d. l ∩ {x. x ∙ k ≤ c} ≠ {}}. norm (g (K ∩ {x. x ∙ k ≤ c})))›
by (rule sum.mono_neutral_right) (auto simp: fin_d g_empty)
have step2R: ‹(∑K∈d. norm (g (K ∩ {x. c ≤ x ∙ k})))
= (∑K∈{l ∈ d. l ∩ {x. c ≤ x ∙ k} ≠ {}}. norm (g (K ∩ {x. c ≤ x ∙ k})))›
by (rule sum.mono_neutral_right) (auto simp: fin_d g_empty)
have collision_L: ‹norm (g (K1 ∩ {x. x ∙ k ≤ c})) = 0›
if K1d: ‹K1 ∈ d› and K2d: ‹K2 ∈ d› and neq: ‹K1 ≠ K2›
and coll: ‹K1 ∩ {x. x ∙ k ≤ c} = K2 ∩ {x. x ∙ k ≤ c}›
for K1 K2
proof -
obtain a1 b1 where K1_eq: ‹K1 = cbox a1 b1› using division_ofD(4)[OF div K1d] by blast
have eq: ‹K1 ∩ {x. x ∙ k ≤ c} = cbox a1 (∑i∈Basis. (if i = k then min (b1 ∙ k) c else b1 ∙ i) *⇩R i)›
using interval_split(1)[OF ‹k ∈ Basis›] K1_eq by simp
have ‹interior (K1 ∩ {x. x ∙ k ≤ c}) ⊆ interior K1 ∩ interior K2›
using coll by (metis inf.cobounded1 interior_mono le_inf_iff)
also have ‹… = {}› using division_ofD(5)[OF div K1d K2d neq] .
finally have ‹box a1 (∑i∈Basis. (if i = k then min (b1 ∙ k) c else b1 ∙ i) *⇩R i) = {}›
using eq interior_cbox by auto
then show ?thesis using null eq by auto
qed
have collision_R: ‹norm (g (K1 ∩ {x. c ≤ x ∙ k})) = 0›
if K1d: ‹K1 ∈ d› and K2d: ‹K2 ∈ d› and neq: ‹K1 ≠ K2›
and coll: ‹K1 ∩ {x. c ≤ x ∙ k} = K2 ∩ {x. c ≤ x ∙ k}›
for K1 K2
proof -
obtain a1 b1 where K1_eq: ‹K1 = cbox a1 b1› using division_ofD(4)[OF div K1d] by blast
have eq: ‹K1 ∩ {x. c ≤ x ∙ k} = cbox (∑i∈Basis. (if i = k then max (a1 ∙ k) c else a1 ∙ i) *⇩R i) b1›
using interval_split(2)[OF ‹k ∈ Basis›] K1_eq by simp
have ‹interior (K1 ∩ {x. c ≤ x ∙ k}) ⊆ interior K1 ∩ interior K2›
using coll by (metis inf.cobounded1 interior_mono le_inf_iff)
also have ‹… = {}› using division_ofD(5)[OF div K1d K2d neq] .
finally have ‹box (∑i∈Basis. (if i = k then max (a1 ∙ k) c else a1 ∙ i) *⇩R i) b1 = {}›
using eq interior_cbox by auto
then show ?thesis using null eq by auto
qed
have fin_filt: ‹finite {l ∈ d. l ∩ S ≠ {}}› for S :: ‹'a set›
using fin_d by auto
have reindexL: ‹(∑K∈dL. norm (g K))
= (∑K∈{l ∈ d. l ∩ {x. x ∙ k ≤ c} ≠ {}}. norm (g (K ∩ {x. x ∙ k ≤ c})))›
unfolding dL_def
using collision_L
by (subst sum.reindex_nontrivial[OF fin_filt]) (auto simp: o_def)
have reindexR: ‹(∑K∈dR. norm (g K))
= (∑K∈{l ∈ d. l ∩ {x. c ≤ x ∙ k} ≠ {}}. norm (g (K ∩ {x. c ≤ x ∙ k})))›
unfolding dR_def
using collision_R
by (subst sum.reindex_nontrivial[OF fin_filt]) (auto simp: o_def)
have step3L: ‹(∑K∈{l ∈ d. l ∩ {x. x ∙ k ≤ c} ≠ {}}. norm (g (K ∩ {x. x ∙ k ≤ c})))
= (∑K∈dL. norm (g K))›
using reindexL by simp
have step3R: ‹(∑K∈{l ∈ d. l ∩ {x. c ≤ x ∙ k} ≠ {}}. norm (g (K ∩ {x. c ≤ x ∙ k})))
= (∑K∈dR. norm (g K))›
using reindexR by simp
have split_ineq: ‹(∑k∈d. norm (g k)) ≤ (∑k∈dL. norm (g k)) + (∑k∈dR. norm (g k))›
using step1 step2L step2R step3L step3R by linarith
have divL: ‹dL division_of (T ∩ {x. x ∙ k ≤ c})›
unfolding dL_def division_of_def
proof (intro conjI ballI allI impI)
show ‹finite ((λl. l ∩ {x. x ∙ k ≤ c}) ` {l ∈ d. l ∩ {x. x ∙ k ≤ c} ≠ {}})›
using fin_d by auto
next
fix K assume ‹K ∈ (λl. l ∩ {x. x ∙ k ≤ c}) ` {l ∈ d. l ∩ {x. x ∙ k ≤ c} ≠ {}}›
then obtain l al bl where ld: ‹l ∈ d› and lne: ‹l ∩ {x. x ∙ k ≤ c} ≠ {}› and Keq: ‹K = l ∩ {x. x ∙ k ≤ c}›
and leq: ‹l = cbox al bl› using division_ofD(4)[OF div] by blast
show ‹K ⊆ T ∩ {x. x ∙ k ≤ c}› using Keq division_ofD(2)[OF div ld] by auto
show ‹K ≠ {}› using Keq lne by auto
show ‹∃a b. K = cbox a b› using Keq leq interval_split(1)[OF ‹k ∈ Basis›] by blast
next
fix K1 K2
assume K1m: ‹K1 ∈ (λl. l ∩ {x. x ∙ k ≤ c}) ` {l ∈ d. l ∩ {x. x ∙ k ≤ c} ≠ {}}›
and K2m: ‹K2 ∈ (λl. l ∩ {x. x ∙ k ≤ c}) ` {l ∈ d. l ∩ {x. x ∙ k ≤ c} ≠ {}}›
and neq: ‹K1 ≠ K2›
obtain l1 where l1d: ‹l1 ∈ d› and K1eq: ‹K1 = l1 ∩ {x. x ∙ k ≤ c}› using K1m by auto
obtain l2 where l2d: ‹l2 ∈ d› and K2eq: ‹K2 = l2 ∩ {x. x ∙ k ≤ c}› using K2m by auto
have ‹l1 ≠ l2› using neq K1eq K2eq by auto
then have ‹interior l1 ∩ interior l2 = {}› using division_ofD(5)[OF div l1d l2d] by auto
then show ‹interior K1 ∩ interior K2 = {}›
using K1eq K2eq by auto
next
show ‹⋃ ((λl. l ∩ {x. x ∙ k ≤ c}) ` {l ∈ d. l ∩ {x. x ∙ k ≤ c} ≠ {}}) = T ∩ {x. x ∙ k ≤ c}›
using division_ofD(6)[OF div] by auto
qed
have divR: ‹dR division_of (T ∩ {x. c ≤ x ∙ k})›
unfolding dR_def division_of_def
proof (intro conjI ballI allI impI)
show ‹finite ((λl. l ∩ {x. c ≤ x ∙ k}) ` {l ∈ d. l ∩ {x. c ≤ x ∙ k} ≠ {}})›
using fin_d by auto
next
fix K assume ‹K ∈ (λl. l ∩ {x. c ≤ x ∙ k}) ` {l ∈ d. l ∩ {x. c ≤ x ∙ k} ≠ {}}›
then obtain l al bl where ld: ‹l ∈ d› and lne: ‹l ∩ {x. c ≤ x ∙ k} ≠ {}› and Keq: ‹K = l ∩ {x. c ≤ x ∙ k}›
and leq: ‹l = cbox al bl› using division_ofD(4)[OF div] by blast
show ‹K ⊆ T ∩ {x. c ≤ x ∙ k}› using Keq division_ofD(2)[OF div ld] by auto
show ‹K ≠ {}› using Keq lne by auto
show ‹∃a b. K = cbox a b› using Keq leq interval_split(2)[OF ‹k ∈ Basis›] by blast
next
fix K1 K2
assume K1m: ‹K1 ∈ (λl. l ∩ {x. c ≤ x ∙ k}) ` {l ∈ d. l ∩ {x. c ≤ x ∙ k} ≠ {}}›
and K2m: ‹K2 ∈ (λl. l ∩ {x. c ≤ x ∙ k}) ` {l ∈ d. l ∩ {x. c ≤ x ∙ k} ≠ {}}›
and neq: ‹K1 ≠ K2›
obtain l1 where l1d: ‹l1 ∈ d› and K1eq: ‹K1 = l1 ∩ {x. c ≤ x ∙ k}› using K1m by auto
obtain l2 where l2d: ‹l2 ∈ d› and K2eq: ‹K2 = l2 ∩ {x. c ≤ x ∙ k}› using K2m by auto
have ‹l1 ≠ l2› using neq K1eq K2eq by auto
then have ‹interior l1 ∩ interior l2 = {}› using division_ofD(5)[OF div l1d l2d] by auto
then show ‹interior K1 ∩ interior K2 = {}›
using K1eq K2eq by auto
next
show ‹⋃ ((λl. l ∩ {x. c ≤ x ∙ k}) ` {l ∈ d. l ∩ {x. c ≤ x ∙ k} ≠ {}}) = T ∩ {x. c ≤ x ∙ k}›
using division_ofD(6)[OF div] by auto
qed
have subL: ‹T ∩ {x. x ∙ k ≤ c} ⊆ cbox a b ∩ {x. x ∙ k ≤ c}› using sub by auto
have subR: ‹T ∩ {x. c ≤ x ∙ k} ⊆ cbox a b ∩ {x. c ≤ x ∙ k}› using sub by auto
have contentL: ‹sum content dL < r1›
proof -
have ‹sum content dL
≤ sum (content ∘ (λl. l ∩ {x. x ∙ k ≤ c})) {l ∈ d. l ∩ {x. x ∙ k ≤ c} ≠ {}}›
unfolding dL_def by (rule sum_image_le) (auto simp: fin_d content_pos_le)
also have ‹… ≤ sum content {l ∈ d. l ∩ {x. x ∙ k ≤ c} ≠ {}}›
proof (rule sum_mono)
fix l assume ‹l ∈ {l ∈ d. l ∩ {x. x ∙ k ≤ c} ≠ {}}›
then have ld: ‹l ∈ d› by auto
obtain al bl where leq: ‹l = cbox al bl› using division_ofD(4)[OF div ld] by blast
have ‹l ∩ {x. x ∙ k ≤ c} = cbox al (∑i∈Basis. (if i = k then min (bl ∙ k) c else bl ∙ i) *⇩R i)›
using interval_split(1)[OF ‹k ∈ Basis›] leq by simp
then show ‹(content ∘ (λl. l ∩ {x. x ∙ k ≤ c})) l ≤ content l›
using content_subset leq
by (metis (lifting) comp_apply inf_le1)
qed
also have ‹… ≤ sum content d›
by (rule sum_mono2) (auto simp: fin_d content_pos_le)
also have ‹… < r1› using content_bound by simp
finally show ?thesis .
qed
have contentR: ‹sum content dR < r2›
proof -
have ‹sum content dR
≤ sum (content ∘ (λl. l ∩ {x. c ≤ x ∙ k})) {l ∈ d. l ∩ {x. c ≤ x ∙ k} ≠ {}}›
unfolding dR_def by (rule sum_image_le) (auto simp: fin_d content_pos_le)
also have ‹… ≤ sum content {l ∈ d. l ∩ {x. c ≤ x ∙ k} ≠ {}}›
proof (rule sum_mono)
fix l assume ‹l ∈ {l ∈ d. l ∩ {x. c ≤ x ∙ k} ≠ {}}›
then have ld: ‹l ∈ d› by auto
obtain al bl where leq: ‹l = cbox al bl› using division_ofD(4)[OF div ld] by blast
have ‹l ∩ {x. c ≤ x ∙ k} = cbox (∑i∈Basis. (if i = k then max (al ∙ k) c else al ∙ i) *⇩R i) bl›
using interval_split(2)[OF ‹k ∈ Basis›] leq by simp
then show ‹(content ∘ (λl. l ∩ {x. c ≤ x ∙ k})) l ≤ content l›
using content_subset leq by (metis (lifting) comp_apply inf_le1)
qed
also have ‹… ≤ sum content d›
by (rule sum_mono2) (auto simp: fin_d content_pos_le)
also have ‹… < r2› using content_bound by simp
finally show ?thesis .
qed
have halves: ‹(∑k∈dL. norm (g k)) + (∑k∈dR. norm (g k)) < e›
using L[OF divL subL contentL] R[OF divR subR contentR] by linarith
show ‹(∑k∈d. norm (g k)) < e›
using split_ineq halves by linarith
qed
qed
qed (use absolutely_setcontinuous_on_subset in fastforce)+
lemma operative_absolutely_continuous_on:
fixes f :: ‹real ⇒ 'a::euclidean_space›
shows ‹operative (∧) True (λS. absolutely_continuous_on S f)›
proof -
define h where ‹h ≡ λS. if S = {} then 0 else f (Sup S) - f (Inf S)›
have op_h: ‹operative (+) 0 h› using operative_function_endpoint_diff[of f, folded h_def] .
have op_ac_h: ‹operative (∧) True (absolutely_setcontinuous_on h)›
using operative_absolutely_setcontinuous_on[OF op_h] .
have h_eq: ‹h k = f (Sup k) - f (Inf k)› if ‹k ≠ {}› for k
using that by (simp add: h_def)
have sum_eq: ‹(∑k∈d. norm (h k)) = (∑k∈d. norm (f (Sup k) - f (Inf k)))›
if div: ‹d division_of T› for d T
by (intro sum.cong refl arg_cong[where f=norm] h_eq) (use division_ofD(3)[OF div] in auto)
have ac_eq: ‹absolutely_setcontinuous_on h S = absolutely_setcontinuous_on (λk. f (Sup k) - f (Inf k)) S› for S
unfolding absolutely_setcontinuous_on_def
by (metis (lifting) local.sum_eq)
show ?thesis
using op_ac_h unfolding absolutely_continuous_on_def ac_eq .
qed
lemma absolutely_continuous_on_imp_has_bounded_variation_on:
assumes ‹absolutely_continuous_on S f› ‹bounded S›
shows ‹has_bounded_variation_on f S›
unfolding has_bounded_variation_on_def
proof -
define h where ‹h ≡ λS. if S = {} then 0 else f (Sup S) - f (Inf S)›
have h_eq: ‹h k = f (Sup k) - f (Inf k)› if ‹k ∈ d› ‹d division_of T› for k d T
using division_ofD(3)[OF that(2) that(1)] by (simp add: h_def)
have sum_eq: ‹(∑k∈d. norm (h k)) = (∑k∈d. norm (f (Sup k) - f (Inf k)))›
if ‹d division_of T› for d T
by (rule sum.cong) (auto simp: h_eq[OF _ that])
have ac_h: ‹absolutely_setcontinuous_on h S›
unfolding absolutely_setcontinuous_on_def
proof (intro allI impI)
fix ε :: real assume ‹ε > 0›
then obtain δ where ‹δ > 0› and δ: ‹⋀d T. d division_of T ⟹ T ⊆ S ⟹
(∑k∈d. content k) < δ ⟹ (∑k∈d. norm (f (Sup k) - f (Inf k))) < ε›
using assms unfolding absolutely_continuous_on_def absolutely_setcontinuous_on_def by meson
show ‹∃δ>0. ∀d T. d division_of T ∧ T ⊆ S ∧ (∑k∈d. content k) < δ ⟶
(∑k∈d. norm (h k)) < ε›
using ‹δ > 0› δ sum_eq by auto
qed
from absolutely_setcontinuous_on_imp_has_bounded_setvariation_on
[OF operative_function_endpoint_diff[of f, folded h_def] this ‹bounded S›]
show ‹has_bounded_setvariation_on (λk. f (Sup k) - f (Inf k)) S›
unfolding has_bounded_setvariation_on_def by (metis sum_eq)
qed
lemma Lipschitz_imp_absolutely_continuous:
assumes "⋀x y. x ∈ S ⟹ y ∈ S ⟹ norm (f x - f y) ≤ B * ¦x - y¦"
shows "absolutely_continuous_on S f"
unfolding absolutely_continuous_on_def absolutely_setcontinuous_on_def
proof (intro allI impI)
fix ε :: real assume "ε > 0"
show "∃δ>0. ∀d T. d division_of T ∧ T ⊆ S ∧ (∑k∈d. content k) < δ ⟶
(∑k∈d. norm (f (Sup k) - f (Inf k))) < ε"
proof (cases "B ≤ 0")
case True
show ?thesis
proof (intro exI conjI allI impI)
show "(1::real) > 0" by simp
next
fix d T assume H: "d division_of T ∧ T ⊆ S ∧ (∑k∈d. content k) < 1"
then have div: "d division_of T" and sub: "T ⊆ S" by auto
have "(∑k∈d. norm (f (Sup k) - f (Inf k))) ≤ (∑k∈d. B * ¦Sup k - Inf k¦)"
proof (rule sum_mono)
fix k assume kd: "k ∈ d"
then obtain u v where uv: "k = cbox u v" and "u ≤ v" "k ⊆ T"
by (metis atLeastatMost_empty_iff box_real(2) cbox_division_memE div)
then have "u ∈ S" "v ∈ S" using sub by auto
then have "norm (f v - f u) ≤ B * ¦v - u¦" using assms by auto
then show "norm (f (Sup k) - f (Inf k)) ≤ B * ¦Sup k - Inf k¦"
using uv ‹u ≤ v› by simp
qed
also have "… ≤ (∑k∈d. 0)"
by (simp add: True split_mult_neg_le sum_nonpos)
also have "… = 0" by simp
finally show "(∑k∈d. norm (f (Sup k) - f (Inf k))) < ε" using ‹ε > 0› by linarith
qed
next
case False
then have Bpos: "B > 0" by linarith
show ?thesis
proof (intro exI conjI allI impI)
show "ε / B > 0" using ‹ε > 0› Bpos by simp
next
fix d T assume H: "d division_of T ∧ T ⊆ S ∧ (∑k∈d. content k) < ε / B"
then have div: "d division_of T" and sub: "T ⊆ S"
and sm: "(∑k∈d. content k) < ε / B" by auto
have "(∑k∈d. norm (f (Sup k) - f (Inf k))) ≤ (∑k∈d. B * content k)"
proof (rule sum_mono)
fix k assume kd: "k ∈ d"
then obtain u v where uv: "k = cbox u v" and "u ≤ v" "k ⊆ T"
by (metis atLeastatMost_empty_iff box_real(2) cbox_division_memE div)
then have "u ∈ S" "v ∈ S" using sub uv ‹u ≤ v› by auto
then have "norm (f v - f u) ≤ B * ¦v - u¦" using assms by auto
also have "… = B * content k" using uv ‹u ≤ v› by (simp add: content_real)
finally show "norm (f (Sup k) - f (Inf k)) ≤ B * content k"
using uv ‹u ≤ v› by simp
qed
also have "… = B * (∑k∈d. content k)" by (simp add: sum_distrib_left)
also have "… < B * (ε / B)" using sm Bpos by (intro mult_strict_left_mono) auto
also have "… = ε" using Bpos by simp
finally show "(∑k∈d. norm (f (Sup k) - f (Inf k))) < ε" .
qed
qed
qed
subsection ‹Combining intervals›
lemma absolutely_continuous_on_combine:
assumes "absolutely_continuous_on {a..c} f"
and "absolutely_continuous_on {c..b} f" and "a ≤ c" "c ≤ b"
shows "absolutely_continuous_on {a..b} f"
proof -
have split: ‹absolutely_continuous_on {a..b} f =
(absolutely_continuous_on ({a..b} ∩ {x. x ≤ c}) f ∧
absolutely_continuous_on ({a..b} ∩ {x. c ≤ x}) f)›
using operative.Basis_imp[OF operative_absolutely_continuous_on[of f],
of 1 a b c] by (simp add: Basis_real_def inner_real_def)
have ‹{a..b} ∩ {x::real. x ≤ c} = {a..c}› using assms by auto
moreover have ‹{a..b} ∩ {x::real. c ≤ x} = {c..b}› using assms by auto
ultimately show ?thesis using split assms by simp
qed
lemma absolutely_continuous_on_division:
assumes "⋀k. k ∈ d ⟹ absolutely_continuous_on k f"
"d division_of {a..b}"
shows "absolutely_continuous_on {a..b} f"
proof -
have ‹comm_monoid_set.F (∧) True (λS. absolutely_continuous_on S f) d
= absolutely_continuous_on (cbox a b) f›
using operative.division[OF operative_absolutely_continuous_on assms(2)[unfolded cbox_interval[symmetric]]] .
then have ‹(finite d ⟶ (∀k∈d. absolutely_continuous_on k f))
= absolutely_continuous_on {a..b} f›
by (simp add: comm_monoid_set_F_and cbox_interval)
moreover have ‹finite d› using division_ofD(1)[OF assms(2)] .
ultimately show ?thesis using assms(1) by simp
qed
subsection ‹Bilinear and product›
lemma ac_on_bounded_image:
assumes ‹absolutely_continuous_on S f› ‹is_interval S› ‹bounded S›
obtains B where ‹B > 0› ‹⋀x. x ∈ S ⟹ norm (f x) < B›
proof -
have ‹bounded (f ` S)›
by (intro has_bounded_variation_on_imp_bounded[OF _ assms(2)]
absolutely_continuous_on_imp_has_bounded_variation_on[OF assms(1,3)])
then obtain B where ‹B > 0› ‹⋀x. x ∈ S ⟹ norm (f x) < B›
unfolding bounded_pos_less by (fastforce simp: image_iff)
then show ?thesis using that by blast
qed
lemma absolutely_continuous_on_bilinear:
fixes h :: ‹'a::euclidean_space ⇒ 'b::euclidean_space ⇒ 'c::euclidean_space›
and f :: ‹real ⇒ 'a› and g :: ‹real ⇒ 'b›
assumes ‹bilinear h›
and f: ‹absolutely_continuous_on S f›
and g: ‹absolutely_continuous_on S g›
and S: ‹is_interval S› ‹bounded S›
shows ‹absolutely_continuous_on S (λx. h (f x) (g x))›
proof -
obtain B1 where ‹B1 > 0› and f_bound: ‹⋀x. x ∈ S ⟹ norm (f x) < B1›
using ac_on_bounded_image[OF f S] by blast
obtain B2 where ‹B2 > 0› and g_bound: ‹⋀x. x ∈ S ⟹ norm (g x) < B2›
using ac_on_bounded_image[OF g S] by blast
obtain K where ‹K > 0› and K: ‹⋀x y. norm (h x y) ≤ K * norm x * norm y›
using bilinear_bounded_pos[OF assms(1)] by auto
note bl = bilinear_ladd[OF assms(1)] bilinear_radd[OF assms(1)]
bilinear_lsub[OF assms(1)] bilinear_rsub[OF assms(1)]
have decomp: ‹h (f (Sup k)) (g (Sup k)) - h (f (Inf k)) (g (Inf k)) =
h (f (Sup k) - f (Inf k)) (g (Sup k)) + h (f (Inf k)) (g (Sup k) - g (Inf k))› for k
by (simp add: bl algebra_simps)
show ?thesis
unfolding absolutely_continuous_on_def absolutely_setcontinuous_on_def
proof (intro allI impI)
fix ε :: real assume ‹ε > 0›
have eB2K: ‹ε/2 / B2 / K > 0› using ‹ε > 0› ‹B2 > 0› ‹K > 0› by simp
have eB1K: ‹ε/2 / B1 / K > 0› using ‹ε > 0› ‹B1 > 0› ‹K > 0› by simp
obtain δ1 where ‹δ1 > 0› and δ1: ‹⋀d T. d division_of T ⟹ T ⊆ S ⟹
(∑k∈d. content k) < δ1 ⟹ (∑k∈d. norm (f (Sup k) - f (Inf k))) < ε/2 / B2 / K›
using f unfolding absolutely_continuous_on_def absolutely_setcontinuous_on_def
using eB2K by (meson order.strict_trans2)
obtain δ2 where ‹δ2 > 0› and δ2: ‹⋀d T. d division_of T ⟹ T ⊆ S ⟹
(∑k∈d. content k) < δ2 ⟹ (∑k∈d. norm (g (Sup k) - g (Inf k))) < ε/2 / B1 / K›
using g unfolding absolutely_continuous_on_def absolutely_setcontinuous_on_def
using eB1K by (meson order.strict_trans2)
show ‹∃δ>0. ∀d T. d division_of T ∧ T ⊆ S ∧ (∑k∈d. content k) < δ ⟶
(∑k∈d. norm (h (f (Sup k)) (g (Sup k)) - h (f (Inf k)) (g (Inf k)))) < ε›
proof (intro exI conjI allI impI)
show ‹min δ1 δ2 > 0› using ‹δ1 > 0› ‹δ2 > 0› by simp
next
fix d T assume H: ‹d division_of T ∧ T ⊆ S ∧ (∑k∈d. content k) < min δ1 δ2›
then have div: ‹d division_of T› and sub: ‹T ⊆ S›
and meas: ‹(∑k∈d. content k) < δ1› ‹(∑k∈d. content k) < δ2› by auto
have fin: ‹finite d› using division_of_finite[OF div] .
have mem_s: ‹Sup k ∈ S› ‹Inf k ∈ S› if kd: ‹k ∈ d› for k
proof -
obtain u v where uv: "k = cbox u v" and "u ≤ v" "k ⊆ T"
by (metis atLeastatMost_empty_iff cbox_division_memE cbox_interval div kd)
then show ‹Sup k ∈ S› ‹Inf k ∈ S›
using sub by (auto simp: interval_bounds_real)
qed
have ‹(∑k∈d. norm (h (f (Sup k)) (g (Sup k)) - h (f (Inf k)) (g (Inf k))))
= (∑k∈d. norm (h (f (Sup k) - f (Inf k)) (g (Sup k)) +
h (f (Inf k)) (g (Sup k) - g (Inf k))))›
by (simp add: decomp)
also have ‹… ≤ (∑k∈d. norm (h (f (Sup k) - f (Inf k)) (g (Sup k))) +
norm (h (f (Inf k)) (g (Sup k) - g (Inf k))))›
by (intro sum_mono norm_triangle_ineq)
also have ‹… ≤ (∑k∈d. K * norm (f (Sup k) - f (Inf k)) * norm (g (Sup k)) +
K * norm (f (Inf k)) * norm (g (Sup k) - g (Inf k)))›
by (intro sum_mono add_mono K)
also have ‹… ≤ (∑k∈d. K * norm (f (Sup k) - f (Inf k)) * B2 +
K * B1 * norm (g (Sup k) - g (Inf k)))›
proof (intro sum_mono add_mono mult_left_mono mult_right_mono)
fix k assume kd: ‹k ∈ d›
show ‹norm (g (Sup k)) ≤ B2›
using g_bound[OF mem_s(1)[OF kd]] by linarith
show ‹norm (f (Inf k)) ≤ B1›
using f_bound[OF mem_s(2)[OF kd]] by linarith
qed (use ‹K > 0› in auto)
also have ‹… = K * B2 * (∑k∈d. norm (f (Sup k) - f (Inf k))) +
K * B1 * (∑k∈d. norm (g (Sup k) - g (Inf k)))›
by (simp add: sum.distrib sum_distrib_left algebra_simps)
also have ‹… < ε›
using δ1[OF div sub meas(1)] δ2[OF div sub meas(2)] ‹K > 0› ‹B1 > 0› ‹B2 > 0›
by (simp add: field_simps)
finally show ‹(∑k∈d. norm (h (f (Sup k)) (g (Sup k)) - h (f (Inf k)) (g (Inf k)))) < ε› .
qed
qed
qed
lemma absolutely_continuous_on_mul:
fixes f :: ‹real ⇒ real› and g :: ‹real ⇒ 'a::euclidean_space›
assumes ‹absolutely_continuous_on S f›
‹absolutely_continuous_on S g›
‹is_interval S› ‹bounded S›
shows ‹absolutely_continuous_on S (λx. f x *⇩R g x)›
using absolutely_continuous_on_bilinear
[OF bilinear_conv_bounded_bilinear[THEN iffD2, OF bounded_bilinear_scaleR] assms] .
lemma absolutely_continuous_on_vsum:
assumes ‹finite k›
‹⋀i. i ∈ k ⟹ absolutely_continuous_on S (f i)›
shows ‹absolutely_continuous_on S (λx. ∑i∈k. f i x)›
using assms
proof (induction k rule: finite_induct)
case empty
then show ?case by (simp add: absolutely_continuous_on_const)
next
case (insert a F)
then have ‹absolutely_continuous_on S (f a)›
and ‹absolutely_continuous_on S (λx. ∑i∈F. f i x)› by auto
then show ?case using insert.hyps
by (simp add: absolutely_continuous_on_add)
qed
lemma absolutely_continuous_on_sing:
‹absolutely_continuous_on {a} f›
using absolutely_continuous_on_null[of a a f] by (simp add: content_real_eq_0)
subsection ‹Fundamental theorem of calculus›
text ‹
Strong form of the fundamental theorem of calculus (Bartle's theorem).
The derivative @{term f'} need only exist outside a negligible set @{term S},
provided the ‹Henstock–Sacks› condition holds: for every @{term ‹ε > 0›}
there is a gauge witnessing that the oscillation of @{term f} over any
fine tagged partial division with all tags in @{term S} is small.
›
theorem fundamental_theorem_of_calculus_Bartle:
fixes f :: ‹real ⇒ 'a::euclidean_space› and f' :: ‹real ⇒ 'a›
assumes neg: ‹negligible S›
and ‹a ≤ b›
and deriv: ‹⋀x. x ∈ {a..b} - S ⟹ (f has_vector_derivative f' x) (at x within {a..b})›
and HS: ‹⋀ε. ε > 0 ⟹
∃g. gauge g ∧
(∀p. p tagged_partial_division_of cbox a b ∧ g fine p ∧ fst ` p ⊆ S ⟶
norm (∑(x,k)∈p. f (Sup k) - f (Inf k)) < ε)›
shows ‹(f' has_integral (f b - f a)) {a..b}›
proof (cases ‹a<b›)
case True
define g where ‹g ≡ (λx. if x ∈ S then 0 else f' x)›
show ?thesis
proof (rule has_integral_spike [OF neg])
show "(g has_integral f b - f a) {a..b}"
unfolding has_integral_real
proof (intro strip)
fix ε :: real
assume "0 < ε"
then obtain g1 where ‹gauge g1›
and g1: ‹⋀p. ⟦p tagged_partial_division_of cbox a b; g1 fine p; fst ` p ⊆ S⟧
⟹ norm (∑(x,k)∈p. f (Sup k) - f (Inf k)) < ε/2›
using HS[of ‹ε/2›] by force
have ‹∃d>0. (x ∈ {a..b} - S ⟶
(∀y. ¦y - x¦ < d ∧ y ∈ {a..b} ⟶
norm (f y - f x - (y - x) *⇩R g x) ≤ ε/2 / (b-a) * ¦y - x¦))› for x
proof (cases ‹x ∈ {a..b} - S›)
case False
then show ?thesis
by (intro exI[of _ 1]) auto
next
case True
then have ‹(f has_derivative (λh. h *⇩R f' x)) (at x within {a..b})›
using deriv has_vector_derivative_def by blast
moreover have ‹0 < ε/2 / (b-a)›
using ‹0 < ε› ‹a < b› by simp
ultimately obtain d where ‹d > 0›
and d: ‹⋀y. y ∈ {a..b} ⟹ norm (y - x) < d ⟹
norm (f y - f x - (y - x) *⇩R f' x) ≤ ε/2 / (b-a) * norm (y - x)›
unfolding has_derivative_within_alt by blast
have gx: ‹g x = f' x›
using True by (simp add: g_def)
show ?thesis
using ‹0 < d› d gx by auto
qed
then obtain d where dpos: ‹⋀x. d x >0›
and D: ‹⋀x. x ∈ {a..b} - S ⟶
(∀y. ¦y - x¦ < d x ∧ y ∈ {a..b} ⟶
norm (f y - f x - (y - x) *⇩R g x) ≤ ε/2 / (b-a) * ¦y - x¦)›
by metis
define γ where ‹γ ≡ λx. g1 x ∩ ball x (d x)›
show "∃γ. gauge γ ∧ (∀𝒟. 𝒟 tagged_division_of {a..b} ∧ γ fine 𝒟 ⟶ norm ((∑(x, k)∈𝒟. content k *⇩R g x) - (f b - f a)) < ε)"
proof (intro exI conjI strip)
show "gauge γ"
by (simp add: γ_def ‹gauge g1› dpos gauge_Int gauge_ball_dependent)
next
fix 𝒟 :: "(real × real set) set"
assume 𝒟: "𝒟 tagged_division_of {a..b} ∧ γ fine 𝒟"
then have *: ‹(∑(x, K)∈𝒟. f (Sup K) - f (Inf K)) = f b - f a›
by (simp add: additive_tagged_division_1 assms)
show "norm ((∑(x, k)∈𝒟. content k *⇩R g x) - (f b - f a)) < ε"
proof -
have tpd: ‹𝒟 tagged_partial_division_of cbox a b›
using 𝒟 tagged_division_of_def by auto
have g1_fine: ‹g1 fine 𝒟›
using 𝒟 unfolding γ_def by (auto simp: fine_Int)
have ball_fine: ‹(λx. ball x (d x)) fine 𝒟›
using 𝒟 unfolding γ_def by (auto simp: fine_Int)
have 𝒟_split: ‹𝒟 = {(x,k) ∈ 𝒟. x ∈ S} ∪ {(x,k) ∈ 𝒟. x ∉ S}›
by auto
define 𝒟S where ‹𝒟S ≡ {(x,k) ∈ 𝒟. x ∈ S}›
define 𝒟N where ‹𝒟N ≡ {(x,k) ∈ 𝒟. x ∉ S}›
have sum_len: ‹(∑(x, K)∈𝒟. Sup K - Inf K) = b - a›
using additive_tagged_division_1[OF ‹a ≤ b›] 𝒟 by force
have S_bound: ‹norm (∑(x,k)∈𝒟S. f (Sup k) - f (Inf k)) < ε/2›
proof (rule g1)
show ‹𝒟S tagged_partial_division_of cbox a b›
unfolding 𝒟S_def using tpd tagged_partial_division_subset
using 𝒟_split by auto
show ‹g1 fine 𝒟S›
using g1_fine fine_subset by (force simp: 𝒟S_def fine_def)
show ‹fst ` 𝒟S ⊆ S›
unfolding 𝒟S_def by force
qed
have N_bound: ‹norm (∑(x,k)∈𝒟N. content k *⇩R g x - (f (Sup k) - f (Inf k))) ≤ ε/2› (is "?L ≤ _")
proof -
have step1: ‹?L ≤ (∑(x,k)∈𝒟N. ε/2 / (b-a) * (Sup k - Inf k))›
proof (rule sum_norm_le)
fix xk assume xk_in: ‹xk ∈ 𝒟N›
obtain x k where xk: ‹xk = (x, k)› and mem: ‹(x, k) ∈ 𝒟› ‹x ∉ S›
using 𝒟N_def xk_in by blast
from 𝒟 mem obtain c e where k_eq: ‹k = {c..e}› and xk_props: ‹x ∈ k› ‹k ⊆ {a..b}›
by (metis box_real(2) tagged_division_ofD(2-4))
with xk_props have ce: ‹c ≤ e› ‹c ≤ x› ‹x ≤ e›
by auto
have sup_k: ‹Sup k = e› and inf_k: ‹Inf k = c›
using ce by (auto simp: k_eq)
have cont: ‹content k = Sup k - Inf k›
using ce content_real k_eq sup_k inf_k by auto
have x_ab: ‹x ∈ {a..b} - S› using xk_props mem by auto
have k_ball: ‹k ⊆ ball x (d x)›
using ball_fine mem unfolding fine_def by auto
have sup_in: ‹Sup k ∈ k› using ce by (auto simp: k_eq)
have inf_in: ‹Inf k ∈ k› using ce by (auto simp: k_eq)
have sup_ab: ‹Sup k ∈ {a..b}› using sup_in xk_props by auto
have inf_ab: ‹Inf k ∈ {a..b}› using inf_in xk_props by auto
have sup_near: ‹¦Sup k - x¦ < d x›
using k_ball sup_in by (auto simp: dist_real_def)
have inf_near: ‹¦Inf k - x¦ < d x›
using k_ball inf_in by (auto simp: dist_real_def)
have bnd_sup: ‹norm (f (Sup k) - f x - (Sup k - x) *⇩R g x)
≤ ε/2 / (b-a) * ¦Sup k - x¦›
using D x_ab sup_near sup_ab by auto
have bnd_inf: ‹norm (f (Inf k) - f x - (Inf k - x) *⇩R g x)
≤ ε/2 / (b-a) * ¦Inf k - x¦›
using D x_ab inf_near inf_ab by auto
have decomp: ‹content k *⇩R g x - (f (Sup k) - f (Inf k))
= (f (Inf k) - f x - (Inf k - x) *⇩R g x)
- (f (Sup k) - f x - (Sup k - x) *⇩R g x)›
by (simp add: cont sup_k inf_k algebra_simps)
have ‹norm (content k *⇩R g x - (f (Sup k) - f (Inf k)))
≤ norm (f (Inf k) - f x - (Inf k - x) *⇩R g x)
+ norm (f (Sup k) - f x - (Sup k - x) *⇩R g x)›
unfolding decomp by (rule norm_triangle_ineq4)
also have ‹… ≤ ε/2 / (b-a) * ¦Inf k - x¦ + ε/2 / (b-a) * ¦Sup k - x¦›
using bnd_inf bnd_sup by linarith
also have ‹… = ε/2 / (b-a) * (Sup k - Inf k)›
by (simp add: ce(2,3) inf_k right_diff_distrib' sup_k)
finally show ‹norm (case xk of (x,k) ⇒ content k *⇩R g x - (f (Sup k) - f (Inf k)))
≤ (case xk of (x,k) ⇒ ε/2 / (b-a) * (Sup k - Inf k))›
by (simp add: xk)
qed
have step2: ‹(∑(x,k)∈𝒟N. ε/2 / (b-a) * (Sup k - Inf k))
≤ (∑(x,k)∈𝒟. ε/2 / (b-a) * (Sup k - Inf k))›
proof (rule sum_mono2)
show ‹finite 𝒟› using tagged_division_of_finite 𝒟 by metis
show ‹𝒟N ⊆ 𝒟› unfolding 𝒟N_def by auto
fix xk assume ‹xk ∈ 𝒟 - 𝒟N›
then obtain x k where ‹xk = (x,k)› ‹(x,k) ∈ 𝒟› by (cases xk) auto
then obtain c e where ‹k = cbox c e› ‹c ≤ e›
using tagged_division_ofD(4,2) 𝒟
by (smt (verit) atLeastAtMost_iff box_real(2) subset_iff)
then have ‹Sup k ≥ Inf k› by simp
then show ‹0 ≤ (case xk of (x,k) ⇒ ε/2 / (b-a) * (Sup k - Inf k))›
using ‹0 < ε› True ‹xk = (x,k)› by (auto intro!: mult_nonneg_nonneg)
qed
have sum_eq: ‹(∑(x,k)∈𝒟. ε/2 / (b-a) * (Sup k - Inf k)) = ε/2 / (b-a) * (b-a)›
by (smt (verit) case_prod_unfold divide_divide_eq_left sum.cong sum_distrib_left sum_len)
have ‹?L ≤ ε/2 / (b-a) * (b-a)›
using step1 step2 sum_eq by linarith
also have ‹… = ε/2›
using True divide_eq_eq by fastforce
finally show ?thesis .
qed
have fin𝒟: ‹finite 𝒟› using tagged_division_of_finite 𝒟 by metis
have disj: ‹𝒟S ∩ 𝒟N = {}› unfolding 𝒟S_def 𝒟N_def by auto
have union: ‹𝒟 = 𝒟S ∪ 𝒟N› unfolding 𝒟S_def 𝒟N_def using 𝒟_split by auto
have fin_S: ‹finite 𝒟S› and fin_N: ‹finite 𝒟N›
using fin𝒟 union by (auto intro: finite_subset)
have ‹norm ((∑(x,k)∈𝒟. content k *⇩R g x) - (f b - f a))
= norm (∑(x,k)∈𝒟. content k *⇩R g x - (f (Sup k) - f (Inf k)))›
by (smt (verit) "*" split_def sum.cong sum_subtractf)
also have ‹… = norm ((∑(x,k)∈𝒟S. content k *⇩R g x - (f (Sup k) - f (Inf k)))
+ (∑(x,k)∈𝒟N. content k *⇩R g x - (f (Sup k) - f (Inf k))))›
by (simp add: sum.union_disjoint[OF fin_S fin_N disj, symmetric] union)
also have ‹(∑(x,k)∈𝒟S. content k *⇩R g x - (f (Sup k) - f (Inf k)))
= (∑(x,k)∈𝒟S. f (Inf k) - f (Sup k))›
proof (rule sum.cong[OF refl])
fix xk assume ‹xk ∈ 𝒟S›
then obtain x k where ‹xk = (x,k)› ‹x ∈ S›
unfolding 𝒟S_def by auto
then show ‹(case xk of (x,k) ⇒ content k *⇩R g x - (f (Sup k) - f (Inf k)))
= (case xk of (x,k) ⇒ (f (Inf k) - f (Sup k)))›
by (simp add: g_def split: prod.splits)
qed
also have ‹… = - (∑(x,k)∈𝒟S. f (Sup k) - f (Inf k))›
by (simp add: split_def sum_subtractf)
also have ‹norm (- (∑(x,k)∈𝒟S. f (Sup k) - f (Inf k))
+ (∑(x,k)∈𝒟N. content k *⇩R g x - (f (Sup k) - f (Inf k))))
≤ norm (∑(x,k)∈𝒟S. f (Sup k) - f (Inf k))
+ norm (∑(x,k)∈𝒟N. content k *⇩R g x - (f (Sup k) - f (Inf k)))›
using norm_add_rule_thm norm_imp_pos_and_ge norm_minus_cancel by blast
also have ‹… < ε/2 + ε/2›
using S_bound N_bound by linarith
also have ‹… = ε› by simp
finally show ?thesis .
qed
qed
qed
qed (auto simp: g_def)
qed (use ‹a ≤ b› in auto)
lemma negligible_content_gauge:
fixes a b :: real
assumes ‹negligible S› ‹δ > 0›
shows ‹∃g. gauge g ∧
(∀p. p tagged_partial_division_of cbox a b ∧ g fine p ∧ fst ` p ⊆ S ⟶
(∑(x,k)∈p. content k) < δ)›
proof -
have int: ‹(indicat_real S has_integral 0) (cbox a b)›
using assms(1) negligible_def by blast
then have intble: ‹indicat_real S integrable_on cbox a b›
by (rule has_integral_integrable)
obtain γ where ‹gauge γ› and γ:
‹⋀p. ⟦p tagged_partial_division_of cbox a b; γ fine p⟧
⟹ (∑(x,k)∈p. norm (content k *⇩R indicat_real S x - integral k (indicat_real S))) < δ›
using Henstock_lemma[OF intble ‹δ > 0›] by blast
show ?thesis
proof (intro exI conjI allI impI)
show ‹gauge γ› by fact
fix p assume p: ‹p tagged_partial_division_of cbox a b ∧ γ fine p ∧ fst ` p ⊆ S›
have eq: ‹content k *⇩R indicat_real S x - integral k (indicat_real S) = content k›
if ‹(x, k) ∈ p› for x k
proof -
from p that have ‹x ∈ S› by force
then have ‹indicat_real S x = 1› by (simp add: indicator_def)
moreover have ‹integral k (indicat_real S) = 0›
by (metis assms(1) integral_unique negligible_def p tagged_partial_division_ofD(4)
that)
ultimately show ?thesis by simp
qed
have ‹(∑(x,k)∈p. content k) = (∑(x,k)∈p. norm (content k *⇩R indicat_real S x - integral k (indicat_real S)))›
using eq content_pos_le
by (intro sum.cong[OF refl]) fastforce
then show ‹(∑(x,k)∈p. content k) < δ›
using γ p by presburger
qed
qed
lemma absolutely_continuous_on_imp_Henstock_Sacks:
assumes ‹negligible S› ‹absolutely_continuous_on {a..b} f› ‹ε > 0›
shows ‹∃g. gauge g ∧
(∀p. p tagged_partial_division_of cbox a b ∧ g fine p ∧ fst ` p ⊆ S ⟶
norm (∑(x,k)∈p. f (Sup k) - f (Inf k)) < ε)›
proof -
define F where ‹F ≡ λk. f (Sup k) - f (Inf k)›
from assms(2) have ac: ‹absolutely_setcontinuous_on F {a..b}›
unfolding absolutely_continuous_on_def F_def .
then obtain δ where ‹δ > 0› and δ:
‹⋀d T. ⟦d division_of T; T ⊆ {a..b}; sum content d < δ⟧ ⟹ (∑k∈d. norm (F k)) < ε›
using assms(3) unfolding absolutely_setcontinuous_on_def by meson
obtain g where ‹gauge g› and g:
‹⋀p. ⟦p tagged_partial_division_of cbox a b; g fine p; fst ` p ⊆ S⟧
⟹ (∑(x,k)∈p. content k) < δ›
using negligible_content_gauge[OF assms(1) ‹δ > 0›, of a b] by auto
show ?thesis
proof (intro exI conjI allI impI)
show ‹gauge g› by fact
fix p assume asm: ‹p tagged_partial_division_of cbox a b ∧ g fine p ∧ fst ` p ⊆ S›
then have pd: ‹p tagged_partial_division_of cbox a b› and fine: ‹g fine p›
and tags: ‹fst ` p ⊆ S› by auto
have inj: ‹inj_on snd p›
proof (rule inj_onI)
fix xk1 xk2 assume ‹xk1 ∈ p› ‹xk2 ∈ p› ‹snd xk1 = snd xk2›
then obtain x1 K1 x2 K2 where eq: ‹xk1 = (x1, K1)› ‹xk2 = (x2, K2)› ‹K1 = K2›
by (metis prod.collapse)
show ‹xk1 = xk2›
proof (rule ccontr)
assume ‹xk1 ≠ xk2›
with eq ‹xk1 ∈ p› ‹xk2 ∈ p› pd
have ‹interior K1 ∩ interior K2 = {}›
using tagged_partial_division_ofD(5) by blast
with eq have ‹interior K1 = {}› by auto
moreover from ‹xk1 ∈ p› pd eq obtain c d where ‹K1 = cbox c d›
using tagged_partial_division_ofD(4) by blast
ultimately have ‹box c d = {}› using interior_cbox by metis
moreover from ‹xk1 ∈ p› pd eq have ‹x1 ∈ K1› using tagged_partial_division_ofD(2) by blast
moreover from ‹xk2 ∈ p› pd eq have ‹x2 ∈ K1› using tagged_partial_division_ofD(2) by blast
ultimately have ‹x1 = x2› using ‹K1 = cbox c d› by (simp add: mem_box)
with eq show False using ‹xk1 ≠ xk2› by auto
qed
qed
have div: ‹snd ` p division_of ⋃(snd ` p)›
using partial_division_of_tagged_division[OF pd] .
have sub: ‹⋃(snd ` p) ⊆ {a..b}›
using asm tagged_partial_division_ofD(3) by fastforce
have content_bound: ‹sum content (snd ` p) < δ›
by (metis (no_types, lifting) asm case_prod_unfold g inj sum.reindex_cong)
have ‹(∑k∈snd ` p. norm (F k)) < ε›
using δ[OF div sub content_bound] .
then have ‹(∑(x,k)∈p. norm (F k)) < ε›
using sum.reindex[OF inj, of ‹λk. norm (F k)›] by (simp add: o_def case_prod_unfold)
then show ‹norm (∑(x,k)∈p. f (Sup k) - f (Inf k)) < ε›
unfolding F_def
by (smt (verit) case_prod_unfold sum_norm_le)
qed
qed
theorem fundamental_theorem_of_calculus_absolutely_continuous:
fixes f :: "real ⇒ 'a::euclidean_space"
assumes "negligible S" "a ≤ b"
"absolutely_continuous_on {a..b} f"
and fvd: "⋀x. x ∈ {a..b} - S ⟹ (f has_vector_derivative f' x) (at x within {a..b})"
shows "(f' has_integral (f b - f a)) {a..b}"
proof (intro fundamental_theorem_of_calculus_Bartle)
fix ε :: real assume ‹ε > 0›
show ‹∃g. gauge g ∧
(∀p. p tagged_partial_division_of cbox a b ∧ g fine p ∧ fst ` p ⊆ S ⟶
norm (∑(x,k)∈p. f (Sup k) - f (Inf k)) < ε)›
using ‹0 < ε› absolutely_continuous_on_imp_Henstock_Sacks assms(1,3) by fastforce
qed (use assms in auto)
subsection ‹Closure and interior›
lemma absolutely_continuous_on_interior:
assumes abc: "absolutely_continuous_on (interior S) f"
and contf: "continuous_on S f"
shows "absolutely_continuous_on S f"
unfolding absolutely_continuous_on_def absolutely_setcontinuous_on_def
proof (intro allI impI)
fix ε :: real assume ‹ε > 0›
then have ‹ε/2 > 0› by simp
from abc[unfolded absolutely_continuous_on_def absolutely_setcontinuous_on_def]
have ‹∀ε>0. ∃δ>0. ∀d T. d division_of T ∧ T ⊆ interior S ∧ (∑k∈d. content k) < δ ⟶
(∑k∈d. norm (f (Sup k) - f (Inf k))) < ε› .
from this[rule_format, OF ‹ε/2 > 0›]
obtain r where ‹r > 0› and
r_int: ‹∀d T. d division_of T ∧ T ⊆ interior S ∧ (∑k∈d. content k) < r ⟶
(∑k∈d. norm (f (Sup k) - f (Inf k))) < ε/2›
by auto
have r_int': ‹(∑k∈d. norm (f (Sup k) - f (Inf k))) < ε/2›
if ‹d division_of ⋃d› ‹⋃d ⊆ interior S› ‹(∑k∈d. content k) < r› for d
using r_int that by blast
show ‹∃δ>0. ∀d T. d division_of T ∧ T ⊆ S ∧ (∑k∈d. content k) < δ ⟶
(∑k∈d. norm (f (Sup k) - f (Inf k))) < ε›
proof (rule exI[of _ r], intro conjI allI impI)
show ‹r > 0› by fact
next
fix d T
assume H: ‹d division_of T ∧ T ⊆ S ∧ (∑k∈d. content k) < r›
have dt: ‹d division_of T› and ts: ‹T ⊆ S› and content_small: ‹(∑k∈d. content k) < r›
using H by auto
show ‹(∑k∈d. norm (f (Sup k) - f (Inf k))) < ε›
proof -
have fin_d: ‹finite d› using dt division_of_finite by blast
define σ where ‹σ n = (∑K∈d. norm (f (Sup K - (Sup K - Inf K) / 2^n) -
f (Inf K + (Sup K - Inf K) / 2^n)))› for n :: nat
define L where ‹L = (∑K∈d. norm (f (Sup K) - f (Inf K)))›
have conv: ‹σ ⇢ L›
proof -
have summand_conv: ‹(λn. norm (f (Sup K - (Sup K - Inf K) / 2^n) -
f (Inf K + (Sup K - Inf K) / 2^n))) ⇢ norm (f (Sup K) - f (Inf K))›
if ‹K ∈ d› for K
proof (intro tendsto_norm tendsto_diff)
obtain a b where Kab: ‹K = cbox a b› and ‹K ⊆ S› ‹a ≤ b›
using division_ofD dt ‹K ∈ d›
by (metis H atLeastatMost_empty_iff2 box_real(2) subset_trans)
then obtain InfK: ‹Inf K = a› and SupK: ‹Sup K = b›
and endpts: ‹Inf K ∈ S› ‹Sup K ∈ S›
using in_mono by fastforce
have mid_in_K: ‹x ∈ K› if ‹Inf K ≤ x› ‹x ≤ Sup K› for x
using that InfK SupK Kab by auto
have *: ‹(λn. f (x + y / 2^n)) ⇢ f x› if ‹x ∈ S› ‹∀n. x + y / 2^n ∈ S› for x y
proof (rule continuous_on_tendsto_compose[OF contf _ that(1)])
show ‹(λn. x + y / 2^n) ⇢ x›
using tendsto_add[OF tendsto_const, of ‹λn. y / 2^n› 0 sequentially x]
by (simp add: LIMSEQ_divide_realpow_zero)
show ‹∀⇩F n in sequentially. x + y / 2^n ∈ S›
using that(2) by simp
qed
show ‹(λn. f (Sup K - (Sup K - Inf K) / 2^n)) ⇢ f (Sup K)›
proof -
have eq: ‹Sup K - (Sup K - Inf K) / 2^n = Sup K + (Inf K - Sup K) / 2^n› for n :: nat
by (simp add: field_simps)
have ‹∀n. Sup K + (Inf K - Sup K) / 2^n ∈ S›
proof
fix n :: nat
have ‹(Sup K - Inf K) * 1 ≤ (Sup K - Inf K) * 2^n›
using ‹a ≤ b› InfK SupK by (intro mult_left_mono) auto
then have ‹Inf K ≤ Sup K + (Inf K - Sup K) / 2^n›
by (simp add: field_simps)
moreover
have ‹(Inf K - Sup K) / 2^n ≤ 0›
using ‹a ≤ b› InfK SupK by (intro divide_nonpos_nonneg) auto
then have ‹Sup K + (Inf K - Sup K) / 2^n ≤ Sup K›
by linarith
ultimately show ‹Sup K + (Inf K - Sup K) / 2^n ∈ S›
using mid_in_K ‹K ⊆ S› by auto
qed
then show ?thesis using *[OF endpts(2)] by (simp add: eq)
qed
show ‹(λn. f (Inf K + (Sup K - Inf K) / 2^n)) ⇢ f (Inf K)›
proof -
have ‹∀n. Inf K + (Sup K - Inf K) / 2^n ∈ S›
proof
fix n :: nat
have ‹Inf K ≤ Inf K + (Sup K - Inf K) / 2^n›
by (simp add: InfK SupK ‹a ≤ b›)
moreover have ‹Inf K + (Sup K - Inf K) / 2^n ≤ Sup K›
by (metis InfK SupK ‹a ≤ b› dual_order.refl mult_1 one_le_numeral
one_le_power power_0 scaling_mono zero_le_power)
ultimately show ‹Inf K + (Sup K - Inf K) / 2^n ∈ S›
using mid_in_K ‹K ⊆ S› by auto
qed
then show ?thesis using *[OF endpts(1)] by simp
qed
qed
show ‹σ ⇢ L›
unfolding σ_def L_def using summand_conv by (rule tendsto_sum)
qed
have bound: ‹∀⇩F n in sequentially. σ n ≤ ε/2›
proof
fix n :: nat
assume "2 ≤ n"
define d' where ‹d' ≡ (λk. cbox (Inf k + (Sup k - Inf k) / 2^n)
(Sup k - (Sup k - Inf k) / 2^n))
` {k ∈ d. content k ≠ 0}›
let ?S = ‹{k ∈ d. content k ≠ 0}›
let ?shrink = ‹λk. cbox (Inf k + (Sup k - Inf k) / 2^n) (Sup k - (Sup k - Inf k) / 2^n)›
have d'_eq: ‹d' = ?shrink ` ?S›
unfolding d'_def ..
have fin_S: ‹finite ?S› using fin_d by auto
have k_props: ‹Inf k < Sup k› ‹k = {Inf k .. Sup k}› ‹k ⊆ S›
‹?shrink k ⊆ k› ‹?shrink k ≠ {}›
if ‹k ∈ ?S› for k
proof -
from that have kd: ‹k ∈ d› and kcont: ‹content k ≠ 0› by auto
obtain a b where kab: ‹k = {a..b}› and ‹a < b›
using H content_real_eq_0 kcont kd by auto
moreover have ‹Inf k = a› ‹Sup k = b› using kab ‹a < b› by auto
ultimately show ‹Inf k < Sup k› by auto
show ‹k = {Inf k .. Sup k}› using kab ‹Inf k = a› ‹Sup k = b› by auto
show ‹k ⊆ S› using division_ofD(2)[OF dt kd] ts by auto
have pos: ‹(Sup k - Inf k) / 2^n > 0› using ‹Inf k < Sup k› by auto
have two_le: ‹(2::real) ≤ 2^n› using ‹2 ≤ n›
by (metis One_nat_def le_eq_less_or_eq le_simps(3) numerals(2) one_le_numeral
power_increasing power_one_right)
show ‹?shrink k ⊆ k›
unfolding box_real using pos ‹k = {Inf k .. Sup k}›
by fastforce
have ‹(Sup k - Inf k) * 2 ≤ (Sup k - Inf k) * 2^n›
using ‹Inf k < Sup k› two_le by (intro mult_left_mono) auto
then have ‹2 * (Sup k - Inf k) / 2^n ≤ Sup k - Inf k›
by (simp add: pos_divide_le_eq)
then show ‹?shrink k ≠ {}›
by auto
qed
have ‹d' division_of ⋃d'›
unfolding division_of_def
proof (intro conjI ballI impI)
fix K :: "real set"
assume "K ∈ d'"
then obtain k where kS: ‹k ∈ ?S› and Keq: ‹K = ?shrink k›
unfolding d'_eq by auto
show ‹K ≠ {}› using Keq k_props(5)[OF kS] by auto
show "∃a b. K = cbox a b"
using ‹K ∈ d'› d'_def by blast
next
fix K1 K2
assume ‹K1 ∈ d'› ‹K2 ∈ d'› ‹K1 ≠ K2›
then obtain k1 k2 where k1S: ‹k1 ∈ ?S› and K1eq: ‹K1 = ?shrink k1›
and k2S: ‹k2 ∈ ?S› and K2eq: ‹K2 = ?shrink k2›
unfolding d'_eq by auto
have ‹k1 ≠ k2› using ‹K1 ≠ K2› K1eq K2eq by auto
have ‹k1 ∈ d› ‹k2 ∈ d› using k1S k2S by auto
have ‹interior k1 ∩ interior k2 = {}›
using division_ofD(5)[OF dt ‹k1 ∈ d› ‹k2 ∈ d› ‹k1 ≠ k2›] .
moreover have ‹interior K1 ⊆ interior k1›
using interior_mono[OF k_props(4)[OF k1S]] K1eq by auto
moreover have ‹interior K2 ⊆ interior k2›
using interior_mono[OF k_props(4)[OF k2S]] K2eq by auto
ultimately show ‹interior K1 ∩ interior K2 = {}› by auto
qed (auto simp: d'_def fin_d Sup_upper)
moreover have ‹⋃d' ⊆ interior S›
proof
fix x assume ‹x ∈ ⋃d'›
then obtain K k where ‹K ∈ d'› ‹x ∈ K› and kS: ‹k ∈ ?S› and Keq: ‹K = ?shrink k›
unfolding d'_eq by auto
have ‹x ∈ interior k›
proof -
have ‹Inf k < Inf k + (Sup k - Inf k) / 2^n›
using k_props(1)[OF kS] by auto
moreover have ‹Sup k - (Sup k - Inf k) / 2^n < Sup k›
using k_props(1)[OF kS] by auto
moreover have ‹x ∈ {Inf k + (Sup k - Inf k) / 2^n .. Sup k - (Sup k - Inf k) / 2^n}›
using ‹x ∈ K› Keq box_real by auto
ultimately have ‹x ∈ {Inf k <..< Sup k}› by auto
also have ‹… = interior {Inf k .. Sup k}›
using interior_atLeastAtMost_real by auto
also have ‹… = interior k› using k_props(2)[OF kS] by auto
finally show ?thesis .
qed
also have ‹interior k ⊆ interior S›
by (rule interior_mono[OF k_props(3)[OF kS]])
finally show ‹x ∈ interior S› .
qed
moreover have ‹(∑k∈d'. content k) < r›
proof -
have ‹(∑k∈d'. content k) ≤ (∑k∈?S. content (?shrink k))›
unfolding d'_eq using sum_image_le[OF fin_S, of content ?shrink] content_pos_le
by fastforce
also have ‹… ≤ (∑k∈?S. content k)›
by (metis (lifting) box_real(2) content_subset k_props(2,4) sum_mono)
also have ‹… ≤ (∑k∈d. content k)›
by (rule sum_mono2[OF fin_d]) (auto simp: content_pos_le)
also have ‹… < r› using content_small .
finally show ?thesis .
qed
ultimately have r_int'_d': ‹(∑k∈d'. norm (f (Sup k) - f (Inf k))) < ε/2›
using r_int by blast
have inj_shrink: ‹inj_on ?shrink ?S›
proof (rule inj_onI)
fix k1 k2
assume k1S: ‹k1 ∈ ?S› and k2S: ‹k2 ∈ ?S› and eq: ‹?shrink k1 = ?shrink k2›
show ‹k1 = k2›
proof (rule ccontr)
assume ‹k1 ≠ k2›
have ‹k1 ∈ d› ‹k2 ∈ d› using k1S k2S by auto
have ‹interior k1 ∩ interior k2 = {}›
using division_ofD(5)[OF dt ‹k1 ∈ d› ‹k2 ∈ d› ‹k1 ≠ k2›] .
moreover have ‹?shrink k1 ⊆ interior k1›
proof
fix x assume ‹x ∈ ?shrink k1›
then have ‹x ∈ {Inf k1 + (Sup k1 - Inf k1) / 2^n .. Sup k1 - (Sup k1 - Inf k1) / 2^n}›
using box_real by auto
moreover have ‹Inf k1 < Inf k1 + (Sup k1 - Inf k1) / 2^n›
using k_props(1)[OF k1S] by auto
moreover have ‹Sup k1 - (Sup k1 - Inf k1) / 2^n < Sup k1›
using k_props(1)[OF k1S] by auto
ultimately have ‹x ∈ {Inf k1 <..< Sup k1}› by auto
also have ‹… = interior {Inf k1 .. Sup k1}›
using interior_atLeastAtMost_real by auto
also have ‹… = interior k1› using k_props(2)[OF k1S] by auto
finally show ‹x ∈ interior k1› .
qed
moreover have ‹?shrink k1 ≠ {}› using k_props(5)[OF k1S] .
ultimately have ‹?shrink k1 ∩ interior k2 = {}› by auto
moreover have ‹?shrink k2 ⊆ interior k2›
proof
fix x assume ‹x ∈ ?shrink k2›
then have ‹x ∈ {Inf k2 + (Sup k2 - Inf k2) / 2^n .. Sup k2 - (Sup k2 - Inf k2) / 2^n}›
using box_real by auto
moreover have ‹Inf k2 < Inf k2 + (Sup k2 - Inf k2) / 2^n›
using k_props(1)[OF k2S] by auto
moreover have ‹Sup k2 - (Sup k2 - Inf k2) / 2^n < Sup k2›
using k_props(1)[OF k2S] by auto
ultimately have ‹x ∈ {Inf k2 <..< Sup k2}› by auto
also have ‹… = interior {Inf k2 .. Sup k2}›
using interior_atLeastAtMost_real by auto
also have ‹… = interior k2› using k_props(2)[OF k2S] by auto
finally show ‹x ∈ interior k2› .
qed
ultimately have ‹?shrink k1 ∩ ?shrink k2 = {}› by blast
then show False using eq k_props(5)[OF k1S]
by blast
qed
qed
have shrink_bounds: ‹Inf (?shrink k) = Inf k + (Sup k - Inf k) / 2^n›
‹Sup (?shrink k) = Sup k - (Sup k - Inf k) / 2^n›
if ‹k ∈ ?S› for k
proof -
have ne: ‹Inf k + (Sup k - Inf k) / 2^n ≤ Sup k - (Sup k - Inf k) / 2^n›
using k_props(5)[OF that] by (auto simp: box_real)
show ‹Inf (?shrink k) = Inf k + (Sup k - Inf k) / 2^n›
unfolding box_real using cInf_atLeastAtMost[OF ne] .
show ‹Sup (?shrink k) = Sup k - (Sup k - Inf k) / 2^n›
unfolding box_real using cSup_atLeastAtMost[OF ne] .
qed
have d'_sum: ‹(∑K∈d'. norm (f (Sup K) - f (Inf K))) =
(∑k∈?S. norm (f (Sup k - (Sup k - Inf k) / 2^n) - f (Inf k + (Sup k - Inf k) / 2^n)))›
proof -
have ‹(∑K∈d'. norm (f (Sup K) - f (Inf K))) =
(∑k∈?S. norm (f (Sup (?shrink k)) - f (Inf (?shrink k))))›
unfolding d'_eq using sum.reindex[OF inj_shrink] by (simp add: o_def)
also have ‹… = (∑k∈?S. norm (f (Sup k - (Sup k - Inf k) / 2^n) -
f (Inf k + (Sup k - Inf k) / 2^n)))›
using shrink_bounds by simp
finally show ?thesis .
qed
have zero_summands: ‹(∑k∈d. norm (f (Sup k - (Sup k - Inf k) / 2^n) -
f (Inf k + (Sup k - Inf k) / 2^n))) =
(∑k∈?S. norm (f (Sup k - (Sup k - Inf k) / 2^n) -
f (Inf k + (Sup k - Inf k) / 2^n)))›
proof (rule sum.mono_neutral_right[OF fin_d])
show ‹?S ⊆ d› by auto
show ‹∀k∈d - ?S. norm (f (Sup k - (Sup k - Inf k) / 2^n) -
f (Inf k + (Sup k - Inf k) / 2^n)) = 0›
proof
fix k assume ‹k ∈ d - ?S›
then have kd: ‹k ∈ d› and kcont: ‹content k = 0› by auto
then obtain a b where kab: ‹k = cbox a b› ‹a = b›
by (metis H antisym atLeastatMost_empty_iff2 cbox_division_memE content_real_eq_0 interval_cbox)
then have ‹Inf k = Sup k› by (auto simp: box_real)
then show ‹norm (f (Sup k - (Sup k - Inf k) / 2^n) -
f (Inf k + (Sup k - Inf k) / 2^n)) = 0› by simp
qed
qed
have ‹σ n = (∑k∈d'. norm (f (Sup k) - f (Inf k)))›
unfolding σ_def using zero_summands d'_sum by auto
then show ‹σ n ≤ ε/2› using r_int'_d' by linarith
qed
have ‹L ≤ ε/2›
by (rule tendsto_le[OF sequentially_bot tendsto_const conv bound])
then show ?thesis unfolding L_def using ‹ε > 0› by linarith
qed
qed
qed
lemma absolutely_continuous_on_closure:
assumes "absolutely_continuous_on (interior S) f"
"continuous_on (closure S) f" "is_interval S"
shows "absolutely_continuous_on S f"
by (meson absolutely_continuous_on_interior assms closure_subset continuous_on_subset)
section ‹Bounded variation and absolutely integrable derivatives›
lemma countable_imp_negligible:
fixes S :: ‹real set›
assumes ‹countable S›
shows ‹negligible S›
using negligible_countable_Union[OF countable_image[OF assms]]
by (metis (mono_tags, lifting) UN_singleton image_iff negligible_sing)
lemma absolutely_setcontinuous_on_componentwise:
fixes f :: ‹'a::euclidean_space set ⇒ 'b::euclidean_space›
shows ‹absolutely_setcontinuous_on f S ⟷
(∀b∈Basis. absolutely_setcontinuous_on (λk. f k ∙ b) S)›
(is ‹?L ⟷ ?R›)
proof
assume L: ‹?L›
show ‹?R›
unfolding absolutely_setcontinuous_on_def
proof (intro ballI allI impI)
fix b :: 'b and ε :: real
assume ‹b ∈ Basis› and ‹0 < ε›
with L obtain δ where ‹0 < δ› and
δ: ‹⋀d T. d division_of T ⟹ T ⊆ S ⟹ sum content d < δ ⟹ (∑k∈d. norm (f k)) < ε›
unfolding absolutely_setcontinuous_on_def
by metis
show ‹∃δ>0. ∀d T. d division_of T ∧ T ⊆ S ∧ (∑k∈d. content k) < δ ⟶
(∑k∈d. norm (f k ∙ b)) < ε›
by (metis (mono_tags, lifting) norm_nth_le δ ‹0 < δ› ‹b ∈ Basis› order.strict_trans1 sum_mono)
qed
next
assume R: ‹?R›
show ‹?L›
unfolding absolutely_setcontinuous_on_def
proof (intro allI impI)
fix ε :: real assume ε_pos: ‹0 < ε›
have comp: ‹∀b∈(Basis :: 'b set). ∃r>0. ∀d T. d division_of T ∧ T ⊆ S ∧ sum content d < r
⟶ (∑k∈d. ¦f k ∙ b¦) < ε / DIM('b)›
proof (intro ballI)
fix b :: 'b assume ‹b ∈ Basis›
with R have ‹absolutely_setcontinuous_on (λk. f k ∙ b) S› by blast
moreover have ‹0 < ε / DIM('b)› using ε_pos DIM_positive by simp
ultimately obtain r where ‹0 < r› and
r: ‹⋀d T. d division_of T ⟹ T ⊆ S ⟹ sum content d < r ⟹ (∑k∈d. norm ((λk. f k ∙ b) k)) < ε / DIM('b)›
unfolding absolutely_setcontinuous_on_def by meson
then show ‹∃r>0. ∀d T. d division_of T ∧ T ⊆ S ∧ sum content d < r
⟶ (∑k∈d. ¦f k ∙ b¦) < ε / DIM('b)›
by (intro exI[of _ r]) (auto simp: real_norm_def)
qed
then obtain r where r_pos: ‹⋀b. b ∈ (Basis :: 'b set) ⟹ (0::real) < r b›
and r_bound: ‹⋀b d T. b ∈ (Basis :: 'b set) ⟹ d division_of T ⟹ T ⊆ S ⟹ sum content d < r b
⟹ (∑k∈d. ¦f k ∙ b¦) < ε / DIM('b)›
by (metis bchoice)
define δ where ‹δ = Min (r ` (Basis :: 'b set))›
have δ_pos: ‹0 < δ›
unfolding δ_def using r_pos finite_Basis nonempty_Basis
by (subst Min_gr_iff) (auto simp: image_is_empty)
moreover have ‹∀d T. d division_of T ∧ T ⊆ S ∧ sum content d < δ
⟶ (∑k∈d. norm (f k)) < ε›
proof (intro allI impI)
fix d T assume asm: ‹d division_of T ∧ T ⊆ S ∧ sum content d < δ›
have finite_d: ‹finite d› using asm division_of_finite by blast
have ‹(∑k∈d. norm (f k)) ≤ (∑k∈d. ∑b∈(Basis :: 'b set). ¦f k ∙ b¦)›
by (rule sum_mono) (rule norm_le_l1)
also have ‹… = (∑b∈(Basis :: 'b set). ∑k∈d. ¦f k ∙ b¦)›
by (rule sum.swap)
also have ‹… < of_nat (DIM('b)) * (ε / of_nat (DIM('b)))›
proof (rule sum_bounded_above_strict)
fix b :: 'b assume ‹b ∈ Basis›
then have ‹δ ≤ r b›
unfolding δ_def by (intro Min_le finite_imageI finite_Basis) (auto simp: image_iff)
then have ‹sum content d < r b›
using asm by linarith
then show ‹(∑k∈d. ¦f k ∙ b¦) < ε / real DIM('b)›
using r_bound ‹b ∈ Basis› asm by blast
next
show ‹0 < card (Basis :: 'b set)› by (simp add: DIM_positive)
qed
also have ‹… = ε›
using DIM_positive[where 'a='b] by simp
finally show ‹(∑k∈d. norm (f k)) < ε› .
qed
ultimately show ‹∃δ>0. ∀d T. d division_of T ∧ T ⊆ S ∧ sum content d < δ ⟶ (∑k∈d. norm (f k)) < ε›
by auto
qed
qed
lemma absolutely_setcontinuous_on_alt:
‹absolutely_setcontinuous_on f S ⟷
(∀ε>0. ∃δ>0. ∀d T. d division_of T ∧ T ⊆ S ∧
(∑k∈d. content k) < δ ⟶ norm (∑k∈d. f k) < ε)› (is ‹?L = ?R›)
proof
show ‹?L ⟹ ?R›
by (meson absolutely_setcontinuous_on_def norm_sum order_le_less_trans)
next
assume R: ‹?R›
show ‹?L›
proof -
have "absolutely_setcontinuous_on (λk. f k ∙ b) S"
if "b ∈ Basis" for b :: 'b
unfolding absolutely_setcontinuous_on_def
proof (intro strip)
fix ε :: real
assume "0 < ε"
show "∃δ>0. ∀d T. d division_of T ∧ T ⊆ S ∧ sum content d < δ ⟶ (∑k∈d. norm (f k ∙ b)) < ε"
proof -
have ‹0 < ε/2› using ‹0 < ε› by simp
with R obtain r where ‹0 < r› and
r: ‹⋀d T. d division_of T ⟹ T ⊆ S ⟹ sum content d < r ⟹ norm (∑k∈d. f k) < ε/2›
by meson
show ?thesis
proof (intro exI conjI allI impI)
show ‹0 < r› by fact
next
fix d T
assume dt: ‹d division_of T ∧ T ⊆ S ∧ sum content d < r›
have fin: ‹finite d› using dt division_of_finite by blast
define d_pos where ‹d_pos = {k ∈ d. 0 ≤ f k ∙ b}›
define d_neg where ‹d_neg = {k ∈ d. f k ∙ b < 0}›
have d_split: ‹d = d_pos ∪ d_neg› and d_disj: ‹d_pos ∩ d_neg = {}›
and fin_pos: ‹finite d_pos› and fin_neg: ‹finite d_neg› and d_pos_sub: ‹d_pos ⊆ d› and d_neg_sub: ‹d_neg ⊆ d›
using fin unfolding d_pos_def d_neg_def by auto
obtain div_pos: ‹d_pos division_of ⋃d_pos› and div_neg: ‹d_neg division_of ⋃d_neg›
by (meson d_neg_sub d_pos_sub division_of_subset division_of_union_self dt)
have union_pos_sub: ‹⋃d_pos ⊆ S› and union_neg_sub: ‹⋃d_neg ⊆ S›
using dt d_pos_sub d_split by blast+
have content_pos: ‹sum content d_pos < r›
by (meson dt content_pos_le d_pos_sub fin order_le_less_trans sum_mono2)
have content_neg: ‹sum content d_neg < r›
by (meson dt content_pos_le d_neg_sub fin order_le_less_trans sum_mono2)
have norm_pos: ‹norm (sum f d_pos) < ε/2›
using r[OF div_pos union_pos_sub content_pos] .
have norm_neg: ‹norm (sum f d_neg) < ε/2›
using r[OF div_neg union_neg_sub content_neg] .
have sum_pos: ‹(∑k∈d_pos. norm (f k ∙ b)) ≤ norm (sum f d_pos)›
proof -
have ‹(∑k∈d_pos. norm (f k ∙ b)) = (∑k∈d_pos. f k ∙ b)›
by (rule sum.cong) (auto simp: d_pos_def real_norm_def abs_of_nonneg)
also have ‹… = (sum f d_pos) ∙ b›
by (simp add: inner_sum_left)
also have ‹… ≤ norm (sum f d_pos)›
by (smt (verit, best) Basis_le_norm that)
finally show ?thesis .
qed
have sum_neg: ‹(∑k∈d_neg. norm (f k ∙ b)) ≤ norm (sum f d_neg)›
proof -
have ‹(∑k∈d_neg. norm (f k ∙ b)) = (∑k∈d_neg. -(f k ∙ b))›
by (rule sum.cong) (auto simp: d_neg_def real_norm_def abs_of_neg)
also have ‹… = -((sum f d_neg) ∙ b)›
by (simp add: inner_sum_left sum_negf)
also have ‹… ≤ norm (sum f d_neg)›
by (smt (verit, best) Basis_le_norm that)
finally show ?thesis .
qed
show ‹(∑k∈d. norm (f k ∙ b)) < ε›
proof -
have ‹(∑k∈d. norm (f k ∙ b)) = (∑k∈d_pos. norm (f k ∙ b)) + (∑k∈d_neg. norm (f k ∙ b))›
by (subst d_split) (rule sum.union_disjoint[OF fin_pos fin_neg d_disj])
also have ‹… ≤ norm (sum f d_pos) + norm (sum f d_neg)›
by (rule add_mono[OF sum_pos sum_neg])
also have ‹… < ε/2 + ε/2›
by (rule add_strict_mono[OF norm_pos norm_neg])
finally show ?thesis by simp
qed
qed
qed
qed
then show ?thesis
using absolutely_setcontinuous_on_componentwise by blast
qed
qed
lemma absolutely_integrable_approximate_continuous_vector:
fixes f :: ‹'a::euclidean_space ⇒ 'b::euclidean_space›
and S :: ‹'a set›
assumes ‹S ∈ lmeasurable›
and ‹f absolutely_integrable_on S›
and ‹e > 0›
obtains g where ‹g absolutely_integrable_on S› ‹continuous_on UNIV g›
‹bounded (range g)›
‹norm (integral S (λx. norm (f x - g x))) < e›
proof -
obtain h where hint: "h absolutely_integrable_on S"
and hbo: "bounded (h ` UNIV)"
and he2: "norm (integral S (λx. norm (f x - h x))) < e/2"
proof -
define trunc where "trunc ≡ λn x. ∑b∈Basis. max (- real n) (min (real n) (f x ∙ b)) *⇩R b"
have trunc_abs_int: ‹trunc n absolutely_integrable_on S› for n
proof -
define c where ‹c = (∑b∈Basis. real n *⇩R b :: 'b)›
have c_inner[simp]: ‹c ∙ b = real n› if ‹b ∈ Basis› for b
unfolding c_def using inner_sum_left_Basis[OF that] by simp
have mc_inner[simp]: ‹(- c) ∙ b = - real n› if ‹b ∈ Basis› for b
by (simp add: that)
have const_int: ‹(λ_::'a. d) absolutely_integrable_on S› for d :: 'b
using absolutely_integrable_on_const assms(1) by blast
have min_int: ‹(λx. ∑b∈Basis. min (f x ∙ b) (c ∙ b) *⇩R b)
absolutely_integrable_on S›
by (rule absolutely_integrable_min[OF assms(2) const_int])
then have min_int': ‹(λx. ∑b∈Basis. min (f x ∙ b) (real n) *⇩R b)
absolutely_integrable_on S›
by (simp cong: sum.cong)
have max_int: ‹(λx. ∑b∈Basis. max ((- c) ∙ b) ((∑b∈Basis. min (f x ∙ b) (real n) *⇩R b) ∙ b) *⇩R b)
absolutely_integrable_on S›
by (rule absolutely_integrable_max[OF const_int min_int'])
then show ?thesis
by (simp add: trunc_def inner_sum_left_Basis max.commute min.commute cong: sum.cong)
qed
have conv: ‹(λk. integral S (λx. norm (f x - trunc k x))) ⇢ 0›
proof -
let ?fn = ‹λk x. norm (f x - trunc k x)›
have ‹(λk. integral S (?fn k)) ⇢ integral S (λx. 0 :: real)›
proof (rule dominated_convergence(2))
show fn_int: ‹(λx. ?fn k x) integrable_on S› for k
by (metis absolutely_integrable_on_def assms(2) set_integral_diff(1) trunc_abs_int)
show dom_int: ‹(λx. 2 * norm (f x)) integrable_on S›
using assms(2)[unfolded absolutely_integrable_on_def]
by (auto intro: integrable_on_mult_right)
show norm_bound: ‹norm (?fn k x) ≤ 2 * norm (f x)› if ‹x ∈ S› for k x
proof -
have trunc_inner: ‹trunc k x ∙ b = max (- real k) (min (real k) (f x ∙ b))›
if ‹b ∈ Basis› for b
using inner_sum_left_Basis[OF that] by (simp add: trunc_def)
have clip_le: ‹¦max (- real k) (min (real k) (c::real))¦ ≤ ¦c¦› for c
by auto
have ‹trunc k x ∙ trunc k x ≤ f x ∙ f x›
by (metis clip_le norm_le norm_le_componentwise trunc_inner)
then have ‹norm (trunc k x) ≤ norm (f x)›
by (simp add: norm_eq_sqrt_inner real_sqrt_le_mono)
then show ?thesis
by (simp add: norm_triangle_ineq4 [THEN order_trans])
qed
show ‹(λk. ?fn k x) ⇢ 0› if ‹x ∈ S› for x
proof -
obtain N where N: ‹real N ≥ norm (f x)›
using real_nat_ceiling_ge by blast
have ‹?fn k x = 0› if ‹k ≥ N› for k
proof -
have ‹real k ≥ norm (f x)› using N that by linarith
then obtain ‹f x ∙ b ≤ real k› ‹- real k ≤ f x ∙ b› if ‹b ∈ Basis› for b
using norm_bound_Basis_le by fastforce
then have ‹trunc k x = f x›
by (simp add: trunc_def euclidean_eqI)
then show ?thesis by simp
qed
then show ?thesis
using LIMSEQ_iff by force
qed
qed
then show ?thesis by simp
qed
then obtain n where n: "norm (integral S (λx. norm (f x - trunc n x))) < e/2"
by (metis (no_types, lifting) LIMSEQ_iff assms(3) half_gt_zero order.refl diff_0_right)
show ?thesis
proof
show "bounded (range (trunc n))"
unfolding bounded_iff
proof (intro exI allI ballI)
fix y assume "y ∈ range (trunc n)"
then obtain x where y: "y = trunc n x" by auto
have "norm (max (- real n) (min (real n) (f x ∙ b)) *⇩R b) ≤ real n" if "b ∈ Basis" for b
by (simp add: that)
then have "norm (trunc n x) ≤ real DIM('b) * real n"
unfolding trunc_def by (rule sum_norm_bound)
then show "norm y ≤ real DIM('b) * real n"
by (simp add: y)
qed
qed (use n trunc_abs_int in auto)
qed
obtain B where "B > 0" and B: "⋀z. norm (h z) ≤ B"
by (meson UNIV_I bounded_pos hbo image_eqI)
obtain k g where neg_k: ‹negligible k›
and g_cont: ‹⋀n. continuous_on UNIV (g n)›
and g_bound: ‹⋀n x. norm (g n x) ≤ norm (B *⇩R (∑b∈Basis. b :: 'b))›
and g_conv: ‹⋀x. x ∈ S - k ⟹ (λn. g n x) ⇢ h x›
proof -
have ‹h integrable_on S›
using hint absolutely_integrable_on_def set_lebesgue_integral_eq_integral(1) by blast
then have ‹h ∈ borel_measurable (lebesgue_on S)›
by (rule integrable_imp_measurable)
then have h_meas: ‹h measurable_on S›
using assms
by (auto simp: measurable_on_iff_borel_measurable lmeasurable_iff_integrable fmeasurable_def)
then obtain N g where "negligible N"
and contg: "⋀n. continuous_on UNIV (g n)"
and lim: "⋀x. x ∉ N ⟹ (λn. g n x) ⇢ (if x ∈ S then h x else 0)"
by (auto simp: measurable_on_def)
define j where "j ≡ λn x. ∑b∈Basis. max (-B) (min B (g n x ∙ b)) *⇩R b :: 'b"
show ?thesis
proof
show "continuous_on UNIV (j n)" for n
unfolding j_def by (intro continuous_intros contg)
fix n x
show "norm (j n x::'b) ≤ norm (B *⇩R (∑b∈Basis. b :: 'b))"
proof (rule norm_le_componentwise)
fix b :: 'b assume b: "b ∈ Basis"
have "¦max (- B) (min B (g n x ∙ b))¦ ≤ B"
using ‹B > 0› by (auto simp: abs_le_iff)
moreover have "(∑i∈Basis. max (- B) (min B (g n x ∙ i)) *⇩R i) ∙ b
= max (- B) (min B (g n x ∙ b))"
using inner_sum_left_Basis[OF b] by simp
moreover have "(B *⇩R (∑i∈Basis. i::'b)) ∙ b = B"
by (simp add: inner_scaleR_left inner_sum_Basis[OF b])
ultimately show "¦j n x ∙ b¦ ≤ ¦(B *⇩R (∑b∈Basis. b::'b)) ∙ b¦"
using ‹B > 0› by (simp add: j_def)
qed
next
fix x :: 'a
assume xS: "x ∈ S - N"
show "(λn. j n x) ⇢ h x"
proof -
define clamp where "clamp ≡ λv::'b. ∑b∈Basis. max (-B) (min B (v ∙ b)) *⇩R b"
have j_eq: "j n x = clamp (g n x)" for n
by (simp add: j_def clamp_def)
have clamp_cont: "continuous_on UNIV clamp"
unfolding clamp_def by (intro continuous_intros)
have clamp_h: "clamp (h x) = h x"
proof -
have *: "max (- B) (min B (h x ∙ b)) = h x ∙ b" if "b ∈ Basis" for b
using norm_nth_le[OF that, of "h x"] B by (smt (verit) real_norm_def)
show ?thesis
unfolding clamp_def using * by (simp cong: sum.cong add: euclidean_representation)
qed
have g_lim: "(λn. g n x) ⇢ h x"
using lim xS by fastforce
have "isCont clamp (h x)"
using clamp_cont continuous_on_eq_continuous_at open_UNIV by fastforce
then have "(λn. clamp (g n x)) ⇢ clamp (h x)"
using continuous_imp_tendsto g_lim by (auto simp: o_def)
then show ?thesis
by (simp add: j_eq clamp_h)
qed
qed (use ‹negligible N› contg in auto)
qed
have S_sets: "S ∈ sets lebesgue"
using assms(1) by blast
have gn_int: "g n absolutely_integrable_on S" for n
proof -
have meas: "g n ∈ borel_measurable (lebesgue_on S)"
using continuous_imp_measurable_on_sets_lebesgue[OF continuous_on_subset[OF g_cont subset_UNIV] S_sets] .
have "integrable (lebesgue_on S) (norm ∘ g n)"
using finite_measure.integrable_const_bound[OF finite_measure_lebesgue_on[OF assms(1)]] g_bound
by (metis (no_types, lifting) ext comp_apply eventuallyI integrable_norm_iff meas)
then show ?thesis
using meas S_sets absolutely_integrable_measurable by blast
qed
show ?thesis
proof -
define fn where "fn ≡ λn x. norm (f x - g n x)"
have fn_int: "fn n integrable_on S" for n
using gn_int absolutely_integrable_on_def assms(2) fn_def
by fastforce
have fn_bound: "fn n x ≤ norm (f x) + norm (B *⇩R (∑b∈Basis. b :: 'b))" for n x
by (metis add_left_mono fn_def g_bound norm_triangle_le_diff)
have dom_int: "(λx. norm (f x) + norm (B *⇩R (∑b∈Basis. b :: 'b))) integrable_on S"
proof -
have "f integrable_on S"
using assms(2) set_lebesgue_integral_eq_integral(1) by blast
then have "(λx. norm (f x)) integrable_on S"
using absolutely_integrable_norm[OF assms(2)] set_lebesgue_integral_eq_integral(1)
by (simp add: absolutely_integrable_on_def)
moreover have "(λ_::'a. norm (B *⇩R (∑b∈Basis. b :: 'b))) integrable_on S"
using absolutely_integrable_on_const[OF assms(1)] set_lebesgue_integral_eq_integral(1) by blast
ultimately show ?thesis
by (rule integrable_add)
qed
have fn_conv: "(λn. fn n x) ⇢ norm (f x - h x)" if "x ∈ S - k" for x
using fn_def g_conv tendsto_diff tendsto_norm that by blast
have conv_Sk: "(λn. integral (S - k) (fn n)) ⇢ integral (S - k) (λx. norm (f x - h x))"
proof (rule dominated_convergence(2))
show "fn n integrable_on (S - k)" for n
using fn_int integrable_spike_set negligible_subset[OF neg_k]
by (simp add: has_integral_iff integrable_negligible integrable_setdiff)
show "(λx. norm (f x) + norm (B *⇩R (∑b∈Basis. b :: 'b))) integrable_on (S - k)"
using dom_int negligible_subset[OF neg_k]
by (metis (lifting) eq_integralD integrable_negligible integrable_setdiff neg_k
negligible_diff)
show "norm (fn n x) ≤ norm (f x) + norm (B *⇩R (∑b∈Basis. b :: 'b))"
if "x ∈ S - k" for n x
using fn_bound fn_def by fastforce
show "(λn. fn n x) ⇢ norm (f x - h x)" if "x ∈ S - k" for x
using fn_conv that by blast
qed
have int_eq: "integral (S - k) (fn n) = integral S (fn n)" for n
using integral_subset_negligible[of "S - k" S "fn n"] neg_k
by (simp add: Diff_Diff_Int negligible_Int)
have int_eq': "integral (S - k) (λx. norm (f x - h x)) = integral S (λx. norm (f x - h x))"
using integral_subset_negligible[of "S - k" S "λx. norm (f x - h x)"] neg_k
by (simp add: Diff_Diff_Int negligible_Int)
have conv_S: "(λn. integral S (fn n)) ⇢ integral S (λx. norm (f x - h x))"
using conv_Sk int_eq int_eq' by simp
have limit_small: "integral S (λx. norm (f x - h x)) < e"
using he2 by simp
then obtain N where "∀n≥N. norm (integral S (fn n) - integral S (λx. norm (f x - h x))) < e - integral S (λx. norm (f x - h x))"
using conv_S LIMSEQ_iff
by (smt (verit) assms(3) diff_gt_0_iff_gt)
then have "norm (integral S (fn N)) < e"
by (smt (verit, best) Henstock_Kurzweil_Integration.integral_norm_bound_integral
dual_order.refl fn_def fn_int norm_ge_zero real_norm_def)
moreover have ‹bounded (range (g N)) ›
using bounded_iff g_bound by blast
ultimately show ?thesis
using that[OF ‹g N absolutely_integrable_on S› g_cont] fn_def by blast
qed
qed
theorem absolutely_integrable_approximate_continuous:
fixes f :: ‹'a::euclidean_space ⇒ 'b::euclidean_space›
and S :: ‹'a set›
assumes S_meas: ‹S ∈ sets lebesgue›
and f_int: ‹f absolutely_integrable_on S›
and e_pos: ‹e > 0›
obtains g where ‹g absolutely_integrable_on S› ‹continuous_on UNIV g›
‹bounded (g ` UNIV)›
‹norm (integral S (λx. norm (f x - g x))) < e›
proof -
text ‹Claim 1: absolute integrability on intersections and differences with boxes.›
have f_int_inter: ‹f absolutely_integrable_on (S ∩ cbox u v)› for u v
by (meson assms fmeasurableD fmeasurable_cbox inf.cobounded1 set_integrable_subset
sets.Int sets_completionI_sets)
have f_int_diff: ‹f absolutely_integrable_on (S - cbox u v)› for u v
by (meson Diff_subset assms fmeasurableD lmeasurable_cbox set_integrable_subset
sets.Diff)
text ‹Claim 2: approximation of the norm integral by boxes.›
have norm_int: ‹(λx. norm (f x)) integrable_on S›
using f_int absolutely_integrable_on_def by blast
obtain a b where approx:
‹norm (integral (S ∩ cbox a b) (λx. norm (f x)) - integral S (λx. norm (f x))) < e / 3›
proof -
have ‹((λx. norm (f x)) has_integral integral S (λx. norm (f x))) S›
using integrable_integral [OF norm_int] .
then have alt: ‹∀ε>0. ∃B>0. ∀a b. ball 0 B ⊆ cbox a b ⟶
norm (integral (cbox a b) (λx. if x ∈ S then norm (f x) else 0) -
integral S (λx. norm (f x))) < ε›
using has_integral_alt' [of ‹λx. norm (f x)› ‹integral S (λx. norm (f x))› S]
by blast
have ‹e / 3 > 0› using e_pos by auto
then obtain B where ‹B > 0› and B:
‹∀a b. ball 0 B ⊆ cbox a b ⟶
norm (integral (cbox a b) (λx. if x ∈ S then norm (f x) else 0) -
integral S (λx. norm (f x))) < e / 3›
using alt by blast
obtain c where ‹ball (0::'a) B ⊆ cbox (- c) c›
using bounded_subset_cbox_symmetric [OF bounded_ball] by blast
then have ‹norm (integral (cbox (- c) c) (λx. if x ∈ S then norm (f x) else 0) -
integral S (λx. norm (f x))) < e / 3›
using B by blast
moreover have ‹integral (cbox (- c) c) (λx. if x ∈ S then norm (f x) else 0) =
integral (S ∩ cbox (- c) c) (λx. norm (f x))›
by (rule integral_restrict_Int)
ultimately show ?thesis
using that by auto
qed
text ‹Apply the existing lemma to get a continuous bounded approximation on the box.›
have meas_inter: ‹S ∩ cbox a b ∈ lmeasurable›
by (intro bounded_set_imp_lmeasurable bounded_Int)
(use S_meas lmeasurable_cbox fmeasurableD sets.Int in auto)
obtain g where g_int: ‹g absolutely_integrable_on (S ∩ cbox a b)›
and g_cont: ‹continuous_on UNIV g›
and g_bdd: ‹bounded (g ` UNIV)›
and g_approx: ‹norm (integral (S ∩ cbox a b) (λx. norm (f x - g x))) < e / 3›
using absolutely_integrable_approximate_continuous_vector[of "S ∩ cbox a b" f "e / 3"]
divide_pos_pos[of e "3"] e_pos f_int_inter[of a b] meas_inter
zero_less_numeral by blast
text ‹Extract an explicit positive bound on @{term g}.›
obtain B where B_pos: ‹B > 0› and B_bound: ‹⋀x. norm (g x) ≤ B›
using g_bdd [unfolded bounded_pos] by (auto simp: image_iff)
have eB: ‹e / 3 / B > 0› using e_pos B_pos by auto
obtain c d where cd_sub: ‹cbox a b ⊆ box c d›
and cd_meas: ‹measure lborel (box c d) - measure lborel (cbox a b) < e / 3 / B›
proof (cases ‹cbox a b = {}›)
case True
then show ?thesis using eB by (intro that [of 0 0]) auto
next
case False
then have ab: ‹⋀i. i ∈ Basis ⟹ a ∙ i ≤ b ∙ i› by (simp add: box_ne_empty)
define F where ‹F ≡ λδ::real. ∏i∈Basis. (b ∙ i - a ∙ i) + 2 * δ›
have F_cont: ‹isCont F 0›
unfolding F_def by (intro continuous_intros)
have F_0: ‹F 0 = measure lborel (cbox a b)›
unfolding F_def using content_cbox' [OF False] by simp
then obtain δ where ‹δ > 0› and
δ_bound: ‹⋀δ'. ¦δ'¦ < δ ⟹ ¦F δ' - F 0¦ < e / 3 / B›
using F_cont [unfolded continuous_at_real_range] eB by (auto simp: real_norm_def)
define δ' where ‹δ' ≡ min δ 1 / 2›
have δ'_pos: ‹δ' > 0› using ‹δ > 0› unfolding δ'_def by auto
have δ'_lt: ‹¦δ'¦ < δ› using ‹δ > 0› unfolding δ'_def by auto
define c' d' where ‹c' ≡ a - δ' *⇩R One› and ‹d' ≡ b + δ' *⇩R One›
have inner_c': ‹i ∈ Basis ⟹ c' ∙ i = a ∙ i - δ'› for i
unfolding c'_def by (simp add: inner_diff_left inner_scaleR_left inner_sum_Basis)
have inner_d': ‹i ∈ Basis ⟹ d' ∙ i = b ∙ i + δ'› for i
unfolding d'_def by (simp add: inner_add_left inner_scaleR_left inner_sum_Basis)
have sub: ‹cbox a b ⊆ box c' d'›
by (intro subset_box_imp ballI conjI)
(simp_all add: inner_c' inner_d' δ'_pos)
have cd_le: ‹i ∈ Basis ⟹ c' ∙ i ≤ d' ∙ i› for i
using ab [of i] δ'_pos by (simp add: inner_c' inner_d')
have cd_ne: ‹cbox c' d' ≠ {}›
using False sub box_subset_cbox [of c' d'] by auto
have content_cd: ‹measure lborel (cbox c' d') = F δ'›
unfolding F_def using content_cbox' [OF cd_ne]
by (simp add: inner_c' inner_d' algebra_simps)
have content_mono: ‹measure lborel (cbox a b) ≤ measure lborel (cbox c' d')›
using Henstock_Kurzweil_Integration.content_subset
[OF subset_trans [OF sub box_subset_cbox]] .
have ‹¦F δ' - F 0¦ < e / 3 / B›
using δ_bound δ'_lt by blast
then have ‹measure lborel (cbox c' d') - measure lborel (cbox a b) < e / 3 / B›
using content_cd F_0 content_mono by linarith
then show ?thesis
using sub that content_box_cbox [of c' d'] by simp
qed
text ‹Apply Tietze to obtain @{term h} extending @{term ‹λx. if x ∈ cbox a b then g x else 0›}
from the closed set @{term ‹cbox a b ∪ (UNIV - box c d)›} to all of @{term UNIV},
with bound @{term B}.›
obtain h where h_cont: ‹continuous_on UNIV h›
and h_eq: ‹⋀x. x ∈ cbox a b ∪ (UNIV - box c d) ⟹ h x = (if x ∈ cbox a b then g x else 0)›
and h_bound: ‹⋀x. norm (h x) ≤ B›
proof (rule Tietze [of ‹cbox a b ∪ (UNIV - box c d)›
‹λx. if x ∈ cbox a b then g x else 0› UNIV B])
show ‹continuous_on (cbox a b ∪ (UNIV - box c d))
(λx. if x ∈ cbox a b then g x else 0)›
proof (rule continuous_on_cases)
show ‹closed (cbox a b)› by (rule closed_cbox)
show ‹closed (UNIV - box c d)›
using closed_Compl [OF open_box] by (simp add: Compl_eq_Diff_UNIV)
show ‹continuous_on (cbox a b) g›
using g_cont continuous_on_subset by blast
show ‹continuous_on (UNIV - box c d) (λx. 0)›
by (rule continuous_on_const)
show ‹∀x. x ∈ cbox a b ∧ x ∉ cbox a b ∨
x ∈ UNIV - box c d ∧ x ∈ cbox a b ⟶ g x = 0›
using cd_sub by auto
qed
show ‹closedin (top_of_set UNIV) (cbox a b ∪ (UNIV - box c d))›
unfolding subtopology_UNIV closed_closedin [symmetric]
by (intro closed_Un closed_cbox closed_Compl [OF open_box, simplified Compl_eq_Diff_UNIV])
show ‹0 ≤ B› using B_pos by linarith
fix x assume ‹x ∈ cbox a b ∪ (UNIV - box c d)›
then show ‹norm (if x ∈ cbox a b then g x else 0) ≤ B›
using B_bound B_pos by (auto simp: less_imp_le)
next
fix h assume ‹continuous_on UNIV h›
and ‹⋀x. x ∈ cbox a b ∪ (UNIV - box c d) ⟹ h x = (if x ∈ cbox a b then g x else 0)›
and ‹⋀x. x ∈ UNIV ⟹ norm (h x) ≤ B›
then show thesis
by (intro that [of h]) auto
qed
text ‹Show that @{term h} is absolutely integrable on @{term S}.›
have h_zero: ‹h x = 0› if ‹x ∉ cbox c d› for x
by (metis DiffI Diff_partition UNIV_I UnCI box_subset_cbox cd_sub h_eq that)
have h_abs_cbox: ‹h absolutely_integrable_on cbox c d›
by (rule absolutely_integrable_continuous [OF continuous_on_subset [OF h_cont subset_UNIV]])
have h_abs_inter: ‹h absolutely_integrable_on (S ∩ cbox c d)›
using h_abs_cbox S_meas
by (meson fmeasurableD fmeasurable_cbox inf.cobounded2 set_integrable_subset
sets.Int sets_completionI_sets)
have h_abs_S: ‹h absolutely_integrable_on S›
proof (rule absolutely_integrable_spike_set [OF h_abs_inter])
show ‹negligible {x ∈ S ∩ cbox c d - S. h x ≠ 0}›
by (simp add: Int_Diff)
show ‹negligible {x ∈ S - S ∩ cbox c d. h x ≠ 0}›
by (simp add: h_zero cong: conj_cong)
qed
have h_int_inter: ‹h absolutely_integrable_on (S ∩ cbox u v)› for u v
by (meson h_abs_S S_meas fmeasurableD fmeasurable_cbox inf.cobounded1 set_integrable_subset
sets.Int sets_completionI_sets)
have h_int_diff: ‹h absolutely_integrable_on (S - cbox u v)› for u v
by (meson h_abs_S S_meas Diff_subset fmeasurableD lmeasurable_cbox set_integrable_subset
sets.Diff)
show ?thesis
proof
show ‹h absolutely_integrable_on S› by (rule h_abs_S)
next
have fh_abs_inter: ‹(λx. f x - h x) absolutely_integrable_on (S ∩ cbox a b)›
using f_int_inter h_int_inter by (rule set_integral_diff(1))
have fh_abs_diff: ‹(λx. f x - h x) absolutely_integrable_on (S - cbox a b)›
using f_int_diff h_int_diff by (rule set_integral_diff(1))
have nfh_int_inter: ‹(λx. norm (f x - h x)) integrable_on (S ∩ cbox a b)›
using absolutely_integrable_norm [OF fh_abs_inter]
by (auto intro: set_lebesgue_integral_eq_integral(1) simp: o_def)
have nfh_int_diff: ‹(λx. norm (f x - h x)) integrable_on (S - cbox a b)›
using absolutely_integrable_norm [OF fh_abs_diff]
by (auto intro: set_lebesgue_integral_eq_integral(1) simp: o_def)
have split_eq: ‹integral S (λx. norm (f x - h x)) =
integral (S ∩ cbox a b) (λx. norm (f x - h x)) + integral (S - cbox a b) (λx. norm (f x - h x))›
by (metis (lifting) Diff_disjoint Int_Diff_Un Int_assoc integral_Un negligible_Int
negligible_empty nfh_int_diff nfh_int_inter)
have h_eq_g_on_ab: ‹h x = g x› if ‹x ∈ cbox a b› for x
using h_eq [of x] that by auto
have integral_fg_eq: ‹integral (S ∩ cbox a b) (λx. norm (f x - g x)) =
integral (S ∩ cbox a b) (λx. norm (f x - h x))›
by (intro integral_unique has_integral_eq [OF _ integrable_integral [OF nfh_int_inter]])
(auto simp: h_eq_g_on_ab)
have nf_int_diff: ‹(λx. norm (f x)) integrable_on (S - cbox a b)›
using absolutely_integrable_norm [OF f_int_diff]
by (auto intro: set_lebesgue_integral_eq_integral(1) simp: o_def)
have nh_int_diff: ‹(λx. norm (h x)) integrable_on (S - cbox a b)›
using absolutely_integrable_norm [OF h_int_diff]
by (auto intro: set_lebesgue_integral_eq_integral(1) simp: o_def)
have nfh_sum_int_diff: ‹(λx. norm (f x) + norm (h x)) integrable_on (S - cbox a b)›
by (rule integrable_add [OF nf_int_diff nh_int_diff])
have norm_diff_bound: ‹norm (integral (S - cbox a b) (λx. norm (f x - h x))) ≤
integral (S - cbox a b) (λx. norm (f x) + norm (h x))›
by (rule integral_norm_bound_integral [OF nfh_int_diff nfh_sum_int_diff])
(simp add: norm_triangle_ineq4)
have nf_int_inter: ‹(λx. norm (f x)) integrable_on (S ∩ cbox a b)›
using absolutely_integrable_norm [OF f_int_inter]
by (auto intro: set_lebesgue_integral_eq_integral(1) simp: o_def)
have nf_split: ‹integral (S ∩ cbox a b) (λx. norm (f x)) + integral (S - cbox a b) (λx. norm (f x))
= integral S (λx. norm (f x))›
by (metis Diff_disjoint Int_Diff_Un Int_assoc integral_Un negligible_Int
negligible_empty nf_int_diff nf_int_inter)
have nf_diff_bound: ‹integral (S - cbox a b) (λx. norm (f x)) < e / 3›
using nf_split approx integral_nonneg [OF nf_int_diff]
by (simp add: abs_le_iff)
have nh_diff_bound: ‹integral (S - cbox a b) (λx. norm (h x)) < e / 3›
proof -
have cd_ab_meas: ‹box c d - cbox a b ∈ lmeasurable›
using lmeasurable_box lmeasurable_cbox by (rule fmeasurable.Diff)
have int1: ‹(λx. if x ∈ S - cbox a b then norm (h x) else 0) integrable_on UNIV›
using nh_int_diff integrable_restrict_UNIV by fastforce
have int2: ‹(λx. if x ∈ box c d - cbox a b then B else 0) integrable_on UNIV›
using integrable_on_const [OF cd_ab_meas] integrable_restrict_UNIV by fastforce
have pw: ‹norm (if x ∈ S - cbox a b then norm (h x) else 0) ≤
(if x ∈ box c d - cbox a b then B else 0)› for x
using B_pos h_bound h_eq by force
have ‹integral (S - cbox a b) (λx. norm (h x)) =
integral UNIV (λx. if x ∈ S - cbox a b then norm (h x) else 0)›
by (rule integral_restrict_UNIV [symmetric])
moreover have ‹integral (box c d - cbox a b) (λx. B) =
integral UNIV (λx. if x ∈ box c d - cbox a b then B else 0)›
by (rule integral_restrict_UNIV [symmetric])
moreover have ‹norm (integral UNIV (λx. if x ∈ S - cbox a b then norm (h x) else 0)) ≤
integral UNIV (λx. if x ∈ box c d - cbox a b then B else 0)›
by (rule integral_norm_bound_integral [OF int1 int2 pw])
ultimately have nh_le_const:
‹integral (S - cbox a b) (λx. norm (h x)) ≤ integral (box c d - cbox a b) (λx. B)›
by simp
also have ‹… = B * (measure lebesgue (box c d) - measure lebesgue (cbox a b))›
by (metis (no_types, lifting) ext Henstock_Kurzweil_Integration.integral_mult_right
cd_ab_meas lmeasure_integral mult_1_right
measurable_measure_Diff [OF lmeasurable_box]
lmeasurable_cbox fmeasurableD cd_sub)
also have ‹… < B * (e / 3 / B)›
using cd_meas B_pos by (intro mult_strict_left_mono) auto
also have ‹… = e / 3›
using B_pos by auto
finally show ?thesis .
qed
have step1: ‹norm (integral (S ∩ cbox a b) (λx. norm (f x - h x))) < e / 3›
using g_approx by (simp add: integral_fg_eq)
have step2: ‹norm (integral (S - cbox a b) (λx. norm (f x - h x))) < 2 / 3 * e›
using norm_diff_bound integral_add [OF nf_int_diff nh_int_diff]
nf_diff_bound nh_diff_bound
by linarith
have ‹norm (integral S (λx. norm (f x - h x))) ≤
norm (integral (S ∩ cbox a b) (λx. norm (f x - h x))) +
norm (integral (S - cbox a b) (λx. norm (f x - h x)))›
by (simp add: split_eq norm_triangle_ineq)
also have ‹… < e / 3 + 2 / 3 * e›
using step1 step2 by linarith
also have ‹… = e› by simp
finally show "norm (integral S (λx. norm (f x - h x))) < e" .
qed (use h_bound h_cont bounded_iff in auto)
qed
lemma absolutely_continuous_integral:
fixes f :: ‹'a::euclidean_space ⇒ 'b::euclidean_space›
assumes ‹f absolutely_integrable_on S› ‹0 < ε›
obtains δ where ‹δ>0› ‹⋀T. T ⊆ S ⟹ T ∈ lmeasurable ⟹ measure lebesgue T < δ
⟹ norm (integral T f) < ε›
proof -
define f0 where "f0 ≡ λx. if x ∈ S then f x else 0"
have f0_ai: "f0 absolutely_integrable_on UNIV"
using assms(1) unfolding f0_def absolutely_integrable_restrict_UNIV .
have f0_int: "f0 integrable_on UNIV"
using f0_ai absolutely_integrable_on_def by blast
have nf0_int: "(λx. norm (f0 x)) integrable_on UNIV"
using f0_ai absolutely_integrable_on_def by blast
have f0_eq: "⋀x. x ∈ S ⟹ f0 x = f x" unfolding f0_def by simp
obtain g :: ‹'a ⇒ 'b› where g_ai: ‹g absolutely_integrable_on UNIV›
and g_bdd: ‹bounded (range g)›
and g_approx: ‹norm (integral UNIV (λx. norm (f0 x - g x))) < ε/2›
using ‹0 < ε› absolutely_integrable_approximate_continuous [OF _ f0_ai, where e = ‹ ε/2›]
by force
obtain B where ‹B > 0› and B: ‹⋀x. norm (g x) ≤ B›
using g_bdd bounded_pos[of ‹range g›] by auto
show ?thesis
proof
show "ε/2/B > 0"
by (simp add: ‹0 < B› ‹0 < ε›)
next
fix T
assume "T ⊆ S"
and "T ∈ lmeasurable"
and *: "Sigma_Algebra.measure lebesgue T < ε/2/B"
have g_ai_t: ‹g absolutely_integrable_on T›
by (meson ‹T ∈ lmeasurable› fmeasurableD g_ai set_integrable_subset subset_UNIV)
have f0_ai_t: ‹f0 absolutely_integrable_on T›
by (meson ‹T ∈ lmeasurable› f0_ai fmeasurableD set_integrable_subset subset_UNIV)
have f_ai_t: ‹f absolutely_integrable_on T›
using ‹T ∈ lmeasurable› ‹T ⊆ S› assms(1) set_integrable_subset by blast
have f0g_ai_t: ‹(λx. f0 x - g x) absolutely_integrable_on T›
using f0_ai_t g_ai_t by blast
have nf0g_int_t: ‹(λx. norm (f0 x - g x)) integrable_on T›
using f0g_ai_t absolutely_integrable_on_def by metis
have ng_int_t: ‹(λx. norm (g x)) integrable_on T›
using g_ai_t absolutely_integrable_on_def by blast
have bnd_int_t: ‹(λx. norm (f0 x - g x) + norm (g x)) integrable_on T›
using nf0g_int_t ng_int_t integrable_add by blast
have ineq1: ‹norm (integral T f) ≤ integral T (λx. norm (f0 x - g x) + norm (g x))›
proof (rule integral_norm_bound_integral)
show ‹f integrable_on T›
using f_ai_t set_lebesgue_integral_eq_integral by blast
show ‹(λx. norm (f0 x - g x) + norm (g x)) integrable_on T›
using bnd_int_t .
fix x assume ‹x ∈ T›
then have ‹f x = f0 x› using ‹T ⊆ S› f0_eq by auto
then show ‹norm (f x) ≤ norm (f0 x - g x) + norm (g x)›
using norm_triangle_ineq[of ‹f0 x - g x› ‹g x›] by simp
qed
also have ‹… = integral T (λx. norm (f0 x - g x)) + integral T (λx. norm (g x))›
using integral_add[OF nf0g_int_t ng_int_t] .
also have ‹… < ε›
proof -
have ineq2a: ‹integral T (λx. norm (f0 x - g x)) < ε/2›
proof -
have nf0g_int: ‹(λx. norm (f0 x - g x)) integrable_on UNIV›
using f0_ai g_ai absolutely_integrable_on_def set_integral_diff
by metis
have ‹integral T (λx. norm (f0 x - g x)) ≤ integral UNIV (λx. norm (f0 x - g x))›
by (rule integral_subset_le[OF subset_UNIV nf0g_int_t nf0g_int]) simp
also have ‹… ≤ norm (integral UNIV (λx. norm (f0 x - g x)))›
by auto
also have ‹… < ε/2›
using g_approx .
finally show ?thesis .
qed
have ineq2b: ‹integral T (λx. norm (g x)) < ε/2›
proof -
have B_int_t: ‹(λx. B) integrable_on T›
using ‹T ∈ lmeasurable› integrable_on_const by blast
have ‹integral T (λx. norm (g x)) ≤ integral T (λx. B)›
by (rule integral_le[OF ng_int_t B_int_t]) (use B in auto)
also have ‹… = B * measure lebesgue T›
using Henstock_Kurzweil_Integration.integral_mult_right[of T B "λ_. 1"] ‹T ∈ lmeasurable›
lmeasure_integral[of T] by fastforce
also have ‹… < ε/2›
using * ‹B > 0› by (simp add: field_simps)
finally show ?thesis .
qed
from ineq2a ineq2b show ?thesis by linarith
qed
finally show "norm (integral T f) < ε" .
qed
qed
text ‹Integration by parts for absolutely integrable functions.
The first lemma is a direct specialisation of @{thm integration_by_parts}
to real-valued multiplication.›
lemma real_integration_by_parts_simple:
fixes f g f' g' :: "real ⇒ real" and a b y :: real
assumes "a ≤ b"
and "continuous_on {a..b} f" and "continuous_on {a..b} g"
and "⋀x. x ∈ {a..b} ⟹ (f has_vector_derivative f' x) (at x)"
and "⋀x. x ∈ {a..b} ⟹ (g has_vector_derivative g' x) (at x)"
and "((λx. f x * g' x) has_integral (f b * g b - f a * g a - y)) {a..b}"
shows "((λx. f' x * g x) has_integral y) {a..b}"
by (rule integration_by_parts [OF bounded_bilinear_mult]) (use assms in auto)
text ‹Integration by parts for absolutely integrable functions with indefinite integrals.
This is the bilinear generalisation.›
lemma L1_bound:
fixes a b :: real and hh' :: "real ⇒ 'a::euclidean_space" and h' :: "real ⇒ 'a"
assumes x_ab: ‹x ∈ {a..b}›
and hh'_int: ‹hh' integrable_on {a..b}›
and h'_int: ‹h' integrable_on {a..b}›
and norm_diff_int: ‹(λt. norm (h' t - hh' t)) integrable_on {a..b}›
and h_eq: ‹h x = integral {a..x} h'›
shows ‹norm (integral {a..x} hh' - h x) ≤ integral {a..b} (λt. norm (h' t - hh' t))›
proof -
have ac_sub: ‹{a..x} ⊆ {a..b}› using x_ab by auto
have hh'_int_x: ‹hh' integrable_on {a..x}›
using integrable_on_subinterval[OF hh'_int ac_sub] .
have h'_int_x: ‹h' integrable_on {a..x}›
using integrable_on_subinterval[OF h'_int ac_sub] .
have diff_int_x: ‹(λt. hh' t - h' t) integrable_on {a..x}›
using integrable_diff[OF hh'_int_x h'_int_x] .
have norm_diff_int_x: ‹(λt. norm (h' t - hh' t)) integrable_on {a..x}›
using integrable_on_subinterval[OF norm_diff_int ac_sub] .
have ‹norm (integral {a..x} hh' - h x) = norm (integral {a..x} hh' - integral {a..x} h')›
using h_eq by simp
also have ‹… = norm (integral {a..x} (λt. hh' t - h' t))›
using integral_diff[OF hh'_int_x h'_int_x] by simp
also have ‹… ≤ integral {a..x} (λt. norm (h' t - hh' t))›
using integral_norm_bound_integral[OF diff_int_x norm_diff_int_x]
by (simp add: norm_minus_commute)
also have ‹… ≤ integral {a..b} (λt. norm (h' t - hh' t))›
using integral_subset_le[OF ac_sub norm_diff_int_x norm_diff_int] by simp
finally show ?thesis .
qed
lemma uniform_from_L1:
fixes a b :: real and hh' :: "[nat, real] ⇒ 'a::euclidean_space"
assumes ab: ‹a ≤ b›
and hh': ‹⋀n. hh' n absolutely_integrable_on {a..b} ∧
norm (integral {a..b} (λx. norm (h' x - hh' n x))) < inverse (real n + 1)›
and h'_abs: ‹h' absolutely_integrable_on {a..b}›
and h'_has: ‹⋀x. x ∈ {a..b} ⟹ (h' has_integral h x) {a..x}›
and hh'_cont: ‹⋀n. continuous_on {a..b} (hh' n)›
defines ‹hh ≡ λn x. integral {a..x} (hh' n)›
shows ‹(λn. SUP x∈{a..b}. norm (hh n x - h x)) ⇢ 0›
proof -
have h'_int: ‹h' integrable_on {a..b}›
using h'_abs set_lebesgue_integral_eq_integral(1) by blast
have hh'_L1: ‹(λn. integral {a..b} (λx. norm (h' x - hh' n x))) ⇢ 0›
by (metis (lifting) LIMSEQ_norm_0 Num.of_nat_simps(3) add.commute hh' inverse_eq_divide)
have hh'n_int: ‹hh' n integrable_on {a..b}› for n
using hh'_cont integrable_continuous_real by blast
have norm_diff_int: ‹(λx. norm (h' x - hh' n x)) integrable_on {a..b}› for n
by (metis absolutely_integrable_on_def h'_abs hh' set_integral_diff(1))
have h'int_eq: ‹h x = integral {a..x} h'› if ‹x ∈ {a..b}› for x
using integral_unique[OF h'_has[OF that]] by simp
show ?thesis
proof (rule Lim_null_comparison[OF _ hh'_L1])
show ‹∀⇩F n in sequentially. norm (SUP x∈{a..b}. norm (hh n x - h x))
≤ integral {a..b} (λx. norm (h' x - hh' n x))›
proof (intro always_eventually allI)
fix n
have ne: ‹{a..b} ≠ {}› using ab by auto
have bound: ‹norm (hh n x - h x) ≤ integral {a..b} (λt. norm (h' t - hh' n t))›
if ‹x ∈ {a..b}› for x
unfolding hh_def using L1_bound h'_int h'int_eq hh'n_int norm_diff_int that by blast
have bdd: ‹bdd_above ((λx. norm (hh n x - h x)) ` {a..b})›
by (meson bdd_above.I2 bound)
have sup_bound: ‹(SUP x∈{a..b}. norm (hh n x - h x)) ≤ integral {a..b} (λt. norm (h' t - hh' n t))›
by (metis (mono_tags, lifting) bound cSUP_least ne)
have sup_nonneg: ‹(SUP x∈{a..b}. norm (hh n x - h x)) ≥ 0›
by (metis (no_types, lifting) ab atLeastAtMost_iff bdd cSUP_upper2 order.refl norm_ge_zero)
show ‹norm (SUP x∈{a..b}. norm (hh n x - h x)) ≤ integral {a..b} (λx. norm (h' x - hh' n x))›
using sup_bound sup_nonneg by simp
qed
qed
qed
lemma pointwise:
fixes a b::real and ff' :: "[nat,real] ⇒ 'a::euclidean_space"
assumes c_ab: ‹c ∈ {a..b}›
and ff': ‹⋀n. ff' n absolutely_integrable_on {a..b} ∧
norm (integral {a..b} (λx. norm (f' x - ff' n x))) < inverse (real n + 1)›
and f'_abs: ‹f' absolutely_integrable_on {a..b}›
and f'_has: ‹⋀x. x ∈ {a..b} ⟹ (f' has_integral f x) {a..x}›
defines ‹ff ≡ λn x. integral {a..x} (ff' n)›
shows ‹(λn. ff n c) ⇢ f c›
proof -
have f'_int: "f' integrable_on {a..b}"
using f'_abs set_lebesgue_integral_eq_integral(1) by blast
have ff'n_int: ‹ff' n integrable_on {a..b}› for n
using absolutely_integrable_on_def ff' by blast
have norm_diff_int: ‹(λx. norm (f' x - ff' n x)) integrable_on {a..b}› for n
using absolutely_integrable_on_def f'_abs set_integrable_norm ff' by blast
have ff'_L1: ‹(λn. integral {a..b} (λx. norm (f' x - ff' n x))) ⇢ 0›
by (metis (lifting) LIMSEQ_norm_0 Num.of_nat_simps(3) add.commute ff' inverse_eq_divide)
have f'int_eq: "f x = integral {a..x} f'" if "x ∈ {a..b}" for x
using integral_unique[OF f'_has[OF that]] by simp
have bound: ‹norm (ff n c - f c) ≤ integral {a..b} (λx. norm (f' x - ff' n x))› for n
unfolding ff_def using L1_bound c_ab f'_int f'int_eq ff'n_int norm_diff_int by blast
show ?thesis
using Lim_null_comparison[OF _ ff'_L1, of "(λn. ff n c - f c)"]
using bound eventually_sequentially by (auto simp: LIM_zero_iff)
qed
lemma L1_inv_bound:
fixes a b :: real and ff' :: "[nat, real] ⇒ 'a::euclidean_space"
assumes x_ab: ‹x ∈ {a..b}›
and ff': ‹⋀n. ff' n absolutely_integrable_on {a..b} ∧
norm (integral {a..b} (λx. norm (f' x - ff' n x))) < inverse (real n + 1)›
and f'_abs: ‹f' absolutely_integrable_on {a..b}›
and f'_has: ‹⋀x. x ∈ {a..b} ⟹ (f' has_integral f x) {a..x}›
and ff'_cont: ‹continuous_on {a..b} (ff' n)›
defines ‹ff ≡ λx. integral {a..x} (ff' n)›
shows ‹norm (ff x - f x) ≤ inverse (real n + 1)›
proof -
have f'_int: ‹f' integrable_on {a..b}›
using f'_abs set_lebesgue_integral_eq_integral(1) by blast
have ff'n_int: ‹ff' n integrable_on {a..b}›
using ff'_cont integrable_continuous_real by blast
have norm_diff_int: ‹(λt. norm (f' t - ff' n t)) integrable_on {a..b}›
by (metis absolutely_integrable_on_def f'_abs ff' set_integral_diff(1))
have f'int_eq: ‹f x = integral {a..x} f'›
using integral_unique[OF f'_has[OF x_ab]] by simp
have bound: ‹norm (ff x - f x) ≤ integral {a..b} (λt. norm (f' t - ff' n t))›
unfolding ff_def
using L1_bound f'_int f'int_eq ff'n_int norm_diff_int x_ab by blast
have ‹integral {a..b} (λt. norm (f' t - ff' n t)) < inverse (real n + 1)›
using integral_nonneg[OF norm_diff_int] ff'[of n] by simp
then show ?thesis using bound by linarith
qed
lemma integral_antiderivative_bound:
fixes a b x :: real and h' :: ‹real ⇒ 'a::banach›
assumes h'_int: ‹h' integrable_on {a..b}› and nh'_int: ‹(λx. norm (h' x)) integrable_on {a..b}›
and h_eq: ‹⋀x. x ∈ {a..b} ⟹ h x = integral {a..x} h'›
and h'_B: ‹integral {a..b} (λx. norm (h' x)) ≤ B› and x_ab: ‹x ∈ {a..b}›
shows ‹norm (h x) ≤ B›
proof -
have sub: ‹{a..x} ⊆ {a..b}› using x_ab by auto
have h'_sub: ‹h' integrable_on {a..x}›
using h'_int sub by (rule integrable_subinterval_real)
have nh'_sub: ‹(λt. norm (h' t)) integrable_on {a..x}›
using nh'_int sub by (rule integrable_subinterval_real)
have ‹norm (h x) = norm (integral {a..x} h')› using h_eq x_ab by simp
also have ‹… ≤ integral {a..x} (λt. norm (h' t))›
using integral_norm_bound_integral[OF h'_sub nh'_sub] by simp
also have ‹… ≤ integral {a..b} (λt. norm (h' t))›
using integral_subset_le[OF sub nh'_sub nh'_int] by simp
also have ‹… ≤ B› using h'_B .
finally show ?thesis .
qed
lemma bilinear_integral_bound:
fixes bop :: ‹'a::euclidean_space ⇒ 'b::euclidean_space ⇒ 'c::euclidean_space›
assumes bop_bound: ‹⋀u v. norm (bop u v) ≤ M * norm u * norm v›
and u_bound: ‹⋀x. x ∈ {a..b} ⟹ norm (u x) ≤ C›
and v_int: ‹(λx. norm (v x)) integrable_on {a..b}›
and bop_int: ‹(λx. bop (u x) (v x)) integrable_on {a..b}›
and ‹M ≥ 0› ‹C ≥ 0›
shows ‹norm (integral {a..b} (λx. bop (u x) (v x))) ≤ M * C * integral {a..b} (λx. norm (v x))›
proof -
have bound_int: ‹(λx. M * C * norm (v x)) integrable_on {a..b}›
using integrable_cmul[OF v_int, of ‹M * C›] by (simp add: scaleR_conv_of_real mult.assoc)
have ‹norm (integral {a..b} (λx. bop (u x) (v x)))
≤ integral {a..b} (λx. M * C * norm (v x))›
proof (rule integral_norm_bound_integral[OF bop_int bound_int])
fix x assume ‹x ∈ {a..b}›
have ‹norm (bop (u x) (v x)) ≤ M * norm (u x) * norm (v x)›
using bop_bound by blast
also have ‹… ≤ M * C * norm (v x)›
using u_bound[OF ‹x ∈ {a..b}›] ‹M ≥ 0›
by (intro mult_right_mono mult_left_mono) auto
finally show ‹norm (bop (u x) (v x)) ≤ M * C * norm (v x)› .
qed
also have ‹… = M * C * integral {a..b} (λx. norm (v x))›
by simp
finally show ?thesis .
qed
lemma L1_approx_setup:
fixes h' :: ‹real ⇒ 'a::euclidean_space› and h :: ‹real ⇒ 'a›
assumes ab: ‹a ≤ b›
and h'abs: ‹h' absolutely_integrable_on {a..b}›
and h'int: ‹⋀x. x ∈ {a..b} ⟹ (h' has_integral h x) {a..x}›
obtains hh' hh where
‹⋀n. hh' n absolutely_integrable_on {a..b}›
‹⋀n. continuous_on {a..b} (hh' n)›
‹⋀n. continuous_on {a..b} (hh n)›
‹⋀n. norm (integral {a..b} (λx. norm (h' x - hh' n x))) < inverse (real n + 1)›
‹(λn. integral {a..b} (λx. norm (h' x - hh' n x))) ⇢ 0›
‹⋀c. c ∈ {a..b} ⟹ (λn. hh n c) ⇢ h c›
‹(λn. SUP x∈{a..b}. norm (hh n x - h x)) ⇢ 0›
‹⋀n. (λx. norm (h' x - hh' n x)) integrable_on {a..b}›
‹⋀n x. x ∈ {a<..<b} ⟹ (hh n has_vector_derivative hh' n x) (at x)›
‹⋀n x. x ∈ {a..b} ⟹ norm (hh n x - h x) ≤ inverse (real n + 1)›
proof -
have ‹∀n. ∃k. k absolutely_integrable_on {a..b} ∧ continuous_on UNIV k ∧ bounded (range k) ∧
norm (integral {a..b} (λx. norm (h' x - k x))) < inverse (real n + 1)›
using absolutely_integrable_approximate_continuous_vector[OF _ h'abs]
by (metis (full_types) bot_nat_0.extremum inverse_positive_iff_positive
lmeasurable_interval(1) nat_le_real_less of_nat_0_eq_iff)
then obtain hh' where hh'_props:
‹⋀n. hh' n absolutely_integrable_on {a..b} ∧ continuous_on UNIV (hh' n) ∧
bounded (range (hh' n)) ∧
norm (integral {a..b} (λx. norm (h' x - hh' n x))) < inverse (real n + 1)›
unfolding choice_iff by blast
define hh where ‹hh ≡ λn x. integral {a..x} (hh' n)›
show thesis
proof
show hh'_absint: ‹hh' n absolutely_integrable_on {a..b}› for n
using hh'_props by blast
show hh'_cont: ‹continuous_on {a..b} (hh' n)› for n
using hh'_props continuous_on_subset by blast
show hh'_approx: ‹norm (integral {a..b} (λx. norm (h' x - hh' n x))) < inverse (real n + 1)› for n
using hh'_props by blast
show ‹continuous_on {a..b} (hh n)› for n
unfolding hh_def using hh'_props indefinite_integral_continuous_1
set_lebesgue_integral_eq_integral(1) by blast
show ‹(λn. integral {a..b} (λx. norm (h' x - hh' n x))) ⇢ 0›
by (metis (lifting) LIMSEQ_norm_0 Num.of_nat_simps(3) add.commute hh'_approx inverse_eq_divide)
show ‹(λn. hh n c) ⇢ h c› if ‹c ∈ {a..b}› for c
unfolding hh_def using h'abs h'int hh'_props pointwise that by blast
have hh'_conj: ‹hh' n absolutely_integrable_on {a..b} ∧
norm (integral {a..b} (λx. norm (h' x - hh' n x))) < inverse (real n + 1)› for n
using hh'_absint hh'_approx by blast
show ‹(λn. SUP x∈{a..b}. norm (hh n x - h x)) ⇢ 0›
unfolding hh_def using uniform_from_L1[OF ab hh'_conj h'abs h'int hh'_cont] .
show ‹(λx. norm (h' x - hh' n x)) integrable_on {a..b}› for n
by (metis absolutely_integrable_on_def h'abs hh'_props set_integral_diff(1))
show ‹(hh n has_vector_derivative hh' n x) (at x)› if ‹x ∈ {a<..<b}› for n x
using integral_has_vector_derivative[OF hh'_cont] that
using at_within_Icc_at hh_def less_eq_real_def by fastforce
show ‹norm (hh n x - h x) ≤ inverse (real n + 1)› if ‹x ∈ {a..b}› for n x
unfolding hh_def using L1_inv_bound[OF that hh'_conj h'abs h'int hh'_cont] .
qed
qed
lemma ibp_fun_setup:
fixes h' :: ‹real ⇒ 'a::euclidean_space›
assumes ab: ‹a ≤ b›
and h'abs: ‹h' absolutely_integrable_on {a..b}›
and h'int: ‹⋀x. x ∈ {a..b} ⟹ (h' has_integral h x) {a..x}›
shows h'int_eq: ‹⋀x. x ∈ {a..b} ⟹ h x = integral {a..x} h'›
and h'_int: ‹h' integrable_on {a..b}›
and h_cont: ‹continuous_on {a..b} h›
and h_meas: ‹h ∈ borel_measurable (lebesgue_on {a..b})›
and h_bounded: ‹bounded (h ` {a..b})›
and norm_h'_int: ‹(λx. norm (h' x)) integrable_on {a..b}›
proof -
show eq: ‹h x = integral {a..x} h'› if ‹x ∈ {a..b}› for x
using integral_unique[OF h'int[OF that]] by simp
show int: ‹h' integrable_on {a..b}›
using h'abs absolutely_integrable_on_def by blast
show ‹continuous_on {a..b} h›
by (metis (mono_tags, lifting) continuous_on_cong int eq indefinite_integral_continuous_1)
then show ‹h ∈ borel_measurable (lebesgue_on {a..b})›
using integrable_imp_measurable[OF integrable_continuous_real] by blast
show ‹bounded (h ` {a..b})›
using compact_continuous_image[OF ‹continuous_on {a..b} h› compact_Icc] compact_imp_bounded by blast
show ‹(λx. norm (h' x)) integrable_on {a..b}›
using h'abs absolutely_integrable_on_def by blast
qed
theorem absolute_integration_by_parts:
fixes bop :: ‹'a::euclidean_space ⇒ 'b::euclidean_space ⇒ 'c::euclidean_space›
and f :: ‹real ⇒ 'a› and g :: ‹real ⇒ 'b›
and f' :: ‹real ⇒ 'a› and g' :: ‹real ⇒ 'b›
assumes ‹bilinear bop›
and ab: ‹a ≤ b›
and f'abs: ‹f' absolutely_integrable_on {a..b}›
and g'abs: ‹g' absolutely_integrable_on {a..b}›
and f'int: ‹⋀x. x ∈ {a..b} ⟹ (f' has_integral f x) {a..x}›
and g'int: ‹⋀x. x ∈ {a..b} ⟹ (g' has_integral g x) {a..x}›
shows ‹(λx. bop (f x) (g' x)) absolutely_integrable_on {a..b}›
and ‹(λx. bop (f' x) (g x)) absolutely_integrable_on {a..b}›
and ‹integral {a..b} (λx. bop (f x) (g' x)) + integral {a..b} (λx. bop (f' x) (g x))
= bop (f b) (g b) - bop (f a) (g a)›
proof -
have ‹bounded_bilinear bop›
using ‹bilinear bop› bilinear_conv_bounded_bilinear by blast
note f_setup = ibp_fun_setup[OF ab f'abs f'int]
note f'int_eq = f_setup(1) and f'_int = f_setup(2) and f_cont = f_setup(3)
and f_meas = f_setup(4) and f_bounded = f_setup(5) and norm_f'_int = f_setup(6)
note g_setup = ibp_fun_setup[OF ab g'abs g'int]
note g'int_eq = g_setup(1) and g'_int = g_setup(2) and g_cont = g_setup(3)
and g_meas = g_setup(4) and g_bounded = g_setup(5) and norm_g'_int = g_setup(6)
have ab_sets: "{a..b} ∈ sets lebesgue"
by simp
have bop_swap: "bilinear (λx y. bop y x)"
using ‹bilinear bop› by (simp add: bilinear_def)
show "(λx. bop (f x) (g' x)) absolutely_integrable_on {a..b}"
using absolutely_integrable_bounded_measurable_product[OF ‹bilinear bop› f_meas ab_sets f_bounded g'abs] .
show "(λx. bop (f' x) (g x)) absolutely_integrable_on {a..b}"
using absolutely_integrable_bounded_measurable_product[OF bop_swap g_meas ab_sets g_bounded f'abs] .
obtain ff' ff where
ff'_absint: ‹⋀n. ff' n absolutely_integrable_on {a..b}› and
ff'_cont_ab: ‹⋀n. continuous_on {a..b} (ff' n)› and
ff_cont: ‹⋀n. continuous_on {a..b} (ff n)› and
ff'_approx: ‹⋀n. norm (integral {a..b} (λx. norm (f' x - ff' n x))) < inverse (real n + 1)› and
ff'_L1: ‹(λn. integral {a..b} (λx. norm (f' x - ff' n x))) ⇢ 0› and
ff_ptwise: ‹⋀c. c ∈ {a..b} ⟹ (λn. ff n c) ⇢ f c› and
ff_uniform: ‹(λn. SUP x∈{a..b}. norm (ff n x - f x)) ⇢ 0› and
norm_ff'_diff_int: ‹⋀n. (λx. norm (f' x - ff' n x)) integrable_on {a..b}› and
ff_deriv: ‹⋀n x. x ∈ {a<..<b} ⟹ (ff n has_vector_derivative ff' n x) (at x)› and
ff_inv_bound: ‹⋀n x. x ∈ {a..b} ⟹ norm (ff n x - f x) ≤ inverse (real n + 1)›
using L1_approx_setup[OF ab f'abs f'int] by blast
obtain gg' gg where
gg'_absint: ‹⋀n. gg' n absolutely_integrable_on {a..b}› and
gg'_cont_ab: ‹⋀n. continuous_on {a..b} (gg' n)› and
gg_cont: ‹⋀n. continuous_on {a..b} (gg n)› and
gg'_approx: ‹⋀n. norm (integral {a..b} (λx. norm (g' x - gg' n x))) < inverse (real n + 1)› and
gg'_L1: ‹(λn. integral {a..b} (λx. norm (g' x - gg' n x))) ⇢ 0› and
gg_ptwise: ‹⋀c. c ∈ {a..b} ⟹ (λn. gg n c) ⇢ g c› and
gg_uniform: ‹(λn. SUP x∈{a..b}. norm (gg n x - g x)) ⇢ 0› and
norm_gg'_diff_int: ‹⋀n. (λx. norm (g' x - gg' n x)) integrable_on {a..b}› and
gg_deriv: ‹⋀n x. x ∈ {a<..<b} ⟹ (gg n has_vector_derivative gg' n x) (at x)› and
gg_inv_bound: ‹⋀n x. x ∈ {a..b} ⟹ norm (gg n x - g x) ≤ inverse (real n + 1)›
using L1_approx_setup[OF ab g'abs g'int] by blast
have bop_absint_cont1: ‹(λx. bop (h x) (k x)) absolutely_integrable_on {a..b}›
if ‹h absolutely_integrable_on {a..b}› ‹continuous_on {a..b} k› for h :: ‹real ⇒ 'a› and k :: ‹real ⇒ 'b›
using continuous_imp_measurable_on_sets_lebesgue[OF that(2) ab_sets]
using compact_imp_bounded[OF compact_continuous_image[OF that(2) compact_Icc]]
using ab_sets absolutely_integrable_bounded_measurable_product bop_swap that(1) by blast
have bop_absint_cont2: ‹(λx. bop (h x) (k x)) absolutely_integrable_on {a..b}›
if ‹continuous_on {a..b} h› ‹k absolutely_integrable_on {a..b}› for h :: ‹real ⇒ 'a› and k :: ‹real ⇒ 'b›
by (simp add: absolutely_integrable_bounded_measurable_product assms(1) compact_continuous_image
compact_imp_bounded continuous_imp_measurable_on_sets_lebesgue that)
define S where ‹S ≡ λn.
(integral {a..b} (λx. bop (ff n x) (gg' n x)) +
integral {a..b} (λx. bop (ff' n x) (gg n x))) -
(bop (ff n b) (gg n b) - bop (ff n a) (gg n a))›
have ‹S n = 0› for n
proof -
have bop_int1: ‹(λx. bop (ff n x) (gg' n x)) integrable_on {a..b}›
using bop_absint_cont2[OF ff_cont gg'_cont_ab[THEN absolutely_integrable_continuous_real]]
set_lebesgue_integral_eq_integral(1) by blast
have ibp: ‹((λx. bop (ff' n x) (gg n x)) has_integral
(bop (ff n b) (gg n b) - bop (ff n a) (gg n a) - integral {a..b} (λx. bop (ff n x) (gg' n x)))) {a..b}›
using integration_by_parts_interior[OF ‹bounded_bilinear bop› ab ff_cont gg_cont ff_deriv gg_deriv]
by (simp add: bop_int1 integrable_integral)
show ?thesis
using integral_unique[OF ibp] by (simp add: S_def algebra_simps)
qed
then have lim_zero: ‹S ⇢ 0›
by (simp add: lim_explicit)
obtain K where ‹K > 0› and K: ‹⋀u v. norm (bop u v) ≤ norm u * norm v * K›
using bounded_bilinear.pos_bounded[OF ‹bounded_bilinear bop›] by blast
have ‹(λn. bop (ff n c) (gg n c)) ⇢ bop (f c) (g c)› if c_ab: ‹c ∈ {a..b}› for c
using ‹bounded_bilinear bop› bounded_bilinear.tendsto c_ab ff_ptwise gg_ptwise by blast
then have *: ‹(λn. bop (ff n b) (gg n b) - bop (ff n a) (gg n a))
⇢ bop (f b) (g b) - bop (f a) (g a)›
by (simp add: ab tendsto_diff)
obtain ff_a: ‹(λn. ff n a) ⇢ f a› and ff_b: ‹(λn. ff n b) ⇢ f b›
by (simp add: ab ff_ptwise)
obtain gg_a: ‹(λn. gg n a) ⇢ g a› and gg_b: ‹(λn. gg n b) ⇢ g b›
by (simp add: ab gg_ptwise)
have bop_b: ‹(λn. bop (ff n b) (gg n b)) ⇢ bop (f b) (g b)›
using Lim_bilinear[OF ff_b gg_b ‹bounded_bilinear bop›] .
have bop_a: ‹(λn. bop (ff n a) (gg n a)) ⇢ bop (f a) (g a)›
using Lim_bilinear[OF ff_a gg_a ‹bounded_bilinear bop›] .
obtain B where ‹B > 0› and B_f': ‹integral {a..b} (λx. norm (f' x)) ≤ B›
and B_g': ‹integral {a..b} (λx. norm (g' x)) ≤ B›
by (smt (verit, best) gt_ex)
obtain M_f where ‹M_f > 0› and M_f: ‹⋀x. x ∈ {a..b} ⟹ norm (f x) ≤ M_f›
using bounded_normE[OF f_bounded] by (metis image_eqI)
obtain M where "M>0" and M: "norm (bop x y) ≤ M * norm x * norm y" for x y
using assms(1) bilinear_bounded_pos by blast
define φ where "φ ≡ λn. 2 * M * B * inverse(real n + 1) + M * inverse(real n + 1)^2"
have int1: ‹(λn. integral {a..b} (λx. bop (ff n x) (gg' n x))) ⇢
integral {a..b} (λx. bop (f x) (g' x))›
proof (rule LIM_zero_iff[THEN iffD1])
have decomp: ‹bop (ff n x) (gg' n x) - bop (f x) (g' x) =
bop (ff n x - f x) (gg' n x - g' x) + bop (ff n x - f x) (g' x) +
bop (f x) (gg' n x - g' x)› for n x
using bounded_bilinear.prod_diff_prod[OF ‹bounded_bilinear bop›] by blast
have fg'_int: ‹(λx. bop (f x) (g' x)) integrable_on {a..b}›
using set_lebesgue_integral_eq_integral(1)
[OF bop_absint_cont2[OF f_cont g'abs]] .
have ffgg'_int: ‹(λx. bop (ff n x) (gg' n x)) integrable_on {a..b}› for n
by (simp add: bop_absint_cont2 ff_cont gg'_absint set_lebesgue_integral_eq_integral(1))
have eq: ‹integral {a..b} (λx. bop (ff n x) (gg' n x)) - integral {a..b} (λx. bop (f x) (g' x))
= integral {a..b} (λx. bop (ff n x) (gg' n x) - bop (f x) (g' x))› for n
by (simp add: Henstock_Kurzweil_Integration.integral_diff ffgg'_int fg'_int)
have t1_int: ‹(λx. bop (ff n x - f x) (gg' n x - g' x)) integrable_on {a..b}› for n
by (metis bop_absint_cont2 continuous_on_diff f_cont ff_cont g'abs gg'_absint set_integral_diff(1)
set_lebesgue_integral_eq_integral(1))
have t2_int: ‹(λx. bop (ff n x - f x) (g' x)) integrable_on {a..b}› for n
using assms by (metis absolutely_integrable_on_def bop_absint_cont2 continuous_on_diff f_cont ff_cont g'abs)
have t3_int: ‹(λx. bop (f x) (gg' n x - g' x)) integrable_on {a..b}› for n
using absolutely_integrable_on_def assms(4) bop_absint_cont2 f_cont gg'_absint by blast
show "(λn. integral {a..b} (λx. bop (ff n x) (gg' n x)) -
integral {a..b} (λx. bop (f x) (g' x))) ⇢ 0"
proof -
have bdd_ff: ‹bdd_above ((λx. norm (ff n x - f x)) ` {a..b})› for n
by (meson bdd_above.I2 ff_inv_bound)
have sup_bound: ‹norm (ff n x - f x) ≤ (SUP x∈{a..b}. norm (ff n x - f x))›
if ‹x ∈ {a..b}› for n x
using cSUP_upper[OF that bdd_ff] .
have I1: ‹(λn. integral {a..b} (λx. bop (ff n x - f x) (gg' n x - g' x))) ⇢ 0›
proof -
have lim_bound: ‹(λn. M * ((SUP x∈{a..b}. norm (ff n x - f x)) *
integral {a..b} (λx. norm (g' x - gg' n x)))) ⇢ 0›
using ff_uniform gg'_L1 tendsto_mult_right_zero tendsto_mult_zero by blast
show ?thesis
proof (rule Lim_null_comparison[OF _ lim_bound])
show ‹∀⇩F n in sequentially. norm (integral {a..b} (λx. bop (ff n x - f x) (gg' n x - g' x)))
≤ M * ((SUP x∈{a..b}. norm (ff n x - f x)) * integral {a..b} (λx. norm (g' x - gg' n x)))›
proof (intro always_eventually allI)
fix n
have ‹norm (integral {a..b} (λx. bop (ff n x - f x) (gg' n x - g' x)))
≤ M * (SUP x∈{a..b}. norm (ff n x - f x)) * integral {a..b} (λx. norm (gg' n x - g' x))›
using bilinear_integral_bound[OF M sup_bound _ t1_int]
norm_gg'_diff_int[of n] ‹M > 0› cSUP_upper[OF _ bdd_ff] ab
by (auto simp: norm_minus_commute intro: order.trans[OF norm_ge_zero])
then show ‹norm (integral {a..b} (λx. bop (ff n x - f x) (gg' n x - g' x))) ≤
M * ((SUP x∈{a..b}. norm (ff n x - f x)) *
integral {a..b} (λx. norm (g' x - gg' n x)))›
by (simp add: norm_minus_commute mult.assoc)
qed
qed
qed
show ?thesis
proof -
have I2: ‹(λn. integral {a..b} (λx. bop (ff n x - f x) (g' x))) ⇢ 0›
proof (rule Lim_null_comparison)
show ‹∀⇩F n in sequentially. norm (integral {a..b} (λx. bop (ff n x - f x) (g' x))) ≤
M * (SUP x∈{a..b}. norm (ff n x - f x)) * integral {a..b} (λx. norm (g' x))›
proof (intro always_eventually allI)
fix n
show ‹norm (integral {a..b} (λx. bop (ff n x - f x) (g' x))) ≤
M * (SUP x∈{a..b}. norm (ff n x - f x)) * integral {a..b} (λx. norm (g' x))›
using bilinear_integral_bound[OF M sup_bound norm_g'_int t2_int]
‹M > 0› cSUP_upper[OF _ bdd_ff] ab by (auto intro: order.trans[OF norm_ge_zero])
qed
next
show ‹(λn. M * (SUP x∈{a..b}. norm (ff n x - f x)) * integral {a..b} (λx. norm (g' x))) ⇢ 0›
using ff_uniform tendsto_mult_left[of _ 0 sequentially M]
using tendsto_mult_left_zero by fastforce
qed
have I3: ‹(λn. integral {a..b} (λx. bop (f x) (gg' n x - g' x))) ⇢ 0›
proof (rule Lim_null_comparison[where g=‹λn. M * M_f * integral {a..b} (λx. norm (g' x - gg' n x))›])
show ‹∀⇩F n in sequentially. norm (integral {a..b} (λx. bop (f x) (gg' n x - g' x))) ≤
M * M_f * integral {a..b} (λx. norm (g' x - gg' n x))›
proof (intro always_eventually allI)
fix n
have ‹norm (integral {a..b} (λx. bop (f x) (gg' n x - g' x)))
≤ M * M_f * integral {a..b} (λx. norm (gg' n x - g' x))›
using bilinear_integral_bound[OF M M_f _ t3_int]
norm_gg'_diff_int[of n] ‹M > 0› ‹M_f > 0›
by (simp add: norm_minus_commute)
then show ‹norm (integral {a..b} (λx. bop (f x) (gg' n x - g' x))) ≤
M * M_f * integral {a..b} (λx. norm (g' x - gg' n x))›
by (simp add: norm_minus_commute)
qed
next
show ‹(λn. M * M_f * integral {a..b} (λx. norm (g' x - gg' n x))) ⇢ 0›
using gg'_L1 tendsto_mult_right_zero by blast
qed
show ?thesis
proof -
have sum_eq: ‹integral {a..b} (λx. bop (ff n x) (gg' n x) - bop (f x) (g' x)) =
integral {a..b} (λx. bop (ff n x - f x) (gg' n x - g' x)) +
integral {a..b} (λx. bop (ff n x - f x) (g' x)) +
integral {a..b} (λx. bop (f x) (gg' n x - g' x))› (is "?L = ?R") for n
proof -
have ‹?L = integral {a..b} (λx. bop (ff n x - f x) (gg' n x - g' x) + bop (ff n x - f x) (g' x) +
bop (f x) (gg' n x - g' x))›
by (simp only: decomp)
also have ‹… = ?R›
by (simp add: Henstock_Kurzweil_Integration.integrable_add
Henstock_Kurzweil_Integration.integral_add t1_int t2_int t3_int)
finally show ?thesis .
qed
then show ?thesis
using I1 I2 I3 add_0 sum_eq by (simp add: eq tendsto_add_zero)
qed
qed
qed
qed
have int2: ‹(λn. integral {a..b} (λx. bop (ff' n x) (gg n x))) ⇢
integral {a..b} (λx. bop (f' x) (g x))›
proof (rule LIM_zero_iff[THEN iffD1, OF Lim_null_comparison])
have fg'_int: ‹(λx. bop (f' x) (g x)) integrable_on {a..b}›
using ‹(λx. bop (f' x) (g x)) absolutely_integrable_on {a..b}›
set_lebesgue_integral_eq_integral(1) by blast
have ffgg'_int: ‹(λx. bop (ff' n x) (gg n x)) integrable_on {a..b}› for n
by (simp add: bop_absint_cont1 ff'_absint gg_cont set_lebesgue_integral_eq_integral(1))
have eq: ‹integral {a..b} (λx. bop (ff' n x) (gg n x)) - integral {a..b} (λx. bop (f' x) (g x))
= integral {a..b} (λx. bop (ff' n x) (gg n x) - bop (f' x) (g x))› for n
by (simp add: Henstock_Kurzweil_Integration.integral_diff ffgg'_int fg'_int)
have g_bound: ‹norm (g x) ≤ B› if ‹x ∈ {a..b}› for x
proof -
have ac_sub: ‹{a..x} ⊆ {a..b}› using that by auto
have ‹norm (g x) = norm (integral {a..x} g')›
using g'int_eq that by presburger
also have ‹… ≤ integral {a..x} (λt. norm (g' t))›
using integral_norm_bound_integral
[OF integrable_on_subinterval[OF g'_int ac_sub]
integrable_on_subinterval[OF norm_g'_int ac_sub]] by simp
also have ‹… ≤ integral {a..b} (λt. norm (g' t))›
using integral_subset_le[OF ac_sub
integrable_on_subinterval[OF norm_g'_int ac_sub] norm_g'_int] by simp
also have ‹… ≤ B› using B_g' .
finally show ?thesis .
qed
have gg_bound: ‹norm (gg n x) ≤ B + inverse (real n + 1)›
if ‹x ∈ {a..b}› for n x
using norm_triangle_sub[of "gg n x" "g x"] g_bound[OF that] gg_inv_bound[OF that, of n]
by linarith
show "∀⇩F n in sequentially.
norm (integral {a..b} (λx. bop (ff' n x) (gg n x)) -
integral {a..b} (λx. bop (f' x) (g x))) ≤ φ n"
proof (rule eventually_sequentiallyI [of 1])
fix n :: nat
assume "1 ≤ n"
have §: ‹bop a b - bop c d = (bop a b - bop c b) + (bop c b - bop c d)› for a b c d
by simp
have f'gg_int: ‹(λx. bop (f' x) (gg n x)) integrable_on {a..b}›
using set_lebesgue_integral_eq_integral(1)[OF bop_absint_cont1[OF assms(3) gg_cont]] .
have split_int: ‹integral {a..b}
(λx. bop (ff' n x) (gg n x) - bop (f' x) (gg n x) +
(bop (f' x) (gg n x) - bop (f' x) (g x))) =
integral {a..b} (λx. bop (ff' n x) (gg n x) - bop (f' x) (gg n x)) +
integral {a..b} (λx. bop (f' x) (gg n x) - bop (f' x) (g x))›
by (intro Henstock_Kurzweil_Integration.integral_add
Henstock_Kurzweil_Integration.integrable_diff ffgg'_int f'gg_int fg'_int)
have "norm (integral {a..b} (λx. bop (ff' n x) (gg n x) - bop (f' x) (g x))) ≤ φ n"
proof -
have M_swap: ‹norm ((λx y. bop y x) u v) ≤ M * norm u * norm v› for u v
using M[of v u] by (simp add: mult.commute mult.left_commute)
have diff_left: ‹bop (ff' n x) (gg n x) - bop (f' x) (gg n x)
= bop (ff' n x - f' x) (gg n x)› for x
using bounded_bilinear.diff_left[OF ‹bounded_bilinear bop›] by simp
have diff_right: ‹bop (f' x) (gg n x) - bop (f' x) (g x) = bop (f' x) (gg n x - g x)› for x
using bounded_bilinear.diff_right[OF ‹bounded_bilinear bop›] by simp
have I1: ‹norm (integral {a..b} (λx. bop (ff' n x) (gg n x) - bop (f' x) (gg n x)))
≤ M * (B + inverse (real n + 1)) * inverse (real n + 1)›
proof -
have int1: ‹(λx. (λu v. bop v u) (gg n x) (ff' n x - f' x)) integrable_on {a..b}›
using Henstock_Kurzweil_Integration.integrable_diff[OF ffgg'_int f'gg_int]
by (simp add: diff_left[symmetric])
have ‹norm (integral {a..b} (λx. bop (ff' n x) (gg n x) - bop (f' x) (gg n x)))
= norm (integral {a..b} (λx. (λu v. bop v u) (gg n x) (ff' n x - f' x)))›
by (simp add: diff_left)
also have ‹… ≤ M * (B + inverse (real n + 1)) * integral {a..b} (λx. norm (ff' n x - f' x))›
using bilinear_integral_bound[OF M_swap gg_bound _ int1] norm_ff'_diff_int[of n]
‹M > 0› ‹B > 0› by (auto simp: norm_minus_commute)
also have ‹… ≤ M * (B + inverse (real n + 1)) * inverse (real n + 1)›
using ff'_approx[of n] ‹M > 0› ‹B > 0›
by (intro mult_left_mono) (auto simp: norm_minus_commute)
finally show ?thesis .
qed
have I2: ‹norm (integral {a..b} (λx. bop (f' x) (gg n x) - bop (f' x) (g x)))
≤ M * B * inverse (real n + 1)›
proof -
have bop_int: ‹(λx. (λu v. bop v u) (gg n x - g x) (f' x)) integrable_on {a..b}›
using Henstock_Kurzweil_Integration.integrable_diff[OF f'gg_int fg'_int]
by (simp add: diff_right)
have ‹norm (integral {a..b} (λx. bop (f' x) (gg n x) - bop (f' x) (g x)))
= norm (integral {a..b} (λx. (λu v. bop v u) (gg n x - g x) (f' x)))›
by (simp add: diff_right)
also have ‹… ≤ M * inverse (real n + 1) * integral {a..b} (λx. norm (f' x))›
using bilinear_integral_bound[OF M_swap gg_inv_bound norm_f'_int bop_int] ‹M > 0›
by auto
also have ‹… ≤ M * inverse (real n + 1) * B›
using B_f' ‹M > 0› by (intro mult_left_mono) auto
also have ‹… = M * B * inverse (real n + 1)›
by (simp add: mult.commute mult.left_commute)
finally show ?thesis .
qed
have step1: ‹integral {a..b} (λx. bop (ff' n x) (gg n x) - bop (f' x) (g x))
= integral {a..b} (λx. bop (ff' n x) (gg n x) - bop (f' x) (gg n x)) +
integral {a..b} (λx. bop (f' x) (gg n x) - bop (f' x) (g x))›
using split_int by auto
have ‹norm (integral {a..b} (λx. bop (ff' n x) (gg n x) - bop (f' x) (g x)))
≤ norm (integral {a..b} (λx. bop (ff' n x) (gg n x) - bop (f' x) (gg n x))) +
norm (integral {a..b} (λx. bop (f' x) (gg n x) - bop (f' x) (g x)))›
by (subst step1, rule norm_triangle_ineq)
also have ‹… ≤ M * (B + inverse (real n + 1)) * inverse (real n + 1) +
M * B * inverse (real n + 1)›
by (intro add_mono I1 I2)
also have ‹… = φ n›
unfolding φ_def by (simp add: algebra_simps power2_eq_square)
finally show ?thesis .
qed
then show "norm (integral {a..b} (λx. bop (ff' n x) (gg n x)) - integral {a..b} (λx. bop (f' x) (g x))) ≤ φ n"
by (simp add: eq)
qed
show "φ ⇢ 0"
unfolding φ_def by real_asymp
qed
then have ‹S ⇢ (integral {a..b} (λx. bop (f x) (g' x)) + integral {a..b} (λx. bop (f' x) (g x)))
- (bop (f b) (g b) - bop (f a) (g a))›
unfolding S_def
using tendsto_diff[OF tendsto_add[OF int1 int2] tendsto_diff[OF bop_b bop_a]]
by blast
then show "integral {a..b} (λx. bop (f x) (g' x)) + integral {a..b} (λx. bop (f' x) (g x))
= bop (f b) (g b) - bop (f a) (g a)"
using lim_zero LIMSEQ_unique eq_iff_diff_eq_0 by blast
qed
text ‹The real-valued specialisation: HOL Light's @{text ABSOLUTE_REAL_INTEGRATION_BY_PARTS}.›
lemma absolute_real_integration_by_parts:
fixes f g f' g' :: "real ⇒ real"
assumes ab: "a ≤ b"
and f'abs: "f' absolutely_integrable_on {a..b}"
and g'abs: "g' absolutely_integrable_on {a..b}"
and f'int: "⋀x. x ∈ {a..b} ⟹ (f' has_integral f x) {a..x}"
and g'int: "⋀x. x ∈ {a..b} ⟹ (g' has_integral g x) {a..x}"
shows fg'_abs: "(λx. f x * g' x) absolutely_integrable_on {a..b}"
and f'g_abs: "(λx. f' x * g x) absolutely_integrable_on {a..b}"
and ibp_eq: "integral {a..b} (λx. f x * g' x) +
integral {a..b} (λx. f' x * g x) = f b * g b - f a * g a"
using absolute_integration_by_parts[OF bilinear_times ab f'abs g'abs f'int g'int]
by auto
lemma absolutely_integrable_bounded_variation_eq:
fixes f :: ‹real ⇒ 'a::euclidean_space›
shows ‹f absolutely_integrable_on (cbox a b) ⟷
f integrable_on (cbox a b) ∧ has_bounded_variation_on (λt. integral (cbox a t) f) (cbox a b)›
proof (cases ‹f integrable_on cbox a b›)
case False
then show ?thesis
by (auto simp: absolutely_integrable_on_def)
next
case fint: True
show ?thesis
proof (intro iffI conjI)
assume abs: ‹f absolutely_integrable_on cbox a b›
from abs show ‹f integrable_on cbox a b›
by (simp add: absolutely_integrable_on_def)
show ‹has_bounded_variation_on (λt. integral (cbox a t) f) (cbox a b)›
unfolding has_bounded_variation_on_def has_bounded_setvariation_on_def
proof (intro exI strip)
fix d T
assume dt: ‹d division_of T ∧ T ⊆ cbox a b›
from abs have nint: ‹(λx. norm (f x)) integrable_on cbox a b›
by (simp add: absolutely_integrable_on_def)
have ‹(∑k∈d. norm (integral (cbox a (Sup k)) f - integral (cbox a (Inf k)) f))
≤ integral (cbox a b) (λx. norm (f x))›
proof -
have div: ‹d division_of T› and sub: ‹T ⊆ cbox a b› using dt by auto
have step1: ‹⋀k. k ∈ d ⟹
integral (cbox a (Sup k)) f - integral (cbox a (Inf k)) f = integral k f›
proof -
fix k assume kd: ‹k ∈ d›
obtain c e where ke: ‹k = cbox c e›
using division_ofD(4)[OF div kd] by auto
have ce: ‹c ≤ e›
using division_ofD(3)[OF div kd] ke
by (simp add: box_real atLeastatMost_empty_iff)
have ksub: ‹k ⊆ cbox a b› using division_ofD(2)[OF div kd] sub by auto
then have ac: ‹a ≤ c› and eb: ‹e ≤ b›
using ke ce by (auto simp: box_real atLeastatMost_subset_iff)
have fint_ae: ‹f integrable_on {a..e}›
using integrable_subinterval_real[OF fint[unfolded box_real]]
ac ce eb by (auto simp: atLeastatMost_subset_iff)
have eq: ‹integral {a..c} f + integral {c..e} f = integral {a..e} f›
using Henstock_Kurzweil_Integration.integral_combine[OF ac ce fint_ae] by simp
have ‹Sup k = e› ‹Inf k = c›
using ke ce by (simp_all add: box_real interval_bounds_real)
then show ‹integral (cbox a (Sup k)) f - integral (cbox a (Inf k)) f = integral k f›
using eq ke by (simp add: box_real algebra_simps)
qed
have step2: ‹⋀k. k ∈ d ⟹ norm (integral k f) ≤ integral k (λx. norm (f x))›
by (smt (verit, ccfv_SIG) integral_norm_bound_integral fint
division_ofD(2,4) dt elementary_interval integrable_on_subdivision nint)
have nf_int_t: ‹(λx. norm (f x)) integrable_on T›
using integrable_on_subdivision[OF div nint sub] .
have ‹(∑k∈d. norm (integral (cbox a (Sup k)) f - integral (cbox a (Inf k)) f))
= (∑k∈d. norm (integral k f))›
by (rule sum.cong[OF refl]) (use step1 in auto)
also have ‹… ≤ (∑k∈d. integral k (λx. norm (f x)))›
by (rule sum_mono) (use step2 in auto)
also have ‹… = integral T (λx. norm (f x))›
using integral_combine_division_topdown[OF nf_int_t div] by simp
also have ‹… ≤ integral (cbox a b) (λx. norm (f x))›
using integral_subset_le[OF sub nf_int_t nint] by auto
finally show ?thesis .
qed
then show ‹(∑k∈d. norm ((λt. integral (cbox a t) f) (Sup k) -
(λt. integral (cbox a t) f) (Inf k))) ≤
integral (cbox a b) (λx. norm (f x))›
by simp
qed
next
assume rhs: ‹f integrable_on cbox a b ∧
has_bounded_variation_on (λt. integral (cbox a t) f) (cbox a b)›
show ‹f absolutely_integrable_on cbox a b›
proof -
from rhs have bv: ‹has_bounded_variation_on (λt. integral (cbox a t) f) (cbox a b)›
by simp
have key: ‹⋀c d. c ≤ d ⟹ {c..d} ⊆ {a..b} ⟹
integral {c..d} f = integral {a..d} f - integral {a..c} f›
proof -
fix c d :: real assume cd: ‹c ≤ d› and sub: ‹{c..d} ⊆ {a..b}›
from sub cd have ac: ‹a ≤ c› and db: ‹d ≤ b›
by auto
have fint_ad: ‹f integrable_on {a..d}›
using integrable_subinterval_real[OF fint[unfolded box_real]] ac cd db
by auto
have eq: ‹integral {a..c} f + integral {c..d} f = integral {a..d} f›
using Henstock_Kurzweil_Integration.integral_combine[OF ac cd fint_ad] by simp
show ‹integral {c..d} f = integral {a..d} f - integral {a..c} f›
using eq by (simp add: algebra_simps)
qed
have integral_eq: ‹integral K f =
integral (cbox a (Sup K)) f - integral (cbox a (Inf K)) f›
if div: ‹d division_of cbox a b› and Kd: ‹K ∈ d› for d K
by (metis Kd atLeastatMost_empty_iff cSup_atLeastAtMost cbox_division_memE cbox_interval
div interval_bounds_real(2) key)
have sum_eq: ‹(∑K∈d. norm (integral K f)) =
(∑K∈d. norm (integral (cbox a (Sup K)) f - integral (cbox a (Inf K)) f))›
if ‹d division_of cbox a b› for d
using integral_eq[OF that] by (intro sum.cong refl) auto
from bv have bvsv: ‹has_bounded_setvariation_on
(λk. integral (cbox a (Sup k)) f - integral (cbox a (Inf k)) f) (cbox a b)›
unfolding has_bounded_variation_on_def .
obtain B where B: ‹⋀d T. d division_of T ⟹ T ⊆ cbox a b ⟹
(∑k∈d. norm (integral (cbox a (Sup k)) f - integral (cbox a (Inf k)) f)) ≤ B›
using bvsv unfolding has_bounded_setvariation_on_def by blast
show ?thesis
using bounded_variation_absolutely_integrable_interval[OF fint] sum_eq
by (metis (lifting) B order.refl)
qed
qed
qed
text ‹If @{term f} is absolutely continuous on $[a,b]$ and has vector derivative $f'(x)$ a.e.,
then @{term f'} is absolutely integrable on $[a,b]$.›
lemma absolutely_integrable_absolutely_continuous_derivative:
fixes f :: ‹real ⇒ 'a::euclidean_space› and f' :: ‹real ⇒ 'a›
assumes ac: ‹absolutely_continuous_on {a..b} f›
and neg: ‹negligible S›
and deriv: ‹⋀x. x ∈ {a..b} - S ⟹ (f has_vector_derivative f' x) (at x within {a..b})›
shows ‹f' absolutely_integrable_on {a..b}›
proof (cases ‹a ≤ b›)
case ab: True
show ?thesis
proof -
have ‹f' integrable_on {a..b} ∧
has_bounded_variation_on (λt. integral {a..t} f') {a..b}›
proof (intro conjI)
show ‹f' integrable_on {a..b}›
using fundamental_theorem_of_calculus_absolutely_continuous [OF neg ab ac deriv]
by (auto simp: integrable_on_def)
next
show ‹has_bounded_variation_on (λt. integral {a..t} f') {a..b}›
proof -
have eq: ‹integral {a..c} f' = f c - f a› if ‹c ∈ {a..b}› for c
proof -
from that have ac_le: ‹a ≤ c› and cb: ‹c ≤ b› by auto
have ‹(f' has_integral (f c - f a)) {a..c}›
proof (rule fundamental_theorem_of_calculus_absolutely_continuous
[OF _ ac_le])
show ‹negligible S› by (rule neg)
show ‹absolutely_continuous_on {a..c} f›
by (rule absolutely_continuous_on_subset[OF ac])
(use cb in auto)
fix x assume ‹x ∈ {a..c} - S›
then have ‹x ∈ {a..b} - S›
using cb by auto
then have ‹(f has_vector_derivative f' x) (at x within {a..b})›
by (rule deriv)
then show ‹(f has_vector_derivative f' x) (at x within {a..c})›
by (rule has_vector_derivative_within_subset) (use cb in auto)
qed
then show ?thesis
by (rule integral_unique)
qed
have ‹absolutely_continuous_on {a..b} (λt. f t - f a)›
by (intro absolutely_continuous_on_sub ac absolutely_continuous_on_const)
then show ?thesis
by (metis (no_types, lifting) absolutely_continuous_on_eq eq
absolutely_continuous_on_imp_has_bounded_variation_on compact_Icc compact_imp_bounded)
qed
qed
then show ?thesis
using box_real absolutely_integrable_bounded_variation_eq by auto
qed
qed auto
lemma absolutely_setcontinuous_indefinite_integral:
fixes f :: ‹real ⇒ 'a::euclidean_space›
assumes ‹f absolutely_integrable_on S› ‹S ∈ lmeasurable›
shows ‹absolutely_setcontinuous_on (λk. integral k f) S›
unfolding absolutely_setcontinuous_on_alt
proof (intro strip)
fix ε :: real
assume "0 < ε"
then obtain δ where "δ>0"
and d: "⋀T. T ⊆ S ⟹ T ∈ lmeasurable ⟹ measure lebesgue T < δ
⟹ norm (integral T f) < ε"
using absolutely_continuous_integral assms(1) by blast
have "norm (∑k∈d. integral k f) < ε"
if "d division_of T" "T ⊆ S" "sum content d < δ" for d T
proof -
have f_int: "f integrable_on T"
using integrable_on_subdivision[OF that(1)] set_lebesgue_integral_eq_integral(1)[OF assms(1)] that(2) by auto
then have eq: "integral T f = (∑k∈d. integral k f)"
using integral_combine_division_topdown[OF _ that(1)] by auto
have meas: "T ∈ lmeasurable"
using lmeasurable_division that(1) by auto
then have "measure lebesgue T < δ"
using that by (metis lebesgue_measure_eq_content)
then show ?thesis
using d[OF that(2) meas] eq by auto
qed
then show "∃δ>0. ∀d T. d division_of T ∧ T ⊆ S ∧ sum content d < δ ⟶ norm (∑k∈d. integral k f) < ε"
using ‹0 < δ› by blast
qed
lemma absolutely_continuous_indefinite_integral_right:
fixes f :: ‹real ⇒ 'a::euclidean_space›
assumes ‹f absolutely_integrable_on {a..b}›
shows ‹absolutely_continuous_on {a..b} (λx. integral {a..x} f)›
proof -
have sc: ‹absolutely_setcontinuous_on (λk. integral k f) {a..b}›
using absolutely_setcontinuous_indefinite_integral assms by blast
have key: ‹integral {a..Sup k} f - integral {a..Inf k} f = integral k f›
if ‹k ∈ d› ‹d division_of T› ‹T ⊆ {a..b}› for k d T
proof -
obtain c e where ke: ‹k = cbox c e› and ‹k ⊆ T›
using division_ofD(4,2) ‹k ∈ d› ‹d division_of T› by meson
have ‹k ≠ {}› using that(1,2) division_ofD(3) by blast
then have ‹c ≤ e› using ke by auto
have ‹c ∈ {a..b}› ‹e ∈ {a..b}›
using ‹k ⊆ T› that(3) ke ‹c ≤ e› by (auto simp add: subset_eq)
then have ‹a ≤ c› ‹a ≤ e› ‹e ≤ b› by auto
have f_int: ‹f integrable_on {a..e}›
using assms absolutely_integrable_on_def integrable_on_subinterval
by (meson ‹a ≤ e› ‹e ≤ b› atLeastatMost_subset_iff order_refl)
have ‹integral {a..e} f - integral {a..c} f
= (if e ≤ c then - integral {e..c} f else integral {c..e} f)›
by (simp add: ‹a ≤ c› ‹a ≤ e› ‹c ≤ e› f_int integral_minus_sets)
then show ?thesis using ke ‹c ≤ e› by auto
qed
show ?thesis
unfolding absolutely_continuous_on_def absolutely_setcontinuous_on_def
proof (intro strip)
fix ε :: real assume ‹0 < ε›
then obtain δ where ‹δ > 0›
and δ: ‹⋀d T. d division_of T ⟹ T ⊆ {a..b} ⟹ sum content d < δ
⟹ (∑k∈d. norm (integral k f)) < ε›
using sc unfolding absolutely_setcontinuous_on_def by meson
show ‹∃δ>0. ∀d T. d division_of T ∧ T ⊆ {a..b} ∧ sum content d < δ ⟶
(∑k∈d. norm (integral {a..Sup k} f - integral {a..Inf k} f)) < ε›
using ‹0 < δ› δ key by auto
qed
qed
lemma absolutely_continuous_indefinite_integral_left:
fixes f :: ‹real ⇒ 'a::euclidean_space›
assumes ‹f absolutely_integrable_on {a..b}›
shows ‹absolutely_continuous_on {a..b} (λx. integral {x..b} f)›
proof (rule absolutely_continuous_on_eq)
show ‹x ∈ {a..b} ⟹ integral {a..b} f - integral {a..x} f = integral {x..b} f› for x
using integral_minus_sets[of a b x f] absolutely_integrable_on_def assms
by (fastforce simp: algebra_simps max_def)
show ‹absolutely_continuous_on {a..b} (λx. integral {a..b} f - integral {a..x} f)›
by (intro absolutely_continuous_on_sub absolutely_continuous_on_const
absolutely_continuous_indefinite_integral_right assms)
qed
theorem has_vector_derivative_indefinite_integral:
fixes f :: ‹real ⇒ 'a::euclidean_space›
assumes ‹f integrable_on {a..b}›
obtains k where ‹negligible k›
‹⋀x. x ∈ {a..b} - k ⟹
((λu. integral {a..u} f) has_vector_derivative f x) (at x within {a..b})›
proof -
have onesided: ‹∃k. negligible k ∧
(∀x∈{u..v} - k. ∀e>0.
∃d>0. ∀x'∈{u..v}.
x < x' ∧ x' < x + d ⟶ norm (integral {x..x'} f - (x' - x) *⇩R f x) / norm (x' - x) < e)›
if ‹f integrable_on {u..v}› for f::"real ⇒ 'a" and u v::real
proof -
define g where ‹g ≡ λx. if x ∈ {u..v} then f x else 0›
have gint: ‹g integrable_on cbox a b› for a b
unfolding g_def using integrable_altD(1) that by blast
show ?thesis
proof (rule integrable_ccontinuous_explicit[OF gint])
fix N :: ‹real set›
assume negN: ‹negligible N›
assume Nprop: ‹⋀x e. x ∉ N ⟹ 0 < e ⟹
∃d>0. ∀h. 0 < h ∧ h < d ⟶ norm (integral (cbox x (x + h *⇩R One)) g /⇩R h ^ DIM(real) - g x) < e›
show ‹∃k. negligible k ∧
(∀x∈{u..v} - k. ∀e>0.
∃d>0. ∀y∈{u..v}.
x < y ∧ y < x + d ⟶ norm (integral {x..y} f - (y - x) *⇩R f x) / norm (y - x) < e)›
proof (intro exI[of _ N] conjI strip)
show ‹negligible N›
by (rule negN)
next
fix x e
assume xmem: ‹x ∈ {u..v} - N› and epos: ‹(0::real) < e›
then have xN: ‹x ∉ N› and xu: ‹u ≤ x› and xv: ‹x ≤ v› by auto
obtain d where dpos: ‹0 < d›
and dprop: ‹⋀h. 0 < h ∧ h < d ⟹
norm (integral (cbox x (x + h *⇩R One)) g /⇩R h ^ DIM(real) - g x) < e›
using Nprop[OF xN epos] by auto
show ‹∃d>0. ∀x'∈{u..v}. x < x' ∧ x' < x + d ⟶
norm (integral {x..x'} f - (x' - x) *⇩R f x) / norm (x' - x) < e›
proof (intro exI[of _ d] conjI ballI impI)
show ‹0 < d› by (rule dpos)
next
fix x'
assume x'mem: ‹x' ∈ {u..v}› and x'bd: ‹x < x' ∧ x' < x + d›
define h where ‹h ≡ x' - x›
have hpos: ‹0 < h› and hd: ‹h < d›
using x'bd unfolding h_def by auto
have x'eq: ‹x' = x + h› unfolding h_def by simp
have sub: ‹{x..x'} ⊆ {u..v}›
using xu xv x'mem by auto
have cbox_eq: ‹cbox x (x + h *⇩R One) = {x..x'}›
by (simp add: x'eq cbox_interval)
have int_if_eq: ‹integral {x..x'} (λt. if t ∈ {u..v} then f t else 0) = integral {x..x'} f›
by (metis (mono_tags) Henstock_Kurzweil_Integration.integral_restrict_Int Int_absorb1 sub)
have int_eq: ‹integral {x..x + h} g = integral {x..x + h} f›
unfolding g_def
using int_if_eq x'eq by simp
have gx_eq: ‹g x = f x›
unfolding g_def using xu xv by simp
have ‹norm (integral (cbox x (x + h *⇩R One)) g /⇩R h ^ DIM(real) - g x) < e›
by (rule dprop) (use hpos hd in auto)
then have ‹norm (integral {x..x'} f /⇩R h - f x) < e›
by (simp add: cbox_eq int_eq gx_eq x'eq)
moreover have ‹norm (integral {x..x'} f - (x' - x) *⇩R f x) / norm (x' - x) =
norm (integral {x..x'} f /⇩R h - f x)›
by (smt (verit, best) mult.commute scale_right_diff_distrib divideR_right divide_inverse h_def
hpos norm_inverse norm_scaleR real_norm_def)
ultimately show ‹norm (integral {x..x'} f - (x' - x) *⇩R f x) / norm (x' - x) < e›
by simp
qed
qed
qed
qed
obtain K1 where ‹negligible K1› and K1:
‹⋀x e. ⟦x ∈ {a..b} - K1; 0 < e⟧ ⟹
∃d>0. ∀x'∈{a..b}. x < x' ∧ x' < x + d ⟶
norm (integral {x..x'} f - (x' - x) *⇩R f x) / norm (x' - x) < e›
using onesided [OF assms] by auto
have ‹((λx. f (- x)) integrable_on {- b..- a})›
by (simp add: assms)
then obtain K2 where ‹negligible K2› and K2:
‹⋀x e. ⟦x ∈ {-b..-a} - K2; 0 < e⟧ ⟹
∃d>0. ∀x'∈{-b..-a}. x < x' ∧ x' < x + d ⟶
norm (integral {x..x'} (λx. f (-x)) - (x' - x) *⇩R f (-x)) / norm (x' - x) < e›
using onesided by metis
define K where "K ≡ K1 ∪ uminus ` K2"
show ?thesis
proof
show "negligible K"
by (simp add: K_def ‹negligible K1› ‹negligible K2› module_hom_uminus negligible_linear_image)
next
fix x :: real
assume x: "x ∈ {a..b} - K"
have "bounded_linear (λu. u *⇩R f x)"
by (simp add: bounded_linear_scaleR_left)
moreover have "∃d>0. ∀y∈{a..b}. ¦y - x¦ < d ⟶ norm (integral {a..y} f - integral {a..x} f - (y - x) *⇩R f x) ≤ e * ¦y - x¦"
if "0 < e"
for e :: real
proof -
have xK1: ‹x ∈ {a..b} - K1› and xK2: ‹-x ∈ {-b..-a} - K2›
using x by (auto simp: K_def image_iff)
obtain d1 where ‹d1 > 0› and d1:
‹⋀x'. ⟦x' ∈ {a..b}; x < x'; x' < x + d1⟧
⟹ norm (integral {x..x'} f - (x' - x) *⇩R f x) / norm (x' - x) < e›
using K1 [OF xK1 ‹0 < e›] x by metis
obtain d2 where ‹d2 > 0› and d2:
‹⋀x'. ⟦x' ∈ {-b..-a}; -x < x'; x' < -x + d2⟧
⟹ norm (integral {-x..x'} (λx. f (-x)) - (x'+x) *⇩R f x) / norm (x' + x) < e›
using K2[OF xK2 ‹0 < e›] xK2 by force
have d2': ‹norm (integral {y'..x} f - (x - y') *⇩R f x) / ¦x - y'¦ < e›
if ‹y' ∈ {a..b}› ‹y' < x› ‹x - y' < d2› for y'
using d2[of ‹-y'›] that by (simp add: integral_reflect_real real_norm_def)
show ?thesis
proof (intro exI conjI strip)
show "0 < min d1 d2"
by (simp add: ‹0 < d1› ‹0 < d2›)
next
fix y :: real
assume "y ∈ {a..b}" and y: "¦y - x¦ < min d1 d2"
have step: ‹norm (integral {a..y} f - integral {a..x} f - (y - x) *⇩R f x) ≤ e * ¦y - x¦›
if local_bound: ‹norm (integral {p..q} f - (q - p) *⇩R f x) / (q - p) < e›
and ord: ‹a ≤ p› ‹p < q› ‹q ≤ b›
and pq_eq: ‹{p..q} = {min x y..max x y}›
for p q
proof -
have fint: ‹f integrable_on {a..q}›
using integrable_on_subinterval[OF assms] ord by auto
have ‹integral {a..p} f + integral {p..q} f = integral {a..q} f›
by (rule Henstock_Kurzweil_Integration.integral_combine) (use ord fint in linarith)+
then have ‹norm (integral {a..y} f - integral {a..x} f - (y - x) *⇩R f x)
= norm (integral {p..q} f - (q - p) *⇩R f x)›
by (smt (verit, best) add_diff_cancel_left' add_uminus_conv_diff interval_bounds_real minus_diff_eq
norm_uminus_minus ord(2) pq_eq scale_minus_left)
also have ‹… < e * (q - p)›
using local_bound ord by (simp add: divide_simps)
also have ‹… = e * ¦y - x¦›
using pq_eq ord by (auto simp: min_def max_def split: if_splits)
finally show ?thesis by simp
qed
show "norm (integral {a..y} f - integral {a..x} f - (y - x) *⇩R f x) ≤ e * ¦y - x¦"
proof (cases ‹x = y›)
case True then show ?thesis by simp
next
case False
define p q where ‹p ≡ min x y› and ‹q ≡ max x y›
have pq: ‹p < q› ‹{p..q} = {min x y..max x y}›
using False by (auto simp: p_def q_def)
have ord: ‹a ≤ p› ‹q ≤ b›
using x ‹y ∈ {a..b}› by (auto simp: p_def q_def K_def)
have bd: ‹norm (integral {p..q} f - (q - p) *⇩R f x) / (q - p) < e›
proof (cases ‹x < y›)
case True
then show ?thesis
using d1[of y] ‹y ∈ {a..b}› y by (auto simp: p_def q_def real_norm_def)
next
case False
then show ?thesis
using ‹x ≠ y› d2'[of y] ‹y ∈ {a..b}› y by (auto simp: p_def q_def real_norm_def)
qed
then show ?thesis
using step[of p q] pq ord by auto
qed
qed
qed
ultimately show "((λu. integral {a..u} f) has_vector_derivative f x) (at x within {a..b})"
unfolding has_vector_derivative_def has_derivative_within_alt2
unfolding eventually_at_filter eventually_nhds_metric
by (force simp: dist_real_def)
qed
qed
lemma absolute_integral_absolutely_continuous_derivative_eq:
fixes f :: ‹real ⇒ 'a::euclidean_space› and f' :: ‹real ⇒ 'a›
shows ‹(f' absolutely_integrable_on {a..b} ∧
(∀x ∈ {a..b}. (f' has_integral (f x - f a)) {a..x}))
⟷ (absolutely_continuous_on {a..b} f ∧
(∃S. negligible S ∧
(∀x ∈ {a..b} - S. (f has_vector_derivative f' x) (at x within {a..b}))))›
(is ‹?L ⟷ ?R›)
proof
assume L: ?L
have f'abs: ‹f' absolutely_integrable_on {a..b}› and
f'int: ‹⋀c. c ∈ {a..b} ⟹ (f' has_integral (f c - f a)) {a..c}›
using L by auto
have feq: ‹f a + integral {a..c} f' = f c› if ‹c ∈ {a..b}› for c
using integral_unique[OF f'int[OF that]] by simp
obtain S where negs: ‹negligible S› and
ideriv: ‹⋀x. x ∈ {a..b} - S ⟹ ((λu. integral {a..u} f') has_vector_derivative f' x) (at x within {a..b})›
using has_vector_derivative_indefinite_integral[of f' a b] f'abs
by (auto simp: absolutely_integrable_on_def)
show ?R
proof (intro conjI)
show ‹absolutely_continuous_on {a..b} f›
proof (rule absolutely_continuous_on_eq)
show ‹absolutely_continuous_on {a..b} (λx. f a + integral {a..x} f')›
using absolutely_continuous_indefinite_integral_right
using absolutely_continuous_on_add absolutely_continuous_on_const f'abs by blast
show ‹⋀x. x ∈ {a..b} ⟹ f a + integral {a..x} f' = f x›
using feq by blast
qed
next
show ‹∃S. negligible S ∧
(∀x ∈ {a..b} - S. (f has_vector_derivative f' x) (at x within {a..b}))›
proof (intro exI conjI ballI)
show ‹negligible S› by (rule negs)
next
fix x assume xmem: ‹x ∈ {a..b} - S›
have ‹((λu. integral {a..u} f') has_vector_derivative f' x) (at x within {a..b})›
using ideriv[OF xmem] .
then have ‹((λu. f a + integral {a..u} f') has_vector_derivative 0 + f' x) (at x within {a..b})›
by (intro has_vector_derivative_add has_vector_derivative_const)
then have ‹((λu. f a + integral {a..u} f') has_vector_derivative f' x) (at x within {a..b})›
by simp
then show ‹(f has_vector_derivative f' x) (at x within {a..b})›
by (metis (no_types, lifting) Diff_iff feq has_vector_derivative_transform xmem)
qed
qed
next
assume R: ?R
then obtain S where ac: ‹absolutely_continuous_on {a..b} f› and negs: ‹negligible S› and
deriv: ‹⋀x. x ∈ {a..b} - S ⟹ (f has_vector_derivative f' x) (at x within {a..b})›
by auto
show ?L
proof (intro conjI ballI)
show ‹f' absolutely_integrable_on {a..b}›
by (rule absolutely_integrable_absolutely_continuous_derivative[OF ac negs deriv])
next
fix c assume cmem: ‹c ∈ {a..b}›
then have ac_le: ‹a ≤ c› and cb: ‹c ≤ b› by auto
show ‹(f' has_integral (f c - f a)) {a..c}›
proof (rule fundamental_theorem_of_calculus_absolutely_continuous[OF negs ac_le])
show ‹absolutely_continuous_on {a..c} f›
by (rule absolutely_continuous_on_subset[OF ac]) (use cb in auto)
next
fix x assume ‹x ∈ {a..c} - S›
then have ‹x ∈ {a..b} - S›
using cb by auto
then have ‹(f has_vector_derivative f' x) (at x within {a..b})›
by (rule deriv)
then show ‹(f has_vector_derivative f' x) (at x within {a..c})›
by (rule has_vector_derivative_within_subset) (use cb in auto)
qed
qed
qed
text ‹Existential version: @{term f'} is absolutely integrable iff there exists an
absolutely continuous antiderivative.›
lemma absolutely_integrable_absolutely_continuous_derivative_eq:
fixes f' :: ‹real ⇒ 'a::euclidean_space›
shows ‹f' absolutely_integrable_on {a..b} ⟷
(∃f S. absolutely_continuous_on {a..b} f ∧
negligible S ∧ (∀x ∈ {a..b} - S. (f has_vector_derivative f' x) (at x within {a..b})))›
(is ‹?L ⟷ ?R›)
proof
assume L: ?L
define f where ‹f ≡ λt. integral {a..t} f'›
have f'int: ‹f' integrable_on {a..b}›
using L set_lebesgue_integral_eq_integral by blast
have f_a: ‹f a = 0›
unfolding f_def by (simp add: integral_singleton)
have hi: ‹(f' has_integral (f x - f a)) {a..x}› if ‹x ∈ {a..b}› for x
using f'int f_def integrable_on_subinterval that by fastforce
have ‹f' absolutely_integrable_on {a..b} ∧
(∀x ∈ {a..b}. (f' has_integral (f x - f a)) {a..x})›
using L hi by auto
then show ?R
by (metis absolute_integral_absolutely_continuous_derivative_eq)
next
assume ?R then show ?L
using absolutely_integrable_absolutely_continuous_derivative by blast
qed
lemma absolute_integral_absolutely_continuous_derivative_eq_alt:
fixes f :: ‹real ⇒ 'a::euclidean_space› and f' :: ‹real ⇒ 'a›
shows ‹(f' absolutely_integrable_on {a..b} ∧
(∀x ∈ {a..b}. (f' has_integral (f x - f a)) {a..x}))
⟷ (absolutely_continuous_on {a..b} f ∧
(∃S. negligible S ∧ (∀x ∈ {a..b} - S. (f has_vector_derivative f' x) (at x))))›
(is ‹?L ⟷ ?R›)
proof -
have base: ‹?L ⟷ (absolutely_continuous_on {a..b} f ∧
(∃S. negligible S ∧ (∀x ∈ {a..b} - S. (f has_vector_derivative f' x) (at x within {a..b}))))›
(is ‹_ ⟷ ?M›)
by (rule absolute_integral_absolutely_continuous_derivative_eq)
also have ‹?M ⟷ ?R›
proof (intro conj_cong refl iffI)
assume ‹∃S. negligible S ∧ (∀x ∈ {a..b} - S. (f has_vector_derivative f' x) (at x within {a..b}))›
then obtain S where negs: ‹negligible S› and
deriv: ‹⋀x. x ∈ {a..b} - S ⟹
(f has_vector_derivative f' x) (at x within {a..b})›
by auto
show ‹∃S. negligible S ∧ (∀x ∈ {a..b} - S. (f has_vector_derivative f' x) (at x))›
proof (intro exI conjI ballI)
show ‹negligible ({a, b} ∪ S)›
using negs by (simp add: negligible_insert)
next
fix x assume xmem: ‹x ∈ {a..b} - ({a, b} ∪ S)›
then show ‹(f has_vector_derivative f' x) (at x)›
by (metis Diff_iff Diff_insert UnCI atLeastAtMost_iff atLeastAtMost_singleton at_within_Icc_at deriv leI)
qed
next
assume ‹∃S. negligible S ∧ (∀x ∈ {a..b} - S. (f has_vector_derivative f' x) (at x))›
then show ‹∃S. negligible S ∧ (∀x ∈ {a..b} - S. (f has_vector_derivative f' x) (at x within {a..b}))›
by (meson has_vector_derivative_at_within)
qed
finally show ?thesis .
qed
text ‹Integration by parts for absolutely integrable functions (shifted / sum version).
Bilinear generalisation: HOL Light's @{text ABSOLUTE_INTEGRATION_BY_PARTS_SUM}.›
theorem absolute_integration_by_parts_sum:
fixes bop :: ‹'a::euclidean_space ⇒ 'b::euclidean_space ⇒ 'c::euclidean_space›
and f :: ‹real ⇒ 'a› and g :: ‹real ⇒ 'b›
and f' :: ‹real ⇒ 'a› and g' :: ‹real ⇒ 'b›
and a b :: real
assumes bop: ‹bilinear bop›
and ab: ‹a ≤ b›
and f'abs: ‹f' absolutely_integrable_on {a..b}›
and g'abs: ‹g' absolutely_integrable_on {a..b}›
and f'int: ‹⋀x. x ∈ {a..b} ⟹ (f' has_integral (f x - f a)) {a..x}›
and g'int: ‹⋀x. x ∈ {a..b} ⟹ (g' has_integral (g x - g a)) {a..x}›
shows ‹(λx. bop (f x) (g' x) + bop (f' x) (g x)) absolutely_integrable_on {a..b}›
and ‹⋀x. x ∈ {a..b} ⟹
((λx. bop (f x) (g' x) + bop (f' x) (g x))
has_integral (bop (f x) (g x) - bop (f a) (g a))) {a..x}›
proof -
have bb: ‹bounded_bilinear bop›
using bop bilinear_conv_bounded_bilinear by blast
have fL: ‹absolutely_continuous_on {a..b} f ∧
(∃S. negligible S ∧ (∀x ∈ {a..b} - S. (f has_vector_derivative f' x) (at x within {a..b})))›
by (subst absolute_integral_absolutely_continuous_derivative_eq[symmetric])
(use f'abs f'int in auto)
have gL: ‹absolutely_continuous_on {a..b} g ∧
(∃S. negligible S ∧ (∀x ∈ {a..b} - S. (g has_vector_derivative g' x) (at x within {a..b})))›
by (subst absolute_integral_absolutely_continuous_derivative_eq[symmetric])
(use g'abs g'int in auto)
obtain S where f_ac: ‹absolutely_continuous_on {a..b} f› and negs: ‹negligible S›
and f_deriv: ‹⋀x. x ∈ {a..b} - S ⟹ (f has_vector_derivative f' x) (at x within {a..b})›
using fL by auto
obtain T where g_ac: ‹absolutely_continuous_on {a..b} g› and negt: ‹negligible T›
and g_deriv: ‹⋀x. x ∈ {a..b} - T ⟹ (g has_vector_derivative g' x) (at x within {a..b})›
using gL by auto
have fg_ac: ‹absolutely_continuous_on {a..b} (λx. bop (f x) (g x))›
by (rule absolutely_continuous_on_bilinear[OF bop f_ac g_ac is_interval_cc
compact_imp_bounded[OF compact_Icc]])
have neg_st: ‹negligible (S ∪ T)›
using negs negt negligible_Un by blast
have fg_deriv: ‹((λx. bop (f x) (g x)) has_vector_derivative bop (f x) (g' x) + bop (f' x) (g x)) (at x within {a..b})›
if ‹x ∈ {a..b} - (S ∪ T)› for x
proof -
have ‹x ∈ {a..b} - S› ‹x ∈ {a..b} - T› using that by auto
then show ?thesis
using bounded_bilinear.has_vector_derivative[OF bb f_deriv g_deriv] by blast
qed
have main: ‹(λx. bop (f x) (g' x) + bop (f' x) (g x)) absolutely_integrable_on {a..b} ∧
(∀x ∈ {a..b}. ((λx. bop (f x) (g' x) + bop (f' x) (g x))
has_integral ((λx. bop (f x) (g x)) x - (λx. bop (f x) (g x)) a)) {a..x})›
by (subst absolute_integral_absolutely_continuous_derivative_eq)
(use fg_ac neg_st fg_deriv in ‹blast+›)
show ‹(λx. bop (f x) (g' x) + bop (f' x) (g x)) absolutely_integrable_on {a..b}›
using main by blast
show ‹((λx. bop (f x) (g' x) + bop (f' x) (g x))
has_integral (bop (f x) (g x) - bop (f a) (g a))) {a..x}›
if ‹x ∈ {a..b}› for x
using main that by auto
qed
text ‹Helper: the indefinite integral of an absolutely integrable function
is absolutely continuous.›
lemmas indefinite_integral_absolutely_continuous = absolutely_continuous_indefinite_integral_right
text ‹The real-valued shifted version›
lemma absolute_real_integration_by_parts_sum:
fixes f g f' g' :: "real ⇒ real"
assumes ab: "a ≤ b"
and f'abs: "f' absolutely_integrable_on {a..b}"
and g'abs: "g' absolutely_integrable_on {a..b}"
and f'int: "⋀x. x ∈ {a..b} ⟹ (f' has_integral (f x - f a)) {a..x}"
and g'int: "⋀x. x ∈ {a..b} ⟹ (g' has_integral (g x - g a)) {a..x}"
shows fgsum_abs: "(λx. f x * g' x + f' x * g x) absolutely_integrable_on {a..b}"
and fgsum_int: "⋀x. x ∈ {a..b} ⟹
((λx. f x * g' x + f' x * g x) has_integral (f x * g x - f a * g a)) {a..x}"
proof -
define F where "F ≡ λx. f x - f a"
define G where "G ≡ λx. g x - g a"
have F_int: "⋀x. x ∈ {a..b} ⟹ (f' has_integral F x) {a..x}"
unfolding F_def using f'int by simp
have G_int: "⋀x. x ∈ {a..b} ⟹ (g' has_integral G x) {a..x}"
unfolding G_def using g'int by simp
note ibp = absolute_real_integration_by_parts[OF ab f'abs g'abs F_int G_int]
have Fg'_abs: "(λx. F x * g' x) absolutely_integrable_on {a..b}" using ibp(1) .
have f'G_abs: "(λx. f' x * G x) absolutely_integrable_on {a..b}" using ibp(2) .
have ibp_eq: "integral {a..b} (λx. F x * g' x) + integral {a..b} (λx. f' x * G x) = F b * G b - F a * G a"
using ibp(3) .
have cg'_abs: "(λx. f a * g' x) absolutely_integrable_on {a..b}"
using absolutely_integrable_scaleR_left[OF g'abs, of "f a"]
by (simp add: scaleR_conv_of_real)
have f'c_abs: "(λx. f' x * g a) absolutely_integrable_on {a..b}"
using absolutely_integrable_scaleR_right[OF f'abs, of "g a"]
by (simp add: scaleR_conv_of_real)
have Fg'_int: "(λx. F x * g' x) integrable_on {a..b}"
using Fg'_abs set_lebesgue_integral_eq_integral by blast
have f'G_int: "(λx. f' x * G x) integrable_on {a..b}"
using f'G_abs set_lebesgue_integral_eq_integral by blast
have cg'_int: "(λx. f a * g' x) integrable_on {a..b}"
using cg'_abs set_lebesgue_integral_eq_integral by blast
have f'c_int: "(λx. f' x * g a) integrable_on {a..b}"
using f'c_abs set_lebesgue_integral_eq_integral by blast
have Fg'_norm: "(λx. norm (F x * g' x)) integrable_on {a..b}"
using Fg'_abs absolutely_integrable_on_def by metis
have f'G_norm: "(λx. norm (f' x * G x)) integrable_on {a..b}"
using f'G_abs absolutely_integrable_on_def by metis
have cg'_norm: "(λx. norm (f a * g' x)) integrable_on {a..b}"
using cg'_abs absolutely_integrable_on_def by metis
have f'c_norm: "(λx. norm (f' x * g a)) integrable_on {a..b}"
using f'c_abs absolutely_integrable_on_def by metis
have decomp: "⋀x. f x * g' x + f' x * g x = F x * g' x + f a * g' x + (f' x * G x + f' x * g a)"
unfolding F_def G_def by (simp add: algebra_simps)
have sum_int: "(λx. f x * g' x + f' x * g x) integrable_on {a..b}"
unfolding decomp using integrable_add[OF integrable_add[OF Fg'_int cg'_int] integrable_add[OF f'G_int f'c_int]] .
have bound_int: "(λx. norm (F x * g' x) + norm (f a * g' x) + (norm (f' x * G x) + norm (f' x * g a))) integrable_on {a..b}"
using integrable_add[OF integrable_add[OF Fg'_norm cg'_norm] integrable_add[OF f'G_norm f'c_norm]] .
have norm_bound: "⋀x. x ∈ {a..b} ⟹ norm (f x * g' x + f' x * g x) ≤
norm (F x * g' x) + norm (f a * g' x) + (norm (f' x * G x) + norm (f' x * g a))"
unfolding decomp by (intro order_trans[OF norm_triangle_ineq] add_mono order_trans[OF norm_triangle_ineq] order_refl)+
show fgsum_abs: "(λx. f x * g' x + f' x * g x) absolutely_integrable_on {a..b}"
by (rule absolutely_integrable_integrable_bound[OF norm_bound sum_int bound_int])
show "⋀x. x ∈ {a..b} ⟹
((λx. f x * g' x + f' x * g x) has_integral (f x * g x - f a * g a)) {a..x}"
proof -
fix x assume xab: "x ∈ {a..b}"
hence ax: "a ≤ x" and xb: "x ≤ b" by auto
have sub: "{a..x} ⊆ {a..b}" using xb by auto
have f'abs_sub: "f' absolutely_integrable_on {a..x}"
using absolutely_integrable_on_subinterval[OF f'abs sub] .
have g'abs_sub: "g' absolutely_integrable_on {a..x}"
using absolutely_integrable_on_subinterval[OF g'abs sub] .
have F_int_sub: "⋀y. y ∈ {a..x} ⟹ (f' has_integral F y) {a..y}"
using F_int sub by auto
have G_int_sub: "⋀y. y ∈ {a..x} ⟹ (g' has_integral G y) {a..y}"
using G_int sub by auto
note ibp_sub = absolute_real_integration_by_parts[OF ax f'abs_sub g'abs_sub F_int_sub G_int_sub]
have Fg'_int_sub: "(λt. F t * g' t) integrable_on {a..x}"
using ibp_sub(1) set_lebesgue_integral_eq_integral by blast
have f'G_int_sub: "(λt. f' t * G t) integrable_on {a..x}"
using ibp_sub(2) set_lebesgue_integral_eq_integral by blast
have ibp_eq_sub: "integral {a..x} (λt. F t * g' t) + integral {a..x} (λt. f' t * G t) = F x * G x - F a * G a"
using ibp_sub(3) .
have Fa: "F a = 0" unfolding F_def by simp
have Ga: "G a = 0" unfolding G_def by simp
have hi_FG: "((λt. F t * g' t + f' t * G t) has_integral (F x * G x)) {a..x}"
using has_integral_add[OF integrable_integral[OF Fg'_int_sub] integrable_integral[OF f'G_int_sub]]
ibp_eq_sub Fa Ga by simp
have hi_cg: "((λt. f a * g' t) has_integral (f a * (g x - g a))) {a..x}"
using has_integral_mult_right[OF g'int[OF xab]] unfolding G_def by simp
have hi_fc: "((λt. f' t * g a) has_integral ((f x - f a) * g a)) {a..x}"
using has_integral_mult_left[OF f'int[OF xab]] unfolding F_def by simp
have hi_const: "((λt. f a * g' t + f' t * g a) has_integral (f a * (g x - g a) + (f x - f a) * g a)) {a..x}"
using has_integral_add[OF hi_cg hi_fc] .
have hi_sum: "((λt. (F t * g' t + f' t * G t) + (f a * g' t + f' t * g a))
has_integral (F x * G x + (f a * (g x - g a) + (f x - f a) * g a))) {a..x}"
using has_integral_add[OF hi_FG hi_const] .
have eq_fn: "⋀T. (F T * g' T + f' T * G T) + (f a * g' T + f' T * g a) = f T * g' T + f' T * g T"
unfolding F_def G_def by (simp add: algebra_simps)
have eq_val: "F x * G x + (f a * (g x - g a) + (f x - f a) * g a) = f x * g x - f a * g a"
unfolding F_def G_def by (simp add: algebra_simps)
show "((λx. f x * g' x + f' x * g x) has_integral (f x * g x - f a * g a)) {a..x}"
using hi_sum unfolding eq_fn eq_val .
qed
qed
end