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
section ‹Basic properties›
lemma rectifiable_path_imp_path:
"rectifiable_path g ⟹ path g"
unfolding rectifiable_path_def by simp
lemma path_length_pos_le:
"rectifiable_path g ⟹ 0 ≤ path_length g"
unfolding rectifiable_path_def path_length_def
by (auto intro: vector_variation_pos_le)
lemma path_length_eq_0:
"rectifiable_path g ⟹
(path_length g = 0 ⟷ (∃c. ∀t ∈ {0..1}. g t = c))"
unfolding rectifiable_path_def path_length_def
by (rule vector_variation_const_eq) auto
lemma simple_path_length_pos_lt:
"rectifiable_path g ⟹ simple_path g ⟹ 0 < path_length g"
proof -
assume rect: "rectifiable_path g" and sp: "simple_path g"
have "path_length g ≠ 0"
proof
assume "path_length g = 0"
then obtain c where c: "⋀t. t ∈ {0..1} ⟹ g t = c"
using path_length_eq_0[OF rect] by auto
hence "g (1/4) = g (3/4)" by auto
moreover from sp have "inj_on g {0<..<1}" by (rule simple_path_inj_on)
ultimately have "(1/4::real) = 3/4"
by (auto dest: inj_onD)
thus False by simp
qed
with path_length_pos_le[OF rect] show "0 < path_length g"
by linarith
qed
section ‹Invariance under transformations›
lemma rectifiable_path_translation_eq:
"rectifiable_path ((λx. a + x) ∘ g) ⟷ rectifiable_path g"
proof -
have "path g"
if "path (λx. a + g x)"
and "has_bounded_variation_on (λx. a + g x) {0..1}"
using that path_translation_eq[of a g] by (simp add: o_def)
moreover have "has_bounded_variation_on g {0..1}"
if "path (λx. a + g x)"
and "has_bounded_variation_on (λx. a + g x) {0..1}"
proof -
have "has_bounded_variation_on (λx. a + g x + (- a)) {0..1}"
using that(2) has_bounded_variation_on_const[of "-a" "{0..1}"]
by (rule has_bounded_variation_on_add)
then show ?thesis by simp
qed
moreover have "path (λx. a + g x)"
if "path g"
and "has_bounded_variation_on g {0..1}"
using that path_translation_eq[of a g] by (simp add: o_def)
moreover have "has_bounded_variation_on (λx. a + g x) {0..1}"
if "path g"
and "has_bounded_variation_on g {0..1}"
using that(2) has_bounded_variation_on_const[of a "{0..1}"]
by (auto intro: has_bounded_variation_on_add)
ultimately show ?thesis
by (auto simp: o_def rectifiable_path_def)
qed
lemma path_length_translation:
"path_length ((λx. a + x) ∘ g) = path_length g"
unfolding path_length_def vector_variation_def comp_def
by (simp add: algebra_simps)
lemma has_bounded_variation_on_linear_image:
assumes "linear f" "has_bounded_variation_on g {0..1}"
shows "has_bounded_variation_on (f ∘ g) {0..1}"
proof -
have bl: "bounded_linear f" using assms(1) linear_conv_bounded_linear by auto
have bound: "⋀d. d division_of {0..1} ⟹
(∑k∈d. norm ((f ∘ g) (Sup k) - (f ∘ g) (Inf k)))
≤ onorm f * vector_variation {0..1} g"
proof -
fix d :: "real set set" assume div: "d division_of {0..1}"
have "(∑k∈d. norm ((f ∘ g) (Sup k) - (f ∘ g) (Inf k)))
= (∑k∈d. norm (f (g (Sup k) - g (Inf k))))"
using assms(1) by (simp add: o_def linear_diff)
also have "… ≤ (∑k∈d. onorm f * norm (g (Sup k) - g (Inf k)))"
by (intro sum_mono onorm[OF bl])
also have "… = onorm f * (∑k∈d. norm (g (Sup k) - g (Inf k)))"
by (simp add: sum_distrib_left)
also have "… ≤ onorm f * vector_variation {0..1} g"
by (intro mult_left_mono has_bounded_variation_works(1)[OF assms(2) div order_refl]
onorm_pos_le[OF bl])
finally show "(∑k∈d. norm ((f ∘ g) (Sup k) - (f ∘ g) (Inf k)))
≤ onorm f * vector_variation {0..1} g" .
qed
then show ?thesis
unfolding has_bounded_variation_on_interval by blast
qed
lemma rectifiable_path_linear_image_eq:
assumes "linear f" "inj f"
shows "rectifiable_path (f ∘ g) ⟷ rectifiable_path g"
proof
assume "rectifiable_path g"
then show "rectifiable_path (f ∘ g)"
unfolding rectifiable_path_def
using path_linear_image_eq[OF assms] has_bounded_variation_on_linear_image[OF assms(1)]
by auto
next
assume fg: "rectifiable_path (f ∘ g)"
have invf: "has_bounded_variation_on g {0..1}"
proof -
obtain B where "B > 0" and Bbound: "⋀x. B * norm x ≤ norm (f x)"
using linear_inj_bounded_below_pos[OF assms(1) assms(2)] by auto
have bv_fg: "has_bounded_variation_on (f ∘ g) {0..1}"
using fg unfolding rectifiable_path_def by auto
show ?thesis unfolding has_bounded_variation_on_interval
proof -
obtain C where C: "⋀d. d division_of {0..1} ⟹
(∑k∈d. norm ((f ∘ g) (Sup k) - (f ∘ g) (Inf k))) ≤ C"
using bv_fg unfolding has_bounded_variation_on_interval by auto
{ fix d :: "real set set" assume div: "d division_of {0..1}"
have "(∑k∈d. B * norm (g (Sup k) - g (Inf k)))
≤ (∑k∈d. norm (f (g (Sup k) - g (Inf k))))"
by (intro sum_mono Bbound)
also have "… = (∑k∈d. norm ((f ∘ g) (Sup k) - (f ∘ g) (Inf k)))"
using assms(1) by (simp add: o_def real_vector.linear_diff)
also have "… ≤ C" using C[OF div] .
finally have "B * (∑k∈d. norm (g (Sup k) - g (Inf k))) ≤ C"
by (simp add: sum_distrib_left)
then have "(∑k∈d. norm (g (Sup k) - g (Inf k))) ≤ C / B"
using ‹B > 0› by (simp add: field_simps) }
then show "∃B. ∀d. d division_of {0..1} ⟶
(∑k∈d. norm (g (Sup k) - g (Inf k))) ≤ B" by blast
qed
qed
moreover have "path g"
using fg path_linear_image_eq[OF assms(1) assms(2)] unfolding rectifiable_path_def by auto
ultimately show "rectifiable_path g"
unfolding rectifiable_path_def by auto
qed
lemma path_length_linear_image:
assumes "linear f" "⋀x. norm (f x) = norm x"
shows "path_length (f ∘ g) = path_length g"
proof -
have eq: "⋀k. norm (f (g (Sup k)) - f (g (Inf k))) = norm (g (Sup k) - g (Inf k))"
by (metis assms(1) assms(2) real_vector.linear_diff)
then show ?thesis
unfolding path_length_def vector_variation_def set_variation_def comp_def by presburger
qed
lemma rectifiable_path_eq:
assumes eq: "⋀t. t ∈ {0..1} ⟹ g t = h t"
and rect: "rectifiable_path g"
shows "rectifiable_path h"
proof -
have "path h"
proof -
have "continuous_on {0..1} h = continuous_on {0..1} g"
by (rule continuous_on_cong_simp[OF refl]) (use eq in ‹simp add: simp_implies_def›)
then show ?thesis using rect unfolding rectifiable_path_def path_def by auto
qed
moreover have "has_bounded_variation_on h {0..1}"
proof -
from rect have bv: "has_bounded_variation_on g {0..1}"
unfolding rectifiable_path_def by auto
have sup_inf_in: "Sup k ∈ {0..1} ∧ Inf k ∈ {0..1}"
if "d division_of {(0::real)..1}" "k ∈ d" for d k
proof -
from division_ofD(2)[OF that] have ks: "k ⊆ {0..1}" .
from division_ofD(3)[OF that] have kne: "k ≠ {}" .
from division_ofD(4)[OF that] obtain a b where kab: "k = cbox a b" by auto
with kne have "a ≤ b" by auto
then have "Sup k = b" "Inf k = a"
using kab by (auto simp: cSup_atLeastAtMost cInf_atLeastAtMost)
then show ?thesis using ks kab ‹a ≤ b› by auto
qed
have sums_eq: "(∑k∈d. norm (h (Sup k) - h (Inf k))) = (∑k∈d. norm (g (Sup k) - g (Inf k)))"
if "d division_of {(0::real)..1}" for d
using sup_inf_in[OF that] by (intro sum.cong refl) (auto simp: eq)
then show ?thesis
using bv unfolding has_bounded_variation_on_interval by auto
qed
ultimately show ?thesis unfolding rectifiable_path_def by auto
qed
lemma path_length_eq:
assumes eq: "⋀t. t ∈ {0..1} ⟹ g t = h t"
and rect: "rectifiable_path g"
shows "path_length g = path_length h"
proof -
have sup_inf_in: "Sup k ∈ {0..1} ∧ Inf k ∈ {0..1}"
if "d division_of t" "t ⊆ {(0::real)..1}" "k ∈ d" for d t k
proof -
from division_ofD(2)[OF that(1) that(3)] that(2) have ks: "k ⊆ {0..1}" by auto
from division_ofD(3)[OF that(1) that(3)] have kne: "k ≠ {}" .
from division_ofD(4)[OF that(1) that(3)] obtain a b where kab: "k = cbox a b" by auto
with kne have "a ≤ b" by auto
then have "Sup k = b" "Inf k = a"
using kab by (auto simp: cSup_atLeastAtMost cInf_atLeastAtMost)
then show ?thesis using ks kab ‹a ≤ b› by auto
qed
have sums_eq: "(∑k∈d. norm (h (Sup k) - h (Inf k))) = (∑k∈d. norm (g (Sup k) - g (Inf k)))"
if "d division_of t" "t ⊆ {(0::real)..1}" for d t
using sup_inf_in[OF that] by (intro sum.cong refl) (auto simp: eq)
have "{∑k∈d. norm (h (Sup k) - h (Inf k)) |d. ∃t. d division_of t ∧ t ⊆ {0..1}}
= {∑k∈d. norm (g (Sup k) - g (Inf k)) |d. ∃t. d division_of t ∧ t ⊆ {0..1}}"
by (metis (lifting) sums_eq)
then show ?thesis
unfolding path_length_def vector_variation_def set_variation_def by auto
qed
lemma path_length_reversepath:
"rectifiable_path g ⟹ path_length (reversepath g) = path_length g"
unfolding path_length_def reversepath_def comp_def[symmetric]
using vector_variation_reflect[of 0 1 g 1] by simp
lemma rectifiable_path_subpath:
"⟦rectifiable_path g; u ∈ {0..1}; v ∈ {0..1}⟧ ⟹
rectifiable_path (subpath u v g)"
unfolding rectifiable_path_def subpath_def
proof (intro conjI)
assume rect: "path g ∧ has_bounded_variation_on g {0..1}" and u: "u ∈ {0..1}" and v: "v ∈ {0..1}"
show "path (λx. g ((v - u) * x + u))"
using rect u v path_subpath unfolding subpath_def by auto
have bv: "has_bounded_variation_on g {0..1}" using rect by auto
have seg: "closed_segment u v ⊆ {0..1}" using u v
by (auto simp: closed_segment_eq_real_ivl split: if_splits)
show "has_bounded_variation_on (λx. g ((v - u) * x + u)) {0..1}"
proof (cases "u ≤ v")
case True
have mono: "mono_on {0..1} (λx. (v - u) * x + u)"
using True by (auto intro!: mono_onI mult_left_mono)
have "has_bounded_variation_on g {u..v}"
using bv seg True by (auto simp: closed_segment_eq_real_ivl
intro: has_bounded_variation_on_subset)
then show ?thesis
using has_bounded_variation_compose_monotone(1)[of g "λx. (v-u)*x+u" 0 1]
mono True by (simp add: comp_def)
next
case False
then have vu: "v ≤ u" by auto
have mono: "mono_on {0..1} (λx. (u - v) * x + v)"
using vu by (auto intro!: mono_onI mult_left_mono)
have bvvu: "has_bounded_variation_on g {v..u}"
using bv seg vu
by (auto simp: closed_segment_eq_real_ivl split: if_splits
intro: has_bounded_variation_on_subset)
have "(λx. g ((v - u) * x + u)) = (λx. g ((u - v) * (1 - x) + v))"
by (auto simp: algebra_simps)
also have "… = (g ∘ (λx. (u-v)*x + v)) ∘ (λx. 1 - x)"
by (auto simp: comp_def)
finally have eq: "(λx. g ((v - u) * x + u)) = (g ∘ (λx. (u-v)*x + v)) ∘ (-) 1"
by (auto simp: comp_def)
have "has_bounded_variation_on (g ∘ (λx. (u-v)*x + v)) {0..1}"
using has_bounded_variation_compose_monotone(1)[of g "λx. (u-v)*x+v" 0 1]
mono bvvu by (simp add: comp_def)
then have "has_bounded_variation_on (g ∘ (λx. (u-v)*x + v)) {1 - 1..1 - 0}"
by simp
then have "has_bounded_variation_on ((g ∘ (λx. (u-v)*x + v)) ∘ (-) 1) {0..1}"
by (rule has_bounded_variation_on_reflect)
then show ?thesis
using eq by simp
qed
qed
lemma division_of_affine_image:
fixes c d :: real
assumes cpos: "c > 0" and div: "D division_of T" and sub: "T ⊆ {a..b}"
shows "((`) (λx. c * x + d)) ` D division_of ((λx. c * x + d) ` T)"
and "(λx. c * x + d) ` T ⊆ {c*a+d..c*b+d}"
proof -
let ?φ = "λx::real. c * x + d"
have inj: "inj ?φ" using cpos by (intro injI) simp
have mono: "mono ?φ" using cpos by (intro monoI) auto
show sub': "?φ ` T ⊆ {c*a+d..c*b+d}"
using sub cpos by (auto simp: mult_left_mono)
show "((`) ?φ) ` D division_of (?φ ` T)"
unfolding division_of_def
proof (intro conjI ballI impI)
show "finite (((`) ?φ) ` D)"
using division_ofD(1)[OF div] by auto
next
fix K assume "K ∈ ((`) ?φ) ` D"
then obtain K0 where K0: "K0 ∈ D" "K = ?φ ` K0" by auto
from division_ofD(2)[OF div K0(1)] have K0sub: "K0 ⊆ T" .
from division_ofD(3)[OF div K0(1)] have K0ne: "K0 ≠ {}" .
then show "K ⊆ ?φ ` T" "K ≠ {}" using K0(2) K0sub by auto
from division_ofD(4)[OF div K0(1)] obtain α β where ab: "K0 = cbox α β" by auto
then have "K0 = {α..β}" by auto
with K0ne have αβ: "α ≤ β" by auto
have "K = ?φ ` {α..β}" using K0(2) ‹K0 = {α..β}› by auto
also have "… = {c*α+d..c*β+d}"
proof -
have "?φ ` {α..β} = {y. ∃x. α ≤ x ∧ x ≤ β ∧ y = c*x+d}"
by (auto simp: image_def)
also have "… = {c*α+d..c*β+d}"
proof (auto simp: mult_left_mono[OF _ less_imp_le[OF cpos]])
fix y assume "c * α + d ≤ y" "y ≤ c * β + d"
then have "α ≤ (y - d) / c" "((y - d) / c) ≤ β"
using cpos by (auto simp: field_simps)
moreover have "y = c * ((y - d) / c) + d" using cpos by auto
ultimately show "∃x≥α. x ≤ β ∧ y = c * x + d" by auto
qed
finally show ?thesis .
qed
finally show "∃α β. K = cbox α β" by (auto simp: cbox_interval)
next
fix K1 K2
assume "K1 ∈ ((`) ?φ) ` D" "K2 ∈ ((`) ?φ) ` D" "K1 ≠ K2"
then obtain K1' K2' where K1': "K1' ∈ D" "K1 = ?φ ` K1'"
and K2': "K2' ∈ D" "K2 = ?φ ` K2'" by auto
have "K1' ≠ K2'" using ‹K1 ≠ K2› K1'(2) K2'(2) inj_image_eq_iff[OF inj] by auto
then have disj: "interior K1' ∩ interior K2' = {}"
using division_ofD(5)[OF div K1'(1) K2'(1)] by auto
show "interior K1 ∩ interior K2 = {}"
proof (rule ccontr)
assume "interior K1 ∩ interior K2 ≠ {}"
then obtain y where "y ∈ interior K1" "y ∈ interior K2" by auto
from division_ofD(4)[OF div K1'(1)] obtain a1 b1 where "K1' = cbox a1 b1" by auto
from division_ofD(4)[OF div K2'(1)] obtain a2 b2 where "K2' = cbox a2 b2" by auto
then have K1eq: "K1' = {a1..b1}" and K2eq: "K2' = {a2..b2}"
using ‹K1' = cbox a1 b1› by auto
from division_ofD(3)[OF div K1'(1)] K1eq have "a1 ≤ b1" by (auto split: if_splits)
from division_ofD(3)[OF div K2'(1)] K2eq have "a2 ≤ b2" by (auto split: if_splits)
have K1img: "K1 = {c*a1+d..c*b1+d}"
proof -
have "K1 = ?φ ` {a1..b1}" using K1'(2) K1eq by auto
also have "… = {c*a1+d..c*b1+d}"
proof safe
fix x assume "x ∈ {a1..b1}"
then show "?φ x ∈ {c*a1+d..c*b1+d}" using cpos
by (auto intro: mult_left_mono)
next
fix y assume "y ∈ {c*a1+d..c*b1+d}"
then have mem: "(y-d)/c ∈ {a1..b1}" using cpos by (auto simp: field_simps)
moreover have "?φ ((y-d)/c) = y" using cpos by (simp add: field_simps)
ultimately show "y ∈ ?φ ` {a1..b1}" by force
qed
finally show ?thesis .
qed
have K2img: "K2 = {c*a2+d..c*b2+d}"
proof -
have "K2 = ?φ ` {a2..b2}" using K2'(2) K2eq by auto
also have "… = {c*a2+d..c*b2+d}"
proof safe
fix x assume "x ∈ {a2..b2}"
then show "?φ x ∈ {c*a2+d..c*b2+d}" using cpos
by (auto intro: mult_left_mono)
next
fix y assume "y ∈ {c*a2+d..c*b2+d}"
then have "(y-d)/c ∈ {a2..b2}" using cpos by (auto simp: field_simps)
moreover have "?φ ((y-d)/c) = y" using cpos by (simp add: field_simps)
ultimately show "y ∈ ?φ ` {a2..b2}" by force
qed
finally show ?thesis .
qed
from ‹y ∈ interior K1› K1img have "c*a1+d < y" "y < c*b1+d"
using ‹a1 ≤ b1› interior_atLeastAtMost_real by auto
then have "a1 < (y-d)/c" "(y-d)/c < b1" using cpos by (auto simp: field_simps)
then have "(y-d)/c ∈ interior K1'"
using K1eq interior_atLeastAtMost_real by auto
from ‹y ∈ interior K2› K2img have "c*a2+d < y" "y < c*b2+d"
using ‹a2 ≤ b2› interior_atLeastAtMost_real by auto
then have "a2 < (y-d)/c" "(y-d)/c < b2" using cpos by (auto simp: field_simps)
then have "(y-d)/c ∈ interior K2'"
using K2eq interior_atLeastAtMost_real by auto
with ‹(y-d)/c ∈ interior K1'› disj show False by auto
qed
next
have "⋃ (((`) ?φ) ` D) = ?φ ` (⋃ D)" by auto
also have "⋃ D = T" using division_ofD(6)[OF div] by auto
finally show "⋃ (((`) ?φ) ` D) = ?φ ` T" .
qed
qed
lemma vector_variation_affine_eq:
fixes g :: "real ⇒ 'a::euclidean_space" and c d :: real
assumes "c > 0" "a ≤ b"
shows "vector_variation {a..b} (g ∘ (λx. c * x + d)) = vector_variation {c*a+d..c*b+d} g"
proof -
let ?φ = "λx::real. c * x + d"
let ?ψ = "λx::real. (x - d) / c"
have cne: "c ≠ 0" using assms(1) by auto
have cpos: "0 < c" using assms(1) .
have inj_φ: "inj ?φ" using cne by (intro injI) simp
have φψ: "⋀x. ?φ (?ψ x) = x" using cne by (simp add: field_simps)
have ψφ: "⋀x. ?ψ (?φ x) = x" using cne by (simp add: field_simps)
have ab': "c*a+d ≤ c*b+d" using assms by (auto intro: mult_left_mono)
have img_ivl: "⋀α β. α ≤ β ⟹ ?φ ` {α..β} = {c*α+d..c*β+d}"
proof safe
fix α β x :: real assume "α ≤ β" "x ∈ {α..β}"
then show "?φ x ∈ {c*α+d..c*β+d}" using cpos by (auto intro: mult_left_mono)
next
fix α β y :: real assume "α ≤ β" "y ∈ {c*α+d..c*β+d}"
then have "(y-d)/c ∈ {α..β}" using cpos by (auto simp: field_simps)
moreover have "?φ ((y-d)/c) = y" using cne by (simp add: field_simps)
ultimately show "y ∈ ?φ ` {α..β}" by force
qed
have sum_transform: "(∑k∈D. norm ((g ∘ ?φ) (Sup k) - (g ∘ ?φ) (Inf k)))
= (∑k∈((`) ?φ) ` D. norm (g (Sup k) - g (Inf k)))"
if "D division_of T" for D :: "real set set" and T :: "real set"
proof -
have div: "D division_of T" using that .
have inj_on_img: "inj_on ((`) ?φ) D"
using inj_image_eq_iff[OF inj_φ] by (auto intro!: inj_onI)
have "(∑k∈D. norm ((g ∘ ?φ) (Sup k) - (g ∘ ?φ) (Inf k)))
= (∑k∈D. norm (g (?φ (Sup k)) - g (?φ (Inf k))))" by (simp add: o_def)
also have "… = (∑k∈D. norm (g (Sup (?φ ` k)) - g (Inf (?φ ` k))))"
proof (intro sum.cong refl arg_cong[where f=norm] arg_cong2[where f="(-)"])
fix k assume "k ∈ D"
from division_ofD(4)[OF div this] obtain α β where kab: "k = cbox α β" by auto
from division_ofD(3)[OF div ‹k ∈ D›] have kne: "k ≠ {}" .
with kab have le: "α ≤ β" by auto
have k_ivl: "k = {α..β}" using kab by auto
have img: "?φ ` k = {c*α+d..c*β+d}" using img_ivl[OF le] k_ivl by simp
have le': "c*α+d ≤ c*β+d" using le cpos by (auto intro: mult_left_mono)
show "g (?φ (Sup k)) = g (Sup (?φ ` k))"
using k_ivl le img le' by (simp add: cSup_atLeastAtMost)
show "g (?φ (Inf k)) = g (Inf (?φ ` k))"
using k_ivl le img le' by (simp add: cInf_atLeastAtMost)
qed
also have "… = (∑k∈((`) ?φ) ` D. norm (g (Sup k) - g (Inf k)))"
by (metis (no_types, lifting) inj_on_img sum.reindex_cong)
finally show "(∑k∈D. norm ((g ∘ ?φ) (Sup k) - (g ∘ ?φ) (Inf k)))
= (∑k∈((`) ?φ) ` D. norm (g (Sup k) - g (Inf k)))" .
qed
have sets_eq: "{∑k∈D. norm ((g ∘ ?φ) (Sup k) - (g ∘ ?φ) (Inf k)) |D.
∃T. D division_of T ∧ T ⊆ {a..b}}
= {∑k∈D. norm (g (Sup k) - g (Inf k)) |D.
∃T. D division_of T ∧ T ⊆ {c*a+d..c*b+d}}"
proof safe
fix D T assume div: "D division_of T" and sub: "T ⊆ {a..b}"
let ?D' = "((`) ?φ) ` D"
have div': "?D' division_of (?φ ` T)"
using division_of_affine_image(1)[OF cpos div sub] .
have sub': "?φ ` T ⊆ {c*a+d..c*b+d}"
using division_of_affine_image(2)[OF cpos div sub] .
have sum_eq: "(∑k∈D. norm ((g ∘ ?φ) (Sup k) - (g ∘ ?φ) (Inf k)))
= (∑k∈?D'. norm (g (Sup k) - g (Inf k)))"
using sum_transform[OF div] .
show "∃Da. (∑k∈D. norm ((g ∘ ?φ) (Sup k) - (g ∘ ?φ) (Inf k)))
= (∑k∈Da. norm (g (Sup k) - g (Inf k)))
∧ (∃T. Da division_of T ∧ T ⊆ {c*a+d..c*b+d})"
using sum_eq div' sub' by blast
next
fix D T assume div: "D division_of T" and sub: "T ⊆ {c*a+d..c*b+d}"
let ?c' = "1/c" and ?d' = "-d/c"
have cpos': "?c' > 0" using cpos by auto
have div': "((`) (λx. ?c' * x + ?d')) ` D division_of ((λx. ?c' * x + ?d') ` T)"
using division_of_affine_image(1)[OF cpos' div sub] .
have sub': "(λx. ?c' * x + ?d') ` T ⊆ {?c'*(c*a+d)+?d'..?c'*(c*b+d)+?d'}"
using division_of_affine_image(2)[OF cpos' div sub] .
have endpoints: "?c'*(c*a+d)+?d' = a" "?c'*(c*b+d)+?d' = b"
using cne by (auto simp: field_simps)
have inv_eq: "(λx::real. ?c' * x + ?d') = ?ψ"
by (rule ext) (simp add: diff_divide_distrib)
have div'': "((`) ?ψ) ` D division_of (?ψ ` T)"
using div' unfolding inv_eq .
have sub'': "?ψ ` T ⊆ {a..b}"
proof -
have "(λx::real. ?c' * x + ?d') ` T ⊆ {a..b}"
using sub' endpoints by auto
then show ?thesis unfolding inv_eq .
qed
have sum_eq: "(∑k∈((`) ?ψ) ` D. norm ((g ∘ ?φ) (Sup k) - (g ∘ ?φ) (Inf k)))
= (∑k∈((`) ?φ) ` ((`) ?ψ) ` D. norm (g (Sup k) - g (Inf k)))"
using sum_transform[OF div''] .
have φψ_img: "?φ ` ?ψ ` S = S" for S :: "real set"
proof -
have "?φ ` ?ψ ` S = (?φ ∘ ?ψ) ` S" by (simp add: image_image)
also have "(?φ ∘ ?ψ) = id"
using cne by (auto simp: o_def field_simps)
also have "id ` S = S" by simp
finally show ?thesis .
qed
have img_back: "((`) ?φ) ` ((`) ?ψ) ` D = D"
proof -
have "((`) ?φ) ` ((`) ?ψ) ` D = ((`) ?φ ∘ (`) ?ψ) ` D"
by (simp add: image_comp)
also have "((`) ?φ ∘ (`) ?ψ) = id"
by (rule ext) (simp add: φψ_img)
also have "id ` D = D" by simp
finally show ?thesis .
qed
have sum_eq': "(∑k∈((`) ?ψ) ` D. norm ((g ∘ ?φ) (Sup k) - (g ∘ ?φ) (Inf k)))
= (∑k∈D. norm (g (Sup k) - g (Inf k)))"
using sum_eq img_back by simp
show "∃E. (∑k∈D. norm (g (Sup k) - g (Inf k))) = (∑k∈E. norm ((g ∘ ?φ) (Sup k) - (g ∘ ?φ) (Inf k)))
∧ (∃T. E division_of T ∧ T ⊆ {a..b})"
using sum_eq' div'' sub'' by (metis (no_types, lifting))
qed
show ?thesis
unfolding vector_variation_def set_variation_def using sets_eq by auto
qed
lemma path_length_subpath_eq:
assumes "s ∈ {0..1}" "t ∈ {0..1}"
and rect: "rectifiable_path g"
shows "path_length (subpath s t g) = vector_variation (closed_segment s t) g"
using assms
proof (cases "s ≤ t")
case True
then have cs: "closed_segment s t = {s..t}"
by (simp add: closed_segment_eq_real_ivl)
show ?thesis
proof (cases "s = t")
case True
then show ?thesis
proof -
from ‹s = t› have cs': "closed_segment s t = {t..t}" using cs by simp
have "path_length (subpath t t g) = 0"
by (metis ‹t ∈ {0..1}› eq_iff_diff_eq_0 mult_zero_left path_length_eq_0 rect
rectifiable_path_subpath subpath_def)
moreover have "vector_variation {t..t} g = 0"
by (rule vector_variation_on_null) (simp add: content_real_eq_0)
ultimately show ?thesis using ‹s = t› cs' by simp
qed
next
case False
with ‹s ≤ t› have "s < t" by auto
then have "t - s > 0" by auto
have "path_length (subpath s t g) = vector_variation {0..1} (g ∘ (λx. (t-s)*x + s))"
unfolding path_length_def subpath_def by (simp add: comp_def)
also have "… = vector_variation {(t-s)*0+s..(t-s)*1+s} g"
using vector_variation_affine_eq[OF ‹t - s > 0› zero_le_one, where d=s and g=g] by simp
also have "… = vector_variation {s..t} g"
by simp
finally show ?thesis by (simp add: cs)
qed
next
case False
then have ts: "t < s" by auto
then have cs: "closed_segment s t = {t..s}"
by (simp add: closed_segment_eq_real_ivl)
have "s - t > 0" using ts by auto
have "path_length (subpath s t g) = vector_variation {0..1} (λx. g ((t - s) * x + s))"
unfolding path_length_def subpath_def by simp
also have "… = vector_variation {0..1} (g ∘ (λx. (s - t) * x + t) ∘ (-) 1)"
by (simp add: comp_def algebra_simps)
finally
show ?thesis
using vector_variation_affine_eq[OF ‹s - t > 0› zero_le_one, where d=t and g=g]
by (simp add: cs vector_variation_reflect)
qed
lemma vector_variation_cong:
assumes "⋀x. x ∈ s ⟹ f x = g x"
shows "vector_variation s f = vector_variation s g"
proof -
have sum_eq: "(∑k∈d. norm (f (Sup k) - f (Inf k))) = (∑k∈d. norm (g (Sup k) - g (Inf k)))"
if "d division_of t" "t ⊆ s" for d t
proof (rule sum.cong[OF refl])
fix k assume "k ∈ d"
then have "k ⊆ t" "k ≠ {}" "∃a b. k = cbox a b"
using division_ofD(2,3,4)[OF that(1)] by auto
then obtain a b where "k = cbox a b" "a ≤ b" by fastforce
then have "Inf k ∈ k" "Sup k ∈ k" by auto
then have "Inf k ∈ s" "Sup k ∈ s" using ‹k ⊆ t› that(2) by auto
then show "norm (f (Sup k) - f (Inf k)) = norm (g (Sup k) - g (Inf k))"
using assms by auto
qed
have "{∑k∈d. norm (f (Sup k) - f (Inf k)) |d. ∃t. d division_of t ∧ t ⊆ s}
= {∑k∈d. norm (g (Sup k) - g (Inf k)) |d. ∃t. d division_of t ∧ t ⊆ s}"
(is "?L = ?R")
proof (rule set_eqI, rule iffI)
fix x assume "x ∈ ?L"
then obtain d t where "x = (∑k∈d. norm (f (Sup k) - f (Inf k)))" "d division_of t" "t ⊆ s"
by auto
then show "x ∈ ?R" using sum_eq by auto
next
fix x assume "x ∈ ?R"
then obtain d t where "x = (∑k∈d. norm (g (Sup k) - g (Inf k)))" "d division_of t" "t ⊆ s"
by auto
then show "x ∈ ?L" using sum_eq
by (metis (mono_tags, lifting) mem_Collect_eq)
qed
then show ?thesis
unfolding vector_variation_def set_variation_def by simp
qed
lemma has_bounded_variation_on_cong:
assumes "⋀x. x ∈ s ⟹ f x = g x"
shows "has_bounded_variation_on f s ⟷ has_bounded_variation_on g s"
proof -
have "⋀d t. d division_of t ⟹ t ⊆ s ⟹
(∑k∈d. norm (f (Sup k) - f (Inf k))) = (∑k∈d. norm (g (Sup k) - g (Inf k)))"
proof -
fix d t assume dt: "d division_of t" "t ⊆ s"
show "(∑k∈d. norm (f (Sup k) - f (Inf k))) = (∑k∈d. norm (g (Sup k) - g (Inf k)))"
proof (rule sum.cong[OF refl])
fix k assume "k ∈ d"
then have "k ⊆ t" "k ≠ {}" "∃a b. k = cbox a b"
using division_ofD(2,3,4)[OF dt(1)] by auto
then obtain a b where "k = cbox a b" "a ≤ b" by fastforce
then have "Inf k ∈ k" "Sup k ∈ k" by auto
then have "Inf k ∈ s" "Sup k ∈ s" using ‹k ⊆ t› dt(2) by auto
then show "norm (f (Sup k) - f (Inf k)) = norm (g (Sup k) - g (Inf k))"
using assms by auto
qed
qed
then show ?thesis
unfolding has_bounded_variation_on_def has_bounded_setvariation_on_def by (metis (lifting))
qed
lemma has_bounded_variation_on_affine_iff:
fixes g :: "real ⇒ 'a::euclidean_space" and c d :: real
assumes "c > 0" "a ≤ b"
shows "has_bounded_variation_on (g ∘ (λx. c * x + d)) {a..b} ⟷
has_bounded_variation_on g {c*a+d..c*b+d}"
proof
assume "has_bounded_variation_on g {c*a+d..c*b+d}"
moreover have "mono_on {a..b} (λx. c * x + d)"
using assms(1) by (auto intro!: mono_onI mult_left_mono)
ultimately show "has_bounded_variation_on (g ∘ (λx. c * x + d)) {a..b}"
by (rule has_bounded_variation_compose_monotone(1))
next
assume bv: "has_bounded_variation_on (g ∘ (λx. c * x + d)) {a..b}"
let ?inv = "λx. (x - d) / c"
have inv_mono: "mono_on {c*a+d..c*b+d} ?inv"
using assms(1) by (smt (verit, ccfv_SIG) divide_less_cancel monotone_on_def)
have inv_a: "?inv (c*a+d) = a" and inv_b: "?inv (c*b+d) = b"
using assms(1) by (auto simp: field_simps)
have comp_eq: "(g ∘ (λx. c * x + d)) ∘ ?inv = g"
using assms(1) by (auto simp: comp_def field_simps)
have "has_bounded_variation_on ((g ∘ (λx. c * x + d)) ∘ ?inv) {c*a+d..c*b+d}"
by (metis (lifting) bv has_bounded_variation_compose_monotone(1) inv_a inv_b
inv_mono)
then show "has_bounded_variation_on g {c*a+d..c*b+d}"
by (simp add: comp_eq)
qed
lemma rectifiable_path_join:
assumes "pathfinish g1 = pathstart g2"
shows "rectifiable_path (g1 +++ g2) ⟷
rectifiable_path g1 ∧ rectifiable_path g2"
proof -
have half: "(0::real) ≤ 1/2" "1/2 ≤ (1::real)" by auto
have eq1: "(g1 +++ g2) x = (g1 ∘ (λx. 2 * x)) x" if "x ∈ {0..1/2}" for x
using that by (auto simp: joinpaths_def)
have eq2: "(g1 +++ g2) x = (g2 ∘ (λx. 2 * x + (-1))) x" if "x ∈ {1/2..1}" for x
proof -
from that have "x = 1/2 ∨ x > 1/2" by auto
then show ?thesis
proof
assume "x = 1/2"
then show ?thesis
using assms by (simp add: joinpaths_def mult.commute pathfinish_def pathstart_def)
next
assume "x > 1/2"
then show ?thesis by (auto simp: joinpaths_def comp_def)
qed
qed
have bv1: "has_bounded_variation_on (g1 +++ g2) {0..1/2} ⟷
has_bounded_variation_on g1 {0..1}"
proof -
have "has_bounded_variation_on (g1 +++ g2) {0..1/2} ⟷
has_bounded_variation_on (g1 ∘ (λx. 2 * x)) {0..1/2}"
by (rule has_bounded_variation_on_cong[OF eq1])
also have "… ⟷ has_bounded_variation_on g1 {2*0+0..2*(1/2)+0}"
using has_bounded_variation_on_affine_iff [of 2 0 ‹1/2› _ 0] by force
also have "{2*0+(0::real)..2*(1/2)+0} = {0..1}" by auto
finally show ?thesis .
qed
have bv2: "has_bounded_variation_on (g1 +++ g2) {1/2..1} ⟷
has_bounded_variation_on g2 {0..1}"
proof -
have "has_bounded_variation_on (g1 +++ g2) {1/2..1} ⟷
has_bounded_variation_on (g2 ∘ (λx. 2 * x + (-1))) {1/2..1}"
by (rule has_bounded_variation_on_cong[OF eq2])
also have "… ⟷ has_bounded_variation_on g2 {2*(1/2)+(-1)..2*1+(-1)}"
by (rule has_bounded_variation_on_affine_iff) auto
also have "{2*(1/2)+(-1::real)..2*1+(-1)} = {0..1}" by auto
finally show ?thesis .
qed
show ?thesis
unfolding rectifiable_path_def
using path_join[OF assms]
has_bounded_variation_on_combine[OF half(1) half(2), of "g1 +++ g2"]
bv1 bv2
by auto
qed
lemma path_length_join:
assumes "rectifiable_path g1"
and "rectifiable_path g2"
and "pathfinish g1 = pathstart g2"
shows "path_length (g1 +++ g2) = path_length g1 + path_length g2"
proof -
have half: "(0::real) ≤ 1/2" "1/2 ≤ (1::real)" by auto
have bvj: "has_bounded_variation_on (g1 +++ g2) {0..1}"
using rectifiable_path_def assms rectifiable_path_join by blast
have eq1: "(g1 +++ g2) x = (g1 ∘ (λx. 2 * x)) x" if "x ∈ {0..1/2}" for x
using that by (auto simp: joinpaths_def)
have eq2: "(g1 +++ g2) x = (g2 ∘ (λx. 2 * x + (-1))) x" if "x ∈ {1/2..1}" for x
proof -
from that have "x = 1/2 ∨ x > 1/2" by auto
then show ?thesis
proof
assume "x = 1/2"
then show ?thesis
using assms by (simp add: joinpaths_def mult.commute pathfinish_def pathstart_def)
next
assume "x > 1/2"
then show ?thesis by (auto simp: joinpaths_def comp_def)
qed
qed
have vv1: "vector_variation {0..1/2} (g1 +++ g2) = path_length g1"
proof -
have "vector_variation {0..1/2} (g1 +++ g2) =
vector_variation {0..1/2} (g1 ∘ (λx. 2 * x))"
by (rule vector_variation_cong[OF eq1])
also have "… = vector_variation {2*0+0..2*(1/2)+0} g1"
using vector_variation_affine_eq
by (metis (no_types, lifting) ext add.right_neutral half(1) zero_less_numeral)
also have "{2*0+(0::real)..2*(1/2)+0} = {0..1}" by auto
finally show ?thesis unfolding path_length_def .
qed
have vv2: "vector_variation {1/2..1} (g1 +++ g2) = path_length g2"
proof -
have "vector_variation {1/2..1} (g1 +++ g2) =
vector_variation {1/2..1} (g2 ∘ (λx. 2 * x + (-1)))"
by (rule vector_variation_cong[OF eq2])
also have "… = vector_variation {2*(1/2)+(-1)..2*1+(-1)} g2"
by (rule vector_variation_affine_eq) auto
also have "{2*(1/2)+(-1::real)..2*1+(-1)} = {0..1}" by auto
finally show ?thesis unfolding path_length_def .
qed
show ?thesis
unfolding path_length_def
using vector_variation_combine[OF bvj, of "1/2"] half vv1 vv2
unfolding path_length_def
by auto
qed
section ‹Shiftpath›
lemma rectifiable_path_shiftpath:
assumes "rectifiable_path g"
and "pathfinish g = pathstart g"
and "t ∈ {0..1}"
shows "rectifiable_path (shiftpath t g)"
proof -
note rg = assms(1) and loop = assms(2) and t01 = assms(3)
from rg have pg: "path g" and bvg: "has_bounded_variation_on g {0..1}"
unfolding rectifiable_path_def by auto
from t01 have t0: "0 ≤ t" and t1: "t ≤ 1" and mt: "0 ≤ 1 - t" and mt1: "1 - t ≤ 1" by auto
have eq1: "shiftpath t g x = (g ∘ (λx. 1 * x + t)) x" if "x ∈ {0..1-t}" for x
by (metis add.commute atLeastAtMost_iff comp_def mult_1 shiftpath_alt_def that)
have eq2: "shiftpath t g x = (g ∘ (λx. 1 * x + (t - 1))) x" if "x ∈ {1-t..1}" for x
proof -
from that have "x = 1-t ∨ x > 1-t" by auto
then show ?thesis
proof
assume "x = 1-t"
then show ?thesis
using loop t1 by (simp add: shiftpath_def pathfinish_def pathstart_def)
next
assume "x > 1-t"
then have "t + x > 1" by auto
then show ?thesis
by (simp add: add.commute add_diff_eq shiftpath_def)
qed
qed
have bv1: "has_bounded_variation_on (shiftpath t g) {0..1-t}"
proof -
have "has_bounded_variation_on (shiftpath t g) {0..1-t} ⟷
has_bounded_variation_on (g ∘ (λx. 1 * x + t)) {0..1-t}"
by (rule has_bounded_variation_on_cong[OF eq1])
also have "… ⟷ has_bounded_variation_on g {1*0+t..1*(1-t)+t}"
using has_bounded_variation_on_affine_iff mt zero_less_one by blast
also have "{1*0+t..1*(1-t)+t} = {t..1::real}" by auto
finally show ?thesis
using has_bounded_variation_on_subset[OF bvg, of "{t..1}"] t0 t1 by auto
qed
have bv2: "has_bounded_variation_on (shiftpath t g) {1-t..1}"
proof -
have "has_bounded_variation_on (shiftpath t g) {1-t..1} ⟷
has_bounded_variation_on (g ∘ (λx. 1 * x + (t - 1))) {1-t..1}"
by (rule has_bounded_variation_on_cong[OF eq2])
also have "… ⟷ has_bounded_variation_on g {1*(1-t)+(t-1)..1*1+(t-1)}"
using has_bounded_variation_on_affine_iff mt1 zero_less_one by blast
also have "{1*(1-t)+(t-1)..1*1+(t-1)} = {0..t::real}" by auto
finally show ?thesis
using has_bounded_variation_on_subset[OF bvg, of "{0..t}"] t0 t1 by auto
qed
have "has_bounded_variation_on (shiftpath t g) {0..1}"
using has_bounded_variation_on_combine[of 0 "1-t" 1 "shiftpath t g"] mt mt1 bv1 bv2 by auto
then show "rectifiable_path (shiftpath t g)"
unfolding rectifiable_path_def
using path_shiftpath[OF pg loop t01] by auto
qed
lemma path_length_shiftpath:
assumes rg: "rectifiable_path g"
and loop: "pathfinish g = pathstart g"
and t01: "t ∈ {0..1}"
shows "path_length (shiftpath t g) = path_length g"
proof -
from rg have bvg: "has_bounded_variation_on g {0..1}"
unfolding rectifiable_path_def by auto
have bvs: "has_bounded_variation_on (shiftpath t g) {0..1}"
using rectifiable_path_shiftpath[OF rg loop t01]
unfolding rectifiable_path_def by auto
from t01 have t0: "0 ≤ t" and t1: "t ≤ 1" and mt: "0 ≤ 1 - t" and mt1: "1 - t ≤ 1" by auto
have eq1: "shiftpath t g x = (g ∘ (λx. 1 * x + t)) x" if "x ∈ {0..1-t}" for x
using that t1 by (auto simp: shiftpath_def algebra_simps)
have eq2: "shiftpath t g x = (g ∘ (λx. 1 * x + (t - 1))) x" if "x ∈ {1-t..1}" for x
using that loop t1 by (auto simp add: shiftpath_def pathfinish_def pathstart_def algebra_simps)
have vv1: "vector_variation {0..1-t} (shiftpath t g) = vector_variation {t..1} g"
proof -
have "vector_variation {0..1-t} (shiftpath t g) =
vector_variation {0..1-t} (g ∘ (λx. 1 * x + t))"
by (rule vector_variation_cong[OF eq1])
also have "… = vector_variation {1*0+t..1*(1-t)+t} g"
by (rule vector_variation_affine_eq) (use t1 in auto)
also have "{1*0+t..1*(1-t)+t} = {t..1::real}" by auto
finally show ?thesis .
qed
have vv2: "vector_variation {1-t..1} (shiftpath t g) = vector_variation {0..t} g"
proof -
have "vector_variation {1-t..1} (shiftpath t g) =
vector_variation {1-t..1} (g ∘ (λx. 1 * x + (t - 1)))"
by (rule vector_variation_cong[OF eq2])
also have "… = vector_variation {1*(1-t)+(t-1)..1*1+(t-1)} g"
by (rule vector_variation_affine_eq) (use t0 in auto)
also have "{1*(1-t)+(t-1)..1*1+(t-1)} = {0..t::real}" by auto
finally show ?thesis .
qed
have "path_length (shiftpath t g) = vector_variation {0..1} (shiftpath t g)"
unfolding path_length_def ..
also have "… = vector_variation {0..1-t} (shiftpath t g) +
vector_variation {1-t..1} (shiftpath t g)"
using vector_variation_combine[OF bvs, of "1-t"] mt mt1 by auto
also have "… = vector_variation {t..1} g + vector_variation {0..t} g"
using vv1 vv2 by simp
also have "… = vector_variation {0..t} g + vector_variation {t..1} g"
by (rule add.commute)
also have "… = vector_variation {0..1} g"
using vector_variation_combine[OF bvg, of t] t01 by auto
also have "… = path_length g"
unfolding path_length_def ..
finally show "path_length (shiftpath t g) = path_length g" .
qed
section ‹Lipschitz and distance bounds›
lemma lipschitz_imp_rectifiable_path:
assumes "⋀x y. x ∈ {0..1} ⟹ y ∈ {0..1} ⟹
norm (g x - g y) ≤ B * norm (x - y)"
shows "rectifiable_path g"
unfolding rectifiable_path_def
proof
show "path g"
unfolding path_def
proof (rule continuous_onI)
fix x e :: real assume "x ∈ {0..1}" "e > 0"
define d where "d = (if B ≤ 0 then 1 else e / B)"
have "d > 0" using ‹e > 0› unfolding d_def by (auto simp: field_simps)
moreover have "⋀x'. x' ∈ {0..1} ⟹ dist x' x < d ⟹ dist (g x') (g x) < e"
proof -
fix x' assume "x' ∈ {0..1}" "dist x' x < d"
have "dist (g x') (g x) = norm (g x' - g x)" by (simp add: dist_norm)
also have "… ≤ B * norm (x' - x)" using assms[OF ‹x' ∈ {0..1}› ‹x ∈ {0..1}›] .
also have "… ≤ B * dist x' x" by (simp add: dist_norm)
also have "… < e"
proof (cases "B ≤ 0")
case True
then have "B * dist x' x ≤ 0" by (simp add: mult_nonpos_nonneg)
also have "0 < e" using ‹e > 0› .
finally show ?thesis .
next
case False
then have "B > 0" by auto
then have "B * dist x' x < B * d"
using ‹dist x' x < d› by auto
also have "… = e" using ‹B > 0› unfolding d_def by auto
finally show ?thesis .
qed
finally show "dist (g x') (g x) < e" .
qed
ultimately show "∃d>0. ∀x'∈{0..1}. dist x' x < d ⟶ dist (g x') (g x) ≤ e"
using less_le_not_le by blast
qed
next
show "has_bounded_variation_on g {0..1}"
using Lipschitz_imp_has_bounded_variation[of "{0..1}" g B] assms
by auto
qed
lemma path_length_lipschitz:
assumes "⋀x y. x ∈ {0..1} ⟹ y ∈ {0..1} ⟹ norm (g x - g y) ≤ B * norm (x - y)"
shows "path_length g ≤ B"
unfolding path_length_def
proof (rule has_bounded_variation_works(2)[OF Lipschitz_imp_has_bounded_variation[of "{0..1}" g B]])
show "bounded {0..1::real}" by simp
show "⋀x y. x ∈ {0..1} ⟹ y ∈ {0..1} ⟹ norm (g x - g y) ≤ B * norm (x - y)"
using assms by auto
next
fix d t assume dt: "d division_of t" "t ⊆ {(0::real)..1}"
have ‹B ≥ 0›
using assms [of 0 1] norm_ge_zero by (fastforce elim: order_trans)
have "(∑k∈d. norm (g (Sup k) - g (Inf k))) ≤ (∑k∈d. B * content k)"
proof (rule sum_mono)
fix k assume kd: "k ∈ d"
from division_ofD(2,3,4)[OF dt(1) kd] obtain l u where
k_eq: "k = cbox l u" and ksub: "k ⊆ t" and kne: "k ≠ {}" by auto
then have lu: "l ≤ u" by fastforce
obtain ls: "l ∈ {0..1}" and us: "u ∈ {0..1}"
using ksub dt(2) lu k_eq cbox_interval atLeastAtMost_iff by blast
have "norm (g (Sup k) - g (Inf k)) = norm (g u - g l)"
using lu k_eq by (simp add: cbox_interval)
also have "… ≤ B * norm (u - l)"
using assms[OF us ls] by (simp add: norm_minus_commute)
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 (g (Sup k) - g (Inf k)) ≤ B * content k" .
qed
also have "… = B * (∑k∈d. content k)" by (simp add: sum_distrib_left)
also have "… ≤ B * 1"
proof (intro mult_left_mono ‹B≥0›)
have "(∑k∈d. content k) ≤ content {0..1::real}"
using subadditive_content_division[OF dt(1)] dt(2) by force
then show "(∑k∈d. content k) ≤ 1" by simp
qed
finally show "(∑k∈d. norm (g (Sup k) - g (Inf k))) ≤ B" by simp
qed
lemma dist_points_le_path_length:
"⟦rectifiable_path g; a ∈ {0..1}; b ∈ {0..1}⟧ ⟹
dist (g a) (g b) ≤ path_length g"
unfolding rectifiable_path_def path_length_def dist_norm
using vector_variation_ge_norm_function by blast
lemma dist_endpoints_le_path_length:
"rectifiable_path g ⟹ dist (pathstart g) (pathfinish g) ≤ path_length g"
using dist_points_le_path_length[of g 0 1]
by (simp add: pathstart_def pathfinish_def)
lemma path_length_eq_line_segment:
assumes rect: "rectifiable_path g"
and len: "path_length g = dist (pathstart g) (pathfinish g)"
shows "path_image g = closed_segment (pathstart g) (pathfinish g)"
proof (rule equalityI)
have pg: "path g" and bv: "has_bounded_variation_on g {0..1}"
using rect unfolding rectifiable_path_def by auto
have vv_eq: "vector_variation {0..1} g = norm (g 1 - g 0)"
using len unfolding path_length_def pathstart_def pathfinish_def dist_norm
by (simp add: norm_minus_commute)
show sub: "path_image g ⊆ closed_segment (pathstart g) (pathfinish g)"
proof
fix x assume "x ∈ path_image g"
then obtain t where t: "t ∈ {0..1}" "x = g t"
unfolding path_image_def by auto
have t01: "0 ≤ t" "t ≤ 1" using t(1) by auto
have bv_0t: "has_bounded_variation_on g {0..t}"
using has_bounded_variation_on_subset[OF bv] t(1) by auto
have bv_t1: "has_bounded_variation_on g {t..1}"
using has_bounded_variation_on_subset[OF bv] t(1) by auto
have n1: "norm (g t - g 0) ≤ vector_variation {0..t} g"
using vector_variation_ge_norm_function[OF bv_0t] t01 by auto
have n2: "norm (g 1 - g t) ≤ vector_variation {t..1} g"
using vector_variation_ge_norm_function[OF bv_t1] t01 by auto
have split: "vector_variation {0..t} g + vector_variation {t..1} g =
vector_variation {0..1} g"
using vector_variation_combine[OF bv] t(1) by auto
have tri: "norm (g 1 - g 0) ≤ norm (g t - g 0) + norm (g 1 - g t)"
using norm_triangle_ineq[of "g t - g 0" "g 1 - g t"] by simp
have "norm (g t - g 0) + norm (g 1 - g t) = norm (g 1 - g 0)"
using n1 n2 split vv_eq tri by linarith
then have "dist (g 0) (g 1) = dist (g 0) (g t) + dist (g t) (g 1)"
by (simp add: dist_norm norm_minus_commute)
then have "between (g 0, g 1) (g t)"
unfolding between by simp
then show "x ∈ closed_segment (pathstart g) (pathfinish g)"
unfolding t(2) pathstart_def pathfinish_def between_mem_segment by simp
qed
show "closed_segment (pathstart g) (pathfinish g) ⊆ path_image g"
proof -
have ne: "path_image g ≠ {}"
unfolding path_image_def by auto
have compact: "compact (path_image g)"
using compact_path_image[OF pg] .
have conn: "connected (path_image g)"
using connected_path_image[OF pg] .
have col: "collinear (path_image g)"
proof -
from sub have "path_image g ⊆ closed_segment (pathstart g) (pathfinish g)" .
moreover have "collinear (closed_segment (pathstart g) (pathfinish g))"
by (rule collinear_closed_segment)
ultimately show ?thesis
unfolding collinear_def by (meson subsetD)
qed
obtain p q where pq: "path_image g = closed_segment p q"
using compact_convex_collinear_segment_alt[OF ne compact conn col] by auto
have "pathstart g ∈ path_image g"
unfolding path_image_def pathstart_def by auto
moreover have "pathfinish g ∈ path_image g"
unfolding path_image_def pathfinish_def by auto
ultimately have "pathstart g ∈ closed_segment p q" "pathfinish g ∈ closed_segment p q"
using pq by auto
then have "closed_segment (pathstart g) (pathfinish g) ⊆ closed_segment p q"
using subset_closed_segment by blast
then show ?thesis using pq by simp
qed
qed
section ‹Linepath›
lemma rectifiable_path_linepath:
"rectifiable_path (linepath a b)"
proof (rule lipschitz_imp_rectifiable_path[where B="dist a b"])
fix x y :: real assume "x ∈ {0..1}" "y ∈ {0..1}"
have "linepath a b x - linepath a b y = (x - y) *⇩R (b - a)"
by (simp add: linepath_def algebra_simps)
then have "norm (linepath a b x - linepath a b y) = ¦x - y¦ * norm (b - a)"
by simp
also have "… = norm (b - a) * norm (x - y)"
by (simp add: abs_real_def real_norm_def mult.commute)
also have "… = dist a b * norm (x - y)"
by (simp add: dist_norm norm_minus_commute)
finally show "norm (linepath a b x - linepath a b y) ≤ dist a b * norm (x - y)"
by simp
qed
lemma path_length_linepath:
"path_length (linepath a b) = dist a b"
proof (rule antisym)
show "path_length (linepath a b) ≤ dist a b"
proof (rule path_length_lipschitz)
fix x y :: real assume "x ∈ {0..1}" "y ∈ {0..1}"
have "linepath a b x - linepath a b y = (x - y) *⇩R (b - a)"
by (simp add: linepath_def algebra_simps)
then have "norm (linepath a b x - linepath a b y) = ¦x - y¦ * norm (b - a)"
by simp
also have "… = dist a b * norm (x - y)"
by (simp add: dist_norm norm_minus_commute abs_real_def real_norm_def mult.commute)
finally show "norm (linepath a b x - linepath a b y) ≤ dist a b * norm (x - y)"
by simp
qed
next
have "dist a b = dist (pathstart (linepath a b)) (pathfinish (linepath a b))"
by (simp add: pathstart_def pathfinish_def linepath_def dist_norm)
also have "… ≤ path_length (linepath a b)"
by (rule dist_endpoints_le_path_length[OF rectifiable_path_linepath])
finally show "dist a b ≤ path_length (linepath a b)" .
qed
section ‹Rectifiable path image bound›
lemma rectifiable_path_image_subset_cball:
assumes "rectifiable_path g"
shows "path_image g ⊆ cball (pathstart g) (path_length g)"
proof
fix x assume "x ∈ path_image g"
then obtain t where t: "t ∈ {0..1}" "x = g t"
unfolding path_image_def by auto
have "dist (pathstart g) x = dist (g 0) (g t)"
by (simp add: t(2) pathstart_def)
also have "… ≤ path_length g"
using dist_points_le_path_length[OF assms _ t(1)] by simp
finally show "x ∈ cball (pathstart g) (path_length g)"
by (simp add: mem_cball)
qed
end