Theory HOL-Analysis.Rectifiable_Path
theory Rectifiable_Path
imports Bounded_Variation Path_Connected Equivalence_Lebesgue_Henstock_Integration
begin
section ‹Rectifiable paths and arc-length reparametrization›
definition rectifiable_path :: ‹(real ⇒ 'a::euclidean_space) ⇒ bool› where
‹rectifiable_path g ⟷ path g ∧ has_bounded_variation_on g {0..1}›
definition path_length :: ‹(real ⇒ 'a::euclidean_space) ⇒ real› where
‹path_length g = vector_variation {0..1} g›
text ‹
We can factor a BV function through its variation. Moreover the factor is
Lipschitz (hence continuous) on its domain, though without continuity of the
original function that domain may not be an interval.
›
lemma factor_through_variation:
fixes f :: ‹real ⇒ 'a::euclidean_space›
assumes ‹has_bounded_variation_on f {a..b}›
shows ‹∃g. (∀x ∈ {a..b}. f x = g (vector_variation {a..x} f)) ∧
continuous_on ((λx. vector_variation {a..x} f) ` {a..b}) g ∧
(∀u ∈ (λx. vector_variation {a..x} f) ` {a..b}.
∀v ∈ (λx. vector_variation {a..x} f) ` {a..b}.
dist (g u) (g v) ≤ dist u v)›
proof -
define S where ‹S ≡ (λx. vector_variation {a..x} f) ` {a..b}›
have claim1: ‹∃g. (∀x ∈ {a..b}. f x = g (vector_variation {a..x} f)) ∧
(∀u ∈ S. ∀v ∈ S. dist (g u) (g v) ≤ dist u v)›
proof (cases ‹{a..b} = {}›)
case True
then show ?thesis unfolding S_def by auto
next
case False
then have ab: ‹a ≤ b› by auto
define V where ‹V x ≡ vector_variation {a..x} f› for x
have f_eq: ‹f x = f y›
if ‹x ∈ {a..b}› ‹y ∈ {a..b}› ‹V x = V y› for x y
proof -
have core: ‹f p = f q›
if ‹p ≤ q› ‹p ∈ {a..b}› ‹q ∈ {a..b}› ‹V p = V q› for p q
proof -
have bv_aq: ‹has_bounded_variation_on f {a..q}›
using has_bounded_variation_on_subset[OF assms] that ab by auto
have p_in: ‹p ∈ {a..q}› using that by auto
have vv0: ‹vector_variation {p..q} f = 0›
by (metis V_def add.right_neutral add_left_cancel bv_aq
‹V p = V q› vector_variation_combine p_in)
have bv_pq: ‹has_bounded_variation_on f {p..q}›
using has_bounded_variation_on_subset[OF assms] that by auto
from vector_variation_const_eq[OF bv_pq is_interval_cc] vv0
show ‹f p = f q› using that by force
qed
show ‹f x = f y›
using core[of x y] core[of y x] that by argo
qed
define g where ‹g v ≡ f (SOME x. x ∈ {a..b} ∧ V x = v)› for v
have g_factor: ‹f x = g (V x)› if ‹x ∈ {a..b}› for x
unfolding g_def
by (metis (mono_tags, lifting) f_eq someI that)
have g_lip: ‹dist (g u) (g v) ≤ dist u v›
if ‹u ∈ S› ‹v ∈ S› for u v
proof -
from that obtain x y where
x: ‹x ∈ {a..b}› ‹u = V x› and y: ‹y ∈ {a..b}› ‹v = V y›
unfolding S_def V_def by auto
have lip: ‹dist (g (V x)) (g (V y)) ≤ dist (V x) (V y)›
if xy: ‹x ≤ y› ‹x ∈ {a..b}› ‹y ∈ {a..b}› for x y
proof -
have bv_ay: ‹has_bounded_variation_on f {a..y}›
using has_bounded_variation_on_subset[OF assms] xy(2,3) ab by auto
have x_in: ‹x ∈ {a..y}› using xy by auto
from vector_variation_combine[OF bv_ay x_in]
have V_split: ‹V y = V x + vector_variation {x..y} f›
unfolding V_def .
have bv_xy: ‹has_bounded_variation_on f {x..y}›
using has_bounded_variation_on_subset[OF assms] xy(1,2,3) by auto
have Vx_le_Vy: ‹V x ≤ V y›
using V_split vector_variation_pos_le[OF bv_xy] by linarith
have ‹dist (g (V x)) (g (V y)) = dist (f x) (f y)›
using g_factor xy(2,3) by simp
also have ‹… = norm (f x - f y)› by (simp add: dist_norm)
also have ‹… ≤ vector_variation {x..y} f›
using vector_variation_ge_norm_function[OF bv_xy] xy(1) by auto
also have ‹… = V y - V x› using V_split by simp
also have ‹… = dist (V x) (V y)› using Vx_le_Vy by (simp add: dist_real_def)
finally show ?thesis .
qed
show ?thesis
proof (cases ‹x ≤ y›)
case True then show ?thesis using lip x y by auto
next
case nle: False
then have ‹y ≤ x› by auto
then have ‹dist (g (V y)) (g (V x)) ≤ dist (V y) (V x)›
using lip y(1) x(1) by auto
then show ?thesis using x y by (simp add: dist_commute)
qed
qed
show ?thesis
using g_factor g_lip unfolding V_def by auto
qed
moreover
have ‹continuous_on S g› if ‹∀u ∈ S. ∀v ∈ S. dist (g u) (g v) ≤ dist u v› for g :: "real⇒'a"
using continuous_on_iff order_le_less_trans that by blast
ultimately show ?thesis
using S_def by blast
qed
lemma factor_continuous_through_variation:
fixes f :: ‹real ⇒ 'a::euclidean_space›
assumes ‹a ≤ b›
and ‹continuous_on {a..b} f›
and ‹has_bounded_variation_on f {a..b}›
defines ‹l ≡ vector_variation {a..b} f›
obtains g where ‹∀x ∈ {a..b}. f x = g (vector_variation {a..x} f)›
and ‹continuous_on {0..l} g›
and ‹∀u ∈ {0..l}. ∀v ∈ {0..l}. dist (g u) (g v) ≤ dist u v›
and ‹has_bounded_variation_on g {0..l}›
and ‹(λx. vector_variation {a..x} f) ` {a..b} = {0..l}›
and ‹g ` {0..l} = f ` {a..b}›
and ‹∀x ∈ {0..l}. vector_variation {0..x} g = x›
proof -
define S where ‹S ≡ (λx. vector_variation {a..x} f) ` {a..b}›
obtain g where g_factor: ‹∀x ∈ {a..b}. f x = g (vector_variation {a..x} f)›
and g_cont: ‹continuous_on S g›
and g_lip: ‹∀u ∈ S. ∀v ∈ S. dist (g u) (g v) ≤ dist u v›
using factor_through_variation[OF assms(3)] unfolding S_def by blast
define V where ‹V ≡ λx. vector_variation {a..x} f›
have V_a: ‹V a = 0›
unfolding V_def using vector_variation_on_null[of a a f] by simp
have V_b: ‹V b = l›
unfolding V_def l_def by simp
have V_mono: ‹V x ≤ V y› if ‹x ∈ {a..b}› ‹y ∈ {a..b}› ‹x ≤ y› for x y
proof -
have bv_ay: ‹has_bounded_variation_on f {a..y}›
using has_bounded_variation_on_subset[OF assms(3)] that by auto
have ‹V y = V x + vector_variation {x..y} f›
unfolding V_def using vector_variation_combine[OF bv_ay] that by auto
moreover have ‹vector_variation {x..y} f ≥ 0›
by (rule vector_variation_pos_le[OF has_bounded_variation_on_subset[OF assms(3)]])
(use that in auto)
ultimately show ?thesis by linarith
qed
have V_cont: ‹continuous_on {a..b} V›
unfolding V_def continuous_on_eq_continuous_within
using vector_variation_continuous[OF assms(3)] assms(2)[unfolded continuous_on_eq_continuous_within]
by simp
have S_eq: ‹S = {0..l}›
proof (rule antisym)
show ‹S ⊆ {0..l}›
using V_a V_b V_mono ‹a ≤ b› unfolding S_def V_def by force
show ‹{0..l} ⊆ S›
proof -
have ‹connected S›
unfolding S_def V_def[symmetric]
using connected_continuous_image[OF V_cont] by auto
moreover have ‹0 ∈ S› using V_a ‹a ≤ b› unfolding S_def V_def by force
moreover have ‹l ∈ S› using V_b ‹a ≤ b› unfolding S_def V_def by force
ultimately show ?thesis using connected_contains_Icc by blast
qed
qed
show thesis
proof
show g_bv: ‹has_bounded_variation_on g {0..l}›
using Lipschitz_imp_has_bounded_variation[where B=1]
by (metis S_eq bounded_closed_interval dist_norm g_lip mult_1)
show ‹g ` {0..l} = f ` {a..b}›
using S_def S_eq g_factor by auto
have ‹vector_variation {0..x} g = x› if ‹x ∈ {0..l}› for x
proof (rule antisym)
show ‹vector_variation {0..x} g ≤ x›
proof (rule has_bounded_variation_works(2)[OF has_bounded_variation_on_subset[OF g_bv]])
show ‹{0..x} ⊆ {0..l}› using that by auto
next
fix d t assume dt: ‹d division_of t› ‹t ⊆ {0..x}›
have ‹(∑k∈d. norm (g (Sup k) - g (Inf k))) ≤ (∑k∈d. content k)›
proof (rule sum_mono)
fix k assume kd: ‹k ∈ d›
obtain lk uk where k_eq: ‹k = {lk..uk}› and lk_le: ‹lk ≤ uk›
by (metis atLeastatMost_empty_iff2 box_real(2) division_ofD(3,4) dt(1) kd)
have k_sub: ‹k ⊆ {0..x}› using division_ofD(2)[OF dt(1) kd] dt(2) by auto
then have lk_in: ‹lk ∈ {0..l}› and uk_in: ‹uk ∈ {0..l}›
using k_eq lk_le that by auto
have ‹norm (g (Sup k) - g (Inf k)) = norm (g uk - g lk)›
using lk_le k_eq by (simp add: cbox_interval)
also have ‹… ≤ dist (g uk) (g lk)› by (simp add: dist_norm)
also have ‹… ≤ dist uk lk›
using g_lip lk_in uk_in S_eq by auto
also have ‹… = uk - lk› using lk_le by (simp add: dist_real_def)
also have ‹… = content k› using lk_le k_eq by (simp add: cbox_interval)
finally show ‹norm (g (Sup k) - g (Inf k)) ≤ content k› .
qed
also have ‹(∑k∈d. content k) ≤ content (cbox 0 x)›
using subadditive_content_division[OF dt(1)] dt(2)
by (simp add: cbox_interval)
also have ‹… = x› using that by (simp add: cbox_interval)
finally show ‹(∑k∈d. norm (g (Sup k) - g (Inf k))) ≤ x› .
qed
next
show ‹x ≤ vector_variation {0..x} g›
proof -
have x_in_S: ‹x ∈ S› using that S_eq by auto
then obtain t where t_in: ‹t ∈ {a..b}› and Vt: ‹V t = x›
unfolding S_def V_def by auto
have bv_at: ‹has_bounded_variation_on f {a..t}›
using has_bounded_variation_on_subset[OF assms(3)] t_in by auto
have mono_V_at: ‹mono_on {a..t} V›
unfolding mono_on_def using V_mono t_in by auto
have g_bv_0x: ‹has_bounded_variation_on g {V a..V t}›
using has_bounded_variation_on_subset[OF g_bv] V_a Vt that by auto
have gV_eq_f: ‹g (V u) = f u› if ‹u ∈ {a..t}› for u
using g_factor t_in that V_def by auto
have var_eq: ‹vector_variation {a..t} (g ∘ V) = vector_variation {a..t} f›
proof -
have eq: ‹norm ((g ∘ V) (Sup k) - (g ∘ V) (Inf k)) = norm (f (Sup k) - f (Inf k))›
if div: ‹d division_of s› ‹s ⊆ {a..t}› and kd: ‹k ∈ d› for d s k
proof -
obtain lk uk where ‹k = cbox lk uk› ‹k ≠ {}› and lu: ‹lk ≤ uk›
using division_ofD(3,4)[OF div(1) kd] by auto
then have k_eq: ‹k = {lk..uk}› and Inf_k: ‹Inf k = lk› and Sup_k: ‹Sup k = uk›
using ‹k = cbox lk uk› by (auto simp: cbox_interval)
have ‹k ⊆ {a..t}›
using division_ofD(2)[OF div(1) kd] div(2) by auto
then have ‹Inf k ∈ {a..t}› ‹Sup k ∈ {a..t}› using lu Inf_k Sup_k k_eq by auto
then show ?thesis using gV_eq_f by (simp add: comp_def)
qed
have sum_eq: ‹(∑k∈d. norm ((g ∘ V) (Sup k) - (g ∘ V) (Inf k))) =
(∑k∈d. norm (f (Sup k) - f (Inf k)))›
if ‹d division_of s› ‹s ⊆ {a..t}› for d s
by (intro sum.cong refl eq[OF that])
have ‹{∑k∈d. norm ((g ∘ V) (Sup k) - (g ∘ V) (Inf k)) |d. ∃s. d division_of s ∧ s ⊆ {a..t}}
= {∑k∈d. norm (f (Sup k) - f (Inf k)) |d. ∃s. d division_of s ∧ s ⊆ {a..t}}›
(is ‹?L = ?R›)
proof (rule antisym; rule subsetI)
fix v assume ‹v ∈ ?L›
then obtain d s where ds: ‹d division_of s› ‹s ⊆ {a..t}›
and ‹v = (∑k∈d. norm ((g ∘ V) (Sup k) - (g ∘ V) (Inf k)))› by auto
then have ‹v = (∑k∈d. norm (f (Sup k) - f (Inf k)))›
using sum_eq[OF ds] by simp
then show ‹v ∈ ?R› using ds by blast
next
fix v assume ‹v ∈ ?R›
then obtain d s where ds: ‹d division_of s› ‹s ⊆ {a..t}›
and ‹v = (∑k∈d. norm (f (Sup k) - f (Inf k)))› by auto
then have ‹v = (∑k∈d. norm ((g ∘ V) (Sup k) - (g ∘ V) (Inf k)))›
using sum_eq[OF ds] by simp
then show ‹v ∈ ?L› using ds by blast
qed
then show ?thesis
unfolding vector_variation_def set_variation_def comp_def by auto
qed
have ‹vector_variation {a..t} (g ∘ V) ≤ vector_variation {V a..V t} g›
using has_bounded_variation_compose_monotone(2)[OF g_bv_0x mono_V_at] .
then have ‹vector_variation {a..t} f ≤ vector_variation {0..x} g›
using var_eq V_a Vt by simp
moreover have ‹x = vector_variation {a..t} f›
using Vt[symmetric] by (simp add: V_def)
ultimately show ?thesis by linarith
qed
qed
then show ‹∀x∈{0..l}. vector_variation {0..x} g = x›
by blast
qed (use S_def S_eq g_cont g_factor g_lip in auto)+
qed
text ‹Arc-length reparametrization and existence of shortest paths.›
lemma arc_length_reparametrization:
fixes g :: ‹real ⇒ 'a::euclidean_space›
assumes ‹rectifiable_path g›
obtains h where
‹rectifiable_path h›
‹path_image h = path_image g›
‹pathstart h = pathstart g›
‹pathfinish h = pathfinish g›
‹path_length h = path_length g›
‹arc g ⟹ arc h›
‹simple_path g ⟹ simple_path h›
‹∀t ∈ {0..1}. path_length (subpath 0 t h) = path_length g * t›
‹∀x ∈ {0..1}. ∀y ∈ {0..1}.
dist (h x) (h y) ≤ path_length g * dist x y›
proof -
define l where ‹l ≡ path_length g›
from assms have g_path: ‹path g› and g_bv: ‹has_bounded_variation_on g {0..1}›
unfolding rectifiable_path_def by auto
then have g_cont: ‹continuous_on {0..1} g›
by (simp add: path_def pathin_def continuous_map_iff_continuous)
have l_eq: ‹l = vector_variation {0..1} g›
unfolding l_def path_length_def by simp
obtain h where
h_factor: ‹∀x ∈ {0..1}. g x = h (vector_variation {0..x} g)›
and h_cont: ‹continuous_on {0..l} h›
and h_lip: ‹∀u ∈ {0..l}. ∀v ∈ {0..l}. dist (h u) (h v) ≤ dist u v›
and h_bv: ‹has_bounded_variation_on h {0..l}›
and h_image_var: ‹(λx. vector_variation {0..x} g) ` {0..1} = {0..l}›
and h_image: ‹h ` {0..l} = g ` {0..1}›
and h_var: ‹∀x ∈ {0..l}. vector_variation {0..x} h = x›
using factor_continuous_through_variation[of 0 1 g, folded l_eq]
using g_cont g_bv by auto
have l_nonneg: ‹0 ≤ l›
using vector_variation_pos_le[OF g_bv] l_eq by simp
have scale_image: ‹(λx. x *⇩R l) ` {0..1} = {0..l}›
using l_nonneg image_mult_atLeastAtMost_if'[of l 0 1] by auto
have scale_mono: ‹mono_on {0..1} (λx. x *⇩R l)›
using l_nonneg by (intro mono_onI) (simp add: mult_right_mono)
have h_0: ‹h 0 = g 0›
using h_factor[rule_format, of 0] vector_variation_on_null[of 0 0 g]
by simp
have h_l: ‹h l = g 1›
using h_factor[rule_format, of 1] l_eq by simp
show ?thesis
proof
show ‹rectifiable_path (h ∘ (λx. x *⇩R l))›
proof -
have ‹continuous_on {0..1} (λx. x * l)›
by (intro continuous_intros)
then have path: ‹path (h ∘ (λx. x *⇩R l))›
unfolding path_def pathin_def continuous_map_iff_continuous
using continuous_on_compose[of ‹{0..1}› ‹λx. x * l› h] h_cont scale_image
by (simp add: image_comp comp_def)
have bv: ‹has_bounded_variation_on (h ∘ (λx. x *⇩R l)) {0..1}›
using has_bounded_variation_compose_monotone(1)[OF _ scale_mono] h_bv
by simp
show ?thesis
unfolding rectifiable_path_def using path bv by simp
qed
show ‹path_image (h ∘ (λx. x *⇩R l)) = path_image g›
unfolding path_image_def image_comp[symmetric] scale_image
using h_image by simp
show ‹pathstart (h ∘ (λx. x *⇩R l)) = pathstart g›
unfolding pathstart_def using h_0 by simp
show ‹pathfinish (h ∘ (λx. x *⇩R l)) = pathfinish g›
unfolding pathfinish_def using h_l by simp
show ‹path_length (h ∘ (λx. x *⇩R l)) = path_length g›
proof -
have h_var_l: ‹vector_variation {0..l} h = l›
using h_var l_nonneg by simp
have upper: ‹vector_variation {0..1} (h ∘ (λx. x *⇩R l)) ≤ l›
by (metis (no_types, lifting) h_bv h_var_l has_bounded_variation_compose_monotone(2) pth_1
pth_4(1) scale_mono)
have lower: ‹l ≤ vector_variation {0..1} (h ∘ (λx. x *⇩R l))›
proof (cases ‹l = 0›)
case True
then show ?thesis
using vector_variation_pos_le[OF has_bounded_variation_compose_monotone(1)[OF _ scale_mono] ] h_bv
by simp
next
case False
then have l_pos: ‹0 < l› using l_nonneg by simp
have inv_mono: ‹mono_on {0..l} (λx. x / l)›
using l_pos by (intro mono_onI) (simp add: divide_right_mono)
have inv_bv: ‹has_bounded_variation_on (h ∘ (λx. x *⇩R l)) {(0::real) / l..l / l}›
using has_bounded_variation_compose_monotone(1)[OF _ scale_mono] h_bv l_pos
by simp
have eq: ‹(h ∘ (λx. x *⇩R l)) ∘ (λx. x / l) = h› (is ‹?lhs = ?rhs›)
using False by auto
have ‹vector_variation {0..l} ((h ∘ (λx. x *⇩R l)) ∘ (λx. x / l))
≤ vector_variation {0 / l..l / l} (h ∘ (λx. x *⇩R l))›
using has_bounded_variation_compose_monotone(2)[OF inv_bv inv_mono] .
then show ?thesis
using eq h_var_l l_pos by simp
qed
show ?thesis
unfolding path_length_def using upper lower l_eq by linarith
qed
show ‹arc (h ∘ (λx. x *⇩R l))› if ‹arc g›
proof -
have g_inj: ‹inj_on g {0..1}›
using arc_def that by blast
have l_pos: ‹0 < l›
proof (rule ccontr)
assume ‹¬ 0 < l›
then have ‹l = 0› using l_nonneg by simp
then have ‹∃c. ∀t ∈ {0..1}. g t = c›
using vector_variation_const_eq[OF g_bv] l_eq by auto
then have ‹g 0 = g 1› by auto
then show False using arc_distinct_ends[OF that]
unfolding pathstart_def pathfinish_def by simp
qed
have h_inj: ‹inj_on h {0..l}›
using that
by (smt (verit, ccfv_SIG) arcD h_factor h_image_var image_iff linorder_inj_onI')
have scale_inj: ‹inj_on (λx. x *⇩R l) {0..1}›
using l_pos by (intro inj_onI) simp
have comp_inj: ‹inj_on (h ∘ (λx. x *⇩R l)) {0..1}›
using comp_inj_on[OF scale_inj] h_inj scale_image by auto
show ‹arc (h ∘ (λx. x *⇩R l))›
unfolding arc_def using comp_inj
using ‹rectifiable_path (h ∘ (λx. x *⇩R l))› rectifiable_path_def by blast
qed
show ‹simple_path (h ∘ (λx. x *⇩R l))› if sp: ‹simple_path g›
proof -
have g_lf: ‹loop_free g›
using simple_path_def that by blast
have l_pos: ‹0 < l›
proof (rule ccontr)
assume ‹¬ 0 < l›
then have ‹l = 0› using l_nonneg by simp
then obtain c where ‹∀t ∈ {0..1}. g t = c›
using vector_variation_const_eq[OF g_bv] l_eq by auto
then have eq: ‹g 0 = g (1/2)› by auto
then show False
using g_lf[unfolded loop_free_def, rule_format, of 0 ‹1/2›] by auto
qed
show ‹simple_path (h ∘ (λx. x *⇩R l))›
unfolding simple_path_def
proof (intro conjI)
show ‹path (h ∘ (λx. x *⇩R l))›
using ‹rectifiable_path (h ∘ (λx. x *⇩R l))› rectifiable_path_def by blast
show ‹loop_free (h ∘ (λx. x *⇩R l))›
unfolding loop_free_def comp_def
proof (intro ballI impI)
fix x y assume x01: ‹x ∈ {0..1}› and y01: ‹y ∈ {0..1}›
and eq: ‹h (x *⇩R l) = h (y *⇩R l)›
have xl_in: ‹x * l ∈ {0..l}› and yl_in: ‹y * l ∈ {0..l}›
using x01 y01 l_nonneg mult_right_mono[of _ 1 l] by auto
from xl_in obtain s where s01: ‹s ∈ {0..1}› and xs: ‹x * l = vector_variation {0..s} g›
using h_image_var[symmetric] by auto
from yl_in obtain t where t01: ‹t ∈ {0..1}› and yt: ‹y * l = vector_variation {0..t} g›
using h_image_var[symmetric] by auto
have ‹g s = h (vector_variation {0..s} g)› using h_factor s01 by auto
also have ‹… = h (y * l)› using xs eq by simp
also have ‹… = h (vector_variation {0..t} g)› using yt by simp
also have ‹… = g t› using h_factor t01 by auto
finally have ‹s = t ∨ s = 0 ∧ t = 1 ∨ s = 1 ∧ t = 0›
using g_lf s01 t01 unfolding loop_free_def by blast
then have ‹x * l = y * l ∨ x * l = 0 ∧ y * l = l ∨ x * l = l ∧ y * l = 0›
using xs yt l_eq vector_variation_on_null[of 0 0 g] by auto
then show ‹x = y ∨ x = 0 ∧ y = 1 ∨ x = 1 ∧ y = 0›
using l_pos by auto
qed
qed
qed
show ‹∀t ∈ {0..1}. path_length (subpath 0 t (h ∘ (λx. x *⇩R l))) = path_length g * t›
proof (intro ballI)
fix t :: real assume t01: ‹t ∈ {0..1}›
then have t_nonneg: ‹0 ≤ t› and t_le1: ‹t ≤ 1› by auto
define m where ‹m = t * l›
have m_nonneg: ‹0 ≤ m› unfolding m_def using t_nonneg l_nonneg by simp
have m_le_l: ‹m ≤ l› unfolding m_def
using mult_right_mono[of t 1 l] t_le1 l_nonneg by simp
have m_in: ‹m ∈ {0..l}› using m_nonneg m_le_l by simp
have sub_eq: ‹subpath 0 t (h ∘ (λx. x *⇩R l)) = h ∘ (λx. x *⇩R m)›
unfolding subpath_def comp_def m_def by (auto simp: algebra_simps)
have scale_m_image: ‹(λx. x *⇩R m) ` {0..1} = {0..m}›
using m_nonneg image_mult_atLeastAtMost_if'[of m 0 1] by auto
have scale_m_mono: ‹mono_on {0..1} (λx. x *⇩R m)›
using m_nonneg by (intro mono_onI) (simp add: mult_right_mono)
have h_bv_m: ‹has_bounded_variation_on h {0..m}›
using has_bounded_variation_on_subset[OF h_bv] m_le_l m_nonneg by auto
have h_var_m: ‹vector_variation {0..m} h = m›
using h_var m_in by auto
have upper: ‹vector_variation {0..1} (h ∘ (λx. x *⇩R m)) ≤ m›
by (metis (no_types, lifting) h_bv_m h_var_m has_bounded_variation_compose_monotone(2)
pth_1 pth_4(1) scale_m_mono)
have lower: ‹m ≤ vector_variation {0..1} (h ∘ (λx. x *⇩R m))›
proof (cases ‹m = 0›)
case True
then show ?thesis
using vector_variation_pos_le[OF has_bounded_variation_compose_monotone(1)[OF _ scale_m_mono]]
h_bv_m by simp
next
case False
then have m_pos: ‹0 < m› using m_nonneg by simp
have inv_mono: ‹mono_on {0..m} (λx. x / m)›
using m_pos by (intro mono_onI) (simp add: divide_right_mono)
have inv_bv: ‹has_bounded_variation_on (h ∘ (λx. x *⇩R m)) {(0::real) / m..m / m}›
using has_bounded_variation_compose_monotone(1)[OF _ scale_m_mono] h_bv_m m_pos
by simp
have eq: ‹(h ∘ (λx. x *⇩R m)) ∘ (λx. x / m) = h›
using False by auto
have ‹vector_variation {0..m} ((h ∘ (λx. x *⇩R m)) ∘ (λx. x / m))
≤ vector_variation {0 / m..m / m} (h ∘ (λx. x *⇩R m))›
using has_bounded_variation_compose_monotone(2)[OF inv_bv inv_mono] .
then show ?thesis
using eq h_var_m m_pos by simp
qed
show ‹path_length (subpath 0 t (h ∘ (λx. x *⇩R l))) = path_length g * t›
unfolding path_length_def sub_eq l_eq[symmetric]
using upper lower m_def by (simp add: mult.commute)
qed
show ‹∀x ∈ {0..1}. ∀y ∈ {0..1}.
dist ((h ∘ (λx. x *⇩R l)) x) ((h ∘ (λx. x *⇩R l)) y) ≤ path_length g * dist x y›
proof (intro ballI)
fix x y :: real assume ‹x ∈ {0..1}› ‹y ∈ {0..1}›
then have ‹x * l ∈ {0..l}› ‹y * l ∈ {0..l}›
using l_nonneg mult_right_mono[of _ 1 l] by auto
then have ‹dist (h (x * l)) (h (y * l)) ≤ dist (x * l) (y * l)›
using h_lip by auto
also have ‹… = l * dist x y›
unfolding dist_real_def using l_nonneg
by (simp add: abs_mult left_diff_distrib[symmetric])
finally show ‹dist ((h ∘ (λx. x *⇩R l)) x) ((h ∘ (λx. x *⇩R l)) y) ≤ path_length g * dist x y›
unfolding l_def comp_def by simp
qed
qed
qed
corollary bounded_variation_absolutely_integrable_real_interval:
fixes f :: "real ⇒ 'm::euclidean_space"
assumes "f integrable_on {a..b}"
and "⋀d. d division_of {a..b} ⟹ sum (λK. norm(integral K f)) d ≤ B"
shows "f absolutely_integrable_on {a..b}"
by (metis assms bounded_variation_absolutely_integrable_interval interval_cbox)
lemma absolutely_integrable_bounded_variation_eq:
fixes f :: ‹real ⇒ 'a::euclidean_space›
shows ‹f absolutely_integrable_on {a..b} ⟷
f integrable_on {a..b} ∧
has_bounded_variation_on (λt. integral {a..t} f) {a..b}›
(is ‹?L ⟷ ?R›)
proof
assume L: ?L
then have int: ‹f integrable_on {a..b}›
using absolutely_integrable_on_def by blast
have nint: ‹(λx. norm (f x)) integrable_on {a..b}›
using L absolutely_integrable_on_def by blast
have bv: ‹has_bounded_variation_on (λt. integral {a..t} f) {a..b}›
unfolding has_bounded_variation_on_def has_bounded_setvariation_on_def
proof (intro exI allI impI)
fix d t assume dt: ‹d division_of t ∧ t ⊆ {a..b}›
then have div: ‹d division_of t› and sub: ‹t ⊆ {a..b}› by auto
have ‹(∑k∈d. norm (integral {a..Sup k} f - integral {a..Inf k} f))
= (∑k∈d. norm (integral k f))›
proof (rule sum.cong[OF refl])
fix k assume kd: ‹k ∈ d›
obtain c e where ke: ‹k = {c..e}› ‹c ≤ e›
using division_ofD(4)[OF div kd] unfolding box_real
by (metis atLeastatMost_empty_iff2 division_ofD(3) dt kd)
have ksub: ‹k ⊆ {a..b}› using division_ofD(2)[OF div kd] sub by auto
then have ce_sub: ‹a ≤ c› ‹e ≤ b› using ke by auto
have ‹Inf k = c› ‹Sup k = e› using ke by auto
have fint_ac: ‹f integrable_on {a..c}›
using integrable_on_subinterval[OF int] ce_sub ‹c ≤ e› by auto
have fint_ce: ‹f integrable_on {c..e}›
using integrable_on_subinterval[OF int] ce_sub ke by auto
have fint_ae: ‹f integrable_on {a..e}›
using integrable_on_subinterval[OF int] ce_sub by auto
have ‹integral {a..e} f = integral {a..c} f + integral {c..e} f›
by (simp add: Henstock_Kurzweil_Integration.integral_combine ce_sub(1) fint_ae ke(2))
then have ‹integral {a..e} f - integral {a..c} f = integral {c..e} f›
by simp
then show ‹norm (integral {a..Sup k} f - integral {a..Inf k} f) = norm (integral k f)›
using ‹Inf k = c› ‹Sup k = e› ke by auto
qed
also have ‹… ≤ (∑k∈d. integral k (λx. norm (f x)))›
proof (rule sum_mono)
fix k assume ‹k ∈ d›
obtain c e where ke: ‹k = {c..e}› ‹c ≤ e›
using division_ofD(4)[OF div ‹k ∈ d›] unfolding box_real
by (metis atLeastatMost_empty_iff2 division_ofD(3) dt ‹k ∈ d›)
have ksub: ‹k ⊆ {a..b}› using division_ofD(2)[OF div ‹k ∈ d›] sub by auto
have fint: ‹f integrable_on k›
using integrable_on_subinterval[OF int] ksub ke(1) by blast
show ‹norm (integral k f) ≤ integral k (λx. norm (f x))›
using Henstock_Kurzweil_Integration.integral_norm_bound_integral fint
integrable_on_subinterval ke(1) ksub nint by blast
qed
also have ‹… ≤ integral t (λx. norm (f x))›
by (metis dt integrable_on_subdivision integral_combine_division_topdown landau_omega.R_refl
nint)
also have ‹… ≤ integral {a..b} (λx. norm (f x))›
by (metis dt integrable_on_subdivision integral_subset_le nint norm_ge_zero)
finally show ‹(∑k∈d. norm (integral {a..Sup k} f - integral {a..Inf k} f))
≤ integral {a..b} (λx. norm (f x))› .
qed
show ?R using int bv by blast
next
assume R: ?R
then have int: ‹f integrable_on {a..b}›
and bv: ‹has_bounded_variation_on (λt. integral {a..t} f) {a..b}›
by auto
then obtain B where B: ‹⋀d t. d division_of t ⟹ t ⊆ {a..b} ⟹
(∑k∈d. norm (integral {a..Sup k} f - integral {a..Inf k} f)) ≤ B›
unfolding has_bounded_variation_on_def has_bounded_setvariation_on_def by meson
show ?L
proof (rule bounded_variation_absolutely_integrable_real_interval[OF int])
fix d assume ddiv: ‹d division_of {a..b}›
have ‹(∑k∈d. norm (integral k f))
= (∑k∈d. norm (integral {a..Sup k} f - integral {a..Inf k} f))›
proof (rule sum.cong[OF refl])
fix k assume kd: ‹k ∈ d›
obtain c e where ke: ‹k = {c..e}› ‹c ≤ e›
using division_ofD(4)[OF ddiv kd] unfolding box_real
by (metis atLeastatMost_empty_iff2 division_ofD(3) ddiv kd)
have ksub: ‹k ⊆ {a..b}› using division_ofD(2)[OF ddiv kd] by auto
then have ce_sub: ‹a ≤ c› ‹e ≤ b› using ke by auto
have ‹Inf k = c› ‹Sup k = e› using ke by auto
have fint_ac: ‹f integrable_on {a..c}›
using integrable_on_subinterval[OF int] ce_sub ‹c ≤ e› by auto
have fint_ce: ‹f integrable_on {c..e}›
using integrable_on_subinterval[OF int] ce_sub ke by auto
have fint_ae: ‹f integrable_on {a..e}›
using integrable_on_subinterval[OF int] ce_sub by auto
have ‹integral {a..e} f = integral {a..c} f + integral {c..e} f›
by (simp add: Henstock_Kurzweil_Integration.integral_combine ce_sub(1) fint_ae ke(2))
then have ‹integral {a..e} f - integral {a..c} f = integral {c..e} f›
by simp
then show ‹norm (integral k f) = norm (integral {a..Sup k} f - integral {a..Inf k} f)›
using ‹Inf k = c› ‹Sup k = e› ke by auto
qed
also have ‹… ≤ B› using B[OF ddiv] by auto
finally show ‹(∑k∈d. norm (integral k f)) ≤ B› .
qed
qed
end