Theory HOL-Analysis.Lebesgue_Differentiation
theory Lebesgue_Differentiation
imports Equivalence_Measurable_On_Borel Bounded_Variation Weierstrass_Theorems
begin
lemma Lebesgue_diff_aux1:
fixes f :: "real ⇒ 'a::euclidean_space" and a b :: real
assumes "has_bounded_variation_on f {a..b}"
shows "∃t. negligible t ∧
(∀x ∈ {a..b} - t.
∃B>0. eventually (λy. norm (f y - f x) ≤ B * norm (y-x)) (at x))"
proof -
define t where "t = {x ∈ {a<..<b}. isCont f x ∧
¬ (∃B>0. eventually (λy. norm (f y - f x) ≤ B * norm (y-x)) (at x))}"
obtain B where B: "⋀d T. ⟦d division_of T; T ⊆ {a..b}⟧ ⟹
(∑k∈d. norm (f (Sup k) - f (Inf k))) ≤ B"
using assms unfolding has_bounded_variation_on_def has_bounded_setvariation_on_def
by blast
obtain T where tn: "negligible T" and
tc: "⋀x. x ∈ {a..b} - T ⟹ isCont f x ⟹
∃B>0. eventually (λy. norm (f y - f x) ≤ B * norm (y-x)) (at x)"
proof
show "negligible ({a, b} ∪ t)"
proof (rule negligible_Un)
show "negligible t"
unfolding negligible_outer_le
proof (intro strip)
fix ε :: real
assume "0 < ε"
define M where "M = 3 * (¦B¦ + 1) / ε"
have "0 < M"
unfolding M_def using ‹0 < ε› by (auto intro: divide_pos_pos)
have interval_witness:
"∃u v. u ∈ {a..b} ∧ v ∈ {a..b} ∧ x ∈ {u<..<v} ∧
M * ¦v - u¦ ≤ norm (f u - f v)" if "x ∈ t" for x
proof -
from that have xab: "x ∈ {a<..<b}" and xcont: "isCont f x"
and xnlip: "¬ (∃B>0. eventually (λy. norm (f y - f x) ≤ B * norm (y-x)) (at x))"
unfolding t_def by auto
from xab obtain d where "d > 0" and dsub: "⋀x'. ¦x' - x¦ < d ⟹ x' ∈ {a<..<b}"
by (meson open_greaterThanLessThan open_real)
have False if "d > 0"
and hd: "⋀y. 0 < dist y x ⟹ dist y x < d ⟹ norm (f y - f x) ≤ (3*M) * norm (y-x)" for d
proof -
have "eventually (λy. norm (f y - f x) ≤ (3*M) * norm (y-x)) (at x)"
unfolding eventually_at using ‹d > 0› hd by auto
then show False using xnlip ‹M>0› by auto
qed
then obtain y where yx: "0 < dist y x" "dist y x < d"
and ylip: "(3*M) * norm (y-x) < norm (f y - f x)"
by (meson ‹0 < d› not_le)
have yab: "y ∈ {a<..<b}"
using dsub yx(2) by (auto simp: dist_real_def)
have xab': "x ∈ {a..b}" and yab': "y ∈ {a..b}"
using xab yab by auto
define δ where "δ = ¦y - x¦"
have "δ > 0" unfolding δ_def using yx by (auto simp: dist_real_def)
have Mδ: "M * δ > 0" using ‹0 < M› ‹δ > 0› by auto
have ylip': "3 * M * δ < norm (f y - f x)"
using ylip unfolding δ_def by (simp add: real_norm_def)
from xcont have "(f ⤏ f x) (at x)" by (simp add: isCont_def)
from tendstoD[OF this Mδ]
obtain d' where "d' > 0" and
hd': "⋀z. z ≠ x ⟹ dist z x < d' ⟹ dist (f z) (f x) < M * δ"
unfolding eventually_at by auto
define z where "z = (if x < y then x - min δ (min d d') / 2
else x + min δ (min d d') / 2)"
have zx: "z ≠ x"
unfolding z_def using ‹d > 0› ‹d' > 0› ‹δ > 0› by (auto simp: min_def)
have dist_zx: "dist z x < min δ (min d d')"
unfolding z_def δ_def dist_real_def
using yx ‹d > 0› ‹d' > 0› by force
have xbetween: "x ∈ {min y z <..< max y z}"
unfolding z_def using yx ‹d > 0› ‹d' > 0› ‹δ > 0›
by (simp add: δ_def dist_real_def min_def max_def field_simps split: if_split_asm)
have zab: "z ∈ {a<..<b}"
using dist_real_def dist_zx dsub by force
have zab': "z ∈ {a..b}" using zab by auto
have fz_bound: "norm (f z - f x) < M * δ"
by (metis dist_norm dist_zx hd' min_less_iff_conj zx)
have gap_bound: "¦max y z - min y z¦ < 2 * δ"
by (smt (verit) δ_def dist_real_def dist_zx)
have key: "norm (f z - f y) > 2 * M * δ"
using norm_triangle_ineq[of "f y - f z" "f z - f x"] ylip' fz_bound
by (simp add: norm_minus_commute)
have "M * ¦max y z - min y z¦ < norm (f (min y z) - f (max y z))"
proof -
have "M * ¦max y z - min y z¦ < M * (2 * δ)"
using gap_bound ‹0 < M› by auto
also have "… < norm (f (min y z) - f (max y z))"
using key by (simp add: min_def norm_minus_commute)
finally show ?thesis .
qed
then show ?thesis
using zab' yab' xbetween
by (intro exI[of _ "min y z"] exI[of _ "max y z"]) auto
qed
then obtain u v where uv: "⋀x. x ∈ t ⟹ u x ∈ {a..b} ∧ v x ∈ {a..b} ∧ x ∈ {u x <..< v x}
∧ M * ¦v x - u x¦ ≤ norm (f (u x) - f (v x))"
by metis
let ?UVT = "(λx. box (u x) (v x)) ` t"
obtain ℱ where "ℱ ⊆ ?UVT" "countable ℱ" "⋃ℱ = ⋃?UVT"
by (smt (verit, best) Lindelof imageE open_box)
then obtain c where "countable c" and "c ⊆ t"
and c: "⋃((λx. box (u x) (v x)) ` c) = ⋃ ?UVT"
by (metis (lifting) countable_subset_image)
show "∃T. t ⊆ T ∧ T ∈ lmeasurable ∧ Sigma_Algebra.measure lebesgue T ≤ ε"
proof (rule ccontr)
assume non: "∄T. t ⊆ T ∧ T ∈ lmeasurable ∧ Sigma_Algebra.measure lebesgue T ≤ ε"
let ?𝒞 = "(λx. cbox (u x) (v x)) ` c"
have cnt: "countable ?𝒞"
using ‹countable c› by auto
have meas: "⋀D. D ∈ ?𝒞 ⟹ D ∈ lmeasurable"
by auto
have tsub: "t ⊆ ⋃?𝒞"
proof
fix x assume "x ∈ t"
then obtain z where "z ∈ c" "x ∈ box (u z) (v z)"
using c uv by fastforce
then show "x ∈ ⋃?𝒞"
using box_subset_cbox by blast
qed
have "∃P. finite P ∧ P ⊆ ?𝒞 ∧ ε < measure lebesgue (⋃P)"
proof (rule ccontr)
assume "¬ ?thesis"
then have bound: "⋀ℰ. ℰ ⊆ ?𝒞 ⟹ finite ℰ ⟹ measure lebesgue (⋃ℰ) ≤ ε"
by (meson linorder_not_less)
then have "∃T. t ⊆ T ∧ T ∈ lmeasurable ∧ measure lebesgue T ≤ ε"
using tsub
by (metis (no_types, lifting) cnt fmeasurable_Union_bound meas measure_Union_bound)
then show False using non by auto
qed
then obtain p where "finite p" "p ⊆ c"
and p: "ε < measure lebesgue (Union ((λx. cbox (u x) (v x)) ` p))"
by (metis (no_types, lifting) finite_subset_image)
show False
proof -
define 𝒟 where "𝒟 = (λx. cbox (u x) (v x)) ` p"
have fin𝒟: "finite 𝒟" unfolding 𝒟_def using ‹finite p› by auto
have cube: "∃k a' b'. D = cbox a' b' ∧ (∀i∈Basis. b' ∙ i - a' ∙ i = k)"
if "D ∈ 𝒟" for D
proof -
from that obtain x where "x ∈ p" "D = cbox (u x) (v x)"
unfolding 𝒟_def by auto
then show ?thesis
by (intro exI[of _ "v x - u x"] exI[of _ "u x"] exI[of _ "v x"])
(auto simp: Basis_real_def inner_real_def)
qed
obtain 𝒞 where "𝒞 ⊆ 𝒟" "disjoint 𝒞"
and 𝒞meas: "measure lebesgue (⋃𝒟) / 3 ^ DIM(real) ≤ measure lebesgue (⋃𝒞)"
using Austin_Lemma[OF fin𝒟 cube] by auto
have "ε / 3 < measure lebesgue (⋃𝒞)"
using p 𝒞meas 𝒟_def by force
moreover obtain p' where "p' ⊆ p" and 𝒞_eq: "𝒞 = (λx. cbox (u x) (v x)) ` p'"
and inj: "inj_on (λx. cbox (u x) (v x)) p'"
proof -
let ?f = "λx. cbox (u x) (v x)"
have Csub_im: "𝒞 ⊆ ?f ` p"
using ‹𝒞 ⊆ 𝒟› unfolding 𝒟_def by auto
define p' where "p' = inv_into p ?f ` 𝒞"
have p'_sub: "p' ⊆ p"
unfolding p'_def using Csub_im by (auto intro: inv_into_into)
have C_eq: "𝒞 = ?f ` p'"
by (metis Csub_im image_inv_into_cancel p'_def)
have "inj_on ?f p'"
proof (rule inj_onI)
fix x y assume "x ∈ p'" "y ∈ p'" and eq: "?f x = ?f y"
from ‹x ∈ p'› obtain K1 where "K1 ∈ 𝒞" and K1: "x = inv_into p ?f K1"
unfolding p'_def by auto
from ‹y ∈ p'› obtain K2 where "K2 ∈ 𝒞" and K2: "y = inv_into p ?f K2"
unfolding p'_def by auto
have "K1 = ?f (inv_into p ?f K1)"
using f_inv_into_f[of K1 ?f p] ‹K1 ∈ 𝒞› Csub_im by auto
also have "… = ?f (inv_into p ?f K2)"
using eq K1 K2 by fastforce
also have "… = K2"
using f_inv_into_f[of K2 ?f p] ‹K2 ∈ 𝒞› Csub_im by auto
finally have "K1 = K2" .
then show "x = y" using K1 K2 by simp
qed
then show ?thesis using that p'_sub C_eq by blast
qed
have finp': "finite p'" using ‹p' ⊆ p› ‹finite p› finite_subset by blast
have p'sub: "p' ⊆ t" using ‹p' ⊆ p› ‹p ⊆ c› ‹c ⊆ t› by auto
have ux_less_vx: "u x < v x" if "x ∈ p'" for x
using uv[of x] p'sub that by auto
have "measure lebesgue (⋃𝒞) ≤ (∑x∈p'. v x - u x)"
proof -
have "measure lebesgue (⋃𝒞) ≤ (∑D∈𝒞. measure lebesgue D)"
by (metis (no_types, lifting) 𝒞_eq ‹𝒞 ⊆ 𝒟› cbox_borel fin𝒟 finite_subset
imageE measure_Union_le sets_completionI_sets sets_lborel)
also have "… ≤ (∑x∈p'. measure lebesgue (cbox (u x) (v x)))"
by (metis (no_types, lifting) 𝒞_eq dual_order.eq_iff inj sum.reindex_cong)
also have "… = (∑x∈p'. v x - u x)"
by (simp add: measure_lborel_cbox_eq content_real less_imp_le ux_less_vx)
finally show ?thesis .
qed
also have "… ≤ (∑x∈p'. norm (f (u x) - f (v x))) / M"
proof -
have "(∑x∈p'. v x - u x) ≤ (∑x∈p'. norm (f (u x) - f (v x)) / M)"
proof (intro sum_mono)
fix x assume "x ∈ p'"
then have "M * (v x - u x) ≤ norm (f (u x) - f (v x))"
using uv p'sub ux_less_vx by fastforce
then show "v x - u x ≤ norm (f (u x) - f (v x)) / M"
using ‹0 < M› by (simp add: field_simps)
qed
also have "… = (∑x∈p'. norm (f (u x) - f (v x))) / M"
by (simp add: sum_divide_distrib)
finally show ?thesis .
qed
also have "… ≤ B / M"
proof -
have div: "𝒞 division_of ⋃𝒞"
unfolding division_of_def
proof (intro conjI)
show "finite 𝒞"
using finp' unfolding 𝒞_eq by auto
show "∀K∈𝒞. K ⊆ ⋃𝒞 ∧ K ≠ {} ∧ (∃a b. K = cbox a b)"
unfolding 𝒞_eq using p'sub uv by fastforce
show "∀K1∈𝒞. ∀K2∈𝒞. K1 ≠ K2 ⟶ interior K1 ∩ interior K2 = {}"
by (metis ‹disjoint 𝒞› disjointD interior_Int interior_empty)
qed auto
have Csub: "⋃𝒞 ⊆ {a..b}"
unfolding 𝒞_eq using p'sub uv by fastforce
have "(∑x∈p'. norm (f (u x) - f (v x)))
= (∑x∈p'. norm (f (Sup (cbox (u x) (v x))) - f (Inf (cbox (u x) (v x)))))"
by (simp add: less_imp_le ux_less_vx norm_minus_commute)
also have "… = (∑K∈𝒞. norm (f (Sup K) - f (Inf K)))"
unfolding 𝒞_eq using sum.reindex[OF inj, of "λK. norm (f (Sup K) - f (Inf K))"]
by (simp add: comp_def)
also have "… ≤ B" using B[OF div Csub] .
finally have "(∑x∈p'. norm (f (u x) - f (v x))) ≤ B" .
then show ?thesis using ‹0 < M› by (simp add: divide_right_mono)
qed
also have "… < ε / 3"
unfolding M_def using ‹0 < ε› by (simp add: abs_if field_simps)
ultimately show False by linarith
qed
qed
qed
qed auto
qed (auto simp: t_def)
define D where "D = {x ∈ {a..b}. ¬ isCont f x}"
have "countable D"
unfolding D_def using has_bounded_variation_countable_discontinuities[OF assms] .
hence "negligible (T ∪ D)"
using tn negligible_Un countable_imp_negligible by blast
then show ?thesis
using D_def tc by blast
qed
lemma cover_T:
fixes f :: "real ⇒ real" and a b k :: real
assumes f: "has_bounded_variation_on f {a..b}" and "0 < k"
and key_fn: "⋀x. x ∈ T ⟹ {cx x..dx x} ∈ D ∧ x ∈ {cx x<..<dx x} ∧
ux x ∈ {cx x<..<dx x} ∧ vx x ∈ {cx x<..<dx x} ∧
x ∈ {ux x<..<vx x} ∧
(f (cx x) ≤ f (dx x) ⟶ f (vx x) - f (ux x) ≤ -k * (vx x - ux x)) ∧
(f (dx x) < f (cx x) ⟶ k * (vx x - ux x) ≤ f (vx x) - f (ux x))"
and D_div: "D division_of {a..b}"
and D_sum: "vector_variation {a..b} f - k * e / 3 < (∑K∈D. norm (f (Sup K) - f (Inf K)))"
obtains C where "T ⊆ C" "C ∈ lmeasurable" "measure lebesgue C ≤ e"
proof (rule ccontr)
assume non: "¬ ?thesis"
have fin_D: "finite D"
using D_div division_of_finite by blast
let ?UVT = "(λx. {ux x<..<vx x}) ` T"
obtain ℱ where "ℱ ⊆ ?UVT" "countable ℱ" "⋃ℱ = ⋃?UVT"
by (smt (verit, best) Lindelof imageE open_greaterThanLessThan)
then obtain c where "countable c" and "c ⊆ T"
and c_union: "⋃((λx. {ux x<..<vx x}) ` c) = ⋃?UVT"
by (metis (lifting) countable_subset_image)
have "∃p. finite p ∧ p ⊆ (λx. {ux x..vx x}) ` c ∧ e < measure lebesgue (⋃p)"
proof (rule ccontr)
assume "¬ ?thesis"
then have le_e: "⋀p. p ⊆ (λx. {ux x..vx x}) ` c ⟹ finite p ⟹ measure lebesgue (⋃p) ≤ e"
by (meson linorder_not_less)
have union_le: "measure lebesgue (⋃((λx. {ux x..vx x}) ` c)) ≤ e"
by (rule measure_Union_bound)
(use ‹countable c› le_e lmeasurable_cbox in ‹auto simp: cbox_interval›)
have "T ⊆ ⋃((λx. {ux x..vx x}) ` c)"
proof
fix x assume "x ∈ T"
then have "x ∈ ⋃((λx. {ux x<..<vx x}) ` T)" using key_fn by auto
then show "x ∈ ⋃((λx. {ux x..vx x}) ` c)" using c_union by force
qed
moreover have "⋃((λx. {ux x..vx x}) ` c) ∈ lmeasurable"
using ‹countable c› le_e by (intro fmeasurable_Union_bound[where B=e]) auto
ultimately have *: "e < measure lebesgue (⋃((λx. {ux x..vx x}) ` c))"
using non that union_le by blast
with union_le show False by linarith
qed
then obtain Q where "finite Q" "Q ⊆ (λx. {ux x..vx x}) ` c"
"e < measure lebesgue (⋃Q)" by auto
from finite_subset_image[OF ‹finite Q› ‹Q ⊆ (λx. {ux x..vx x}) ` c›]
obtain p where "p ⊆ c" "finite p" "Q = (λx. {ux x..vx x}) ` p" by auto
then have fin_p: "finite p" and p_sub: "p ⊆ c"
and p_meas: "e < measure lebesgue (⋃((λx. {ux x..vx x}) ` p))"
using ‹e < measure lebesgue (⋃Q)› by auto
define 𝒟 where "𝒟 = (λx. {ux x..vx x}) ` p"
have fin𝒟: "finite 𝒟" unfolding 𝒟_def using fin_p by auto
have cube: "∃k a b. D = cbox a b ∧ (∀i∈Basis. b ∙ i - a ∙ i = k)" if "D ∈ 𝒟" for D
using 𝒟_def that by auto
obtain d where "d ⊆ 𝒟" "disjoint d"
and d_meas: "measure lebesgue (⋃𝒟) / 3 ^ DIM(real) ≤ measure lebesgue (⋃d)"
using Austin_Lemma[OF fin𝒟 cube] by auto
have "∃j. j ∈ D ∧ i ⊆ j" if "i ∈ d" for i
proof -
from that ‹d ⊆ 𝒟› obtain x where "x ∈ p" and x: "i = {ux x..vx x}"
unfolding 𝒟_def by auto
then have "x ∈ T" using p_sub ‹c ⊆ T› by auto
from key_fn[OF this] show ?thesis
by (metis atLeastatMost_subset_iff greaterThanLessThan_iff less_eq_real_def x)
qed
then have d_decomp: "⋃d = (⋃j∈D. ⋃{i ∈ d. i ⊆ j})"
by blast
let ?F = "(λj. ⋃{i ∈ d. i ⊆ j}) ` D"
have fin_F: "finite ?F"
using fin_D by auto
have fin_d: "finite d" using finite_subset[OF ‹d ⊆ 𝒟› fin𝒟] .
have meas_F: "S ∈ sets lebesgue" if "S ∈ ?F" for S
using fin_d ‹d ⊆ 𝒟› fmeasurableD[OF fmeasurable_cbox] that
by (auto intro!: sets.finite_Union simp: 𝒟_def cbox_interval)
have "measure lebesgue (⋃d) = measure lebesgue (⋃?F)"
using d_decomp by (simp add: image_UN)
also have "… ≤ sum (measure lebesgue) ?F"
using measure_Union_le[OF fin_F meas_F] .
also have "… ≤ (∑j∈D. measure lebesgue (⋃{i ∈ d. i ⊆ j}))"
using sum_image_le [unfolded o_def] fin_D measure_nonneg by blast
also have "… < e / 3"
proof -
have per_elt: "measure lebesgue (⋃{i ∈ d. i ⊆ K}) * k ≤ vector_variation K f - norm (f (Sup K) - f (Inf K))"
if "K ∈ D" for K
proof -
obtain l r where K_eq: "K = {l..r}" and "l ≤ r"
using division_ofD[OF D_div] ‹K ∈ D› by (metis atLeastatMost_empty_iff2 box_real(2))
have meas_i: "i ∈ sets lebesgue" if "i ∈ d" "i ⊆ {l..r}" for i
using fmeasurableD[OF fmeasurable_cbox[of "ux x" "vx x"]]
using 𝒟_def ‹d ⊆ 𝒟› that(1) by auto
define d' where "d' = {i ∈ d. i ⊆ {l..r}}"
have disj_d': "disjoint d'"
using ‹disjoint d› d'_def pairwise_subset by force
have d'_ne: "K ≠ {}" if "K ∈ d'" for K
proof -
from that obtain x where "x ∈ p" "K = {ux x..vx x}"
using ‹d ⊆ 𝒟› unfolding d'_def 𝒟_def by auto
then have "x ∈ T" using p_sub ‹c ⊆ T› by auto
from key_fn[OF this] show ?thesis using ‹K = {ux x..vx x}› by auto
qed
have fin_d': "finite d'" unfolding d'_def using fin_d by auto
have d'_div: "d' division_of ⋃d'"
unfolding division_of_def
proof (intro conjI ballI impI)
fix K assume "K ∈ d'"
then have "K ∈ 𝒟" using ‹d ⊆ 𝒟› d'_def by blast
then show "∃a b. K = cbox a b"
unfolding 𝒟_def by (auto simp: cbox_interval)
next
fix K1 K2 assume "K1 ∈ d'" "K2 ∈ d'" "K1 ≠ K2"
then show "interior K1 ∩ interior K2 = {}"
using disj_d' by (metis disjointD interior_Int interior_empty)
qed (use fin_d' d'_ne in auto)
have d'_sub_lr: "⋃d' ⊆ {l..r}"
unfolding d'_def by auto
obtain d'' where d'_sub_d'': "d' ⊆ d''" and d''_div: "d'' division_of {l..r}"
and "finite d''"
by (metis box_real(2) d'_div d'_sub_lr division_of_finite partial_division_extend_interval)
have "measure lebesgue (⋃ d') ≤ (∑i∈d'. measure lebesgue i)"
using meas_i d'_div by (intro measure_Union_le) (auto simp: d'_def)
also have "… ≤ (vector_variation {l..r} f - ¦f r - f l¦) / k"
proof -
define s where "s ≡ if f l ≤ f r then (1::real) else -1"
have s_abs: "s * (f r - f l) = ¦f r - f l¦"
unfolding s_def by auto
have bv_lr: "has_bounded_variation_on f {l..r}"
by (metis D_div K_eq assms(1) cbox_division_memE has_bounded_variation_on_subset that)
have sum_abs_le: "(∑i∈d''. ¦f (Sup i) - f (Inf i)¦) ≤ vector_variation {l..r} f"
using has_bounded_variation_works(1)[OF bv_lr d''_div order_refl]
by (simp add: real_norm_def)
have sum_telesc: "(∑i∈d''. f (Sup i) - f (Inf i)) = f r - f l"
using division_telescope_eq[OF d''_div ‹l ≤ r›] .
have elt_bound: "measure lebesgue i * k ≤ ¦f (Sup i) - f (Inf i)¦ - s * (f (Sup i) - f (Inf i))"
if i_in_d': "i ∈ d'" for i
proof -
from i_in_d' obtain x where "x ∈ p" "i = {ux x..vx x}"
using ‹d ⊆ 𝒟› unfolding d'_def 𝒟_def by auto
have "x ∈ T" using ‹x ∈ p› p_sub ‹c ⊆ T› by auto
have uv_lt: "ux x < vx x" using key_fn[OF ‹x ∈ T›] by auto
have i_sub_lr: "{ux x..vx x} ⊆ {l..r}"
using i_in_d' unfolding d'_def ‹i = {ux x..vx x}› by auto
have "interior {l..r} ∩ interior {cx x..dx x} ≠ {}"
using key_fn[OF ‹x ∈ T›] i_sub_lr by auto
then have "{cx x..dx x} = {l..r}"
using D_div K_eq ‹K ∈ D› key_fn[OF ‹x ∈ T›] by blast
then have "cx x = l" "dx x = r"
using key_fn[OF ‹x ∈ T›] ‹l ≤ r› by (auto simp: Icc_eq_Icc)
have meas_eq: "measure lebesgue i = vx x - ux x"
unfolding ‹i = {ux x..vx x}›
using uv_lt by (simp add: measure_lborel_cbox_eq content_real less_imp_le cbox_interval)
have eq: "Sup i = vx x" "Inf i = ux x" unfolding ‹i = {ux x..vx x}›
using uv_lt by (simp_all add: less_imp_le)
show ?thesis
proof (cases "f l ≤ f r")
case True
then have "f (vx x) - f (ux x) ≤ - k * (vx x - ux x)"
using key_fn[OF ‹x ∈ T›] ‹cx x = l› ‹dx x = r› by auto
with True uv_lt ‹0 < k›
have fvu_neg: "f (vx x) - f (ux x) ≤ 0"
by (smt (verit, ccfv_threshold) mult_neg_pos)
then show ?thesis unfolding eq meas_eq s_def
using ‹f (vx x) - f (ux x) ≤ - k * (vx x - ux x)› uv_lt ‹0 < k› True
by (simp add: mult.commute)
next
case False
then have "k * (vx x - ux x) ≤ f (vx x) - f (ux x)"
using key_fn[OF ‹x ∈ T›] ‹cx x = l› ‹dx x = r› by auto
with False uv_lt ‹0 < k›
have fvu_pos: "f (vx x) - f (ux x) ≥ 0"
by (metis order.trans ge_iff_diff_ge_0 less_le zero_le_mult_iff)
then show ?thesis unfolding eq meas_eq s_def
using ‹k * (vx x - ux x) ≤ f (vx x) - f (ux x)› uv_lt ‹0 < k›
by (simp add: False mult.commute)
qed
qed
have "(∑i∈d'. measure lebesgue i) * k = (∑i∈d'. measure lebesgue i * k)"
by (simp add: sum_distrib_right)
also have "… ≤ (∑i∈d'. ¦f (Sup i) - f (Inf i)¦ - s * (f (Sup i) - f (Inf i)))"
by (rule sum_mono) (use elt_bound in auto)
also have "… ≤ (∑i∈d''. ¦f (Sup i) - f (Inf i)¦ - s * (f (Sup i) - f (Inf i)))"
using ‹finite d''› d'_sub_d''
by (intro sum_mono2) (auto simp: s_def)
also have "… = (∑i∈d''. ¦f (Sup i) - f (Inf i)¦) - s * (∑i∈d''. f (Sup i) - f (Inf i))"
by (simp add: sum_subtractf sum_distrib_left[symmetric])
also have "… = (∑i∈d''. ¦f (Sup i) - f (Inf i)¦) - s * (f r - f l)"
by (simp add: sum_telesc)
also have "… ≤ vector_variation {l..r} f - ¦f r - f l¦"
using sum_abs_le by (simp add: s_abs)
finally show ?thesis using ‹0 < k›
by (simp add: divide_simps)
qed
finally show ?thesis using ‹l ≤ r› ‹k>0›
by (simp add: K_eq d'_def divide_simps)
qed
have "(∑j∈D. measure lebesgue (⋃{i ∈ d. i ⊆ j})) * k
= (∑j∈D. measure lebesgue (⋃{i ∈ d. i ⊆ j}) * k)"
by (simp add: sum_distrib_right)
also have "… ≤ (∑j∈D. vector_variation j f - norm (f (Sup j) - f (Inf j)))"
by (rule sum_mono) (rule per_elt)
also have "… = (∑j∈D. vector_variation j f) - (∑K∈D. norm (f (Sup K) - f (Inf K)))"
by (simp add: sum_subtractf)
also have "… ≤ vector_variation {a..b} f - (∑K∈D. norm (f (Sup K) - f (Inf K)))"
proof -
have "(∑j∈E. vector_variation j f) ≤ vector_variation (⋃E) f"
if "finite E" "E ⊆ D" for E
using that
proof (induction rule: finite_induct)
case empty
then show ?case by (simp add: vector_variation_def set_variation_def)
next
case (insert K F)
then have "F ⊆ D" and K_in_D: "K ∈ D" by auto
have IH: "(∑j∈F. vector_variation j f) ≤ vector_variation (⋃F) f"
using insert(3)[OF ‹F ⊆ D›] .
have disj_int: "interior K ∩ interior (⋃F) = {}"
proof (rule Int_interior_Union_intervals)
fix U assume "U ∈ F"
then have "U ∈ D" using ‹F ⊆ D› by auto
show "∃a b. U = cbox a b"
using division_ofD(4)[OF D_div ‹U ∈ D›] by auto
have "K ≠ U" using insert ‹U ∈ F› by auto
show "interior K ∩ interior U = {}"
using division_ofD(5)[OF D_div K_in_D ‹U ∈ D› ‹K ≠ U›] .
qed (use insert in auto)
have bv_KF: "has_bounded_variation_on f (K ∪ ⋃F)"
using division_ofD(2)[OF D_div] insert(4)
by (intro has_bounded_variation_on_subset[OF assms(1)]) auto
have "(∑j∈insert K F. vector_variation j f) = vector_variation K f + (∑j∈F. vector_variation j f)"
using insert by auto
also have "… ≤ vector_variation (K ∪ ⋃F) f"
using vector_variation_le_Un[OF bv_KF disj_int] IH by linarith
also have "K ∪ ⋃F = ⋃(insert K F)" by auto
finally show ?case by simp
qed
then show ?thesis
by (metis (lifting) ext D_div diff_mono division_ofD(6) fin_D order.refl)
qed
finally have sum_k_le: "(∑j∈D. measure lebesgue (⋃{i ∈ d. i ⊆ j})) * k
≤ vector_variation {a..b} f - (∑K∈D. norm (f (Sup K) - f (Inf K)))" .
with D_sum have "(∑j∈D. measure lebesgue (⋃{i ∈ d. i ⊆ j})) * k < k * e / 3"
by linarith
then show ?thesis
using ‹0 < k› by (simp add: field_simps)
qed
finally have d_bound: "measure lebesgue (⋃d) < e / 3" .
show False
using p_meas d_meas d_bound unfolding 𝒟_def by auto
qed
lemma Lebesgue_diff_aux2:
fixes f :: "real ⇒ real" and a b k :: real
assumes f: "has_bounded_variation_on f {a..b}" and "a < b" "0 < k"
shows "negligible
{x ∈ {a..b}.
∀S. open S ∧ x ∈ S ⟶
(∃u v. u ∈ {a..b} ∧ u ∈ S ∧
v ∈ {a..b} ∧ v ∈ S ∧
x ∈ {u<..<v} ∧ k ≤ (f v - f u) / (v-u)) ∧
(∃u v. u ∈ {a..b} ∧ u ∈ S ∧
v ∈ {a..b} ∧ v ∈ S ∧
x ∈ {u<..<v} ∧ (f v - f u) / (v-u) ≤ -k)}" (is "negligible ?N")
proof -
define N where "N ≡ ?N"
have "negligible N"
unfolding negligible_outer_le
proof (intro allI impI)
fix e :: real assume "e > 0"
have ke3_pos: "0 < k * e / 3"
using ‹0 < k› ‹e > 0› by auto
define S where "S ≡ {∑k∈d. norm (f (Sup k) - f (Inf k)) |d. d division_of {a..b}}"
have S_ne: "S ≠ {}"
by (metis (mono_tags, lifting) S_def box_real(2) elementary_interval empty_Collect_eq)
have "vector_variation {a..b} f - k * e / 3 < Sup S"
using ke3_pos vector_variation_on_interval[OF f] unfolding S_def by linarith
then obtain x where "x ∈ S" "vector_variation {a..b} f - k * e / 3 < x"
using less_cSupD[OF S_ne] by auto
then obtain D where D_div: "D division_of {a..b}"
and D_sum: "vector_variation {a..b} f - k * e / 3 < (∑K∈D. norm (f (Sup K) - f (Inf K)))"
unfolding S_def by auto
have fin_D: "finite D"
using D_div division_of_finite by blast
define N' where "N' ≡ N - ⋃(frontier ` D)"
have neg_frontiers: "negligible (⋃(frontier ` D))"
using fin_D D_div convex_box(1) negligible_convex_frontier by blast
have key: "∃c d u v. {c..d} ∈ D ∧ x ∈ {c<..<d} ∧ u ∈ {c<..<d} ∧ v ∈ {c<..<d} ∧
x ∈ {u<..<v} ∧
(f c ≤ f d ⟶ f v - f u ≤ -k * (v-u)) ∧
(f d < f c ⟶ k * (v-u) ≤ f v - f u)" if "x ∈ N'" for x
proof -
have xN: "x ∈ N" and xnf: "x ∉ ⋃(frontier ` D)" and xab: "x ∈ {a..b}"
using that unfolding N'_def N_def by auto
have "x ∈ ⋃D" using xab division_ofD(6)[OF D_div] by auto
then obtain K c d where "K ∈ D" "x ∈ K" and Kcd: "K = {c..d}"
by (metis D_div UnionE box_real(2) division_ofD(4))
then obtain KD: "{c..d} ∈ D" and xK: "x ∈ {c..d}"
by blast
have "x ∉ frontier K" using xnf ‹K ∈ D› by auto
then have "x ∉ {c..d} - {c<..<d}"
by (simp add: Kcd frontier_def)
then have x_int: "x ∈ {c<..<d}" using xK by auto
show ?thesis
proof (cases "f c ≤ f d")
case True
from x_int xN obtain u v where
uv: "u ∈ {c<..<d}" "v ∈ {c<..<d}" "x ∈ {u<..<v}" "(f v - f u) / (v-u) ≤ -k"
using N_def by auto
then have "f v - f u ≤ -k * (v-u)"
by (simp add: pos_divide_le_eq mult.commute)
then show ?thesis
by (smt (verit, ccfv_SIG) KD True uv x_int)
next
case False
from x_int xN obtain u v where uv: "u ∈ {c<..<d}" "v ∈ {c<..<d}"
"x ∈ {u<..<v}" "k ≤ (f v - f u) / (v-u)"
using N_def by auto
then have "k * (v-u) ≤ f v - f u" by (simp add: pos_le_divide_eq mult.commute)
then show ?thesis using False KD uv x_int by blast
qed
qed
then obtain cx dx ux vx where
key_fn: "⋀x. x ∈ N' ⟹ {cx x..dx x} ∈ D ∧ x ∈ {cx x<..<dx x} ∧
ux x ∈ {cx x<..<dx x} ∧ vx x ∈ {cx x<..<dx x} ∧
x ∈ {ux x<..<vx x} ∧
(f (cx x) ≤ f (dx x) ⟶ f (vx x) - f (ux x) ≤ -k * (vx x - ux x)) ∧
(f (dx x) < f (cx x) ⟶ k * (vx x - ux x) ≤ f (vx x) - f (ux x))"
by metis
obtain C where C_sub: "N' ⊆ C" and C_meas: "C ∈ lmeasurable" and C_bound: "measure lebesgue C ≤ e"
using cover_T [OF f ‹k>0› key_fn D_div D_sum] by metis
define T where "T ≡ C ∪ ⋃(frontier ` D)"
have "N ⊆ T" unfolding T_def using C_sub unfolding N'_def by auto
moreover have "T ∈ lmeasurable"
using T_def C_meas neg_frontiers negligible_imp_measurable by blast
moreover have "measure lebesgue T ≤ e"
by (simp add: C_bound C_meas T_def measure_Un2 neg_frontiers negligible_diff
negligible_imp_measurable negligible_imp_measure0)
ultimately show "∃T. N ⊆ T ∧ T ∈ lmeasurable ∧ measure lebesgue T ≤ e"
by blast
qed
then show ?thesis
by (simp add: N_def)
qed
lemma Lebesgue_diff_aux3:
fixes f :: "real ⇒ real" and a b k :: real
assumes "has_bounded_variation_on f {a..b}" "a < b" "0 < k"
defines "I ≡ λn x. ball x (inverse (real n + 1)) ∩ {a..b}"
shows "negligible
{x ∈ {a..b}.
∀n::nat. ∃u v. u ∈ I n x ∧ v ∈ I n x ∧
u ≠ x ∧ v ≠ x ∧ k ≤ (f v - f x) / (v-x) ∧
(f u - f x) / (u-x) ≤ -k}" (is "negligible ?T")
proof -
define T where "T ≡ ?T"
define L2 where "L2 ≡ {x ∈ {a..b}.
∀S. open S ∧ x ∈ S ⟶
(∃u v. u ∈ {a..b} ∧ u ∈ S ∧ v ∈ {a..b} ∧ v ∈ S ∧
x ∈ {u<..<v} ∧ k/2 ≤ (f v - f u) / (v-u)) ∧
(∃u v. u ∈ {a..b} ∧ u ∈ S ∧ v ∈ {a..b} ∧ v ∈ S ∧
x ∈ {u<..<v} ∧ (f v - f u) / (v-u) ≤ -(k/2))}"
have neg_endpts: "negligible {a, b}"
by (rule negligible_finite) simp
have neg_discont: "negligible {x ∈ {a..b}. ¬ isCont f x}"
using countable_imp_negligible[OF has_bounded_variation_countable_discontinuities[OF assms(1)]] .
have neg_L2: "negligible L2"
unfolding L2_def using Lebesgue_diff_aux2[OF assms(1,2), of "k/2"] assms(3) by simp
have neg_super: "negligible (({a, b} ∪ {x ∈ {a..b}. ¬ isCont f x}) ∪ L2)"
by (rule negligible_Un[OF negligible_Un[OF neg_endpts neg_discont] neg_L2])
show "negligible T"
proof (rule negligible_subset[OF neg_super])
show "T ⊆ ({a, b} ∪ {x ∈ {a..b}. ¬ isCont f x}) ∪ L2"
proof (rule subsetI)
fix x assume "x ∈ T"
show "x ∈ ({a, b} ∪ {x ∈ {a..b}. ¬ isCont f x}) ∪ L2"
proof (cases "x = a ∨ x = b ∨ ¬ isCont f x")
case True
with ‹x ∈ T› show ?thesis by (auto simp: T_def)
next
case False
have "x ∈ L2"
unfolding L2_def
proof (intro CollectI conjI strip)
show "x ∈ {a..b}"
using ‹x ∈ T› by (auto simp: T_def)
next
fix S :: "real set"
assume "open S ∧ x ∈ S"
then have "open S" "x ∈ S" by auto
have "x ∈ {a<..<b}"
using ‹x ∈ T› False by (auto simp: T_def)
have "open (S ∩ {a<..<b})"
using ‹open S› open_real_greaterThanLessThan by blast
then have "∃e>0. ball x e ⊆ S ∩ {a<..<b}"
using ‹x ∈ S› ‹x ∈ {a<..<b}›
by (simp add: open_contains_ball)
then obtain e where "e > 0" "ball x e ⊆ S ∩ {a<..<b}"
by auto
obtain n :: nat where n_pos: "n ≠ 0" and inv_lt: "inverse (real n) < e"
using real_arch_invD[OF ‹e > 0›] by blast
have inv_n1_lt: "inverse (real n + 1) < e"
by (smt (verit) inv_lt less_imp_inverse_less n_pos of_nat_0_eq_iff of_nat_less_0_iff)
have ball_sub: "ball x (inverse (real n + 1)) ⊆ S ∩ {a<..<b}"
using ‹ball x e ⊆ S ∩ {a<..<b}› inv_n1_lt by auto
from ‹x ∈ T› obtain u v where
uv: "u ∈ I n x" "v ∈ I n x" "u ≠ x" "v ≠ x"
"k ≤ (f v - f x) / (v-x)" "(f u - f x) / (u-x) ≤ -k"
by (force simp add: T_def)
have uS: "u ∈ S" and u_int: "u ∈ {a<..<b}" and vS: "v ∈ S" and v_int: "v ∈ {a<..<b}"
and uab: "u ∈ {a..b}" and vab: "v ∈ {a..b}"
using uv ball_sub by (auto simp: I_def)
have fx_cont: "isCont f x" using False by simp
have cont_slope: "isCont (λy. (f v - f y) / (v-y)) x"
by (intro fx_cont continuous_intros) (auto simp: uv)
then have eps_delta: "∀ε>0. ∃δ>0. ∀y. ¦y - x¦ < δ ⟶
¦(f v - f y) / (v-y) - (f v - f x) / (v-x)¦ < ε"
by (simp add: continuous_at_real_range real_norm_def)
with half_gt_zero[OF ‹k>0›]
obtain d where "d > 0" and
d_prop: "∀y. ¦y - x¦ < d ⟶ ¦(f v - f y) / (v-y) - (f v - f x) / (v-x)¦ < k / 2"
by blast
have min_pos: "min d (inverse (real n + 1)) > 0"
using ‹d > 0› by (simp add: min_def)
show "∃u v. u ∈ {a..b} ∧ u ∈ S ∧ v ∈ {a..b} ∧ v ∈ S ∧ x ∈ {u<..<v} ∧ k / 2 ≤ (f v - f u) / (v-u)"
proof (cases "v < x")
case True
define y where "y = x + min d (inverse (real n + 1)) / 2"
have y_gt_x: "x < y"
unfolding y_def using min_pos by simp
have y_dist_d: "¦y - x¦ < d" and y_in_ball: "y ∈ ball x (inverse (real n + 1))"
unfolding y_def using ‹d > 0› min_pos by (auto simp: min_def dist_real_def ball_def)
have yS: "y ∈ S" and y_int: "y ∈ {a<..<b}" and yab: "y ∈ {a..b}"
using y_in_ball ball_sub by auto
have x_between: "x ∈ {v<..<y}"
using True y_gt_x by auto
have "(f v - f y) / (v-y) > (f v - f x) / (v-x) - k / 2"
using d_prop y_dist_d by (smt (verit))
with uv have "(f v - f y) / (v-y) > k / 2"
by linarith
hence "k / 2 ≤ (f y - f v) / (y-v)"
using True y_gt_x by (simp add: field_simps)
then show ?thesis
using vS vab x_between yS yab by blast
next
case False
define y where "y = x - min d (inverse (real n + 1)) / 2"
have y_dist: "¦y - x¦ < inverse (real n + 1)" and y_dist_d: "¦y - x¦ < d"
unfolding y_def using ‹d > 0› min_pos by (auto simp: min_def)
have y_in_ball: "y ∈ ball x (inverse (real n + 1))"
using y_dist by (simp add: dist_real_def ball_def)
have yS: "y ∈ S" and y_int: "y ∈ {a<..<b}"
using y_in_ball ball_sub by auto
have x_between: "x ∈ {y<..<v}"
using y_def min_pos False uv by (fastforce simp: I_def)
have slope_close: "(f v - f y) / (v-y) > (f v - f x) / (v-x) - k / 2"
using d_prop y_dist_d by (smt (verit))
with uv have "(f v - f y) / (v-y) > k / 2"
by linarith
then show ?thesis
using less_le uv vS x_between yS y_int by (fastforce simp: I_def)
qed
have cont_slope_u: "isCont (λy. (f u - f y) / (u-y)) x"
by (intro fx_cont continuous_intros) (auto simp: uv)
then have eps_delta_u: "∀ε>0. ∃δ>0. ∀y. ¦y - x¦ < δ ⟶
¦(f u - f y) / (u-y) - (f u - f x) / (u-x)¦ < ε"
by (simp add: continuous_at_real_range real_norm_def)
obtain d' where "d' > 0" and
d'_prop: "∀y. ¦y - x¦ < d' ⟶
¦(f u - f y) / (u-y) - (f u - f x) / (u-x)¦ < k / 2"
using ‹0 < k / 2› eps_delta_u by blast
have min_pos': "min d' (inverse (real n + 1)) > 0"
using ‹d' > 0› by (simp add: min_def)
show "∃u v. u ∈ {a..b} ∧ u ∈ S ∧ v ∈ {a..b} ∧ v ∈ S ∧ x ∈ {u<..<v} ∧ (f v - f u) / (v-u) ≤ - (k/2)"
proof (cases "u < x")
case True
define y where "y = x + min d' (inverse (real n + 1)) / 2"
have y_gt_x: "x < y"
unfolding y_def using min_pos' by simp
have y_dist: "¦y - x¦ < inverse (real n + 1)" and y_dist_d: "¦y - x¦ < d'"
unfolding y_def using ‹d' > 0› min_pos' by (auto simp: min_def)
have y_in_ball: "y ∈ ball x (inverse (real n + 1))"
using y_dist by (simp add: dist_real_def ball_def)
have yS: "y ∈ S" and y_int: "y ∈ {a<..<b}"
using y_in_ball ball_sub by auto
have x_between: "x ∈ {u<..<y}"
using True y_gt_x by auto
have "¦(f u - f y) / (u-y) - (f u - f x) / (u-x)¦ < k / 2"
using d'_prop y_dist_d by auto
then have slope_upper: "(f u - f y) / (u-y) < - (k/2)"
using uv by linarith
have "(f y - f u) / (y-u) = (f u - f y) / (u-y)"
using True y_gt_x by (simp add: field_simps)
hence "(f y - f u) / (y-u) ≤ - (k/2)"
using slope_upper by linarith
then show ?thesis
using uS uv x_between yS y_int less_le_not_le by (force simp: I_def)
next
case False
hence xu: "x < u" using uv by linarith
define y where "y = x - min d' (inverse (real n + 1)) / 2"
have y_lt_x: "y < x"
unfolding y_def using min_pos' by simp
have y_dist: "¦y - x¦ < inverse (real n + 1)"
unfolding y_def using ‹d' > 0› min_pos' by (auto simp: min_def)
have y_dist_d: "¦y - x¦ < d'"
unfolding y_def using ‹d' > 0› min_pos' by (auto simp: min_def)
have y_in_ball: "y ∈ ball x (inverse (real n + 1))"
using y_dist by (simp add: dist_real_def ball_def)
have yS: "y ∈ S" and y_int: "y ∈ {a<..<b}"
using y_in_ball ball_sub by auto
have yab: "y ∈ {a..b}"
using y_int by auto
have x_between: "x ∈ {y<..<u}"
using y_lt_x xu by auto
have y_lt_u: "y < u" using y_lt_x xu by linarith
have "¦(f u - f y) / (u-y) - (f u - f x) / (u-x)¦ < k / 2"
using d'_prop y_dist_d by auto
with uv have slope_upper: "(f u - f y) / (u-y) ≤ - (k/2)"
by linarith
then show ?thesis
using uS uv x_between yS yab unfolding I_def by blast
qed
qed
then show ?thesis
by fastforce
qed
qed
qed
qed
lemma Lebesgue_diff_aux4:
fixes f :: "real ⇒ real" and a b k :: real
assumes f: "has_bounded_variation_on f {a..b}" and "a < b" "0 < k"
defines "I ≡ λn x. ball x (inverse (real n + 1)) ∩ {a..b}"
shows "negligible
{x ∈ {a..b}.
∀n::nat. ∃u v. u ∈ I n x ∧ v ∈ I n x ∧ u ≠ x ∧ v ≠ x ∧
k ≤ (f v - f x) / (v-x) - (f u - f x) / (u-x)}"
(is "negligible ?T")
proof -
define T where "T ≡ ?T"
from Lebesgue_diff_aux1[OF assms(1)]
obtain U where neg_U: "negligible U"
and U_prop: "∀x ∈ {a..b} - U. ∃B>0. ∀⇩F y in at x. norm (f y - f x) ≤ B * norm (y-x)"
by auto
define S where "S q ≡ {x ∈ {a..b}.
∀n::nat. ∃u v. u ∈ I n x ∧ v ∈ I n x ∧ u ≠ x ∧ v ≠ x ∧
k / 3 ≤ (f v - f x) / (v-x) - q ∧
(f u - f x) / (u-x) - q ≤ -(k/3)}" for q :: real
have neg_super: "negligible (U ∪ ⋃(S ` ℚ))"
proof (rule negligible_Un[OF neg_U])
show "negligible (⋃(S ` ℚ))"
proof (rule negligible_countable_Union)
show "countable (S ` ℚ)"
using countable_rat by (rule countable_image)
next
fix Sq assume "Sq ∈ S ` ℚ"
then obtain q where "q ∈ ℚ" and "Sq = S q" by auto
show "negligible Sq"
proof -
define g where "g ≡ λx. f x - q * x"
have bv_id: "has_bounded_variation_on id {a..b}"
by (rule increasing_bounded_variation) (auto simp: mono_on_def)
have "has_bounded_variation_on (λx. q *⇩R x) {a..b}"
using has_bounded_variation_on_cmul[OF bv_id] by simp
then have bv_g: "has_bounded_variation_on g {a..b}"
unfolding g_def using f has_bounded_variation_on_sub by force
have Sq_eq: "S q = {x ∈ {a..b}.
∀n::nat. ∃u v. u ∈ I n x ∧ v ∈ I n x ∧ u ≠ x ∧ v ≠ x ∧
k / 3 ≤ (g v - g x) / (v-x) ∧ (g u - g x) / (u-x) ≤ -(k/3)}"
unfolding S_def
apply (intro arg_cong[where f="λP. {x ∈ {a..b}. P x}"] ext all_cong1 ex_cong1)
by (auto simp: g_def algebra_simps divide_simps)
show ?thesis unfolding ‹Sq = S q› Sq_eq
using Lebesgue_diff_aux3[OF bv_g ‹a<b›, of "k/3"] ‹k>0› by (simp add: I_def)
qed
qed
qed
show "negligible T"
proof (rule negligible_subset[OF neg_super])
show "T ⊆ U ∪ ⋃(S ` ℚ)"
proof (rule subsetI)
fix x assume "x ∈ T"
then obtain xab: "x ∈ {a..b}" and
xprop: "∀n::nat. ∃u v. u ∈ I n x ∧ v ∈ I n x ∧ u ≠ x ∧ v ≠ x ∧
k ≤ (f v - f x) / (v-x) - (f u - f x) / (u-x)"
unfolding T_def by blast
show "x ∈ U ∪ ⋃(S ` ℚ)"
proof (cases "x ∈ U")
case True then show ?thesis by auto
next
case False
have "x ∈ {a..b} - U" using xab False by auto
from U_prop[rule_format, OF this]
obtain B where "B > 0" and
B_ev: "eventually (λy. norm (f y - f x) ≤ B * norm (y-x)) (at x)"
by auto
obtain N where dq_bound: "⋀n u. N ≤ n ⟹ u ∈ ball x (inverse (real n + 1)) ⟹ u ≠ x
⟹ ¦(f u - f x) / (u-x)¦ ≤ B"
proof -
from B_ev obtain d :: real where "d > 0" and
d_prop: "⋀y. y ≠ x ⟹ dist y x < d ⟹ norm (f y - f x) ≤ B * norm (y-x)"
unfolding eventually_at by auto
from real_arch_invD[OF ‹d > 0›]
obtain N :: nat where "N ≠ 0" and "inverse (real N) < d" by auto
show thesis
proof
fix n u
assume "N ≤ n" "u ∈ ball x (inverse (real n + 1))" "u ≠ x"
then have "dist u x < inverse (real n + 1)"
by (simp add: dist_commute)
also have "inverse (real n + 1) ≤ inverse (real N)"
using ‹N ≤ n› ‹N ≠ 0› by auto
also have "… < d" by fact
finally have "dist u x < d" .
have "¦u - x¦ > 0" using ‹u ≠ x› by auto
with d_prop[OF ‹u ≠ x›] show "¦(f u - f x) / (u-x)¦ ≤ B"
by (simp add: ‹dist u x < d› pos_divide_le_eq)
qed
qed
have balls_nonempty: "⋀n. ∃u. u ∈ I n x ∧ u ≠ x"
using xprop by blast
define DQ where "DQ n = {(f u - f x) / (u-x) | u.
u ∈ I n x ∧ u ≠ x}" for n
have S_nonempty: "DQ n ≠ {}" for n
using balls_nonempty[of n] unfolding DQ_def by blast
have S_bdd: "bdd_below (DQ n)" if "N ≤ n" for n
using DQ_def abs_le_D2[OF dq_bound[OF ‹N ≤ n›]] that
by (auto simp: bdd_below.unfold minus_le_iff I_def)
have S_subset: "DQ n ⊆ DQ m" if "m ≤ n" for m n
unfolding DQ_def I_def using less_le_trans that by fastforce
define g where "g ≡ λn. Inf (DQ n)"
have g_mono: "g m ≤ g n" if "N ≤ m" "m ≤ n" for m n
by (simp add: S_bdd S_nonempty S_subset cInf_superset_mono g_def that)
have g_bounded: "norm (g (n+N)) ≤ B" for n
proof -
have nN: "N ≤ n + N" by simp
obtain u where u: "u ∈ ball x (inverse (real (n+N) + 1))" "u ∈ {a..b}" "u ≠ x"
using balls_nonempty[of "n + N"] I_def by auto
have mem: "(f u - f x) / (u-x) ∈ DQ (n+N)"
unfolding DQ_def I_def using u by auto
have "g (n+N) ≤ (f u - f x) / (u-x)"
unfolding g_def by (rule cInf_lower[OF mem S_bdd[OF nN]])
also have "… ≤ B"
using abs_le_D1[OF dq_bound[OF nN u(1) u(3)]] .
finally have upper: "g (n+N) ≤ B" .
have "- B ≤ y" if y: "y ∈ DQ (n+N)" for y
using dq_bound nN y
by (simp add: DQ_def I_def) (metis of_nat_add abs_divide abs_le_D2 add.commute le_add1 minus_le_iff)
then have "- B ≤ Inf (DQ (n+N))"
using le_cInf_iff[OF S_nonempty S_bdd[OF nN]] by auto
with upper show ?thesis
by (simp add: g_def abs_le_iff)
qed
have bseq: "Bseq (λn. g (n+N))"
unfolding Bseq_def using ‹B > 0› g_bounded by auto
have "convergent g"
using Bseq_monoseq_convergent'_inc bseq g_mono by blast
then obtain l where l_conv: "g ⇢ l" using convergentD by auto
have S_upper: "y ≤ B" if "N ≤ n" "y ∈ DQ n" for n y
using abs_le_D1[OF dq_bound] DQ_def I_def that by auto
have S_bdd_above: "bdd_above (DQ n)" if "N ≤ n" for n
using S_upper[OF ‹N ≤ n›] by fastforce
define h where "h ≡ λn. Sup (DQ n)"
have h_mono: "h n ≤ h m" if "N ≤ m" "m ≤ n" for m n
by (simp add: S_bdd_above S_nonempty S_subset cSup_subset_mono h_def that)
have h_bounded: "norm (h (n+N)) ≤ B" for n
proof -
have nN: "N ≤ n + N" by simp
have upper: "h (n+N) ≤ B"
using cSup_le_iff[OF S_nonempty S_bdd_above[OF nN]]
by (metis S_upper add.commute h_def le_add1)
obtain u where u: "u ∈ ball x (inverse (real (n+N) + 1))" "u ∈ {a..b}" "u ≠ x"
using balls_nonempty[of "n + N"] I_def by auto
have mem: "(f u - f x) / (u-x) ∈ DQ (n+N)"
unfolding DQ_def I_def using u by auto
have "(f u - f x) / (u-x) ≤ h (n+N)"
unfolding h_def by (rule cSup_upper[OF mem S_bdd_above[OF nN]])
moreover have "- B ≤ (f u - f x) / (u-x)"
using abs_le_D2[OF dq_bound[OF nN u(1) u(3)]] by linarith
ultimately have lower: "- B ≤ h (n+N)" by linarith
from upper lower show ?thesis
by (simp add: abs_le_iff)
qed
have bseq_h: "Bseq (λn. h (n+N))"
unfolding Bseq_def using ‹B > 0› h_bounded by auto
obtain m where m_conv: "h ⇢ m"
using convergentD Bseq_monoseq_convergent'_dec bseq_h h_mono by blast
have diff_conv: "(λn. h n - g n) ⇢ m - l"
by (rule tendsto_diff[OF m_conv l_conv])
have "k ≤ (λn. h n - g n) n" if "N ≤ n" for n
proof -
obtain u v where uv: "u ∈ I n x" "v ∈ I n x" "u ≠ x" "v ≠ x"
and kle: "k ≤ (f v - f x) / (v-x) - (f u - f x) / (u-x)"
by (meson xab xprop)
have *: "(f u - f x) / (u-x) ∈ DQ n" "(f v - f x) / (v-x) ∈ DQ n"
unfolding DQ_def using uv by auto
have "g n ≤ (f u - f x) / (u-x)"
by (simp add: "*" S_bdd g_def cInf_lower that)
moreover have "(f v - f x) / (v-x) ≤ h n"
by (simp add: "*" S_bdd_above h_def cSup_upper that)
ultimately show "k ≤ (λn. h n - g n) n" using kle by linarith
qed
then have k_le: "k ≤ m - l" using Lim_bounded2[OF diff_conv]
by blast
have mid: "(l+m) / 2 - k / 6 < (l+m) / 2 + k / 6"
using assms by auto
then obtain q where q: "q ∈ ℚ" "(l+m) / 2 - k / 6 < q" "q < (l+m) / 2 + k / 6"
using Rats_dense_in_real by blast
with k_le ‹0 < k› have q_l: "k / 3 < q - l" and q_m: "k / 3 < m - q"
by (auto simp add: field_simps)
have main: "∃u v. u ∈ I n x ∧ v ∈ I n x ∧ u ≠ x ∧ v ≠ x ∧
k / 3 ≤ (f v - f x) / (v-x) - q ∧
(f u - f x) / (u-x) - q ≤ - (k/3)" for n
proof -
have neg_lower: False
if A: "∀u. u ∈ I n x ∧ u ≠ x ⟶ q - k / 3 ≤ (f u - f x) / (u-x)"
proof -
have lb: "q - k / 3 ≤ y" if "y ∈ DQ p" "n ≤ p" for y p
using S_subset[OF that(2)] that(1) using A DQ_def by auto
have "q - k / 3 ≤ g p" if "max n N ≤ p" for p
proof -
have "q - k / 3 ≤ Inf (DQ p)"
using le_cInf_iff[OF S_nonempty S_bdd[OF max.cobounded2[THEN le_trans[OF _ that]]]]
lb[OF _ max.cobounded1[THEN le_trans[OF _ that]]]
by auto
then show ?thesis unfolding g_def .
qed
with Lim_bounded2[OF l_conv] have "q - k / 3 ≤ l" by blast
with q_l show False by linarith
qed
have neg_upper: False
if A: "∀v. v ∈ I n x ∧ v ≠ x ⟶ (f v - f x) / (v-x) ≤ k / 3 + q"
proof -
have ub: "y ≤ k / 3 + q" if "y ∈ DQ p" "n ≤ p" for y p
using S_subset[OF that(2)] that(1) using A DQ_def by auto
have "h p ≤ k / 3 + q" if "max n N ≤ p" for p
proof -
have "Sup (DQ p) ≤ k / 3 + q"
using cSup_le_iff[OF S_nonempty S_bdd_above[OF max.cobounded2[THEN le_trans[OF _ that]]]]
ub[OF _ max.cobounded1[THEN le_trans[OF _ that]]]
by auto
then show ?thesis unfolding h_def .
qed
then have "∀p ≥ max n N. h p ≤ k / 3 + q" by auto
with Lim_bounded[OF m_conv] have "m ≤ k / 3 + q" .
with q_m show False by linarith
qed
show ?thesis
by (smt (verit) neg_lower neg_upper)
qed
have "x ∈ S q" unfolding S_def using xab main by auto
with ‹q ∈ ℚ› q_l show ?thesis
by blast
qed
qed
qed
qed
lemma Lebesgue_diff_aux5:
fixes f :: "real ⇒ real" and a b k :: real
assumes f: "has_bounded_variation_on f {a..b}" and "a < b" "0 < k"
defines "I n x ≡ ball x (inverse (real n + 1)) ∩ {a..b}"
shows "negligible
{x ∈ {a..b}.
∀n::nat. ∃u v. u ∈ I n x ∧ v ∈ I n x ∧ u ≠ x ∧ v ≠ x ∧
k ≤ ¦(f v - f x) / (v-x) - (f u - f x) / (u-x)¦}"
proof -
have neg_union: "negligible (
{x ∈ {a..b}.
∀n::nat. ∃u v. u ∈ I n x ∧ v ∈ I n x ∧
u ≠ x ∧ v ≠ x ∧
k ≤ (f v - f x) / (v-x) - (f u - f x) / (u-x)} ∪
{x ∈ {a..b}.
∀n::nat. ∃u v. u ∈ I n x ∧ v ∈ I n x ∧
u ≠ x ∧ v ≠ x ∧
k ≤ ((-f v) - (-f x)) / (v-x) - ((-f u) - (-f x)) / (u-x)})"
using Lebesgue_diff_aux4 assms unfolding I_def
by (blast intro: negligible_Un has_bounded_variation_on_neg[OF f])+
then show ?thesis
proof (rule negligible_subset)
show "{x ∈ {a..b}.
∀n::nat. ∃u v. u ∈ I n x ∧ v ∈ I n x ∧
u ≠ x ∧ v ≠ x ∧
k ≤ ¦(f v - f x) / (v-x) - (f u - f x) / (u-x)¦} ⊆
{x ∈ {a..b}. ∀n::nat. ∃u v. u ∈ I n x ∧ v ∈ I n x ∧
u ≠ x ∧ v ≠ x ∧
k ≤ (f v - f x) / (v-x) - (f u - f x) / (u-x)} ∪
{x ∈ {a..b}. ∀n::nat. ∃u v. u ∈ I n x ∧ v ∈ I n x ∧
u ≠ x ∧ v ≠ x ∧
k ≤ ((-f v) - (-f x)) / (v-x) - ((-f u) - (-f x)) / (u-x)}"
proof (rule subsetI)
fix x assume x: "x ∈ {x ∈ {a..b}.
∀n::nat. ∃u v. u ∈ I n x ∧ v ∈ I n x ∧
u ≠ x ∧ v ≠ x ∧
k ≤ ¦(f v - f x) / (v-x) - (f u - f x) / (u-x)¦}"
have "∃u v. (u ∈ I m x ∧ v ∈ I m x ∧ u ≠ x ∧ v ≠ x ∧
k ≤ (f v - f x) / (v-x) - (f u - f x) / (u-x)) ∨
(u ∈ I n x ∧ v ∈ I n x ∧ u ≠ x ∧ v ≠ x ∧
k ≤ ((-f v) - (-f x)) / (v-x) - ((-f u) - (-f x)) / (u-x))" for m n
proof -
from x
obtain u v where uv: "u ∈ I (m+n) x" "v ∈ I (m+n) x" "u ≠ x" "v ≠ x"
"k ≤ ¦(f v - f x) / (v-x) - (f u - f x) / (u-x)¦"
by blast
have ball_m: "ball x (inverse (real (m+n) + 1)) ⊆ ball x (inverse (real m + 1))"
by (intro subset_ball le_imp_inverse_le) linarith+
have ball_n: "ball x (inverse (real (m+n) + 1)) ⊆ ball x (inverse (real n + 1))"
by (intro subset_ball le_imp_inverse_le) linarith+
from uv have "k ≤ (f v - f x) / (v-x) - (f u - f x) / (u-x) ∨
k ≤ -((f v - f x) / (v-x) - (f u - f x) / (u-x))"
by linarith
then show ?thesis
using uv ball_m ball_n x unfolding I_def
by (smt (verit, ccfv_threshold) mem_Collect_eq)
qed
then show "x ∈ {x ∈ {a..b}. ∀n::nat. ∃u v. u ∈ I n x ∧ v ∈ I n x ∧ u ≠ x ∧ v ≠ x ∧
k ≤ (f v - f x) / (v-x) - (f u - f x) / (u-x)} ∪
{x ∈ {a..b}. ∀n::nat. ∃u v. u ∈ I n x ∧ v ∈ I n x ∧ u ≠ x ∧ v ≠ x ∧
k ≤ ((-f v) - (-f x)) / (v-x) - ((-f u) - (-f x)) / (u-x)}"
by (smt (verit) UnCI mem_Collect_eq x)
qed
qed
qed
lemma Lebesgue_diff_aux6:
fixes f :: "real ⇒ real"
assumes "has_bounded_variation_on f {a..b}" "a < b"
defines "I ≡ λn x. ball x (inverse (real n + 1)) ∩ {a..b}"
shows "negligible {x ∈ {a..b}. ¬ f differentiable (at x within {a..b})}"
proof -
have "negligible {x ∈ {a..b}. ¬ (∃f'. ((λy. (f y - f x) / (y-x)) ⤏ f') (at x within {a..b}))}"
proof -
define S where "S m = {x ∈ {a..b}.
∀n::nat. ∃u v. u ∈ I n x ∧ v ∈ I n x ∧ u ≠ x ∧ v ≠ x ∧
inverse (real m + 1) ≤ ¦(f v - f x) / (v-x) - (f u - f x) / (u-x)¦}" for m
have neg: "negligible (S m)" for m
unfolding S_def using Lebesgue_diff_aux5 assms by auto
have "negligible (⋃(range S))"
by (rule negligible_Union_nat[OF neg])
moreover have "{x ∈ {a..b}. ¬ (∃f'. ((λy. (f y - f x) / (y-x)) ⤏ f') (at x within {a..b}))} ⊆ ⋃(range S)"
proof (rule subsetI)
fix x assume x: "x ∈ {x ∈ {a..b}. ¬ (∃f'. ((λy. (f y - f x) / (y-x)) ⤏ f') (at x within {a..b}))}"
then obtain e where "e > 0" and osc: "∀d>0. ∃u∈{a..b}. ∃v∈{a..b}.
u ≠ x ∧ dist u x < d ∧ v ≠ x ∧ dist v x < d ∧
e ≤ dist ((f u - f x) / (u-x)) ((f v - f x) / (v-x))"
unfolding convergent_eq_Cauchy_within by (force simp: not_less)
obtain m where m: "inverse (real m + 1) < e"
using reals_Archimedean[OF ‹e > 0›] by (metis add.commute of_nat_Suc)
have "x ∈ S m"
unfolding S_def
proof (intro CollectI conjI allI)
fix n :: nat
have "inverse (real n + 1) > 0" by auto
with osc obtain u v where "u ∈ {a..b}" "v ∈ {a..b}" "u ≠ x" "dist u x < inverse (real n + 1)"
"v ≠ x" "dist v x < inverse (real n + 1)"
"e ≤ dist ((f u - f x) / (u-x)) ((f v - f x) / (v-x))"
by blast
then have "inverse (real m + 1) ≤ ¦(f v - f x) / (v-x) - (f u - f x) / (u-x)¦"
using m by (simp add: dist_real_def)
moreover have "u ∈ ball x (inverse (real n + 1))" "v ∈ ball x (inverse (real n + 1))"
using ‹dist u x < inverse (real n + 1)› ‹dist v x < inverse (real n + 1)›
by (simp_all add: dist_commute)
ultimately show "∃u v. u ∈ I n x ∧ v ∈ I n x ∧ u ≠ x ∧ v ≠ x ∧
inverse (real m + 1) ≤ ¦(f v - f x) / (v-x) - (f u - f x) / (u-x)¦"
using ‹u ∈ {a..b}› ‹v ∈ {a..b}› ‹u ≠ x› ‹v ≠ x›
using I_def by blast
qed (use x in auto)
then show "x ∈ ⋃(range S)" by auto
qed
ultimately show ?thesis by (rule negligible_subset)
qed
moreover
have "⋀x. f differentiable (at x within {a..b}) ⟷
(∃D. ((λy. (f y - f x) / (y-x)) ⤏ D) (at x within {a..b}))"
unfolding vector_differentiable has_vector_derivative_within_1D
by (simp add: mult.commute[of "inverse _"] divide_inverse)
ultimately show ?thesis by simp
qed
theorem Lebesgue_differentiation_thm_compact:
fixes f :: "real ⇒ 'a::euclidean_space"
assumes "has_bounded_variation_on f (cbox a b)"
shows "negligible {x ∈ cbox a b. ¬ f differentiable (at x)}"
proof -
let ?g = "λi. (λx. f x ∙ i)"
have cw: "(f differentiable at x) = (∀i∈Basis. ?g i differentiable at x)" for x
proof -
have "at x within UNIV = at x" by (rule at_within_open[OF UNIV_I open_UNIV])
then show ?thesis using differentiable_componentwise_within[where S=UNIV and a=x and f=f]
by simp
qed
have eq: "{x ∈ cbox a b. ¬ f differentiable (at x)} =
(⋃i∈Basis. {x ∈ cbox a b. ¬ ?g i differentiable (at x)})"
by (auto simp: cw)
show ?thesis unfolding eq
proof (rule negligible_Union[OF finite_imageI[OF finite_Basis]], clarsimp)
fix i :: 'a assume "i ∈ Basis"
show "negligible {x. a ≤ x ∧ x ≤ b ∧ ¬ ?g i differentiable (at x)}"
proof (cases "a < b")
case True
have sub: "{x ∈ {a..b}. ¬ ?g i differentiable (at x)} ⊆
insert a (insert b {x ∈ {a..b}. ¬ ?g i differentiable (at x within {a..b})})"
by (auto simp: at_within_Icc_at)
have "negligible (insert a (insert b {x ∈ {a..b}. ¬ ?g i differentiable (at x within {a..b})}))"
using Lebesgue_diff_aux6 [OF has_bounded_variation_on_inner_left] assms True by auto
with negligible_subset [OF _ sub] show ?thesis by simp
next
case False
then show ?thesis
by (force intro: negligible_subset[OF negligible_sing[of a]])
qed
qed
qed
lemma Lebesgue_differentiation_thm_open:
fixes f :: "real ⇒ 'a::euclidean_space"
assumes "open S" "has_bounded_variation_on f S"
shows "negligible {x ∈ S. ¬ f differentiable (at x)}"
proof -
obtain 𝒟 where cnt: "countable 𝒟" and sub: "𝒟 ⊆ Pow S"
and boxes: "⋀X. X ∈ 𝒟 ⟹ ∃a b. X = cbox a b" and cov: "⋃ 𝒟 = S"
using open_countable_Union_open_cbox[OF assms(1)] by metis
have eq: "{x ∈ S. ¬ f differentiable (at x)} = ⋃ ((λT. {x ∈ T. ¬ f differentiable (at x)}) ` 𝒟)"
using cov by auto
have "negligible (⋃ ((λT. {x ∈ T. ¬ f differentiable (at x)}) ` 𝒟))"
proof (rule negligible_countable_Union)
show "countable ((λT. {x ∈ T. ¬ f differentiable (at x)}) ` 𝒟)"
using cnt by (rule countable_image)
next
fix U assume "U ∈ (λT. {x ∈ T. ¬ f differentiable (at x)}) ` 𝒟"
then obtain T where T: "T ∈ 𝒟" and Seq: "U = {x ∈ T. ¬ f differentiable (at x)}"
by auto
obtain a b where Tab: "T = cbox a b" using boxes[OF T] by auto
have "has_bounded_variation_on f T"
using has_bounded_variation_on_subset[OF assms(2)] sub T by auto
then show "negligible U"
unfolding Seq Tab
by (rule Lebesgue_differentiation_thm_compact)
qed
then show ?thesis using eq by simp
qed
corollary Lebesgue_differentiation_thm:
fixes f :: "real ⇒ 'a::euclidean_space"
assumes "is_interval S" "has_bounded_variation_on f S"
shows "negligible {x ∈ S. ¬ f differentiable (at x)}"
proof -
have sub: "{x ∈ S. ¬ f differentiable (at x)} ⊆
{x ∈ frontier S. ¬ f differentiable (at x)} ∪
{x ∈ interior S. ¬ f differentiable (at x)}"
using closure_subset[of S] by (auto simp: frontier_def)
have fr: "negligible {x ∈ frontier S. ¬ f differentiable (at x)}"
proof (rule negligible_subset[OF negligible_finite])
show "finite (frontier S)"
using finite_frontier_interval_real[OF assms(1)] by blast
show "{x ∈ frontier S. ¬ f differentiable (at x)} ⊆ frontier S"
by auto
qed
have int: "negligible {x ∈ interior S. ¬ f differentiable (at x)}"
proof -
have bv: "has_bounded_variation_on f (interior S)"
using has_bounded_variation_on_subset[OF assms(2) interior_subset] .
have op: "open (interior S)" by (rule open_interior)
show ?thesis using Lebesgue_differentiation_thm_open[OF op bv] .
qed
show ?thesis
using negligible_subset[OF negligible_Un[OF fr int] sub] .
qed
corollary Lebesgue_differentiation_thm_alt:
fixes f :: "real ⇒ 'a::euclidean_space"
assumes "is_interval S" "has_bounded_variation_on f S"
shows "∃t. t ⊆ S ∧ negligible t ∧ (∀x ∈ S - t. f differentiable (at x))"
proof -
let ?t = "{x ∈ S. ¬ f differentiable (at x)}"
have "?t ⊆ S" "negligible ?t"
using Lebesgue_differentiation_thm[OF assms] by auto
moreover have "∀x ∈ S - ?t. f differentiable (at x)" by auto
ultimately show ?thesis by blast
qed
corollary Lebesgue_differentiation_thm_gen:
fixes f :: "real ⇒ 'a::euclidean_space"
assumes "countable (components S)" "has_bounded_variation_on f S"
shows "negligible {x ∈ S. ¬ f differentiable (at x)}" proof -
have "∃y∈components S. x ∈ y"
if "x ∈ S" and "¬ f differentiable at x"
for x
using that
by (metis UnionE Union_components)
then have eq: "{x ∈ S. ¬ f differentiable (at x)} =
⋃ ((λC. {x ∈ C. ¬ f differentiable (at x)}) ` components S)"
using in_components_subset by blast
show ?thesis unfolding eq
proof (rule negligible_countable_Union)
show "countable ((λC. {x ∈ C. ¬ f differentiable (at x)}) ` components S)"
using assms(1) by (rule countable_image)
next
fix U assume "U ∈ (λC. {x ∈ C. ¬ f differentiable (at x)}) ` components S"
then obtain C where C: "C ∈ components S" and Seq: "U = {x ∈ C. ¬ f differentiable (at x)}"
by auto
have "is_interval C"
using in_components_connected[OF C] is_interval_connected_1 by auto
moreover have "has_bounded_variation_on f C"
using has_bounded_variation_on_subset[OF assms(2) in_components_subset[OF C]] .
ultimately show "negligible U"
unfolding Seq by (rule Lebesgue_differentiation_thm)
qed
qed
corollary Lebesgue_differentiation_thm_increasing:
fixes f :: "real ⇒ real"
assumes "is_interval S" "mono_on S f"
shows "negligible {x ∈ S. ¬ f differentiable (at x)}"
proof -
let ?N = "{x ∈ S. ¬ f differentiable (at x)}"
have "locally negligible ?N"
unfolding locally_def
proof (intro allI impI)
fix w x assume wx: "openin (top_of_set ?N) w ∧ x ∈ w"
then have xN: "x ∈ ?N" using openin_imp_subset by blast
then have "x ∈ S" by simp
from interval_contains_compact_neighbourhood[OF ‹is_interval S› this]
obtain a b d where "0 < d" "x ∈ cbox a b" "cbox a b ⊆ S"
and ball_sub: "ball x d ∩ S ⊆ cbox a b"
by auto
have mono_ab: "mono_on {a..b} f"
using mono_on_subset[OF ‹mono_on S f› ‹cbox a b ⊆ S›] by (simp add: cbox_interval)
have neg: "negligible {y ∈ cbox a b. ¬ f differentiable (at y)}"
by (rule Lebesgue_differentiation_thm_compact[OF
increasing_bounded_variation[OF mono_ab, folded cbox_interval]])
let ?U = "w ∩ ball x d"
let ?V = "{y ∈ cbox a b. ¬ f differentiable (at y)} ∩ w"
have U_open: "openin (top_of_set ?N) ?U"
using wx by (auto intro!: openin_Int_open[OF _ open_ball])
have "x ∈ ?U" using wx ‹0 < d› by auto
moreover have "?U ⊆ ?V"
using wx openin_imp_subset ball_sub by fastforce
moreover have "?V ⊆ w" by auto
ultimately show "∃U V. openin (top_of_set ?N) U ∧ negligible V ∧ x ∈ U ∧ U ⊆ V ∧ V ⊆ w"
using U_open negligible_subset[OF neg] by (meson inf_le1)
qed
then show ?thesis by (simp add: locally_negligible)
qed
corollary Lebesgue_differentiation_thm_decreasing:
fixes f :: "real ⇒ real"
assumes "is_interval S" "antimono_on S f"
shows "negligible {x ∈ S. ¬ f differentiable (at x)}"
proof -
have mono: "mono_on S (λx. - f x)"
using assms(2) by (auto simp: monotone_on_def)
have sub: "{x ∈ S. ¬ f differentiable (at x)} ⊆ {x ∈ S. ¬ (λx. - f x) differentiable (at x)}"
using differentiable_minus[of "(λx. - f x)"] by auto
moreover have "negligible {x ∈ S. ¬ (λx. - f x) differentiable (at x)}"
by (rule Lebesgue_differentiation_thm_increasing[OF assms(1) mono])
ultimately show ?thesis by (rule negligible_subset[rotated])
qed
end