Theory HOL-Analysis.Bounded_Variation
theory Bounded_Variation
imports Henstock_Kurzweil_Integration Starlike
begin
text ‹
Bounded variation and vector variation for functions @{typ "real ⇒ 'a::euclidean_space"},
following HOL Light's @{text "Multivariate/integration.ml"}.
HOL Light works with @{text "real^1 ⇒ real^N"} and defines bounded variation via
set variation of the increment function. We adapt this to Isabelle's @{typ real}
domain directly.
›
section ‹Set variation›
definition set_variation :: "real set ⇒ (real set ⇒ 'a::euclidean_space) ⇒ real" where
"set_variation S f = Sup {(∑k∈d. norm (f k)) | d. ∃T. d division_of T ∧ T ⊆ S}"
definition has_bounded_setvariation_on ::
"(real set ⇒ 'a::euclidean_space) ⇒ real set ⇒ bool" where
"has_bounded_setvariation_on f S ⟷
(∃B. ∀d T. d division_of T ∧ T ⊆ S ⟶ (∑k∈d. norm (f k)) ≤ B)"
section ‹Bounded variation for functions›
definition has_bounded_variation_on ::
"(real ⇒ 'a::euclidean_space) ⇒ real set ⇒ bool" where
"has_bounded_variation_on f S ⟷
has_bounded_setvariation_on (λk. f (Sup k) - f (Inf k)) S"
definition vector_variation :: "real set ⇒ (real ⇒ 'a::euclidean_space) ⇒ real" where
"vector_variation S f = set_variation S (λk. f (Sup k) - f (Inf k))"
subsection ‹Closure and subset properties›
lemma has_bounded_variation_on_subset:
"has_bounded_variation_on f S ⟹ T ⊆ S ⟹ has_bounded_variation_on f T"
unfolding has_bounded_variation_on_def has_bounded_setvariation_on_def
by (meson order_trans)
lemma has_bounded_variation_on_const:
"has_bounded_variation_on (λx. c) S"
unfolding has_bounded_variation_on_def has_bounded_setvariation_on_def
by (rule exI[of _ 0]) simp
lemma has_bounded_variation_on_cmul:
"has_bounded_variation_on f S ⟹ has_bounded_variation_on (λx. a *⇩R f x) S"
unfolding has_bounded_variation_on_def has_bounded_setvariation_on_def
proof -
assume "∃B. ∀d T. d division_of T ∧ T ⊆ S ⟶
(∑k∈d. norm (f (Sup k) - f (Inf k))) ≤ B"
then obtain B where B: "⋀d T. d division_of T ⟹ T ⊆ S ⟹
(∑k∈d. norm (f (Sup k) - f (Inf k))) ≤ B"
by meson
show "∃B. ∀d T. d division_of T ∧ T ⊆ S ⟶
(∑k∈d. norm (a *⇩R f (Sup k) - a *⇩R f (Inf k))) ≤ B"
proof (intro exI allI impI)
fix d T assume §: "d division_of T ∧ T ⊆ S"
have "(∑k∈d. norm (a *⇩R f (Sup k) - a *⇩R f (Inf k))) =
(∑k∈d. ¦a¦ * norm (f (Sup k) - f (Inf k)))"
by (simp add: scaleR_diff_right[symmetric])
also have "… = ¦a¦ * (∑k∈d. norm (f (Sup k) - f (Inf k)))"
by (simp add: sum_distrib_left)
also have "… ≤ ¦a¦ * B"
using B § abs_ge_zero mult_left_mono by blast
finally show "(∑k∈d. norm (a *⇩R f (Sup k) - a *⇩R f (Inf k))) ≤ ¦a¦ * B" .
qed
qed
lemma has_bounded_variation_on_neg:
"has_bounded_variation_on f S ⟹ has_bounded_variation_on (λx. - f x) S"
using has_bounded_variation_on_cmul[of f S "-1"]
by simp
lemma has_bounded_variation_on_add:
"has_bounded_variation_on f S ⟹ has_bounded_variation_on g S ⟹
has_bounded_variation_on (λx. f x + g x) S"
unfolding has_bounded_variation_on_def has_bounded_setvariation_on_def
proof -
assume "∃B. ∀d T. d division_of T ∧ T ⊆ S ⟶
(∑k∈d. norm (f (Sup k) - f (Inf k))) ≤ B"
then obtain Bf where Bf: "⋀d T. d division_of T ⟹ T ⊆ S ⟹
(∑k∈d. norm (f (Sup k) - f (Inf k))) ≤ Bf"
by blast
assume "∃B. ∀d T. d division_of T ∧ T ⊆ S ⟶
(∑k∈d. norm (g (Sup k) - g (Inf k))) ≤ B"
then obtain Bg where Bg: "⋀d T. d division_of T ⟹ T ⊆ S ⟹
(∑k∈d. norm (g (Sup k) - g (Inf k))) ≤ Bg"
by blast
show "∃B. ∀d T. d division_of T ∧ T ⊆ S ⟶
(∑k∈d. norm (f (Sup k) + g (Sup k) - (f (Inf k) + g (Inf k)))) ≤ B"
proof (intro exI allI impI)
fix d T assume §: "d division_of T ∧ T ⊆ S"
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)) + (g (Sup k) - g (Inf k))))"
by (simp add: algebra_simps)
also have "… ≤ (∑k∈d. norm (f (Sup k) - f (Inf k)) + norm (g (Sup k) - g (Inf k)))"
by (intro sum_mono norm_triangle_ineq)
also have "… ≤ Bf + Bg"
by (metis (mono_tags) Bf Bg § add_mono sum.distrib)
finally show "(∑k∈d. norm (f (Sup k) + g (Sup k) - (f (Inf k) + g (Inf k)))) ≤ Bf + Bg" .
qed
qed
lemma has_bounded_variation_on_sub:
"has_bounded_variation_on f S ⟹ has_bounded_variation_on g S ⟹
has_bounded_variation_on (λx. f x - g x) S"
using has_bounded_variation_on_add[of f S "λx. - g x"]
has_bounded_variation_on_neg[of g S]
by simp
lemma has_bounded_variation_on_norm:
assumes "has_bounded_variation_on f S"
shows "has_bounded_variation_on (λx. norm (f x) *⇩R e) S"
unfolding has_bounded_variation_on_def has_bounded_setvariation_on_def
proof -
obtain B where B: "⋀d T. d division_of T ⟹ T ⊆ S ⟹
(∑k∈d. norm (f (Sup k) - f (Inf k))) ≤ B"
using assms
by (metis (full_types) has_bounded_setvariation_on_def has_bounded_variation_on_def)
show "∃B. ∀d T. d division_of T ∧ T ⊆ S ⟶
(∑k∈d. norm (norm (f (Sup k)) *⇩R e - norm (f (Inf k)) *⇩R e)) ≤ B"
proof (intro exI allI impI)
fix d T assume dt: "d division_of T ∧ T ⊆ S"
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])
also have "… ≤ (∑k∈d. norm (f (Sup k) - f (Inf k)) * norm e)"
by (intro sum_mono mult_right_mono) (auto simp: norm_triangle_ineq3)
also have "… = (∑k∈d. norm (f (Sup k) - f (Inf k))) * norm e"
by (simp add: sum_distrib_right)
also have "… ≤ B * norm e"
using B dt landau_o.R_mult_right_mono by force
finally show "(∑k∈d. norm (norm (f (Sup k)) *⇩R e - norm (f (Inf k)) *⇩R e)) ≤ B * norm e" .
qed
qed
lemma has_bounded_variation_on_inner_left:
assumes ‹has_bounded_variation_on f S›
shows ‹has_bounded_variation_on (λx. f x ∙ b) S›
unfolding has_bounded_variation_on_def has_bounded_setvariation_on_def
proof -
from assms obtain B where B: ‹⋀d T. d division_of T ⟹ T ⊆ S ⟹
(∑k∈d. norm (f (Sup k) - f (Inf k))) ≤ B›
unfolding has_bounded_variation_on_def has_bounded_setvariation_on_def by meson
show ‹∃B. ∀d T. d division_of T ∧ T ⊆ S ⟶ (∑k∈d. norm (f (Sup k) ∙ b - f (Inf k) ∙ b)) ≤ B›
proof (intro exI[of _ ‹B * norm b›] allI impI)
fix d T assume dt: ‹d division_of T ∧ T ⊆ S›
have ‹(∑k∈d. norm (f (Sup k) ∙ b - f (Inf k) ∙ b)) =
(∑k∈d. ¦(f (Sup k) - f (Inf k)) ∙ b¦)›
by (simp add: inner_diff_left)
also have ‹… ≤ (∑k∈d. norm (f (Sup k) - f (Inf k)) * norm b)›
by (intro sum_mono) (auto simp: Cauchy_Schwarz_ineq2)
also have ‹… = (∑k∈d. norm (f (Sup k) - f (Inf k))) * norm b›
by (simp add: sum_distrib_right)
also have ‹… ≤ B * norm b›
using B dt by (intro mult_right_mono) auto
finally show ‹(∑k∈d. norm (f (Sup k) ∙ b - f (Inf k) ∙ b)) ≤ B * norm b› .
qed
qed
subsection ‹Other fundamental properties›
lemma has_bounded_variation_on_interval:
"has_bounded_variation_on f {a..b} ⟷
(∃B. ∀d. d division_of {a..b} ⟶
(∑k∈d. norm (f (Sup k) - f (Inf k))) ≤ B)" (is "_ = ?R")
unfolding has_bounded_variation_on_def has_bounded_setvariation_on_def
proof
assume ?R
then obtain B where B: "⋀d. d division_of {a..b} ⟹ (∑k∈d. norm (f (Sup k) - f (Inf k))) ≤ B"
by auto
show "∃B. ∀d T. d division_of T ∧ T ⊆ {a..b} ⟶ (∑k∈d. norm (f (Sup k) - f (Inf k))) ≤ B"
proof (intro exI allI impI)
fix d T
assume dt: "d division_of T ∧ T ⊆ {a..b}"
then obtain q where dq: "d ⊆ q" and q_div: "q division_of cbox a b"
by (metis elementary_interval interval_cbox partial_division_extend)
have q_div': "q division_of {a..b}"
using q_div unfolding cbox_interval .
have fin_q: "finite q"
using division_of_finite[OF q_div] .
have "(∑k∈d. norm (f (Sup k) - f (Inf k))) ≤ (∑k∈q. norm (f (Sup k) - f (Inf k)))"
by (rule sum_mono2[OF fin_q dq]) auto
also have "… ≤ B"
using B[OF q_div'] .
finally show "(∑k∈d. norm (f (Sup k) - f (Inf k))) ≤ B" .
qed
qed auto
lemma vector_variation_on_interval:
assumes "has_bounded_variation_on f {a..b}"
shows "vector_variation {a..b} f =
Sup {(∑k∈d. norm (f (Sup k) - f (Inf k))) | d. d division_of {a..b}}"
proof -
let ?g = "λk. f (Sup k) - f (Inf k)"
define A where "A ≡ {(∑k∈d. norm (?g k)) | d. ∃T. d division_of T ∧ T ⊆ {a..b}}"
define B where "B ≡ {(∑k∈d. norm (?g k)) | d. d division_of {a..b}}"
have vv: "vector_variation {a..b} f = Sup A"
unfolding vector_variation_def set_variation_def A_def by simp
have B_sub_A: "B ⊆ A" unfolding A_def B_def by blast
have B_ne: "B ≠ {}"
by (metis (mono_tags, lifting) B_def Collect_empty_eq box_real(2)
elementary_interval)
have A_ne: "A ≠ {}" using B_sub_A B_ne by auto
have bdd_A: "bdd_above A"
proof -
from assms obtain M where M: "∀d T. d division_of T ∧ T ⊆ {a..b} ⟶
(∑k∈d. norm (?g k)) ≤ M"
unfolding has_bounded_variation_on_def has_bounded_setvariation_on_def by auto
show ?thesis unfolding bdd_above_def A_def
using M by blast
qed
have bdd_B: "bdd_above B"
using bdd_above_mono[OF bdd_A B_sub_A] .
have A_le_B: "∀x ∈ A. ∃y ∈ B. x ≤ y"
proof
fix x assume "x ∈ A"
then obtain d T where dt: "d division_of T" "T ⊆ {a..b}"
and x_eq: "x = (∑k∈d. norm (?g k))" unfolding A_def by auto
then obtain q where dq: "d ⊆ q" and q_div: "q division_of {a..b}"
using partial_division_extend_interval
by (metis (no_types, opaque_lifting) division_ofD(6) interval_cbox)
have "x ≤ (∑k∈q. norm (?g k))"
unfolding x_eq by (rule sum_mono2[OF division_of_finite[OF q_div] dq]) auto
moreover have "(∑k∈q. norm (?g k)) ∈ B" unfolding B_def using q_div by auto
ultimately show "∃y ∈ B. x ≤ y" by auto
qed
have "Sup A = Sup B"
by (meson A_le_B A_ne B_ne B_sub_A bdd_A bdd_B cSup_mono cSup_subset_mono order.eq_iff)
with vv show ?thesis unfolding B_def by simp
qed
lemma vector_variation_pos_le:
assumes "has_bounded_variation_on f {a..b}"
shows "0 ≤ vector_variation {a..b} f"
proof -
have "vector_variation {a..b} f =
Sup {(∑k∈d. norm (f (Sup k) - f (Inf k))) | d. d division_of {a..b}}"
using vector_variation_on_interval[OF assms] .
moreover have "0 ≤ Sup {(∑k∈d. norm (f (Sup k) - f (Inf k))) | d. d division_of {a..b}}"
proof -
let ?S = "{(∑k∈d. norm (f (Sup k) - f (Inf k))) | d. d division_of {a..b}}"
obtain p where p: "p division_of cbox a b" using elementary_interval by blast
then have "(∑k∈p. norm (f (Sup k) - f (Inf k))) ∈ ?S"
by (auto simp: cbox_interval)
moreover have "0 ≤ (∑k∈p. norm (f (Sup k) - f (Inf k)))"
by (intro sum_nonneg) auto
moreover have "bdd_above ?S"
using assms by (auto simp: bdd_above_def has_bounded_variation_on_interval)
ultimately show "0 ≤ Sup ?S"
by (metis (no_types, lifting) cSup_upper2)
qed
ultimately show ?thesis by linarith
qed
lemma vector_variation_ge_norm_function:
assumes "has_bounded_variation_on f {a..b}" "x ∈ {a..b}" "y ∈ {a..b}"
shows "norm (f x - f y) ≤ vector_variation {a..b} f"
proof -
let ?g = "λk. f (Sup k) - f (Inf k)"
define S where "S ≡ {(∑k∈d. norm (?g k)) | d. ∃t. d division_of t ∧ t ⊆ {a..b}}"
have vv: "vector_variation {a..b} f = Sup S"
unfolding vector_variation_def set_variation_def S_def by simp
have bdd: "bdd_above S"
using assms unfolding bdd_above_def S_def has_bounded_variation_on_def has_bounded_setvariation_on_def
by blast
have "norm (f x - f y) = norm (f (min x y) - f (max x y))"
by (simp add: min_def max_def norm_minus_commute)
also have "… = norm (f (max x y) - f (min x y))"
by (simp add: norm_minus_commute)
also have "… ≤ Sup S"
proof -
let ?lo = "min x y" and ?hi = "max x y"
have lo_le_hi: "?lo ≤ ?hi" by simp
have sub: "{?lo..?hi} ⊆ {a..b}" using assms(2,3) by auto
have ne: "cbox ?lo ?hi ≠ {}" using lo_le_hi by (simp add: cbox_interval)
have div: "{{?lo..?hi}} division_of {?lo..?hi}"
using division_of_self[OF ne] by (simp add: cbox_interval)
have "norm (f ?hi - f ?lo) = (∑k∈{{?lo..?hi}}. norm (?g k))"
using lo_le_hi by (simp add: interval_bounds_real)
also have "… ∈ S" unfolding S_def using div sub by blast
finally show "norm (f ?hi - f ?lo) ≤ Sup S"
using cSup_upper[OF _ bdd] by auto
qed
also have "Sup S = vector_variation {a..b} f" using vv by simp
finally show ?thesis by simp
qed
lemma vector_variation_const_eq:
assumes "has_bounded_variation_on f {a..b}" "is_interval {a..b}"
shows "vector_variation {a..b} f = 0 ⟷ (∃c. ∀t ∈ {a..b}. f t = c)"
proof
assume vv0: "vector_variation {a..b} f = 0"
then show "∃c. ∀t ∈ {a..b}. f t = c"
by (metis assms(1) norm_pths(1) vector_variation_ge_norm_function)
next
assume "∃c. ∀t ∈ {a..b}. f t = c"
then obtain c where c: "⋀t. t ∈ {a..b} ⟹ f t = c" by auto
have eq: "vector_variation {a..b} f =
Sup {(∑k∈d. norm (f (Sup k) - f (Inf k))) | d. d division_of {a..b}}"
using vector_variation_on_interval[OF assms(1)] .
have all_zero: "⋀d. d division_of {a..b} ⟹ (∑k∈d. norm (f (Sup k) - f (Inf k))) = 0"
proof -
fix d assume div: "d division_of {a..b}"
show "(∑k∈d. norm (f (Sup k) - f (Inf k))) = 0"
proof (intro sum.neutral ballI)
fix k assume kd: "k ∈ d"
have ksub: "k ⊆ {a..b}" using division_ofD(2)[OF div kd] .
have kne: "k ≠ {}" using division_ofD(3)[OF div kd] .
obtain u v where kuv: "k = cbox u v" using division_ofD(4)[OF div kd] by auto
then have "k = {u..v}" by (simp add: cbox_interval)
with kne have uv: "u ≤ v" by auto
then show "norm (f (Sup k) - f (Inf k)) = 0"
using c ksub kuv by auto
qed
qed
obtain p where "p division_of {a..b}"
by (metis box_real(2) elementary_interval)
then have "{(∑k∈d. norm (f (Sup k) - f (Inf k))) | d. d division_of {a..b}} = {0}"
using all_zero by fastforce
with eq show "vector_variation {a..b} f = 0" using cSup_singleton by simp
qed
lemma vector_variation_on_null:
assumes "content {a..b} = 0"
shows "vector_variation {a..b} f = 0"
proof -
let ?g = "λk. f (Sup k) - f (Inf k)"
from assms have ba: "b ≤ a" using content_real_eq_0 by auto
have all_zero: "⋀d t. d division_of t ⟹ t ⊆ {a..b} ⟹
(∑k∈d. norm (?g k)) = 0"
proof -
fix d t assume div: "d division_of t" and sub: "t ⊆ {a..b}"
show "(∑k∈d. norm (?g k)) = 0"
proof (intro sum.neutral ballI)
fix k assume kd: "k ∈ d"
obtain u v where kuv: "k = {u..v}" and kne: "k ≠ {}" and ksub: "k ⊆ {a..b}"
by (metis cbox_division_memE div cbox_interval order.trans kd sub)
with ba have uv: "u = a" "v = a" by auto
then show "norm (?g k) = 0" unfolding ‹k = {u..v}›
by simp
qed
qed
have "{(∑k∈d. norm (?g k)) | d. ∃t. d division_of t ∧ t ⊆ {a..b}} = {0}"
using all_zero by (auto intro!: exI[of _ "{}"] exI[of _ "{}"])
then show ?thesis using cSup_singleton
by (simp add: set_variation_def vector_variation_def)
qed
lemma vector_variation_monotone:
assumes "has_bounded_variation_on f {a..b}" "{c..d} ⊆ {a..b}"
shows "vector_variation {c..d} f ≤ vector_variation {a..b} f"
proof -
let ?g = "λk. f (Sup k) - f (Inf k)"
define A where "A ≡ {(∑k∈p. norm (?g k)) | p. ∃t. p division_of t ∧ t ⊆ {a..b}}"
define C where "C ≡ {(∑k∈p. norm (?g k)) | p. ∃t. p division_of t ∧ t ⊆ {c..d}}"
have vvab: "vector_variation {a..b} f = Sup A"
unfolding vector_variation_def set_variation_def A_def by simp
have vvcd: "vector_variation {c..d} f = Sup C"
unfolding vector_variation_def set_variation_def C_def by simp
have C_sub_A: "C ⊆ A" unfolding C_def A_def using assms(2) by blast
have C_ne: "C ≠ {}"
using C_def division_of_trivial by blast
have bdd_A: "bdd_above A"
using assms
unfolding has_bounded_variation_on_def has_bounded_setvariation_on_def bdd_above_def A_def
by blast+
have "Sup C ≤ Sup A"
using cSup_subset_mono[OF C_ne bdd_A C_sub_A] .
with vvab vvcd show ?thesis by simp
qed
lemma has_bounded_setvariation_works:
assumes "has_bounded_setvariation_on f S"
shows "(⋀d T. d division_of T ⟹ T ⊆ S ⟹ (∑k∈d. norm (f k)) ≤ set_variation S f)"
and "(⋀B. (⋀d T. d division_of T ⟹ T ⊆ S ⟹ (∑k∈d. norm (f k)) ≤ B) ⟹
set_variation S f ≤ B)"
proof -
define U where "U = {∑k∈d. norm (f k) | d. ∃T. d division_of T ∧ T ⊆ S}"
have sv_eq: "set_variation S f = Sup U"
unfolding set_variation_def U_def ..
have U_ne: "U ≠ {}"
using U_def division_of_trivial by blast
have bdd: "bdd_above U"
using assms unfolding has_bounded_setvariation_on_def bdd_above_def U_def by blast
{
fix d T assume "d division_of T" "T ⊆ S"
then show "(∑k∈d. norm (f k)) ≤ set_variation S f"
using cSup_upper[OF _ bdd] unfolding sv_eq U_def by blast
}
{
fix B
assume "⋀d T. d division_of T ⟹ T ⊆ S ⟹ (∑k∈d. norm (f k)) ≤ B"
then show "set_variation S f ≤ B"
using cSup_le_iff[OF U_ne bdd] unfolding sv_eq U_def by blast
}
qed
lemma has_bounded_variation_works:
assumes "has_bounded_variation_on f S"
shows "(⋀d T. d division_of T ⟹ T ⊆ S ⟹
(∑k∈d. norm (f (Sup k) - f (Inf k))) ≤ vector_variation S f)"
and "(⋀B. (⋀d T. d division_of T ⟹ T ⊆ S ⟹
(∑k∈d. norm (f (Sup k) - f (Inf k))) ≤ B) ⟹
vector_variation S f ≤ B)"
using has_bounded_setvariation_works[of "λk. f (Sup k) - f (Inf k)" S] assms
unfolding vector_variation_def has_bounded_variation_on_def by auto
lemma vector_variation_le_component_sum:
assumes ‹has_bounded_variation_on f S›
shows ‹vector_variation S f ≤ (∑b∈Basis. vector_variation S (λu. f u ∙ b))›
proof (rule has_bounded_variation_works(2)[OF assms])
fix d T assume dt: ‹d division_of T› ‹T ⊆ S›
have ‹(∑k∈d. norm (f (Sup k) - f (Inf k))) ≤
(∑k∈d. ∑b∈Basis. ¦(f (Sup k) - f (Inf k)) ∙ b¦)›
by (intro sum_mono norm_le_l1)
also have ‹… = (∑b∈Basis. ∑k∈d. ¦(f (Sup k) - f (Inf k)) ∙ b¦)›
by (rule sum.swap)
also have ‹… = (∑b∈Basis. ∑k∈d. norm (f (Sup k) ∙ b - f (Inf k) ∙ b))›
by (simp add: inner_diff_left)
also have ‹… ≤ (∑b∈Basis. vector_variation S (λu. f u ∙ b))›
by (intro sum_mono has_bounded_variation_works(1)[OF has_bounded_variation_on_inner_left[OF assms] dt(1,2)])
finally show ‹(∑k∈d. norm (f (Sup k) - f (Inf k))) ≤
(∑b∈Basis. vector_variation S (λu. f u ∙ b))› .
qed
lemma vector_variation_triangle:
assumes "has_bounded_variation_on f S" "has_bounded_variation_on g S"
shows "vector_variation S (λx. f x + g x) ≤ vector_variation S f + vector_variation S g"
proof (rule has_bounded_variation_works(2)[OF has_bounded_variation_on_add[OF assms]])
fix d T assume dt: "d division_of T" "T ⊆ S"
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)) + (g (Sup k) - g (Inf k))))"
by (simp add: algebra_simps)
also have "… ≤ (∑k∈d. norm (f (Sup k) - f (Inf k)) + norm (g (Sup k) - g (Inf k)))"
by (intro sum_mono norm_triangle_ineq)
also have "… = (∑k∈d. norm (f (Sup k) - f (Inf k))) + (∑k∈d. norm (g (Sup k) - g (Inf k)))"
by (simp add: sum.distrib)
also have "… ≤ vector_variation S f + vector_variation S g"
by (metis (mono_tags, lifting) add_mono assms dt has_bounded_variation_works(1))
finally show "(∑k∈d. norm (f (Sup k) + g (Sup k) - (f (Inf k) + g (Inf k))))
≤ vector_variation S f + vector_variation S g" .
qed
lemma vector_variation_neg:
shows "vector_variation S (λx. - f x) = vector_variation S f"
unfolding vector_variation_def set_variation_def
by (simp add: norm_minus_commute)
lemma vector_variation_triangle_sub:
assumes "has_bounded_variation_on f S" "has_bounded_variation_on g S"
shows "vector_variation S (λx. f x - g x) ≤ vector_variation S f + vector_variation S g"
proof -
have "vector_variation S (λx. f x - g x) = vector_variation S (λx. f x + (- g x))"
by simp
also have "… ≤ vector_variation S f + vector_variation S (λx. - g x)"
by (rule vector_variation_triangle[OF assms(1) has_bounded_variation_on_neg[OF assms(2)]])
also have "vector_variation S (λx. - g x) = vector_variation S g"
by (rule vector_variation_neg)
finally show ?thesis .
qed
lemma vector_variation_le_Un:
assumes fst: "has_bounded_variation_on f (S ∪ T)" and "interior S ∩ interior T = {}"
shows "vector_variation S f + vector_variation T f
≤ vector_variation (S ∪ T) f"
proof -
obtain bvs: "has_bounded_variation_on f S" and bvt: "has_bounded_variation_on f T"
using fst has_bounded_variation_on_subset by blast
have "vector_variation S f ≤ vector_variation (S ∪ T) f - vector_variation T f"
proof (rule has_bounded_variation_works(2)[OF bvs])
fix ds s' assume ds: "ds division_of s'" "s' ⊆ S"
have "vector_variation T f
≤ vector_variation (S ∪ T) f - (∑k∈ds. norm (f (Sup k) - f (Inf k)))"
proof (rule has_bounded_variation_works(2)[OF bvt])
fix dt t' assume dt: "dt division_of t'" "t' ⊆ T"
have disj: "interior s' ∩ interior t' = {}"
by (metis assms(2) ds(2) dt(2) inf_mono interior_mono subset_empty)
have "ds ∪ dt division_of s' ∪ t'"
by (rule division_disjoint_union[OF ds(1) dt(1) disj])
moreover have "s' ∪ t' ⊆ S ∪ T"
using ds(2) dt(2) by auto
moreover have "(∑k∈ds. norm (f (Sup k) - f (Inf k)))
+ (∑k∈dt. norm (f (Sup k) - f (Inf k)))
= (∑k∈ds ∪ dt. norm (f (Sup k) - f (Inf k)))"
proof (rule sum.union_inter_neutral[symmetric])
show "∀x∈ds ∩ dt. norm (f (Sup x) - f (Inf x)) = 0"
proof
fix k assume k: "k ∈ ds ∩ dt"
then have ks: "k ∈ ds" and kt: "k ∈ dt" by auto
obtain a b where kab: "k = cbox a b" and "k ≠ {}"
by (metis division_ofD(3,4) dt(1) kt)
then have ab: "a ≤ b" using kab by (simp add: box_real)
have "interior k = {}" using disj
by (metis Int_greatest bot.extremum_uniqueI division_ofD(2) ds(1) dt(1) interior_mono ks
kt)
then have "box a b = {}" using kab by simp
with ab have "a = b" by (simp add: box_eq_empty inner_Basis)
then show "norm (f (Sup k) - f (Inf k)) = 0"
using kab by simp
qed
qed (use ds dt in blast)+
ultimately have "(∑k∈ds. norm (f (Sup k) - f (Inf k))) + (∑k∈dt. norm (f (Sup k) - f (Inf k)))
≤ vector_variation (S ∪ T) f"
using has_bounded_variation_works(1)[OF fst] by auto
then show "(∑k∈dt. norm (f (Sup k) - f (Inf k)))
≤ vector_variation (S ∪ T) f - (∑k∈ds. norm (f (Sup k) - f (Inf k)))"
by linarith
qed
then show "(∑k∈ds. norm (f (Sup k) - f (Inf k)))
≤ vector_variation (S ∪ T) f - vector_variation T f"
by linarith
qed
then show ?thesis by linarith
qed
lemma finite_frontier_interval_real:
fixes S :: "real set"
assumes "is_interval S"
shows "finite (frontier S) ∧ card (frontier S) ≤ 2"
proof (cases "interior S = {}")
case True
have "S = {} ∨ (∃a. S = {a})"
proof (cases "S = {}")
case False
then obtain x where xs: "x ∈ S" by auto
have "S = {x}"
proof (rule ccontr)
assume "S ≠ {x}"
then obtain y where ys: "y ∈ S" and yx: "y ≠ x" using xs by blast
have convS: "convex S" using assms is_interval_convex by blast
then obtain a b where ab: "a < b" "{a..b} ⊆ S"
by (meson atMostAtLeast_subset_convex linorder_less_linear xs ys yx)
then have "{a <..< b} ⊆ interior S"
using interior_atLeastAtMost_real interior_mono by blast
moreover have "{a <..< b} ≠ {}" using ab(1) by auto
ultimately show False using True by auto
qed
then show ?thesis by auto
qed auto
then show "finite (frontier S) ∧ card (frontier S) ≤ 2" by (auto simp: frontier_def)
next
case False
then obtain c where c_int: "c ∈ interior S" by blast
have convS: "convex S" using assms is_interval_convex_1 by blast
show ?thesis
proof (rule ccontr)
assume inf: "¬ ?thesis"
then consider "infinite (frontier S)" | "card (frontier S) ≥ 3"
by linarith
then obtain F where "finite F" "F ⊆ frontier S" "card F = 3"
by (meson infinite_arbitrarily_large obtain_subset_with_card_n)
then obtain x y z where "x ∈ F" "y ∈ F" "z ∈ F" "x<y" "y<z"
apply (simp add: eval_nat_numeral card_Suc_eq)
by (metis antisym insert_subset linorder_not_le order.refl)
have y_cls: "y ∈ closure S" and y_nint: "y ∉ interior S"
using ‹F ⊆ frontier S› ‹y ∈ F› frontier_def by auto
have x_cls: "x ∈ closure S"
using ‹F ⊆ frontier S› ‹x ∈ F› frontier_def by auto
have z_cls: "z ∈ closure S"
using ‹F ⊆ frontier S› ‹z ∈ F› frontier_def by auto
have "y ∈ interior S"
proof (cases "c ≤ y")
case True
have "c < y" using True
using c_int less_eq_real_def y_nint by blast
have "open_segment c z ⊆ interior S"
by (rule in_interior_closure_convex_segment[OF convS c_int z_cls])
moreover have "y ∈ open_segment c z"
using ‹c < y› ‹y < z› open_segment_eq_real_ivl by auto
ultimately show ?thesis by auto
next
case False
have "open_segment c x ⊆ interior S"
by (rule in_interior_closure_convex_segment[OF convS c_int x_cls])
moreover have "y ∈ open_segment c x"
using ‹x < y› False open_segment_eq_real_ivl by auto
ultimately show ?thesis by auto
qed
with y_nint show False by contradiction
qed
qed
lemma has_bounded_variation_on_closure:
fixes f :: "real ⇒ 'a::euclidean_space"
assumes "is_interval S" "has_bounded_variation_on f S"
shows "has_bounded_variation_on f (closure S)"
proof -
have fin_fr: "finite (frontier S)" and card2: "card (frontier S) ≤ 2"
using finite_frontier_interval_real [OF ‹is_interval S›] by auto
have "bounded (f ` closure S)"
proof (rule bounded_subset)
show "bounded (f ` (S ∪ frontier S))"
proof -
have "bounded (f ` S)"
proof (cases "S = {}")
case True then show ?thesis by simp
next
case False
then obtain a where aS: "a ∈ S" by auto
obtain K where K: "⋀d T. d division_of T ⟹ T ⊆ S ⟹
(∑k∈d. norm (f (Sup k) - f (Inf k))) ≤ K"
using assms(2) unfolding has_bounded_variation_on_def has_bounded_setvariation_on_def
by blast
show ?thesis unfolding bounded_iff
proof (intro exI[of _ "norm (f a) + K"] ballI)
fix y assume "y ∈ f ` S"
then obtain x where xS: "x ∈ S" and y_eq: "y = f x" by auto
have sub: "{min a x..max a x} ⊆ S"
using assms
by (metis aS xS cbox_interval interval_subset_is_interval max_def min_def)
have d: "{{min a x..max a x}} division_of {min a x..max a x}"
by (intro division_ofI) auto
have "norm (f x - f a) ≤ (∑k∈{{min a x..max a x}}. norm (f (Sup k) - f (Inf k)))"
by simp (smt (verit) norm_minus_commute)
also have "… ≤ K" using K[OF d sub] .
finally show "norm y ≤ norm (f a) + K"
by (metis add.commute diff_le_eq norm_triangle_ineq2 order_trans y_eq)
qed
qed
moreover have "bounded (f ` frontier S)"
using fin_fr by (intro finite_imp_bounded finite_imageI)
ultimately show ?thesis
by (simp add: image_Un bounded_Un)
qed
next
show "f ` closure S ⊆ f ` (S ∪ frontier S)"
by (simp add: closure_Un_frontier)
qed
then obtain B' where B'bd: "⋀x. x ∈ closure S ⟹ norm (f x) ≤ B'"
unfolding bounded_iff by (auto simp: image_iff)
define B where "B = max B' 0"
have Bbd: "norm (f x) ≤ B" if "x ∈ closure S" for x
using B'bd[OF that] unfolding B_def by simp
have Bge0: "B ≥ 0" unfolding B_def by simp
obtain K where K: "⋀d T. d division_of T ⟹ T ⊆ S ⟹ (∑k∈d. norm (f (Sup k) - f (Inf k))) ≤ K"
using assms(2) unfolding has_bounded_variation_on_def has_bounded_setvariation_on_def
by blast
let ?B = "K + 8*B"
show ?thesis
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 ⊆ closure S"
then have ‹finite d›
by blast
define dd where "dd ≡ {k ∈ d. k ⊆ S} ∪ {k ∈ d. ¬ k ⊆ S}"
have ‹d = dd›
unfolding dd_def by blast
have ‹(∑k∈d. norm (f (Sup k) - f (Inf k)))
= (∑k∈{k ∈ d. k ⊆ S}. norm (f (Sup k) - f (Inf k))) + (∑k∈{k ∈ d. ¬ k ⊆ S}. norm (f (Sup k) - f (Inf k))) ›
using ‹finite d› ‹d = dd› dd_def sum.union_disjoint
by (metis (mono_tags, lifting) IntE equals0I finite_Un mem_Collect_eq)
also have ‹... ≤ ?B›
proof (rule add_mono)
show "(∑k | k ∈ d ∧ k ⊆ S. norm (f (Sup k) - f (Inf k))) ≤ K"
proof (rule K)
show "{k ∈ d. k ⊆ S} division_of ⋃ {k ∈ d. k ⊆ S}"
by (metis (lifting) ‹d = dd› dd_def division_ofD(6) division_of_subset dt sup_ge1)
show "⋃{k ∈ d. k ⊆ S} ⊆ S"
by blast
qed
have "(∑k | k ∈ d ∧ ¬ k ⊆ S. norm (f (Sup k) - f (Inf k)))
= (∑k | k ∈ d ∧ ¬ k ⊆ S ∧ f (Sup k) ≠ f (Inf k). norm (f (Sup k) - f (Inf k)))"
using ‹finite d› by (intro sum.mono_neutral_right) auto
also have ‹... ≤ real (card {k ∈ d. ¬ k ⊆ S ∧ f (Sup k) ≠ f (Inf k)}) * (2 * B)›
proof (rule sum_bounded_above)
fix i :: "real set"
assume "i ∈ {k ∈ d. ¬ k ⊆ S ∧ f (Sup k) ≠ f (Inf k)}"
then have "i ∈ d" " ¬ i ⊆ S" "f (Sup i) ≠ f (Inf i)"
by auto
show "norm (f (Sup i) - f (Inf i)) ≤ 2 * B"
proof -
obtain a b where isub: "i ⊆ closure S" and "i ≠ {}" and iab: "i = cbox a b"
by (metis ‹i ∈ d› cbox_division_memE dt subset_trans)
then have ab: "a ≤ b" by (simp add: cbox_interval)
then have "Sup i = b" "Inf i = a"
using iab by (simp_all add: cbox_interval cSup_atLeastAtMost cInf_atLeastAtMost)
moreover have "a ∈ i" "b ∈ i" using iab ab by (auto simp: cbox_interval)
ultimately have "Sup i ∈ closure S" "Inf i ∈ closure S"
using isub by auto
then have "norm (f (Sup i)) ≤ B" "norm (f (Inf i)) ≤ B"
using Bbd by auto
then show ?thesis
using norm_triangle_ineq4[of "f (Sup i)" "f (Inf i)"] by linarith
qed
qed
also have ‹... ≤ 8 * B›
proof -
have "card {k ∈ d. ¬ k ⊆ S ∧ f (Sup k) ≠ f (Inf k)} ≤ 4"
proof -
let ?S = "{k ∈ d. ¬ k ⊆ S ∧ f (Sup k) ≠ f (Inf k)}"
define g where "g k = (if Inf k ∈ frontier S then (Inf k, True) else (Sup k, False))" for k
have endpt_frontier: "Inf k ∈ frontier S ∨ Sup k ∈ frontier S" if "k ∈ ?S" for k
proof -
from that have kd: "k ∈ d" and nks: "¬ k ⊆ S" and neq: "f (Sup k) ≠ f (Inf k)" by auto
obtain a b where kab: "k = cbox a b" and "a ≤ b"
using division_ofD(4)[OF conjunct1[OF dt] kd] nks by auto
have inf_k: "Inf k = a" "Sup k = b"
using kab ‹a ≤ b› by (simp_all add: cbox_interval cSup_atLeastAtMost cInf_atLeastAtMost)
have "a ∈ k" "b ∈ k" using kab ‹a ≤ b› by (auto simp: cbox_interval)
then have "Inf k ∈ closure S" "Sup k ∈ closure S"
using inf_k dt kd by blast+
moreover have "Inf k ∉ S ∨ Sup k ∉ S"
using assms(1) inf_k interval_subset_is_interval kab nks by blast
ultimately show ?thesis
using closure_Un_frontier by auto
qed
have g_img: "g ` ?S ⊆ frontier S × UNIV"
using endpt_frontier unfolding g_def by auto
have g_inj: "inj_on g ?S"
proof (rule inj_onI)
fix k1 k2
assume k1S: "k1 ∈ ?S" and k2S: "k2 ∈ ?S" and geq: "g k1 = g k2"
then have k1d: "k1 ∈ d" and ne1: "f (Sup k1) ≠ f (Inf k1)"
and k2d: "k2 ∈ d" and ne2: "f (Sup k2) ≠ f (Inf k2)" by auto
obtain a1 b1 a2 b2 where k1ab: "k1 = cbox a1 b1" and k2ab: "k2 = cbox a2 b2"
and "a1 < b1" "a2 < b2"
by (metis atLeastatMost_empty' box_real(2) cbox_division_memE dt interval_bounds_real k1d k2d less_eq_real_def ne1 ne2)
have int: "interior k1 = {a1<..<b1}" "interior k2 = {a2<..<b2}"
using k1ab k2ab by (simp_all add: cbox_interval interior_atLeastAtMost_real)
show "k1 = k2"
proof (cases "Inf k1 ∈ frontier S")
case True
then have "Inf k2 ∈ frontier S" and "Inf k1 = Inf k2"
using geq unfolding g_def by (auto split: if_splits)
then have "a1 = a2"
by (simp add: ‹a1 < b1› ‹a2 < b2› k1ab k2ab less_eq_real_def)
then have "(a1 + min b1 b2) / 2 ∈ {a1<..<b1} ∩ {a2<..<b2}"
using ‹a1 < b1› ‹a2 < b2› by (auto simp: field_simps min_def)
then have "interior k1 ∩ interior k2 ≠ {}" if "k1 ≠ k2"
using int by auto
then show "k1 = k2"
using division_ofD(5)[OF conjunct1[OF dt] k1d k2d] by auto
next
case False
then have "Inf k2 ∉ frontier S" and "Sup k1 = Sup k2"
using geq unfolding g_def by (auto split: if_splits)
then have "b1 = b2"
by (simp add: ‹a1 < b1› ‹a2 < b2› k1ab k2ab less_eq_real_def)
then have "(max a1 a2 + b1) / 2 ∈ {a1<..<b1} ∩ {a2<..<b2}"
using ‹a1 < b1› ‹a2 < b2› by (auto simp: field_simps max_def)
then have "interior k1 ∩ interior k2 ≠ {}" if "k1 ≠ k2"
using int by auto
then show "k1 = k2"
using division_ofD(5)[OF conjunct1[OF dt] k1d k2d] by auto
qed
qed
have "card ?S ≤ card (frontier S × (UNIV :: bool set))"
using card_inj_on_le[OF g_inj g_img] fin_fr finite by blast
also have "... = card (frontier S) * 2"
using card_cartesian_product card_UNIV_bool by metis
also have "... ≤ 2 * 2" using card2 by auto
finally show ?thesis by simp
qed
then have card_le: "real (card {k ∈ d. ¬ k ⊆ S ∧ f (Sup k) ≠ f (Inf k)}) ≤ 4"
by auto
show ?thesis
using mult_right_mono [OF card_le Bge0] by linarith
qed
finally show "(∑k | k ∈ d ∧ ¬ k ⊆ S. norm (f (Sup k) - f (Inf k))) ≤ 8 * B" .
qed
finally show "(∑k∈d. norm (f (Sup k) - f (Inf k))) ≤ ?B" .
qed
qed
lemma has_bounded_variation_on_closure_eq:
fixes f :: "real ⇒ 'a::euclidean_space"
assumes "is_interval S"
shows "has_bounded_variation_on f (closure S) ⟷ has_bounded_variation_on f S"
by (meson assms closure_subset has_bounded_variation_on_closure has_bounded_variation_on_subset)
lemma has_bounded_set_variation:
"has_bounded_setvariation_on f S ∧ set_variation S f ≤ c ⟷
(∀d T. d division_of T ∧ T ⊆ S ⟶ (∑k∈d. norm (f k)) ≤ c)"
by (metis has_bounded_setvariation_on_def has_bounded_setvariation_works order_trans)
lemma has_bounded_vector_variation_on_interval:
"has_bounded_variation_on f {a..b} ∧ vector_variation {a..b} f ≤ c ⟷
(∀d. d division_of {a..b} ⟶
(∑k∈d. norm (f (Sup k) - f (Inf k))) ≤ c)"
(is "?L ⟷ ?R")
proof
assume L: ?L
then have bdd: "has_bounded_variation_on f {a..b}"
and le: "vector_variation {a..b} f ≤ c" by auto
show ?R
using has_bounded_variation_works(1)[OF bdd]
by (meson dual_order.trans le subset_refl)
next
assume R: ?R
show ?L
proof (intro conjI)
show bv: "has_bounded_variation_on f {a..b}"
unfolding has_bounded_variation_on_interval using R by blast
show "vector_variation {a..b} f ≤ c"
proof (rule has_bounded_variation_works(2)[OF bv])
fix d t assume "d division_of t" "t ⊆ {a..b}"
then have div_d: "d division_of t" and sub: "t ⊆ {a..b}" by auto
have "d division_of ⋃d"
using division_of_union_self[OF div_d] .
moreover have "⋃d = t"
using division_ofD(6)[OF div_d] .
ultimately have "⋃d ⊆ cbox a b"
using sub by (simp add: cbox_interval)
then obtain q where dq: "d ⊆ q" and q_div: "q division_of {a..b}"
using partial_division_extend_interval ‹d division_of ⋃d› cbox_interval by metis
have "(∑k∈d. norm (f (Sup k) - f (Inf k))) ≤ (∑k∈q. norm (f (Sup k) - f (Inf k)))"
using division_of_finite[OF q_div]
by (rule sum_mono2[OF _ dq]) auto
also have "… ≤ c"
using R q_div by auto
finally show "(∑k∈d. norm (f (Sup k) - f (Inf k))) ≤ c" .
qed
qed
qed
lemma has_bounded_vector_variation:
"has_bounded_variation_on f S ∧ vector_variation S f ≤ c ⟷
(∀d t. d division_of t ∧ t ⊆ S ⟶
(∑k∈d. norm (f (Sup k) - f (Inf k))) ≤ c)"
unfolding has_bounded_variation_on_def vector_variation_def
using has_bounded_set_variation .
lemma
fixes f :: "real ⇒ 'a::euclidean_space" and S T :: "real set"
assumes "is_interval S" "is_interval T"
"has_bounded_variation_on f S" "has_bounded_variation_on f T"
shows has_bounded_variation_on_Un: "has_bounded_variation_on f (S ∪ T)" (is ?th1)
and vector_variation_Un_le:
"(S ∩ T = {} ⟹ S ∩ closure T = {} ∧ T ∩ closure S = {})
⟹ vector_variation (S ∪ T) f ≤ vector_variation S f + vector_variation T f" (is "PROP ?th2")
proof -
have combined: "has_bounded_variation_on f (S ∪ T) ∧ vector_variation (S ∪ T) f
≤ vector_variation S f + vector_variation T f"
if "is_interval S" and "is_interval T"
and clo: "S ∩ T = {} ⟹ S ∩ closure T = {} ∧ T ∩ closure S = {}"
and bv_fs: "has_bounded_variation_on f S"
and bv_ft: "has_bounded_variation_on f T"
for f :: "real ⇒ 'a" and S T
proof (cases "S={} ∨ T={}")
case True
then show ?thesis
using that vector_variation_pos_le [of f]
by (metis Un_empty_left add.commute atLeastatMost_empty_iff2 le_add_same_cancel2
sup_bot_right)
next
case False
then obtain p q where "p ∈ S" and "q ∈ T"
by blast
show ?thesis
unfolding has_bounded_vector_variation
proof (intro strip)
fix d u
assume du: "d division_of u ∧ u ⊆ S ∪ T"
have "∃j k. j ≠ {} ∧ k ≠ {} ∧ (∃a b. j = {a..b}) ∧ (∃a b. k = {a..b})
∧ j ⊆ S ∧ k ⊆ T ∧ (j ⊆ i ∨ interior j = {}) ∧ (k ⊆ i ∨ interior k = {})
∧ norm (f (Sup i) - f (Inf i)) ≤ norm (f (Sup j) - f (Inf j)) + norm (f (Sup k) - f (Inf k))"
if "i ∈ d" for i
proof -
obtain a b where iab: "i = {a..b}" and ne: "{a..b} ≠ {}"
by (metis ‹i ∈ d› box_real(2) division_ofD(3,4) du)
then have ab: "a ≤ b"
using atLeastatMost_empty_iff by blast
then have "a ∈ {a..b}" "b ∈ {a..b}" using ab by auto
have iSup: "Sup i = b" and iInf: "Inf i = a"
using ab iab by auto
have isub: "i ⊆ u" and usub: "u ⊆ S ∪ T"
using du that division_ofD(2) by (blast, meson)
then have ab_st: "{a,b} ⊆ S ∪ T"
using iab ‹a ∈ {a..b}› by auto
have one_in_each: ?thesis
if aS: "a ∈ U" and bT: "b ∈ V" and ivS: "is_interval U" and ivT: "is_interval V"
and st: "(U = S ∧ V = T) ∨ (U = T ∧ V = S)"
for U V
proof (cases "S ∩ T = {}")
case True
have sep: "S ∩ closure T = {} ∧ T ∩ closure S = {}" using clo True by blast
have sub: "{a..b} ⊆ S ∪ T" using isub usub iab by blast
have o1: "open (- closure T)" and o2: "open (- closure S)"
using open_Compl closed_closure by blast+
have s_sub: "S ⊆ - closure T" and t_sub: "T ⊆ - closure S"
using sep by blast+
have "{a..b} ⊆ (- closure T) ∪ (- closure S)"
using sub s_sub t_sub by blast
moreover have "(- closure T) ∩ (- closure S) ∩ {a..b} = {}"
using sub closure_subset by blast
moreover have "(- closure T) ∩ {a..b} ≠ {} ∧ (- closure S) ∩ {a..b} ≠ {}"
using aS bT st s_sub t_sub ab by auto
ultimately show ?thesis
by (meson connectedD connected_Icc o1 o2)
next
case False
obtain c where "c ∈ S" "c ∈ T" using False by blast
with aS bT ivS ivT st
have c': "max a (min c b) ∈ S ∧ max a (min c b) ∈ T ∧ max a (min c b) ∈ {a..b}"
by (smt (verit) ab atLeastAtMost_iff max.absorb1 max.absorb2 mem_is_interval_1_I
min_le_iff_disj)
define c' where "c' = max a (min c b)"
then have c'_s: "c' ∈ S" and c'_t: "c' ∈ T" and c'_ab: "a ≤ c'" "c' ≤ b"
using c' by auto
have lo_sub_S: "{a..c'} ⊆ U"
using aS c'_s c'_t ivS st interval_subset_is_interval[of U a c']
by (auto simp: box_real)
have hi_sub_T: "{c'..b} ⊆ V"
using bT c'_s c'_t ivT st interval_subset_is_interval[of V c' b]
by (auto simp: box_real)
have lo_sub_i: "{a..c'} ⊆ {a..b}" and hi_sub_i: "{c'..b} ⊆ {a..b}"
using c'_ab ab by auto
have tri: "norm (f b - f a) ≤ norm (f c' - f a) + norm (f b - f c')"
by (simp add: order_trans [OF _ norm_triangle_ineq])
show ?thesis using st
proof
assume st': "U = S ∧ V = T"
show ?thesis
apply (rule_tac x="{a..c'}" in exI, rule_tac x="{c'..b}" in exI)
using c'_ab ab lo_sub_S hi_sub_T lo_sub_i hi_sub_i iab ne tri st'
by (auto simp: iSup iInf)
next
assume st': "U = T ∧ V = S"
show ?thesis
apply (rule_tac x="{c'..b}" in exI, rule_tac x="{a..c'}" in exI)
using c'_ab ab lo_sub_S hi_sub_T lo_sub_i hi_sub_i iab ne tri st'
by (auto simp: iSup iInf)
qed
qed
from ab_st consider "a ∈ S ∧ b ∈ S" | "a ∈ S ∧ b ∈ T" | "a ∈ T ∧ b ∈ S" | "a ∈ T ∧ b ∈ T"
by blast
then show ?thesis
proof cases
case 1
show ?thesis
apply (rule exI[where x="{a..b}"])
apply (rule exI[where x="{q..q}"])
using 1 ne ‹q ∈ T› iab ab ‹is_interval S› interval_subset_is_interval[of _ a b]
by (force simp: iSup iInf interior_atLeastAtMost_real)
next
case 2
then show ?thesis using one_in_each[where U=S and V=T] ‹is_interval S› ‹is_interval T› by blast
next
case 3
then show ?thesis using one_in_each[where U=T and V=S] ‹is_interval S› ‹is_interval T› by blast
next
case 4
show ?thesis
apply (rule exI[where x="{p..p}"])
apply (rule exI[where x="{a..b}"])
using 4 ne ‹p ∈ S› iab ab ‹is_interval T› interval_subset_is_interval[of _ a b]
by (force simp: iSup iInf interior_atLeastAtMost_real)
qed
qed
then obtain L R where LR: "∀i∈d. L i ≠ {} ∧ R i ≠ {} ∧ (∃a b. L i = {a..b})
∧ (∃a b. R i = {a..b}) ∧ L i ⊆ S ∧ R i ⊆ T ∧ (L i ⊆ i ∨ interior (L i) = {})
∧ (R i ⊆ i ∨ interior (R i) = {})
∧ norm (f (Sup i) - f (Inf i)) ≤ norm (f (Sup (L i)) - f (Inf (L i))) + norm (f (Sup (R i)) - f (Inf (R i)))"
by metis
have ‹finite d›
using du by blast
have div_sum_bound: "(∑k∈d. norm (f (Sup (g k)) - f (Inf (g k)))) ≤ vector_variation S f"
if gne: "∀i∈d. g i ≠ {}"
and gcbox: "∀i∈d. ∃a b. g i = {a..b}"
and gsub: "∀i∈d. g i ⊆ S"
and gcontain: "∀i∈d. g i ⊆ i ∨ interior (g i) = {}"
and bvS: "has_bounded_variation_on f S"
for g :: "real set ⇒ real set" and S
proof -
define d' where "d' = {k ∈ d. interior (g k) ≠ {}}"
have fd': "finite d'" unfolding d'_def using ‹finite d› by auto
have d'_sub: "d' ⊆ d" unfolding d'_def by auto
have zero: "norm (f (Sup (g k)) - f (Inf (g k))) = 0" if "k ∈ d - d'" for k
proof -
from that have kd: "k ∈ d" and int: "interior (g k) = {}" by (auto simp: d'_def)
from gcbox kd obtain a b where ab: "g k = {a..b}" by blast
have ne: "g k ≠ {}" using gne kd by blast
have "a = b"
using ab int ne by auto
then show "norm (f (Sup (g k)) - f (Inf (g k))) = 0"
by (simp add: ab)
qed
have split_sum: "(∑k∈d. norm (f (Sup (g k)) - f (Inf (g k))))
= (∑k∈d'. norm (f (Sup (g k)) - f (Inf (g k))))"
using sum.subset_diff[OF d'_sub ‹finite d›] zero
by (simp add: ‹finite d› d'_sub sum.mono_neutral_right)
have inj_g: "inj_on g d'"
proof (rule inj_onI)
fix x y assume "x ∈ d'" "y ∈ d'" "g x = g y"
then have §: "x ∈ d" "y ∈ d" "interior (g x) ≠ {}" "interior (g y) ≠ {}"
unfolding d'_def by auto
then show "x = y"
using du ‹x ∈ d› ‹y ∈ d› interior_mono gcontain §
by (metis ‹g x = g y› division_ofD(5) inf.boundedI subset_empty)
qed
have gd'_div: "g ` d' division_of ⋃ (g ` d')"
unfolding division_of_def
proof (intro conjI ballI allI impI)
fix K1 K2 assume "K1 ∈ g ` d'" "K2 ∈ g ` d'" "K1 ≠ K2"
then obtain x1 x2 where k12: "x1 ∈ d'" "K1 = g x1" "x2 ∈ d'" "K2 = g x2" by auto
then have "x1 ≠ x2" using ‹K1 ≠ K2› by auto
have "x1 ∈ d" "x2 ∈ d" using k12 d'_sub by auto
have "interior (g x1) ≠ {}" "interior (g x2) ≠ {}" using k12 d'_def by auto
then have "g x1 ⊆ x1" "g x2 ⊆ x2" using gcontain ‹x1 ∈ d› ‹x2 ∈ d› by meson+
then have "interior (g x1) ⊆ interior x1" "interior (g x2) ⊆ interior x2"
using interior_mono by blast+
then show "interior K1 ∩ interior K2 = {}"
using k12 du ‹x1 ∈ d› ‹x2 ∈ d› ‹x1 ≠ x2› division_ofD(5) by blast
qed (use fd' gcbox gne in ‹auto simp: d'_def›)
have gd'_sub_S: "⋃ (g ` d') ⊆ S"
using gsub bot.extremum by (fastforce simp: d'_def)
have "(∑k∈d'. norm (f (Sup (g k)) - f (Inf (g k))))
= (∑k ∈ g ` d'. norm (f (Sup k) - f (Inf k)))"
by (metis (no_types, lifting) inj_g sum.reindex_cong)
also have "… ≤ vector_variation S f"
using has_bounded_variation_works(1)[OF bvS gd'_div gd'_sub_S] .
finally show ?thesis using split_sum by simp
qed
have "(∑k∈d. norm (f (Sup k) - f (Inf k)))
≤ (∑k∈d. norm (f (Sup (L k)) - f (Inf (L k))) + norm (f (Sup (R k)) - f (Inf (R k))))"
by (meson LR sum_mono)
also have "… ≤ vector_variation S f + vector_variation T f"
unfolding sum.distrib
proof (intro add_mono)
show "(∑k∈d. norm (f (Sup (L k)) - f (Inf (L k)))) ≤ vector_variation S f"
using div_sum_bound[of L S] LR bv_fs by blast
next
show "(∑k∈d. norm (f (Sup (R k)) - f (Inf (R k)))) ≤ vector_variation T f"
using div_sum_bound[of R T] LR bv_ft by blast
qed
finally show "(∑k∈d. norm (f (Sup k) - f (Inf k))) ≤ vector_variation S f + vector_variation T f" .
qed
qed
show "has_bounded_variation_on f (S ∪ T)"
proof -
have "has_bounded_variation_on f (closure S ∪ closure T)"
by (metis (lifting) ext assms closure_closure combined convex_closure
has_bounded_variation_on_closure_eq inf_commute is_interval_convex_1)
then have "has_bounded_variation_on f (closure S ∪ closure T)"
using combined by blast
then show ?thesis
by (metis has_bounded_variation_on_subset closure_Un closure_subset)
qed
show "(S ∩ T = {} ⟹ S ∩ closure T = {} ∧ T ∩ closure S = {})
⟹ vector_variation (S ∪ T) f ≤ vector_variation S f + vector_variation T f"
using combined assms by blast
qed
text ‹
The key splitting lemma for vector variation on general interval sets,
following HOL Light's @{text VECTOR_VARIATION_SPLIT}.
Given an interval set @{term S} and a split point @{term a}, the variation
over @{term S} equals the sum of variations over the left part
@{term "S ∩ {..a}"} and the right part @{term "S ∩ {a..}"}.
›
lemma vector_variation_split:
assumes "is_interval S" "has_bounded_variation_on f S"
shows "vector_variation (S ∩ {..a}) f + vector_variation (S ∩ {a..}) f =
vector_variation S f"
proof -
let ?L = "S ∩ {..a}" and ?R = "S ∩ {a..}"
have split: "?L ∪ ?R = S"
by auto
have "vector_variation ?L f + vector_variation ?R f ≤ vector_variation S f"
proof (rule vector_variation_le_Un[of f ?L ?R, unfolded split])
show "has_bounded_variation_on f S"
by (rule assms(2))
show "interior ?L ∩ interior ?R = {}"
by force
qed
moreover have "vector_variation (?L ∪ ?R) f ≤ vector_variation ?L f + vector_variation ?R f"
proof (rule vector_variation_Un_le)
show "is_interval ?L" "is_interval ?R"
by (auto intro: is_interval_Int assms(1) is_interval_ic is_interval_ci)
show "has_bounded_variation_on f ?L" "has_bounded_variation_on f ?R"
by (auto intro: has_bounded_variation_on_subset[OF assms(2)])
show "?L ∩ closure ?R = {} ∧ ?R ∩ closure ?L = {}" if disj: "?L ∩ ?R = {}"
proof -
obtain "closure ?R ⊆ {a..}" "closure ?L ⊆ {..a}"
by (simp add: closure_minimal)
with disj show "?L ∩ closure ?R = {} ∧ ?R ∩ closure ?L = {}"
by auto
qed
qed
ultimately show ?thesis
by (simp add: split)
qed
lemma has_bounded_variation_on_split:
assumes "is_interval S"
shows "has_bounded_variation_on f S ⟷
has_bounded_variation_on f (S ∩ {..a}) ∧ has_bounded_variation_on f (S ∩ {a..})"
(is "?lhs ⟷ ?rhs")
proof
assume bv: ?lhs
then show ?rhs
by (auto intro: has_bounded_variation_on_subset)
next
assume ?rhs
then have "has_bounded_variation_on f (S ∩ {..a} ∪ S ∩ {a..})"
by (intro has_bounded_variation_on_Un is_interval_Int assms is_interval_ic is_interval_ci) auto
moreover have "S ∩ {..a} ∪ S ∩ {a..} = S"
by auto
ultimately show ?lhs
by simp
qed
lemma has_bounded_variation_on_combine:
assumes "a ≤ c" "c ≤ b"
shows "has_bounded_variation_on f {a..b} ⟷
has_bounded_variation_on f {a..c} ∧ has_bounded_variation_on f {c..b}"
proof -
have *: "has_bounded_variation_on f {a..b} ⟷
has_bounded_variation_on f ({a..b} ∩ {..c}) ∧ has_bounded_variation_on f ({a..b} ∩ {c..})"
by (rule has_bounded_variation_on_split) (simp add: is_interval_cc)
show ?thesis
using * assms by (simp add: Int_atLeastAtMostL1 Int_atLeastAtMostL2 min_absorb2 max_absorb2)
qed
lemma vector_variation_combine:
assumes bv: "has_bounded_variation_on f {a..b}" and cab: "c ∈ {a..b}"
shows "vector_variation {a..b} f = vector_variation {a..c} f + vector_variation {c..b} f"
proof -
from cab have ac: "a ≤ c" and cb: "c ≤ b" by auto
have *: "vector_variation ({a..b} ∩ {..c}) f + vector_variation ({a..b} ∩ {c..}) f =
vector_variation {a..b} f"
by (rule vector_variation_split[OF is_interval_cc bv])
show ?thesis
using * ac cb by (simp add: Int_atLeastAtMostL1 Int_atLeastAtMostL2 min_absorb2 max_absorb2)
qed
subsection ‹Composition and monotonicity›
lemma has_bounded_variation_compose_monotone:
assumes bv: "has_bounded_variation_on g {f a..f b}"
and mono: "mono_on {a..b} f"
shows "has_bounded_variation_on (g ∘ f) {a..b}" (is ?th1)
and "vector_variation {a..b} (g ∘ f) ≤ vector_variation {f a..f b} g" (is ?th2)
proof -
have ‹(∑k∈d. norm ((g ∘ f) (Sup k) - (g ∘ f) (Inf k))) ≤ vector_variation {f a..f b} g›
if "d division_of {a..b}" for d
proof -
define D where ‹D ≡ (λk. {f (Inf k)..f(Sup k)}) ` d›
have "finite d" using division_of_finite[OF that] .
have kprops: "⋀k. k ∈ d ⟹ k ⊆ {a..b} ∧ k ≠ {} ∧ (∃l u. k = cbox l u)"
using division_ofD(2,3,4)[OF that] by auto
have int_disj: "⋀k1 k2. k1 ∈ d ⟹ k2 ∈ d ⟹ k1 ≠ k2 ⟹ interior k1 ∩ interior k2 = {}"
using division_ofD(5)[OF that] by auto
have k_interval: "⋀k. k ∈ d ⟹ ∃l u. l ≤ u ∧ k = {l..u} ∧ Inf k = l ∧ Sup k = u"
using kprops by fastforce
have mono_le: "⋀x y. x ∈ {a..b} ⟹ y ∈ {a..b} ⟹ x ≤ y ⟹ f x ≤ f y"
using mono by (simp add: monotone_on_def)
have fInf_le_fSup: "⋀k. k ∈ d ⟹ f (Inf k) ≤ f (Sup k)"
using kprops mono_le by fastforce
have ‹D division_of ⋃D›
unfolding division_of_def
proof (intro conjI ballI allI impI)
show "finite D" unfolding D_def using ‹finite d› by auto
next
fix K assume "K ∈ D"
then obtain k where kd: "k ∈ d" and K_eq: "K = {f (Inf k)..f (Sup k)}"
unfolding D_def by auto
show "K ⊆ ⋃D" "K ≠ {}" using ‹K ∈ D› K_eq fInf_le_fSup[OF kd] by auto
show "∃a b. K = cbox a b" using K_eq by (auto simp: cbox_interval)
next
fix K1 K2 assume K1D: "K1 ∈ D" and K2D: "K2 ∈ D" and ne: "K1 ≠ K2"
from K1D obtain k1 where k1d: "k1 ∈ d" and K1_eq: "K1 = {f (Inf k1)..f (Sup k1)}"
unfolding D_def by auto
from K2D obtain k2 where k2d: "k2 ∈ d" and K2_eq: "K2 = {f (Inf k2)..f (Sup k2)}"
unfolding D_def by auto
obtain l1 u1 where lu1: "l1 ≤ u1" "k1 = {l1..u1}" "Inf k1 = l1" "Sup k1 = u1"
using k_interval[OF k1d] by blast
obtain l2 u2 where lu2: "l2 ≤ u2" "k2 = {l2..u2}" "Inf k2 = l2" "Sup k2 = u2"
using k_interval[OF k2d] by blast
have k1_sub: "k1 ⊆ {a..b}" using kprops k1d by auto
have k2_sub: "k2 ⊆ {a..b}" using kprops k2d by auto
have l1a: "l1 ∈ {a..b}" "u1 ∈ {a..b}" using k1_sub lu1 by auto
have l2a: "l2 ∈ {a..b}" "u2 ∈ {a..b}" using k2_sub lu2 by auto
have fl1u1: "f l1 ≤ f u1" using mono_le l1a lu1(1) by auto
have fl2u2: "f l2 ≤ f u2" using mono_le l2a lu2(1) by auto
have k1_ne_k2: "k1 ≠ k2"
using K1_eq K2_eq ne by blast
have int_k1k2: "interior k1 ∩ interior k2 = {}"
using int_disj[OF k1d k2d k1_ne_k2] .
show "interior K1 ∩ interior K2 = {}"
proof (rule ccontr)
assume "interior K1 ∩ interior K2 ≠ {}"
then obtain y where y1: "y ∈ interior K1" and y2: "y ∈ interior K2" by auto
have int_K1: "interior K1 = {f l1<..<f u1}"
using K1_eq lu1 fl1u1 by (auto simp: interior_atLeastAtMost_real)
then have y_in1: "f l1 < y" "y < f u1" using y1 by auto
have int_K2: "interior K2 = {f l2<..<f u2}"
using K2_eq lu2 fl2u2 by (auto simp: interior_atLeastAtMost_real)
then have y_in2: "f l2 < y" "y < f u2" using y2 by auto
have fl1_lt_fu1: "f l1 < f u1"
using int_K1 y1 by auto
have fl2_lt_fu2: "f l2 < f u2"
using int_K2 y2 by auto
have l1_lt_u1: "l1 < u1"
using fl1_lt_fu1 lu1(1) by (cases "l1 = u1") auto
have l2_lt_u2: "l2 < u2"
using fl2_lt_fu2 lu2(1) by (cases "l2 = u2") auto
have "l1 < u2" "l2 < u1"
using l1a l2a mono_le y_in1 y_in2 by fastforce+
then have "max l1 l2 < min u1 u2"
using l1_lt_u1 l2_lt_u2 by auto
then have "(max l1 l2 + min u1 u2) / 2 ∈ {l1<..<u1} ∩ {l2<..<u2}"
using l1_lt_u1 l2_lt_u2 by auto
then have "(max l1 l2 + min u1 u2) / 2 ∈ interior k1 ∩ interior k2"
using lu1(2) lu2(2) by (simp add: interior_atLeastAtMost_real)
with int_k1k2 show False by auto
qed
next
show "⋃D = ⋃D" ..
qed
moreover have ‹⋃D ⊆ {f a..f b}›
proof
fix x assume "x ∈ ⋃D"
then obtain K where KD: "K ∈ D" and xK: "x ∈ K" by auto
from KD obtain k where kd: "k ∈ d" and K_eq: "K = {f (Inf k)..f (Sup k)}"
and k_sub: "k ⊆ {a..b}"
unfolding D_def using kprops by auto
obtain l u where lu: "l ≤ u" "k = {l..u}" "Inf k = l" "Sup k = u"
using k_interval[OF kd] by blast
have k_sub: "k ⊆ {a..b}" using kprops kd by auto
then have "l ∈ {a..b}" "u ∈ {a..b}" using lu by auto
then have "f a ≤ f l" "f u ≤ f b" using mono_le by auto
then show "x ∈ {f a..f b}" using xK K_eq lu by auto
qed
ultimately have *: ‹(∑k∈D. norm (g (Sup k) - g (Inf k))) ≤ vector_variation {f a..f b} g›
using has_bounded_variation_works [OF bv] by auto
have **: "norm (g (f (Sup x)) - g (f (Inf x))) = 0"
if "x ∈ d" "y ∈ d" "x ≠ y"
and eq: "{f (Inf x)..f (Sup x)} = {f (Inf y)..f (Sup y)}"
for x y
proof -
obtain l1 u1 where lu1: "l1 ≤ u1" "x = {l1..u1}" "Inf x = l1" "Sup x = u1"
using k_interval[OF ‹x ∈ d›] by blast
obtain l2 u2 where lu2: "l2 ≤ u2" "y = {l2..u2}" "Inf y = l2" "Sup y = u2"
using k_interval[OF ‹y ∈ d›] by blast
have x_sub: "x ⊆ {a..b}" using kprops ‹x ∈ d› by auto
have y_sub: "y ⊆ {a..b}" using kprops ‹y ∈ d› by auto
have la1: "l1 ∈ {a..b}" "u1 ∈ {a..b}" using x_sub lu1 by auto
have la2: "l2 ∈ {a..b}" "u2 ∈ {a..b}" using y_sub lu2 by auto
have fl1u1: "f l1 ≤ f u1" using fInf_le_fSup[OF ‹x ∈ d›] lu1 by simp
have fl2u2: "f l2 ≤ f u2" using fInf_le_fSup[OF ‹y ∈ d›] lu2 by simp
have eq': "{f l1..f u1} = {f l2..f u2}" using eq lu1 lu2 by simp
have fl_eq: "f l1 = f l2" and fu_eq: "f u1 = f u2"
using eq' fl1u1 fl2u2 by (auto simp: Icc_eq_Icc)
have int_xy: "interior x ∩ interior y = {}"
using int_disj[OF ‹x ∈ d› ‹y ∈ d› ‹x ≠ y›] .
have disj: "{l1<..<u1} ∩ {l2<..<u2} = {}"
using int_xy lu1(2) lu2(2) by (simp add: interior_atLeastAtMost_real)
have "f l1 = f u1"
proof (cases "u1 ≤ l2")
case True
then have "f u1 ≤ f l2" using mono_le la1(2) la2(1) by auto
then show ?thesis using fl_eq fl1u1 by linarith
next
case False
then have "l2 < u1" by linarith
show ?thesis
proof (cases "u2 ≤ l1")
case True
then have "f u2 ≤ f l1" using mono_le la2(2) la1(1) by auto
then show ?thesis using fu_eq fl2u2 fl_eq by linarith
next
case False
then have "l1 < u2" by linarith
have "l1 = u1 ∨ l2 = u2"
using ‹l1 < u2› ‹l2 < u1› disj lu1(1) lu2(1) by force
then show ?thesis
using fl_eq fu_eq by fastforce
qed
qed
then show ?thesis using lu1 lu2 by simp
qed
show ?thesis
proof -
let ?h = ‹λk. {f (Inf k)..f (Sup k)}›
let ?G = ‹λK. norm (g (Sup K) - g (Inf K))›
have D_eq: ‹D = ?h ` d› unfolding D_def ..
have sup_h: ‹Sup {f (Inf k)..f (Sup k)} = f (Sup k)› if ‹k ∈ d› for k
using fInf_le_fSup[OF that] by (simp add: cSup_atLeastAtMost)
have inf_h: ‹Inf {f (Inf k)..f (Sup k)} = f (Inf k)› if ‹k ∈ d› for k
using fInf_le_fSup[OF that] by (simp add: cInf_atLeastAtMost)
have ‹?G (?h x) = 0› if ‹x ∈ d› ‹y ∈ d› ‹x ≠ y› ‹?h x = ?h y› for x y
using ** fInf_le_fSup that by auto
then have eq1: ‹sum ?G D = sum (?G ∘ ?h) d›
unfolding D_eq using ‹finite d› by (intro sum.reindex_nontrivial)
have ‹(?G ∘ ?h) k = norm (g (f (Sup k)) - g (f (Inf k)))› if ‹k ∈ d› for k
by (simp add: o_def sup_h[OF that] inf_h[OF that])
then have ‹(∑k∈d. norm ((g ∘ f) (Sup k) - (g ∘ f) (Inf k))) = sum (?G ∘ ?h) d›
by auto
then show ?thesis using eq1 * by linarith
qed
qed
then show ?th1 ?th2
using has_bounded_vector_variation_on_interval by blast+
qed
lemma Lipschitz_imp_has_bounded_variation:
assumes "bounded S"
and "⋀x y. x ∈ S ⟹ y ∈ S ⟹ norm (f x - f y) ≤ B * norm (x - y)"
shows "has_bounded_variation_on f S"
unfolding has_bounded_variation_on_def has_bounded_setvariation_on_def
proof -
from assms(1) obtain R where R: "⋀x. x ∈ S ⟹ ¦x¦ ≤ R"
unfolding bounded_real by auto
have R_nonneg: "0 ≤ R" if "S ≠ {}" using that R by (auto intro: order_trans[OF abs_ge_zero])
then have s_sub: "S ⊆ cbox (-R) R" using R
by fastforce
show "∃M. ∀d t. d division_of t ∧ t ⊆ S ⟶
(∑k∈d. norm (f (Sup k) - f (Inf k))) ≤ M"
proof (intro exI[of _ "¦B¦ * content (cbox (-R) R)"] allI impI)
fix d t assume dt: "d division_of t ∧ t ⊆ S"
obtain fin_d: "finite d" and union_d: "⋃d = t"
and div_union: "d division_of ⋃d" and union_sub: "⋃d ⊆ cbox (-R) R"
by (metis division_of_def dt order.trans s_sub)
obtain q where dq: "d ⊆ q" and q_div: "q division_of cbox (-R) R" and "finite q"
using partial_division_extend_interval[OF div_union union_sub]
by (metis division_of_finite)
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"
with division_ofD dt kd obtain l u where
k_eq: "k = cbox l u" and kne: "k ≠ {}" and lu: "l ≤ u"
using dt kd
by (metis atLeastatMost_empty_iff box_real(2))
then have lu: "l ≤ u"
by fastforce
have "k ⊆ t" using kd union_d by auto
then have ls: "l ∈ S" and us: "u ∈ S"
using lu dt k_eq by (auto simp: cbox_interval)
have "norm (f u - f l) ≤ B * norm (u - l)"
using assms(2)[OF us ls] .
also have "… = B * (u - l)" using lu by (simp add: real_norm_def)
also have "… ≤ ¦B¦ * (u - l)" by (intro mult_right_mono) (use lu in auto)
also have "… = ¦B¦ * content k"
using lu k_eq by (simp add: cbox_interval)
finally show "norm (f (Sup k) - f (Inf k)) ≤ ¦B¦ * content k"
using lu k_eq by (simp add: cbox_interval)
qed
also have "… = ¦B¦ * (∑k∈d. content k)"
by (simp add: sum_distrib_left)
also have "… ≤ ¦B¦ * (∑k∈q. content k)"
by (intro mult_left_mono sum_mono2[OF ‹finite q› dq]) auto
also have "(∑k∈q. content k) = content (cbox (-R) R)"
using additive_content_division[OF q_div] .
finally show "(∑k∈d. norm (f (Sup k) - f (Inf k))) ≤ ¦B¦ * content (cbox (-R) R)" .
qed
qed
lemma Lipschitz_vector_variation_le:
assumes bv: ‹has_bounded_variation_on f {a..b}›
and R: ‹∀x y. x ∈ {a..b} ⟶ y ∈ {a..b} ⟶ norm (f x - f y) ≤ B * ¦x - y¦›
and xab: ‹x ∈ {a..b}› and yab: ‹y ∈ {a..b}› and le: ‹x ≤ y›
shows ‹¦vector_variation {a..x} f - vector_variation {a..y} f¦ ≤ B * ¦x - y¦›
proof -
have bv_ay: ‹has_bounded_variation_on f {a..y}›
using has_bounded_variation_on_subset[OF bv] yab by auto
have x_in: ‹x ∈ {a..y}›
using xab le by auto
have combine: ‹vector_variation {a..y} f =
vector_variation {a..x} f + vector_variation {x..y} f›
using vector_variation_combine[OF bv_ay x_in] .
have bv_xy: ‹has_bounded_variation_on f {x..y}›
using has_bounded_variation_on_subset[OF bv] xab yab le by auto
have vv_xy_le: ‹vector_variation {x..y} f ≤ B * (y - x)›
proof (rule has_bounded_variation_works(2)[OF bv_xy])
fix d t assume dt: ‹d division_of t› ‹t ⊆ {x..y}›
show ‹(∑k∈d. norm (f (Sup k) - f (Inf k))) ≤ B * (y - x)›
proof -
have fin_d: ‹finite d›
using division_of_finite[OF dt(1)] .
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›
from division_ofD(2,4)[OF dt(1) kd] obtain l u where
k_eq: ‹k = cbox l u› and kne: ‹k ≠ {}›
by (metis cbox_division_memE dt(1) kd)
then have lu: ‹l ≤ u› by fastforce
have ‹k ⊆ {x..y}›
using kd dt by blast
then have ls: ‹l ∈ {a..b}› and us: ‹u ∈ {a..b}›
using lu k_eq xab yab le by (auto simp: cbox_interval)
have ‹norm (f (Sup k) - f (Inf k)) = norm (f u - f l)›
using lu k_eq by (simp add: cbox_interval)
also have ‹… ≤ B * norm (u - l)›
using R us ls by auto
also have ‹… = B * (u - l)›
using lu by (simp add: real_norm_def)
also have ‹… = B * content k›
using lu k_eq by (simp add: cbox_interval)
finally show ‹norm (f (Sup k) - f (Inf k)) ≤ B * content k› .
qed
also have §: ‹… = B * (∑k∈d. content k)›
by (simp add: sum_distrib_left)
also have ‹… ≤ B * (y - x)›
proof -
have sum_le: ‹(∑k∈d. content k) ≤ y - x›
by (metis le cbox_interval dt measure_lborel_Icc subadditive_content_division)
show ?thesis
proof (cases ‹B ≥ 0›)
case True
then show ?thesis using sum_le by (intro mult_left_mono) auto
next
case False
then have Bneg: ‹B < 0› by linarith
have ‹∀k∈d. content k ≥ 0› by (simp add: content_nonneg)
then have ‹∀k∈d. B * content k ≤ 0›
using Bneg by (simp add: mult_nonpos_nonneg)
then have ‹(∑k∈d. B * content k) ≤ 0›
using sum_nonpos by metis
moreover have ‹(∑k∈d. norm (f (Sup k) - f (Inf k))) ≤ (∑k∈d. B * content k)›
using ‹(∑k∈d. norm (f (Sup k) - f (Inf k))) ≤ (∑k∈d. B * content k)› .
ultimately show ?thesis
using Bneg le
by (smt (verit) R § diff_ge_0_iff_ge norm_ge_zero order.trans xab yab)
qed
qed
finally show ?thesis .
qed
qed
have vv_nonneg: ‹vector_variation {x..y} f ≥ 0›
using vector_variation_pos_le using bv_xy by blast
have ‹¦vector_variation {a..x} f - vector_variation {a..y} f¦ =
vector_variation {x..y} f›
using combine vv_nonneg by linarith
also have ‹… ≤ B * (y - x)›
using vv_xy_le .
also have ‹… = B * ¦x - y¦›
using le by (simp add: abs_if)
finally show ?thesis .
qed
lemma Lipschitz_vector_variation:
assumes ‹has_bounded_variation_on f {a..b}›
shows ‹(∀x y. x ∈ {a..b} ⟶ y ∈ {a..b} ⟶
¦vector_variation {a..x} f - vector_variation {a..y} f¦ ≤ B * ¦x - y¦)
⟷ (∀x y. x ∈ {a..b} ⟶ y ∈ {a..b} ⟶
norm (f x - f y) ≤ B * ¦x - y¦)›
(is "?L = ?R")
proof
assume L: ?L
have ‹(∀x y. x ≤ y ⟶ x ∈ {a..b} ⟶ y ∈ {a..b} ⟶
norm (f x - f y) ≤ B * ¦x - y¦)›
proof (intro allI impI)
fix x y :: real assume xy: ‹x ≤ y› ‹x ∈ {a..b}› ‹y ∈ {a..b}›
have bv_ay: ‹has_bounded_variation_on f {a..y}›
using has_bounded_variation_on_subset[OF assms] xy(3) by auto
have x_in: ‹x ∈ {a..y}›
using xy by auto
have combine: ‹vector_variation {a..y} f =
vector_variation {a..x} f + vector_variation {x..y} f›
using vector_variation_combine[OF bv_ay x_in] .
have bv_xy: ‹has_bounded_variation_on f {x..y}›
using has_bounded_variation_on_subset[OF assms] xy by auto
have ‹norm (f x - f y) ≤ vector_variation {x..y} f›
using vector_variation_ge_norm_function[OF bv_xy] xy(1) by auto
then show ‹norm (f x - f y) ≤ B * ¦x - y¦›
using combine L xy(2,3) by fastforce
qed
then show ?R
by (metis abs_minus_commute linorder_linear norm_minus_commute)
next
assume R: ?R
then show ?L
by (smt (verit, ccfv_SIG) Lipschitz_vector_variation_le assms norm_minus_commute
real_norm_def)
qed
lemma vector_variation_minus_function_monotone:
assumes "has_bounded_variation_on f {a..b}" "x ∈ {a..b}" "y ∈ {a..b}" "x ≤ y"
shows "norm (f y - f x) ≤ vector_variation {x..y} f"
and "vector_variation {a..x} f - norm (f x - f a) ≤
vector_variation {a..y} f - norm (f y - f a)"
proof -
have bv_xy: "has_bounded_variation_on f {x..y}"
using has_bounded_variation_on_subset[OF assms(1)] assms(2,3) by auto
then show 1: "norm (f y - f x) ≤ vector_variation {x..y} f"
using vector_variation_ge_norm_function assms(4) by force
have "has_bounded_variation_on f {a..y}"
using has_bounded_variation_on_subset[OF assms(1)] assms(3) by auto
then have combine: "vector_variation {a..y} f =
vector_variation {a..x} f + vector_variation {x..y} f"
using vector_variation_combine assms by auto
have "norm (f y - f a) ≤ norm (f y - f x) + norm (f x - f a)"
using norm_triangle_ineq[of "f y - f x" "f x - f a"] by simp
with 1 show "vector_variation {a..x} f - norm (f x - f a) ≤
vector_variation {a..y} f - norm (f y - f a)"
using combine by linarith
qed
subsection ‹Bounded variation implies bounded›
lemma has_bounded_variation_on_imp_bounded:
assumes bv: "has_bounded_variation_on f S" "is_interval S"
shows "bounded (f ` S)"
proof (cases "S = {}")
case True then show ?thesis by (simp add: bounded_empty)
next
case False
then obtain a where a_s: "a ∈ S" by blast
have norm_le: "norm (f b - f a) ≤ vector_variation S f" if b_s: "b ∈ S" for b
proof -
let ?lo = "min a b" and ?hi = "max a b"
have lo_le_hi: "?lo ≤ ?hi" by simp
have sub: "{?lo..?hi} ⊆ S"
by (metis a_s box_real(2) bv(2) interval_subset_is_interval max_def min_def that)
have ne: "cbox ?lo ?hi ≠ {}" using lo_le_hi by (simp add: cbox_interval)
have div: "{{?lo..?hi}} division_of {?lo..?hi}"
using division_of_self[OF ne] by (simp add: cbox_interval)
have "norm (f b - f a) = norm (f ?hi - f ?lo)"
by (simp add: min_def max_def norm_minus_commute)
also have "… = (∑k∈{{?lo..?hi}}. norm (f (Sup k) - f (Inf k)))"
using lo_le_hi by (simp add: interval_bounds_real)
also have "… ≤ vector_variation S f"
using has_bounded_variation_works(1)[OF bv(1) div sub] .
finally show ?thesis .
qed
show ?thesis
proof (rule boundedI)
fix y assume "y ∈ f ` S"
then obtain b where b_s: "b ∈ S" and y_eq: "y = f b" by auto
have "norm (f b) ≤ norm (f a) + norm (f b - f a)"
by (rule norm_triangle_sub)
also have "… ≤ norm (f a) + vector_variation S f"
using norm_le[OF b_s] by simp
finally show "norm y ≤ norm (f a) + vector_variation S f"
by (simp add: y_eq)
qed
qed
corollary has_bounded_variation_on_imp_bounded_on_interval:
assumes "has_bounded_variation_on f {a..b}"
shows "bounded (f ` {a..b})"
using has_bounded_variation_on_imp_bounded[OF assms is_interval_cc] .
subsection ‹Increasing/decreasing functions›
lemma division_telescope_eq:
fixes g :: "real ⇒ real"
assumes "d division_of {a..b}" and "a ≤ b"
shows "(∑k∈d. (g (Sup k) - g (Inf k))) = g b - g a"
proof -
define h where "h S = (if S = {} then 0 else g (Sup S) - g (Inf S))" for S :: "real set"
have h_singleton: "h {x} = 0" for x unfolding h_def by simp
have h_interval: "h {l..u} = g u - g l" if "l ≤ u" for l u
unfolding h_def using that by auto
have "operative (+) 0 h"
proof (rule operative.intro)
show "comm_monoid_set (+) (0::real)"
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 have "a' ≥ b'" by (simp add: box_eq_empty)
then show "h (cbox a' b') = 0"
by (auto simp: h_def cbox_interval)
next
fix a' b' c :: real and k :: real
assume kB: "k ∈ Basis"
then have k1: "k = 1" by (simp add: Basis_real_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 ab: True
have eq1: "cbox a' b' ∩ {x. x ∙ k ≤ c} = {a'..min b' c}"
using k1 ab by (auto simp: cbox_interval min_def)
have eq2: "cbox a' b' ∩ {x. c ≤ x ∙ k} = {max a' c..b'}"
using k1 ab by (auto simp: cbox_interval max_def)
have whole: "h (cbox a' b') = g b' - g a'"
using h_interval[OF ab] by (simp add: cbox_interval)
show ?thesis
proof (cases "c < a'")
case True
then have "{a'..min b' c} = {}" by auto
moreover have "max a' c = a'" using True by auto
ultimately show ?thesis using eq1 eq2 whole h_def by auto
next
case False
then show ?thesis
using eq1 eq2 h_def by fastforce
qed
next
case False
then have "cbox a' b' = {}" by (auto simp: cbox_interval)
moreover have "cbox a' b' ∩ {x. x ∙ k ≤ c} = {}" using calculation by auto
moreover have "cbox a' b' ∩ {x. c ≤ x ∙ k} = {}" using calculation by auto
ultimately show ?thesis unfolding h_def by simp
qed
qed
qed
then have eq: "sum h d = h (cbox a b)"
using assms(1) operative.division[of "(+)" 0 h d a b]
by (simp add: sum_def cbox_interval)
have "h (cbox a b) = g b - g a"
using h_interval[OF assms(2)] by (simp add: cbox_interval)
moreover have "sum h d = (∑k∈d. (g (Sup k) - g (Inf k)))"
by (metis (mono_tags, lifting) assms(1) division_ofD(3) h_def sum.cong)
ultimately show ?thesis using eq by simp
qed
lemma increasing_bounded_variation:
fixes f :: "real ⇒ 'a::ordered_euclidean_space"
assumes "mono_on {a..b} f"
shows "has_bounded_variation_on f {a..b}"
unfolding has_bounded_variation_on_interval
proof (intro exI allI impI)
fix d assume div_d: "d division_of {a..b}"
have fin_d: "finite d" using division_of_finite[OF div_d] .
have "(∑k∈d. norm (f (Sup k) - f (Inf k))) ≤ (∑k∈d. (∑i∈Basis. ¦(f (Sup k) - f (Inf k)) ∙ i¦))"
by (intro sum_mono norm_le_l1)
also have "… = (∑i∈Basis. (∑k∈d. ¦(f (Sup k) - f (Inf k)) ∙ i¦))"
by (rule sum.swap)
also have "… = (∑i∈Basis. (∑k∈d. (f (Sup k) ∙ i - f (Inf k) ∙ i)))"
proof (intro sum.cong refl)
fix i::'a and k assume iBasis: "i ∈ Basis" and kd: "k ∈ d"
from division_ofD(2,4)[OF div_d kd] obtain l u where
k_eq: "k = cbox l u" and "k ≠ {}"
by (metis div_d division_ofD(3) kd)
then have lu: "l ≤ u"
by force
have "k ⊆ {a..b}" using division_ofD(2)[OF div_d kd] by auto
then have "l ∈ {a..b}" "u ∈ {a..b}" using lu k_eq by (auto simp: cbox_interval)
have "f l ≤ f u"
using assms ‹l ∈ {a..b}› ‹u ∈ {a..b}› lu by (simp add: monotone_on_def)
then have "f l ∙ i ≤ f u ∙ i" using iBasis eucl_le by metis
have "Inf k = l" "Sup k = u" using lu k_eq by (auto simp: cbox_interval)
then show "¦(f (Sup k) - f (Inf k)) ∙ i¦ = f (Sup k) ∙ i - f (Inf k) ∙ i"
using ‹f l ∙ i ≤ f u ∙ i› by (simp add: inner_diff_left abs_of_nonneg)
qed
also have "… ≤ (∑i∈Basis. ¦(f b - f a) ∙ i¦)"
proof (intro sum_mono)
fix i::'a assume iBasis: "i ∈ Basis"
show "(∑k∈d. (f (Sup k) ∙ i - f (Inf k) ∙ i)) ≤ ¦(f b - f a) ∙ i¦"
proof (cases "d = {}")
case True
then show ?thesis by simp
next
case False
then obtain k where "k ∈ d" and "k ⊆ {a..b}" "k ≠ {}" "a ≤ b" using division_ofD(2,3)[OF div_d]
by fastforce
then have tele: "(∑k∈d. (f (Sup k) ∙ i - f (Inf k) ∙ i)) = f b ∙ i - f a ∙ i"
using division_telescope_eq[OF div_d, of "λx. f x ∙ i"] by simp
also have "… ≤ ¦(f b - f a) ∙ i¦" by (simp add: inner_diff_left)
finally show ?thesis .
qed
qed
also have "… ≤ (∑i::'a∈Basis. norm (f b - f a))"
by (intro sum_mono) (auto simp: Basis_le_norm)
also have "… = DIM('a) * norm (f b - f a)"
by simp
finally show "(∑k∈d. norm (f (Sup k) - f (Inf k))) ≤ DIM('a) * norm (f b - f a)" .
qed
lemma increasing_vector_variation:
fixes f :: "real ⇒ real"
assumes mono: "mono_on {a..b} f"
and ab: "a ≤ b"
shows "vector_variation {a..b} f = norm (f b - f a)"
proof (rule antisym)
have bv: "has_bounded_variation_on f {a..b}"
using increasing_bounded_variation[OF mono] .
show "norm (f b - f a) ≤ vector_variation {a..b} f"
using vector_variation_ge_norm_function[OF bv] ab by auto
have vv_eq: "vector_variation {a..b} f =
Sup {(∑k∈d. norm (f (Sup k) - f (Inf k))) | d. d division_of {a..b}}"
using vector_variation_on_interval[OF bv] .
have fa_le_fb: "f a ≤ f b" using mono ab
by (simp add: monotone_on_def)
show "vector_variation {a..b} f ≤ norm (f b - f a)"
unfolding vv_eq
proof (rule cSup_least)
obtain p where "p division_of cbox a b" using elementary_interval by blast
then show "{(∑k∈d. norm (f (Sup k) - f (Inf k))) | d. d division_of {a..b}} ≠ {}"
by (auto simp: cbox_interval)
next
fix S assume "S ∈ {(∑k∈d. norm (f (Sup k) - f (Inf k))) | d. d division_of {a..b}}"
then obtain d where div_d: "d division_of {a..b}"
and s_eq: "S = (∑k∈d. norm (f (Sup k) - f (Inf k)))" by auto
have "(∑k∈d. norm (f (Sup k) - f (Inf k))) = (∑k∈d. (f (Sup k) - f (Inf k)))"
proof (rule sum.cong[OF refl])
fix k assume kd: "k ∈ d"
from division_ofD(2,4)[OF div_d kd] obtain l u where
k_eq: "k = cbox l u" and "k ≠ {}" and lu: "l ≤ u" and "k ⊆ {a..b}"
by (metis atLeastatMost_empty_iff2 box_real(2) div_d division_ofD(3) kd)
then have "l ∈ {a..b}" "u ∈ {a..b}" using lu k_eq by (auto simp: cbox_interval)
then have "f l ≤ f u"
using mono lu by (simp add: monotone_on_def)
have "Inf k = l" "Sup k = u" using lu k_eq by (auto simp: cbox_interval)
then show "norm (f (Sup k) - f (Inf k)) = f (Sup k) - f (Inf k)"
using ‹f l ≤ f u› by auto
qed
also have "… = f b - f a"
using division_telescope_eq[OF div_d ab] .
also have "… = norm (f b - f a)"
using fa_le_fb by auto
finally show "S ≤ norm (f b - f a)" using s_eq by simp
qed
qed
subsection ‹Darboux decomposition›
text ‹A function of bounded variation on an interval can be written as the difference
of two monotone functions. This is the Darboux (or Jordan) decomposition theorem.›
lemma has_bounded_variation_Darboux_gen:
fixes f :: "real ⇒ real"
assumes ivs: "is_interval S" and bv: "has_bounded_variation_on f S"
shows "∃g h. mono_on S g ∧ mono_on S h ∧ (∀x. f x = g x - h x)"
proof -
define g where "g x = vector_variation (S ∩ {..x}) f" for x
define h where "h x = vector_variation (S ∩ {..x}) f - f x" for x
have sub_xy: "{x..y} ⊆ S" if "x ∈ S" "y ∈ S" "x ≤ y" for x y
using ivs that unfolding is_interval_def
by (metis cbox_interval interval_subset_is_interval ivs)
have g_mono: "mono_on S g"
unfolding mono_on_def g_def
proof (intro allI impI)
fix x y assume "x ∈ S ∧ y ∈ S ∧ x ≤ y"
then have xy: "x ∈ S" "y ∈ S" "x ≤ y" by auto
have bv_sy: "has_bounded_variation_on f (S ∩ {..y})"
using has_bounded_variation_on_subset[OF bv] by auto
have sub: "S ∩ {..x} ⊆ S ∩ {..y}" using xy(3) by auto
show "vector_variation (S ∩ {..x}) f ≤ vector_variation (S ∩ {..y}) f"
using bv_sy sub
by (metis (mono_tags, lifting) dual_order.trans has_bounded_variation_on_subset
has_bounded_variation_works)
qed
have h_mono: "mono_on S h"
unfolding mono_on_def h_def
proof (intro allI impI)
fix x y assume "x ∈ S ∧ y ∈ S ∧ x ≤ y"
then have xy: "x ∈ S" "y ∈ S" "x ≤ y" by auto
have xy_sub: "{x..y} ⊆ S" by (rule sub_xy[OF xy])
have bv_sy: "has_bounded_variation_on f (S ∩ {..y})"
using has_bounded_variation_on_subset[OF bv] by auto
have iv_sy: "is_interval (S ∩ {..y})"
by (rule is_interval_Int[OF ivs is_interval_ic])
have x_in: "x ∈ S ∩ {..y}" using xy by auto
have split: "vector_variation (S ∩ {..y}) f =
vector_variation (S ∩ {..y} ∩ {..x}) f + vector_variation (S ∩ {..y} ∩ {x..}) f"
using vector_variation_split[OF iv_sy bv_sy, of x] by linarith
have eq1: "S ∩ {..y} ∩ {..x} = S ∩ {..x}" using xy(3) by auto
have eq2: "S ∩ {..y} ∩ {x..} = S ∩ {x..y}" using xy(3) by auto
have "S ∩ {x..y} = {x..y}" using xy_sub by auto
then have eq3: "S ∩ {..y} ∩ {x..} = {x..y}" using eq2 by auto
have bv_xy: "has_bounded_variation_on f {x..y}"
using has_bounded_variation_on_subset[OF bv xy_sub] .
have "f y - f x ≤ ¦f y - f x¦" by (rule abs_ge_self)
also have "… = norm (f y - f x)" by (simp add: real_norm_def)
also have "… ≤ vector_variation {x..y} f"
using vector_variation_ge_norm_function[OF bv_xy] xy(3) by auto
also have "… = vector_variation (S ∩ {..y}) f - vector_variation (S ∩ {..x}) f"
using split eq1 eq3 by simp
finally show "vector_variation (S ∩ {..x}) f - f x ≤ vector_variation (S ∩ {..y}) f - f y"
by linarith
qed
have eq: "∀x. f x = g x - h x"
unfolding g_def h_def by simp
show ?thesis
using g_mono h_mono eq by blast
qed
lemma has_bounded_variation_Darboux:
fixes f :: "real ⇒ real"
shows "has_bounded_variation_on f {a..b} ⟷
(∃g h. mono_on {a..b} g ∧ mono_on {a..b} h ∧ (∀x. f x = g x - h x))"
(is "?L ⟷ ?R")
proof
assume bv: ?L
define g where "g x = vector_variation {a..x} f" for x
define h where "h x = vector_variation {a..x} f - f x" for x
have g_mono: "mono_on {a..b} g"
unfolding mono_on_def g_def
by (metis atLeastAtMost_iff atLeastatMost_subset_iff bv has_bounded_variation_on_combine
landau_omega.R_refl vector_variation_monotone)
have h_mono: "mono_on {a..b} h"
unfolding mono_on_def h_def
proof (intro allI impI)
fix x y assume "x ∈ {a..b} ∧ y ∈ {a..b} ∧ x ≤ y"
then have xy: "x ∈ {a..b}" "y ∈ {a..b}" "x ≤ y" by auto
have "f y - f x ≤ ¦f y - f x¦"
by (rule abs_ge_self)
also have "… = norm (f y - f x)"
by (simp add: real_norm_def)
also have "… ≤ vector_variation {x..y} f"
using vector_variation_minus_function_monotone(1)[OF bv xy] .
also have "… = vector_variation {a..y} f - vector_variation {a..x} f"
by (smt (verit) bv has_bounded_variation_on_combine interval_cbox mem_box_real(2)
vector_variation_combine xy)
finally show "vector_variation {a..x} f - f x ≤ vector_variation {a..y} f - f y"
by linarith
qed
have eq: "∀x. f x = g x - h x"
unfolding g_def h_def by simp
show ?R
using g_mono h_mono eq by blast
next
assume ?R
then obtain g h where mono_g: "mono_on {a..b} g" and mono_h: "mono_on {a..b} h"
and eq: "∀x. f x = g x - h x" by blast
then show ?L
by (metis (no_types, lifting) ext has_bounded_variation_on_sub increasing_bounded_variation)
qed
lemma has_bounded_variation_Darboux_strict:
fixes f :: "real ⇒ real"
shows "has_bounded_variation_on f {a..b} ⟷
(∃g h. strict_mono_on {a..b} g ∧ strict_mono_on {a..b} h ∧ (∀x. f x = g x - h x))"
(is "?L ⟷ ?R")
proof
assume ?L
then obtain g h where mono_g: "mono_on {a..b} g" and mono_h: "mono_on {a..b} h"
and eq: "∀x. f x = g x - h x"
using has_bounded_variation_Darboux by blast
define g' where "g' x = g x + x" for x
define h' where "h' x = h x + x" for x
have sg: "strict_mono_on {a..b} g'"
unfolding strict_mono_on_def g'_def
by (metis add_le_less_mono linorder_not_less mono_g nle_le ord.mono_on_def)
have sh: "strict_mono_on {a..b} h'"
by (smt (verit, del_insts) h'_def mono_h monotone_on_def)
have "∀x. f x = g' x - h' x"
unfolding g'_def h'_def using eq by simp
then show ?R using sg sh by blast
next
assume ?R
then obtain g h where sg: "strict_mono_on {a..b} g" and sh: "strict_mono_on {a..b} h"
and eq: "∀x. f x = g x - h x" by blast
have mono_g: "mono_on {a..b} g"
using sg unfolding strict_mono_on_def mono_on_def
by (metis order_le_less)
have mono_h: "mono_on {a..b} h"
using sh unfolding strict_mono_on_def mono_on_def
by (metis le_less)
show ?L
using has_bounded_variation_Darboux mono_g mono_h eq by blast
qed
subsection ‹One-sided limits of monotone and BV functions›
text ‹A monotone increasing function on a closed interval has a left limit at every
point of that interval. The limit is the supremum of the function values to the left.›
lemma increasing_left_limit:
fixes f :: ‹real ⇒ real›
assumes mono: ‹mono_on {a..b} f› and c_in: ‹c ∈ {a..b}›
shows ‹∃l. (f ⤏ l) (at c within {a..c})›
proof (cases ‹c islimpt {a..c}›)
case False
then have ‹at c within {a..c} = bot›
by (simp add: trivial_limit_within)
then show ?thesis
using tendsto_bot by (intro exI) auto
next
case True
have ac: ‹a < c›
proof (rule ccontr)
assume ‹¬ a < c›
then have ‹{a..c} ⊆ {c}› using c_in by auto
then have ‹finite {a..c}› using finite_subset by blast
then show False using True islimpt_finite by blast
qed
define S where ‹S = f ` ({a..b} ∩ {..<c})›
have S_ne: ‹S ≠ {}›
unfolding S_def using ac c_in by force
have S_bdd: ‹bdd_above S›
unfolding S_def bdd_above_def using mono mono_onD
by(intro exI[of _ ‹f b›] ballI, fastforce)
define l where ‹l = Sup S›
show ?thesis
proof (intro exI tendstoI)
fix e :: real assume ‹e > 0›
have ‹l - e < l› using ‹e > 0› by simp
then obtain y where ‹y ∈ S› ‹l - e < y›
using less_cSup_iff[OF S_ne S_bdd] l_def by blast
then obtain d where d_in: ‹d ∈ {a..b}› and dc: ‹d < c› and fd: ‹l - e < f d›
unfolding S_def by auto
show ‹∀⇩F x in at c within {a..c}. dist (f x) l < e›
unfolding eventually_at_filter eventually_nhds
proof (intro exI conjI ballI impI)
show ‹open {d<..}› by auto
show ‹c ∈ {d<..}› using dc by auto
fix x assume ‹x ∈ {d<..}› ‹x ≠ c› ‹x ∈ {a..c}›
then have xc: ‹x < c› and xab: ‹x ∈ {a..b}› and dx: ‹d < x›
using c_in by auto
have fx_le_l: ‹f x ≤ l›
unfolding l_def
by (intro cSup_upper[OF _ S_bdd]) (auto simp: S_def intro: xab xc)
have ‹f d ≤ f x›
using mono d_in xab dx unfolding mono_on_def by auto
then have ‹l - e < f x› using fd by linarith
then show ‹dist (f x) l < e›
using fx_le_l unfolding dist_real_def by linarith
qed
qed
qed
lemma decreasing_left_limit:
fixes f :: ‹real ⇒ real›
assumes mono: ‹antimono_on {a..b} f› and c_in: ‹c ∈ {a..b}›
shows ‹∃l. (f ⤏ l) (at c within {a..c})›
proof -
have ‹mono_on {a..b} (λx. - f x)›
using mono unfolding mono_on_def monotone_on_def by auto
from increasing_left_limit[OF this c_in]
obtain l where ‹((λx. - f x) ⤏ l) (at c within {a..c})› by blast
then have ‹(f ⤏ - l) (at c within {a..c})›
by (rule tendsto_minus_cancel[where a=‹- l›, simplified])
then show ?thesis by blast
qed
lemma increasing_right_limit:
fixes f :: ‹real ⇒ real›
assumes mono: ‹mono_on {a..b} f› and c_in: ‹c ∈ {a..b}›
shows ‹∃l. (f ⤏ l) (at c within {c..b})›
proof (cases ‹c islimpt {c..b}›)
case False
then have ‹at c within {c..b} = bot›
by (simp add: trivial_limit_within)
then show ?thesis
using tendsto_bot by (intro exI) auto
next
case True
have cb: ‹c < b›
proof (rule ccontr)
assume ‹¬ c < b›
then have ‹{c..b} ⊆ {c}› using c_in by auto
then have ‹finite {c..b}› using finite_subset by blast
then show False using True islimpt_finite by blast
qed
define S where ‹S = f ` ({a..b} ∩ {c<..})›
have S_ne: ‹S ≠ {}›
proof -
have ‹b ∈ {a..b} ∩ {c<..}› using cb c_in by auto
then show ?thesis unfolding S_def by blast
qed
have S_bdd: ‹bdd_below S›
proof -
have ‹f a ≤ f x› if ‹x ∈ {a..b}› for x
using mono_onD[OF mono] that c_in by auto
then show ?thesis unfolding S_def bdd_below_def by (intro exI[of _ ‹f a›]) auto
qed
define l where ‹l = Inf S›
show ?thesis
proof (intro exI tendstoI)
fix e :: real assume ‹e > 0›
have ‹l < l + e› using ‹e > 0› by simp
then obtain y where ‹y ∈ S› ‹y < l + e›
using cInf_less_iff[OF S_ne S_bdd] l_def by blast
then obtain d where d_in: ‹d ∈ {a..b}› and dc: ‹c < d› and fd: ‹f d < l + e›
unfolding S_def by auto
show ‹∀⇩F x in at c within {c..b}. dist (f x) l < e›
unfolding eventually_at_filter eventually_nhds
proof (intro exI conjI ballI impI)
show ‹open {..<d}› by auto
show ‹c ∈ {..<d}› using dc by auto
fix x assume ‹x ∈ {..<d}› ‹x ≠ c› ‹x ∈ {c..b}›
then have xc: ‹c < x› and xab: ‹x ∈ {a..b}› and xd: ‹x < d›
using c_in by auto
have l_le_fx: ‹l ≤ f x›
unfolding l_def
by (intro cInf_lower[OF _ S_bdd]) (auto simp: S_def intro: xab xc)
have ‹f x ≤ f d›
using mono d_in xab xd unfolding mono_on_def by auto
then have ‹f x < l + e› using fd by linarith
then show ‹dist (f x) l < e›
using l_le_fx unfolding dist_real_def by linarith
qed
qed
qed
lemma decreasing_right_limit:
fixes f :: ‹real ⇒ real›
assumes mono: ‹antimono_on {a..b} f› and c_in: ‹c ∈ {a..b}›
shows ‹∃l. (f ⤏ l) (at c within {c..b})›
proof -
have ‹mono_on {a..b} (λx. - f x)›
using mono unfolding mono_on_def monotone_on_def by auto
from increasing_right_limit[OF this c_in]
obtain l where ‹((λx. - f x) ⤏ l) (at c within {c..b})› by blast
then have ‹(f ⤏ - l) (at c within {c..b})›
by (rule tendsto_minus_cancel[where a=‹- l›, simplified])
then show ?thesis by blast
qed
lemma has_bounded_variation_left_limit:
fixes f :: ‹real ⇒ real›
assumes bv: ‹has_bounded_variation_on f {a..b}› and c_in: ‹c ∈ {a..b}›
shows ‹∃l. (f ⤏ l) (at c within {a..c})›
proof -
from bv obtain g h where mono_g: ‹mono_on {a..b} g› and mono_h: ‹mono_on {a..b} h›
and eq: ‹∀x. f x = g x - h x›
using has_bounded_variation_Darboux by blast
from increasing_left_limit[OF mono_g c_in]
obtain l1 where l1: ‹(g ⤏ l1) (at c within {a..c})› by blast
from increasing_left_limit[OF mono_h c_in]
obtain l2 where l2: ‹(h ⤏ l2) (at c within {a..c})› by blast
have ‹(f ⤏ l1 - l2) (at c within {a..c})›
proof (rule Lim_transform_eventually[OF tendsto_diff[OF l1 l2]])
show ‹∀⇩F x in at c within {a..c}. g x - h x = f x›
using eq by (intro always_eventually) auto
qed
then show ?thesis by blast
qed
lemma has_bounded_variation_right_limit:
fixes f :: ‹real ⇒ real›
assumes bv: ‹has_bounded_variation_on f {a..b}› and c_in: ‹c ∈ {a..b}›
shows ‹∃l. (f ⤏ l) (at c within {c..b})›
proof -
from bv obtain g h where mono_g: ‹mono_on {a..b} g› and mono_h: ‹mono_on {a..b} h›
and eq: ‹∀x. f x = g x - h x›
using has_bounded_variation_Darboux by blast
from increasing_right_limit[OF mono_g c_in]
obtain l1 where l1: ‹(g ⤏ l1) (at c within {c..b})› by blast
from increasing_right_limit[OF mono_h c_in]
obtain l2 where l2: ‹(h ⤏ l2) (at c within {c..b})› by blast
have ‹(f ⤏ l1 - l2) (at c within {c..b})›
proof (rule Lim_transform_eventually[OF tendsto_diff[OF l1 l2]])
show ‹∀⇩F x in at c within {c..b}. g x - h x = f x›
using eq by (intro always_eventually) auto
qed
then show ?thesis by blast
qed
subsection ‹Continuity of vector variation›
lemma continuous_vector_variation_left_1:
fixes f :: ‹real ⇒ real›
assumes ‹has_bounded_variation_on f {a..b}› ‹c ∈ {a..b}›
shows ‹continuous (at c within {a..c}) (λx. vector_variation {a..x} f) ⟷
continuous (at c within {a..c}) f› (is ‹?L = ?R ›)
proof
assume L: ?L
show ?R
proof -
from assms have ac: ‹a ≤ c› and cb: ‹c ≤ b› by auto
have bv_ac: ‹has_bounded_variation_on f {a..c}›
using has_bounded_variation_on_subset[OF assms(1)] assms(2) by auto
from L have vv_tend: ‹((λx. vector_variation {a..x} f) ⤏ vector_variation {a..c} f) (at c within {a..c})›
by (simp add: continuous_within)
have diff_tend: ‹((λx. vector_variation {a..c} f - vector_variation {a..x} f) ⤏ 0) (at c within {a..c})›
using tendsto_diff[OF tendsto_const vv_tend] by (metis diff_self)
have bound: ‹∀⇩F x in at c within {a..c}. norm (f x - f c) ≤ vector_variation {a..c} f - vector_variation {a..x} f›
proof (unfold at_within_def eventually_inf_principal, rule always_eventually, rule allI, rule impI)
fix x assume xS: ‹x ∈ {a..c} - {c}›
then have xac: ‹x ∈ {a..c}› and xc: ‹x ≠ c› by auto
then have xle: ‹x ≤ c› by auto
have bv_xc: ‹has_bounded_variation_on f {x..c}›
using has_bounded_variation_on_subset[OF bv_ac] xac by auto
have ‹norm (f x - f c) ≤ vector_variation {x..c} f›
using vector_variation_ge_norm_function[OF bv_xc] xac by auto
also have ‹… = vector_variation {a..c} f - vector_variation {a..x} f›
using vector_variation_combine[OF bv_ac xac] by linarith
finally show ‹norm (f x - f c) ≤ vector_variation {a..c} f - vector_variation {a..x} f› .
qed
have ‹((λx. f x - f c) ⤏ 0) (at c within {a..c})›
by (rule Lim_null_comparison[OF bound diff_tend])
then show ?R
by (simp add: continuous_within LIM_zero_iff)
qed
next
assume R: ?R
show ?L
proof (cases ‹c islimpt {a..c}›)
case False
then show ?thesis
using trivial_limit_within continuous_bot by metis
next
case True
from assms(1) obtain g h where
mono_g: ‹mono_on {a..b} g› and mono_h: ‹mono_on {a..b} h›
and eq: ‹⋀x. f x = g x - h x›
using has_bounded_variation_Darboux[of f a b] by auto
obtain gc where gc: ‹(g ⤏ gc) (at c within {a..c})›
using increasing_left_limit[OF mono_g assms(2)] by auto
obtain hc where hc: ‹(h ⤏ hc) (at c within {a..c})›
using increasing_left_limit[OF mono_h assms(2)] by auto
define k where "k ≡ gc - g c"
have ‹k = hc - h c›
proof -
have ‹(f ⤏ gc - hc) (at c within {a..c})›
by (metis (lifting) ext eq gc hc tendsto_diff)
moreover have ‹(f ⤏ f c) (at c within {a..c})›
using R by (simp add: continuous_within)
moreover have ‹at c within {a..c} ≠ bot›
using True trivial_limit_within by blast
ultimately have ‹f c = gc - hc›
using tendsto_unique by blast
then show ?thesis unfolding k_def eq by algebra
qed
define g' where ‹g' ≡ λx. if c ≤ x then g(x) + k else g(x)›
define h' where ‹h' ≡ λx. if c ≤ x then h(x) + k else h(x)›
have not_bot: ‹at c within {a..c} ≠ bot›
using True trivial_limit_within by blast
have mono_shift: ‹mono_on {a..c} (λx. if c ≤ x then φ x + k else φ x)›
if mono_φ: ‹mono_on {a..b} φ› and lim_φ: ‹(φ ⤏ φc) (at c within {a..c})›
and k_eq: ‹k = φc - φ c› for φ φc
proof (unfold mono_on_def, intro allI impI, elim conjE)
fix r S assume rs: ‹r ∈ {a..c}› ‹S ∈ {a..c}› ‹r ≤ S›
have φ_le_φc: ‹φ x ≤ φc› if ‹x ∈ {a..c}› ‹x < c› for x
proof (rule tendsto_lowerbound[OF lim_φ _ not_bot])
show ‹∀⇩F y in at c within {a..c}. φ x ≤ φ y›
unfolding eventually_at_filter
proof (rule eventually_nhds_metric[THEN iffD2], rule exI[of _ ‹c - x›], intro conjI allI impI)
show ‹0 < c - x› using that by simp
next
fix y assume dy: ‹dist y c < c - x› and yc: ‹y ≠ c› and yac: ‹y ∈ {a..c}›
then have ‹y ∈ {a..b}› using assms(2) by auto
have ‹x ∈ {a..b}› using that assms(2) by auto
have ‹x ≤ y› using dy by (auto simp: dist_real_def)
show ‹φ x ≤ φ y›
using mono_onD[OF mono_φ ‹x ∈ {a..b}› ‹y ∈ {a..b}› ‹x ≤ y›] .
qed
qed
show ‹(if c ≤ r then φ r + k else φ r) ≤ (if c ≤ S then φ S + k else φ S)›
proof (cases ‹S < c›)
case True
then show ?thesis
using mono_onD[OF mono_φ] rs assms(2) by auto
next
case False
then show ?thesis
using φ_le_φc rs k_eq by auto
qed
qed
have mono_g': ‹mono_on {a..c} g'›
unfolding g'_def using mono_shift[OF mono_g gc] k_def by simp
have mono_h': ‹mono_on {a..c} h'›
unfolding h'_def using mono_shift[OF mono_h hc ‹k = hc - h c›] .
have ‹f = (λx. g' x - h' x)›
by (force simp: eq g'_def h'_def)
show ?thesis
proof -
have ac: ‹a ≤ c› using assms(2) by auto
have bv_ac: ‹has_bounded_variation_on f {a..c}›
using has_bounded_variation_on_subset[OF assms(1)] assms(2) by auto
have cont_shift: ‹((λx. if c ≤ x then φ x + k else φ x) ⤏
(if c ≤ c then φ c + k else φ c)) (at c within {a..c})›
if ‹(φ ⤏ φc) (at c within {a..c})› ‹k = φc - φ c› for φ φc
proof -
have ‹∀⇩F x in at c within {a..c}. (if c ≤ x then φ x + k else φ x) = φ x›
unfolding eventually_at_filter by auto
then have ‹((λx. if c ≤ x then φ x + k else φ x) ⤏ φc) (at c within {a..c})›
using that(1) tendsto_cong by force
then show ?thesis using that(2) by simp
qed
have cont_g': ‹(g' ⤏ g' c) (at c within {a..c})›
unfolding g'_def using cont_shift[OF gc] k_def by simp
have cont_h': ‹(h' ⤏ h' c) (at c within {a..c})›
unfolding h'_def using cont_shift[OF hc ‹k = hc - h c›] .
have vv_mono: ‹vector_variation {x..c} φ' = norm (φ' c - φ' x)›
if ‹mono_on {a..c} φ'› ‹x ∈ {a..c}› for φ' :: ‹real ⇒ real› and x
using increasing_vector_variation[OF mono_on_subset[OF that(1)]] that(2) by auto
show ‹continuous (at c within {a..c}) (λx. vector_variation {a..x} f)›
unfolding continuous_within tendsto_iff
proof (intro allI impI)
fix ε :: real assume ‹ε > 0›
then have e2: ‹ε / 2 > 0› by simp
have ev_gh': ‹∀⇩F x in at c within {a..c}.
dist (g' x) (g' c) < ε / 2 ∧ dist (h' x) (h' c) < ε / 2 ∧ x ∈ {a..c}›
proof (intro eventually_conj)
show ‹∀⇩F x in at c within {a..c}. dist (g' x) (g' c) < ε / 2›
using tendstoD[OF cont_g' e2] .
show ‹∀⇩F x in at c within {a..c}. dist (h' x) (h' c) < ε / 2›
using tendstoD[OF cont_h' e2] .
show ‹∀⇩F x in at c within {a..c}. x ∈ {a..c}›
unfolding eventually_at_filter by (auto intro: always_eventually)
qed
show ‹∀⇩F x in at c within {a..c}. dist (vector_variation {a..x} f) (vector_variation {a..c} f) < ε›
proof (rule eventually_mono[OF ev_gh'])
fix x
assume H: ‹dist (g' x) (g' c) < ε / 2 ∧ dist (h' x) (h' c) < ε / 2 ∧ x ∈ {a..c}›
then have dg: ‹dist (g' x) (g' c) < ε / 2›
and dh: ‹dist (h' x) (h' c) < ε / 2›
and xac: ‹x ∈ {a..c}› by auto
show ‹dist (vector_variation {a..x} f) (vector_variation {a..c} f) < ε›
proof (cases ‹x = c›)
case True
then show ?thesis using ‹ε > 0› by simp
next
case False
then have xc: ‹x < c› and xle: ‹x ≤ c› using xac by auto
have bv_xc: ‹has_bounded_variation_on f {x..c}›
using has_bounded_variation_on_subset[OF bv_ac] xac by auto
have vv_f_xc: ‹vector_variation {x..c} f ≤ vector_variation {x..c} g' + vector_variation {x..c} h'›
proof -
have ‹{x..c} ⊆ {a..c}› using xac by auto
have ‹vector_variation {x..c} f = vector_variation {x..c} (λt. g' t - h' t)›
using ‹f = (λx. g' x - h' x)› by simp
also have ‹… ≤ vector_variation {x..c} g' + vector_variation {x..c} h'›
using vector_variation_triangle_sub
[OF increasing_bounded_variation[OF mono_on_subset[OF mono_g' ‹{x..c} ⊆ {a..c}›]]
increasing_bounded_variation[OF mono_on_subset[OF mono_h' ‹{x..c} ⊆ {a..c}›]]] .
finally show ?thesis .
qed
have ‹dist (vector_variation {a..x} f) (vector_variation {a..c} f)
= ¦vector_variation {a..x} f - vector_variation {a..c} f¦›
by (simp add: dist_real_def)
also have ‹… = vector_variation {x..c} f›
using vector_variation_combine[OF bv_ac xac] vector_variation_pos_le[OF bv_xc]
by linarith
also have ‹… ≤ vector_variation {x..c} g' + vector_variation {x..c} h'›
using vv_f_xc .
also have ‹… = norm (g' c - g' x) + norm (h' c - h' x)›
using vv_mono[OF mono_g' xac] vv_mono[OF mono_h' xac] by simp
also have ‹… = dist (g' x) (g' c) + dist (h' x) (h' c)›
by (simp add: dist_real_def dist_commute)
also have ‹… < ε / 2 + ε / 2›
using dg dh by linarith
also have ‹… = ε› by simp
finally show ?thesis .
qed
qed
qed
qed
qed
qed
lemma continuous_vector_variation_left:
fixes f :: ‹real ⇒ 'a::euclidean_space›
assumes ‹has_bounded_variation_on f {a..b}› ‹c ∈ {a..b}›
shows ‹continuous (at c within {a..c}) (λx. vector_variation {a..x} f) ⟷
continuous (at c within {a..c}) f› (is ‹?L = ?R›)
proof
assume L: ?L
show ?R
proof -
have bv_ac: ‹has_bounded_variation_on f {a..c}›
using has_bounded_variation_on_subset[OF assms(1)] assms(2) by auto
show ?thesis unfolding continuous_within Lim_within
proof (intro allI impI)
fix ε :: real assume ‹ε > 0›
from L[unfolded continuous_within Lim_within, rule_format, OF ‹ε > 0›]
obtain δ where ‹δ > 0› and δ: ‹⋀x. x ∈ {a..c} ⟹ 0 < dist x c ⟹ dist x c < δ ⟹
dist (vector_variation {a..x} f) (vector_variation {a..c} f) < ε›
by auto
show ‹∃δ>0. ∀x∈{a..c}. 0 < dist x c ∧ dist x c < δ ⟶ dist (f x) (f c) < ε›
proof (intro exI[of _ δ] conjI ballI impI)
show ‹δ > 0› by fact
next
fix x assume ‹x ∈ {a..c}› ‹0 < dist x c ∧ dist x c < δ›
then have xac: ‹x ∈ {a..c}› and xnc: ‹x ≠ c› and xd: ‹dist x c < δ› by auto
have bv_xc: ‹has_bounded_variation_on f {x..c}›
using has_bounded_variation_on_subset[OF bv_ac] xac by auto
have vv_split: ‹vector_variation {a..c} f = vector_variation {a..x} f + vector_variation {x..c} f›
using vector_variation_combine[OF bv_ac xac] .
have vv_pos: ‹vector_variation {x..c} f ≥ 0›
using vector_variation_pos_le[OF bv_xc] .
have dist_vv: ‹dist (vector_variation {a..x} f) (vector_variation {a..c} f) < ε›
using δ[OF xac] xnc xd by auto
have ‹vector_variation {x..c} f = dist (vector_variation {a..x} f) (vector_variation {a..c} f)›
by (simp add: dist_norm vv_pos vv_split)
also have ‹… < ε› by fact
finally have vv_bound: ‹vector_variation {x..c} f < ε› .
have ‹dist (f x) (f c) = norm (f x - f c)› by (simp add: dist_norm)
also have ‹… ≤ vector_variation {x..c} f›
using vector_variation_ge_norm_function[OF bv_xc] xac by auto
also have ‹… < ε› by fact
finally show ‹dist (f x) (f c) < ε› .
qed
qed
qed
next
assume R: ?R
show ?L
proof (cases ‹c islimpt {a..c}›)
case False
then show ?thesis using continuous_bot
by (metis trivial_limit_within)
next
case True
show ?thesis
proof (rule continuous_within_comparison
[where g = ‹λx. ∑b∈Basis. vector_variation {a..x} (λu. f u ∙ b)›])
have bv_ac: ‹has_bounded_variation_on f {a..c}›
using has_bounded_variation_on_subset[OF assms(1)] assms(2) by auto
show ‹continuous (at c within {a..c})
(λx. ∑i∈Basis. vector_variation {a..x} (λu. f u ∙ i))›
proof (rule continuous_sum)
fix i :: 'a assume iB: ‹i ∈ Basis›
have bv_comp: ‹has_bounded_variation_on (λu. f u ∙ i) {a..b}›
using has_bounded_variation_on_inner_left[OF assms(1)] .
have cont_comp: ‹continuous (at c within {a..c}) (λu. f u ∙ i)›
using R continuous_componentwise iB by blast
show ‹continuous (at c within {a..c}) (λx. vector_variation {a..x} (λu. f u ∙ i))›
using continuous_vector_variation_left_1[OF bv_comp assms(2)] cont_comp by simp
qed
next
have bv_ac: ‹has_bounded_variation_on f {a..c}›
using has_bounded_variation_on_subset[OF assms(1)] assms(2) by auto
fix x assume xac: ‹x ∈ {a..c}›
have bv_xc: ‹has_bounded_variation_on f {x..c}›
using has_bounded_variation_on_subset[OF bv_ac] xac by auto
have bv_comp_ac: ‹⋀b. has_bounded_variation_on (λu. f u ∙ b) {a..c}›
using has_bounded_variation_on_inner_left[OF bv_ac] .
have bv_comp_xc: ‹⋀b. has_bounded_variation_on (λu. f u ∙ b) {x..c}›
using has_bounded_variation_on_inner_left[OF bv_xc] .
have vv_split: ‹vector_variation {a..c} f =
vector_variation {a..x} f + vector_variation {x..c} f›
using vector_variation_combine[OF bv_ac xac] .
have vv_comp_split: ‹vector_variation {a..c} (λu. f u ∙ b) =
vector_variation {a..x} (λu. f u ∙ b) + vector_variation {x..c} (λu. f u ∙ b)›
if ‹b ∈ Basis› for b
using vector_variation_combine[OF bv_comp_ac xac] .
have lhs: ‹dist (vector_variation {a..c} f) (vector_variation {a..x} f) =
vector_variation {x..c} f›
by (simp add: bv_xc dist_norm vector_variation_pos_le vv_split)
have rhs: ‹dist (∑b∈Basis. vector_variation {a..c} (λu. f u ∙ b))
(∑b∈Basis. vector_variation {a..x} (λu. f u ∙ b)) =
(∑b∈Basis. vector_variation {x..c} (λu. f u ∙ b))›
proof -
have eq: ‹(∑b∈Basis. vector_variation {a..c} (λu. f u ∙ b)) -
(∑b∈Basis. vector_variation {a..x} (λu. f u ∙ b)) =
(∑b∈Basis. vector_variation {x..c} (λu. f u ∙ b))›
using vv_comp_split by (simp add: sum.distrib)
moreover have ‹(∑b∈Basis. vector_variation {x..c} (λu. f u ∙ b)) ≥ 0›
by (intro sum_nonneg vector_variation_pos_le bv_comp_xc)
ultimately show ?thesis
by (simp add: dist_real_def)
qed
show ‹dist (vector_variation {a..c} f) (vector_variation {a..x} f) ≤
dist (∑b∈Basis. vector_variation {a..c} (λu. f u ∙ b))
(∑b∈Basis. vector_variation {a..x} (λu. f u ∙ b))›
unfolding lhs rhs
using vector_variation_le_component_sum[OF bv_xc] .
qed
qed
qed
lemma division_of_reflect:
fixes S :: real
assumes ‹d division_of t›
shows ‹(`) ((-) S) ` d division_of ((-) S) ` t›
proof -
define d' where ‹d' = (`) ((-) S) ` d›
have fin: ‹finite d'›
unfolding d'_def using division_of_finite[OF assms] by auto
have props: ‹K ⊆ (-) S ` t ∧ K ≠ {} ∧ (∃a b. K = cbox a b)›
if ‹K ∈ d'› for K
proof -
from that obtain k where kd: ‹k ∈ d› and K_eq: ‹K = (-) S ` k›
unfolding d'_def by auto
have ksub: ‹k ⊆ t› and kne: ‹k ≠ {}› using division_ofD(2,3)[OF assms kd] by auto
from division_ofD(4)[OF assms kd] obtain u v where kuv: ‹k = cbox u v› by auto
with kne have uv: ‹u ≤ v› by (simp add: cbox_interval)
have ‹K ⊆ (-) S ` t›
using ksub K_eq by (auto intro: image_mono)
moreover have ‹K ≠ {}› using kne K_eq by auto
moreover have ‹∃a b. K = cbox a b›
using K_eq kuv uv by (auto simp: cbox_interval image_diff_atLeastAtMost intro!: exI)
ultimately show ?thesis by blast
qed
have disj: ‹interior K1 ∩ interior K2 = {}›
if ‹K1 ∈ d'› ‹K2 ∈ d'› ‹K1 ≠ K2› for K1 K2
proof -
from that obtain k1 k2 where k1d: ‹k1 ∈ d› and K1_eq: ‹K1 = (-) S ` k1›
and k2d: ‹k2 ∈ d› and K2_eq: ‹K2 = (-) S ` k2›
unfolding d'_def by auto
have ‹k1 ≠ k2› using that K1_eq K2_eq by auto
from division_ofD(5)[OF assms k1d k2d this]
have ‹interior k1 ∩ interior k2 = {}› .
have interior_diff: ‹interior ((-) S ` A) = (-) S ` interior A› for A :: ‹real set›
proof -
have ‹(-) S = (+) S ∘ uminus› by (auto simp: fun_eq_iff)
then have ‹(-) S ` A = (+) S ` (uminus ` A)›
by (metis image_comp)
then have ‹interior ((-) S ` A) = interior ((+) S ` (uminus ` A))› by simp
also have ‹… = (+) S ` interior (uminus ` A)› by (simp add: interior_translation)
also have ‹… = (+) S ` (uminus ` interior A)› by (simp add: interior_negations)
also have ‹… = (-) S ` interior A› by (auto simp: image_comp fun_eq_iff)
finally show ?thesis .
qed
show ?thesis
unfolding K1_eq K2_eq interior_diff
using ‹interior k1 ∩ interior k2 = {}›
by (metis image_Int inj_on_diff_left image_empty image_is_empty)
qed
have ‹⋃ d' = (-) S ` t›
proof -
have ‹⋃ d = t› using division_ofD(6)[OF assms] .
then show ?thesis
unfolding d'_def by (simp add: image_Union[symmetric])
qed
then show ?thesis
unfolding d'_def[symmetric] division_of_def
using fin props disj by auto
qed
lemma has_bounded_variation_on_reflect:
assumes ‹has_bounded_variation_on f {S - β..S - α}›
shows ‹has_bounded_variation_on (f ∘ (λt. S - t)) {α..β}›
proof -
from assms obtain B where B: ‹⋀d. d division_of {S - β..S - α} ⟹
(∑k∈d. norm (f (Sup k) - f (Inf k))) ≤ B›
unfolding has_bounded_variation_on_interval by blast
show ?thesis
unfolding has_bounded_variation_on_interval
proof (intro exI[of _ B] allI impI)
fix d assume d: ‹d division_of {α..β}›
define d' where ‹d' = (`) ((-) S) ` d›
have d': ‹d' division_of {S - β..S - α}›
unfolding d'_def using division_of_reflect[OF d] by (simp add: image_diff_atLeastAtMost)
have k_interval: ‹∃u v. u ≤ v ∧ k = {u..v}› if ‹k ∈ d› for k
proof -
from division_ofD(3,4)[OF d that] obtain u v where ‹k ≠ {}› ‹k = cbox u v› by auto
then have ‹u ≤ v› by force
then show ?thesis using ‹k = cbox u v› by (auto simp: cbox_interval)
qed
have sum_eq: ‹(∑k∈d. norm ((f ∘ (λt. S - t)) (Sup k) - (f ∘ (λt. S - t)) (Inf k))) =
(∑k∈d'. norm (f (Sup k) - f (Inf k)))›
proof -
have inj: ‹inj_on ((`) ((-) S)) d›
by (intro inj_onI) (auto simp: inj_image_eq_iff dest: inj_onD[OF inj_on_diff_left])
have ‹(∑k∈d'. norm (f (Sup k) - f (Inf k))) =
(∑k∈d. norm (f (Sup ((-) S ` k)) - f (Inf ((-) S ` k))))›
unfolding d'_def using sum.reindex[OF inj] by simp
also have ‹… = (∑k∈d. norm (f (S - Inf k) - f (S - Sup k)))›
proof (rule sum.cong[OF refl])
fix k assume ‹k ∈ d›
then obtain u v where uv: ‹u ≤ v› ‹k = {u..v}› using k_interval by blast
then have ‹(-) S ` k = {S - v..S - u}› by (simp add: image_diff_atLeastAtMost)
moreover have ‹S - v ≤ S - u› using uv by simp
ultimately show ‹norm (f (Sup ((-) S ` k)) - f (Inf ((-) S ` k))) =
norm (f (S - Inf k) - f (S - Sup k))›
using uv by simp
qed
also have ‹… = (∑k∈d. norm ((f ∘ (λt. S - t)) (Sup k) - (f ∘ (λt. S - t)) (Inf k)))›
by (simp add: norm_minus_commute)
finally show ?thesis by simp
qed
show ‹(∑k∈d. norm ((f ∘ (λt. S - t)) (Sup k) - (f ∘ (λt. S - t)) (Inf k))) ≤ B›
unfolding sum_eq using B[OF d'] .
qed
qed
lemma vector_variation_reflect:
assumes ‹α ≤ β›
shows ‹vector_variation {α..β} (f ∘ (λt. S - t)) = vector_variation {S - β..S - α} f›
proof -
have sum_eq: ‹(∑k∈d. norm ((f ∘ (λt. S - t)) (Sup k) - (f ∘ (λt. S - t)) (Inf k))) =
(∑k∈(`) ((-) S) ` d. norm (f (Sup k) - f (Inf k)))›
if d_div: ‹d division_of t› and t_sub: ‹t ⊆ {α..β}› for d t
proof -
define d' where ‹d' = (`) ((-) S) ` d›
have inj: ‹inj_on ((`) ((-) S)) d›
by (intro inj_onI) (auto simp: inj_image_eq_iff dest: inj_onD[OF inj_on_diff_left])
have k_interval: ‹∃u v. u ≤ v ∧ k = {u..v}› if ‹k ∈ d› for k
proof -
from division_ofD(3,4)[OF d_div that] obtain u v where ‹k ≠ {}› ‹k = cbox u v› by auto
then have ‹u ≤ v› by force
then show ?thesis using ‹k = cbox u v› by (auto simp: cbox_interval)
qed
have ‹(∑k∈d'. norm (f (Sup k) - f (Inf k))) =
(∑k∈d. norm (f (Sup ((-) S ` k)) - f (Inf ((-) S ` k))))›
unfolding d'_def using sum.reindex[OF inj] by simp
also have ‹… = (∑k∈d. norm (f (S - Inf k) - f (S - Sup k)))›
proof (rule sum.cong[OF refl])
fix k assume ‹k ∈ d›
then obtain u v where uv: ‹u ≤ v› ‹k = {u..v}› using k_interval by blast
then have ‹(-) S ` k = {S - v..S - u}› by (simp add: image_diff_atLeastAtMost)
moreover have ‹S - v ≤ S - u› using uv by simp
ultimately show ‹norm (f (Sup ((-) S ` k)) - f (Inf ((-) S ` k))) =
norm (f (S - Inf k) - f (S - Sup k))›
using uv by simp
qed
also have ‹… = (∑k∈d. norm ((f ∘ (λt. S - t)) (Sup k) - (f ∘ (λt. S - t)) (Inf k)))›
by (simp add: norm_minus_commute)
finally show ?thesis unfolding d'_def by simp
qed
have set_eq: ‹{∑k∈d. norm ((f ∘ (λt. S - t)) (Sup k) - (f ∘ (λt. S - t)) (Inf k)) |
d. ∃t. d division_of t ∧ t ⊆ {α..β}} =
{∑k∈d. norm (f (Sup k) - f (Inf k)) |
d. ∃t. d division_of t ∧ t ⊆ {S - β..S - α}}›
(is ‹?A = ?B›)
proof (intro equalityI subsetI)
fix x assume ‹x ∈ ?A›
then obtain d t where dt: ‹d division_of t› ‹t ⊆ {α..β}›
and x_eq: ‹x = (∑k∈d. norm ((f ∘ (λt. S - t)) (Sup k) - (f ∘ (λt. S - t)) (Inf k)))›
by auto
have ‹x = (∑k∈(`) ((-) S) ` d. norm (f (Sup k) - f (Inf k)))›
unfolding x_eq using sum_eq[OF dt] .
moreover have ‹(`) ((-) S) ` d division_of (-) S ` t›
using division_of_reflect[OF dt(1)] by auto
moreover have ‹(-) S ` t ⊆ {S - β..S - α}›
using dt(2) by (auto simp: image_diff_atLeastAtMost)
ultimately show ‹x ∈ ?B› by blast
next
fix x assume ‹x ∈ ?B›
then obtain d t where dt: ‹d division_of t› ‹t ⊆ {S - β..S - α}›
and x_eq: ‹x = (∑k∈d. norm (f (Sup k) - f (Inf k)))› by auto
define d' where ‹d' = (`) ((-) S) ` d›
have d'_div: ‹d' division_of (-) S ` t›
unfolding d'_def using division_of_reflect[OF dt(1)] by auto
have t'_sub: ‹(-) S ` t ⊆ {α..β}›
using dt(2) by (auto simp: image_diff_atLeastAtMost)
have ‹(∑k∈d'. norm ((f ∘ (λt. S - t)) (Sup k) - (f ∘ (λt. S - t)) (Inf k))) =
(∑k∈(`) ((-) S) ` d'. norm (f (Sup k) - f (Inf k)))›
using sum_eq[OF d'_div t'_sub] .
also have ‹(`) ((-) S) ` d' = d›
unfolding d'_def by (auto simp: image_image)
also have ‹(∑k∈d. norm (f (Sup k) - f (Inf k))) = x› using x_eq by simp
finally show ‹x ∈ ?A› using d'_div t'_sub by blast
qed
show ?thesis
unfolding vector_variation_def set_variation_def set_eq ..
qed
lemma continuous_reflect:
fixes f :: ‹real ⇒ 'a::topological_space›
shows ‹continuous (at c within S) (f ∘ (λt. s - t)) ⟷
continuous (at (s - c) within ((-) s) ` S) f›
proof -
have filt: ‹filtermap ((-) s) (at c within S) = at (s - c) within (-) s ` S›
by (simp add: bij_diff filtermap_linear_at_within open_neg_translation)
show ?thesis
unfolding continuous_within
by (simp add: tendsto_compose_filtermap filt)
qed
lemma continuous_vector_variation_at_right:
fixes f :: ‹real ⇒ 'a::euclidean_space›
assumes ‹has_bounded_variation_on f {a..b}› ‹c ∈ {a..b}›
shows ‹continuous (at c within {c..b}) (λx. vector_variation {a..x} f) ⟷
continuous (at c within {c..b}) f›
proof -
define s where ‹s = a + b›
define c' where ‹c' = s - c›
have sc: ‹s - c' = c› unfolding c'_def by simp
have sa: ‹s - a = b› and sb: ‹s - b = a› unfolding s_def by auto
have ac: ‹a ≤ c› and cb: ‹c ≤ b› using assms(2) by auto
have c'_mem: ‹c' ∈ {a..b}› unfolding c'_def s_def using ac cb by auto
have img: ‹(-) s ` {c..b} = {a..c'}› and img': ‹(-) s ` {a..c'} = {c..b}›
unfolding c'_def s_def by (auto simp: image_diff_atLeastAtMost)
define g where ‹g = f ∘ (-) s›
have bv_g: ‹has_bounded_variation_on g {a..b}›
unfolding g_def using has_bounded_variation_on_reflect[of f s b a] assms(1)
by (simp add: s_def)
have left: ‹continuous (at c' within {a..c'}) (λy. vector_variation {a..y} g) ⟷
continuous (at c' within {a..c'}) g›
using continuous_vector_variation_left[OF bv_g c'_mem] .
have cont_f_g: ‹continuous (at c within {c..b}) f ⟷ continuous (at c' within {a..c'}) g›
unfolding g_def using continuous_reflect[of c' ‹{a..c'}› f s]
by (simp add: sc sa image_diff_atLeastAtMost)
have comp_eq: ‹vector_variation {a..s - x} g = vector_variation {x..b} f› for x
proof (cases ‹a ≤ s - x›)
case True
then show ?thesis
unfolding g_def using vector_variation_reflect[of a ‹s - x› f s] by (simp add: sa)
next
case False
then have ‹{a..s - x} = {}› and ‹{x..b} = {}›
unfolding s_def by auto
then show ?thesis by (simp add: vector_variation_def set_variation_def)
qed
have cont_vv_reflect: ‹continuous (at c' within {a..c'}) (λy. vector_variation {a..y} g) ⟷
continuous (at c within {c..b}) (λx. vector_variation {x..b} f)›
proof -
have eq: ‹(λy. vector_variation {a..y} g) ∘ (-) s = (λx. vector_variation {x..b} f)›
by (rule ext) (simp add: comp_eq)
show ?thesis
using continuous_reflect[of c ‹{c..b}› ‹λy. vector_variation {a..y} g› s]
using eq img by force
qed
have vv_split: ‹vector_variation {a..b} f - vector_variation {a..x} f = vector_variation {x..b} f›
if ‹x ∈ {a..b}› for x
using vector_variation_combine[OF assms(1) that] by linarith
have cont_vv_shift: ‹continuous (at c within {c..b}) (λx. vector_variation {x..b} f) ⟷
continuous (at c within {c..b}) (λx. vector_variation {a..x} f)›
(is ‹?P ⟷ ?Q›)
proof
assume ?Q
have ‹continuous (at c within {c..b}) (λx. vector_variation {a..b} f - vector_variation {a..x} f)›
using continuous_diff[OF continuous_const ‹?Q›] .
moreover have ‹∀⇩F x in at c within {c..b}. vector_variation {a..b} f - vector_variation {a..x} f =
vector_variation {x..b} f›
unfolding eventually_at_topological
by (meson vv_split ac atLeastAtMost_iff first_countable_basis order_trans)
ultimately show ?P
unfolding continuous_within
using assms(2) tendsto_cong vv_split by fastforce
next
assume ?P
have ‹continuous (at c within {c..b}) (λx. vector_variation {a..b} f - vector_variation {x..b} f)›
using continuous_diff[OF continuous_const ‹?P›] .
moreover have ‹∀⇩F x in at c within {c..b}. vector_variation {a..b} f - vector_variation {x..b} f =
vector_variation {a..x} f›
unfolding eventually_at_topological
proof (intro exI[of _ UNIV] conjI ballI impI open_UNIV UNIV_I)
fix x assume ‹x ≠ c› ‹x ∈ {c..b}›
then have ‹x ∈ {a..b}› using ac by auto
from vv_split[OF this] show ‹vector_variation {a..b} f - vector_variation {x..b} f = vector_variation {a..x} f›
by linarith
qed
ultimately show ?Q
by (metis (no_types, lifting) ext add.commute add.left_cancel assms(2)
continuous_at_within_cong diff_add_cancel vv_split)
qed
show ?thesis
using left cont_f_g cont_vv_reflect cont_vv_shift by simp
qed
lemma vector_variation_continuous:
fixes f :: ‹real ⇒ 'a::euclidean_space›
assumes ‹has_bounded_variation_on f {a..b}› ‹c ∈ {a..b}›
shows ‹continuous (at c within {a..b}) (λx. vector_variation {a..x} f) ⟷
continuous (at c within {a..b}) f›
unfolding continuous_within_ivl_split[OF assms(2)]
using continuous_vector_variation_left[OF assms] continuous_vector_variation_at_right[OF assms]
by simp
end