ReleaseArcLength.lean

1 import Mathlib.Analysis.ConstantSpeed
2 import Mathlib.Analysis.Complex.Basic
3 import Mathlib.Topology.MetricSpace.Lipschitz
4 import Mathlib.Topology.Order.IntermediateValue
5 
6 /-! # Arclength parameterization of continuous rectifiable complex paths
7 This constructs a Lipschitz path on the unit interval from bounded variation,
8 with exact recovery through the monotone cumulative-length map. -/
9 
10 set_option autoImplicit false
11 noncomputable section
12 namespace Komorebi.PaperII.ReleaseArcLength
13 open Set
14 open scoped NNReal ENNReal
15 
16 /-- Unit metric speed controls distances, including noninjective paths. -/
17 theorem unitSpeed_lipschitz {g : ℝ → ℂ} {s : Set ℝ}
18     (hg : HasUnitSpeedOn g s) : LipschitzOnWith 1 g s := by
19   apply LipschitzOnWith.of_dist_le_mul
20   intro x hx y hy
21   rcases le_total x y with hxy | hyx
22   · have hb := hg.hasLocallyBoundedVariationOn x y hx hy
23     have hd := hb.dist_le (show x ∈ s ∩ Icc x y from ⟨hx, le_rfl, hxy⟩)
24       (show y ∈ s ∩ Icc x y from ⟨hy, hxy, le_rfl⟩)
25     rw [hg hx hy] at hd
26     simpa only [NNReal.coe_one, one_mul, ENNReal.toReal_ofReal (sub_nonneg.mpr hxy),
27       Real.dist_eq, abs_of_nonpos (sub_nonpos.mpr hxy), neg_sub] using hd
28   · have hb := hg.hasLocallyBoundedVariationOn y x hy hx
29     have hd := hb.dist_le (show y ∈ s ∩ Icc y x from ⟨hy, le_rfl, hyx⟩)
30       (show x ∈ s ∩ Icc y x from ⟨hx, hyx, le_rfl⟩)
31     rw [hg hy hx] at hd
32     simpa only [NNReal.coe_one, one_mul, ENNReal.toReal_ofReal (sub_nonneg.mpr hyx),
33       Real.dist_eq, abs_of_nonneg (sub_nonneg.mpr hyx), dist_comm] using hd
34 
35 def geometricLength (f : ℝ → ℂ) : ℝ := (eVariationOn f (Icc (0:ℝ) 1)).toReal
36 
37 def arcMap (f : ℝ → ℂ) : ℝ → ℝ := variationOnFromTo f (Icc 0 1) 0
38 
39 def arcPath (f : ℝ → ℂ) : ℝ → ℂ := naturalParameterization f (Icc 0 1) 0
40 
41 def unitIntervalPath (f : ℝ → ℂ) (s : ℝ) : ℂ := arcPath f (geometricLength f * s)
42 
43 @[simp] theorem arcMap_zero (f : ℝ → ℂ) : arcMap f 0 = 0 := by
44   simp only [arcMap, variationOnFromTo.self]
45 
46 @[simp] theorem arcMap_one (f : ℝ → ℂ) : arcMap f 1 = geometricLength f := by
47   rw [arcMap, variationOnFromTo.eq_of_le f (Icc 0 1) (by norm_num : (0:ℝ) ≤ 1)]
48   simp only [inter_self, geometricLength]
49 
50 theorem arcMap_monotone {f : ℝ → ℂ} (hf : BoundedVariationOn f (Icc (0:ℝ) 1)) :
51     MonotoneOn (arcMap f) (Icc (0:ℝ) 1) :=
52   variationOnFromTo.monotoneOn hf.locallyBoundedVariationOn (by norm_num)
53 
54 theorem arcMap_continuous {f : ℝ → ℂ} (hf : BoundedVariationOn f (Icc (0:ℝ) 1))
55     (hc : ContinuousOn f (Icc (0:ℝ) 1)) : ContinuousOn (arcMap f) (Icc (0:ℝ) 1) := by
56   intro x hx
57   exact (hf.continuousWithinAt_variationOnFromTo_iff (by norm_num) hx).mpr (hc x hx)
58 
59 theorem arcMap_image {f : ℝ → ℂ} (hf : BoundedVariationOn f (Icc (0:ℝ) 1))
60     (hc : ContinuousOn f (Icc (0:ℝ) 1)) :
61     arcMap f '' Icc (0:ℝ) 1 = Icc 0 (geometricLength f) := by
62   simpa only [arcMap_zero, arcMap_one] using
63     (arcMap_continuous hf hc).image_Icc_of_monotoneOn (by norm_num) (arcMap_monotone hf)
64 
65 /-- Reconstruction is pointwise equality in the genuine metric complex plane. -/
66 theorem arcPath_recovers {f : ℝ → ℂ} (hf : BoundedVariationOn f (Icc (0:ℝ) 1))
67     (s : ℝ) (hs : s ∈ Icc (0:ℝ) 1) : arcPath f (arcMap f s) = f s := by
68   exact edist_eq_zero.mp
69     (edist_naturalParameterization_eq_zero hf.locallyBoundedVariationOn (by norm_num) hs)
70 
71 theorem arcPath_unitSpeed {f : ℝ → ℂ} (hf : BoundedVariationOn f (Icc (0:ℝ) 1))
72     (hc : ContinuousOn f (Icc (0:ℝ) 1)) :
73     HasUnitSpeedOn (arcPath f) (Icc 0 (geometricLength f)) := by
74   have h := has_unit_speed_naturalParameterization f hf.locallyBoundedVariationOn
75     (show (0:ℝ) ∈ Icc (0:ℝ) 1 by norm_num)
76   change HasUnitSpeedOn (arcPath f) (arcMap f '' Icc (0:ℝ) 1) at h
77   rwa [arcMap_image hf hc] at h
78 
79 theorem scale_image (L : ℝ) (hL : 0 ≤ L) :
80     (fun s : ℝ ↦ L * s) '' Icc (0:ℝ) 1 = Icc 0 L := by
81   have hm : MonotoneOn (fun s : ℝ ↦ L * s) (Icc (0:ℝ) 1) :=
82     fun _ _ _ _ hxy ↦ mul_le_mul_of_nonneg_left hxy hL
83   have hc : Continuous (fun s : ℝ ↦ L * s) := continuous_const.mul continuous_id
84   simpa only [mul_zero, mul_one] using
85     hc.continuousOn.image_Icc_of_monotoneOn (by norm_num : (0:ℝ) ≤ 1) hm
86 
87 theorem unitIntervalPath_lipschitz {f : ℝ → ℂ} (hf : BoundedVariationOn f (Icc (0:ℝ) 1))
88     (hc : ContinuousOn f (Icc (0:ℝ) 1)) :
89     LipschitzOnWith ⟨geometricLength f, ENNReal.toReal_nonneg⟩
90       (unitIntervalPath f) (Icc (0:ℝ) 1) := by
91   have hg := unitSpeed_lipschitz (arcPath_unitSpeed hf hc)
92   have hmap : MapsTo (fun s : ℝ ↦ geometricLength f * s) (Icc (0:ℝ) 1)
93       (Icc 0 (geometricLength f)) := by
94     intro s hs
95     rw [← scale_image (geometricLength f) ENNReal.toReal_nonneg]
96     exact mem_image_of_mem _ hs
97   apply LipschitzOnWith.of_dist_le_mul
98   intro x hx y hy
99   calc
100     dist (unitIntervalPath f x) (unitIntervalPath f y) ≤
101         dist (geometricLength f * x) (geometricLength f * y) := by
102       simpa only [NNReal.coe_one, one_mul, unitIntervalPath] using
103         hg.dist_le_mul _ (hmap hx) _ (hmap hy)
104     _ = geometricLength f * dist x y := by
105       rw [dist_eq_norm, ← mul_sub, norm_mul, Real.norm_of_nonneg (show 0 ≤ geometricLength f from ENNReal.toReal_nonneg),
106         dist_eq_norm]
107 
108 @[simp] theorem unitIntervalPath_zero {f : ℝ → ℂ}
109     (hf : BoundedVariationOn f (Icc (0:ℝ) 1)) : unitIntervalPath f 0 = f 0 := by
110   simpa only [unitIntervalPath, mul_zero, arcMap_zero] using arcPath_recovers hf 0 (by norm_num)
111 
112 @[simp] theorem unitIntervalPath_one {f : ℝ → ℂ}
113     (hf : BoundedVariationOn f (Icc (0:ℝ) 1)) : unitIntervalPath f 1 = f 1 := by
114   simpa only [unitIntervalPath, mul_one, arcMap_one] using arcPath_recovers hf 1 (by norm_num)
115 
116 theorem unitIntervalPath_closed {f : ℝ → ℂ} (hf : BoundedVariationOn f (Icc (0:ℝ) 1))
117     (hclosed : f 1 = f 0) : unitIntervalPath f 1 = unitIntervalPath f 0 := by
118   rw [unitIntervalPath_one hf, unitIntervalPath_zero hf, hclosed]
119 
120 /-- The arclength construction preserves the trace, even when length is zero. -/
121 theorem unitIntervalPath_image {f : ℝ → ℂ} (hf : BoundedVariationOn f (Icc (0:ℝ) 1))
122     (hc : ContinuousOn f (Icc (0:ℝ) 1)) :
123     unitIntervalPath f '' Icc (0:ℝ) 1 = f '' Icc (0:ℝ) 1 := by
124   have hcomp : (arcPath f ∘ arcMap f) '' Icc (0:ℝ) 1 = f '' Icc (0:ℝ) 1 := by
125     apply image_congr
126     intro s hs
127     exact arcPath_recovers hf s hs
128   rw [image_comp, arcMap_image hf hc] at hcomp
129   change (arcPath f ∘ (fun s : ℝ ↦ geometricLength f * s)) '' Icc (0:ℝ) 1 = _
130   rw [image_comp, scale_image (geometricLength f) (show 0 ≤ geometricLength f from ENNReal.toReal_nonneg)]
131   exact hcomp
132 
133 /-- Total geometric variation is preserved by the constructed reparameterization. -/
134 theorem unitIntervalPath_variation {f : ℝ → ℂ} (hf : BoundedVariationOn f (Icc (0:ℝ) 1))
135     (hc : ContinuousOn f (Icc (0:ℝ) 1)) :
136     eVariationOn (unitIntervalPath f) (Icc (0:ℝ) 1) = eVariationOn f (Icc (0:ℝ) 1) := by
137   have hm : MonotoneOn (fun s : ℝ ↦ geometricLength f * s) (Icc (0:ℝ) 1) :=
138     fun _ _ _ _ hxy ↦ mul_le_mul_of_nonneg_left hxy ENNReal.toReal_nonneg
139   change eVariationOn (arcPath f ∘ (fun s : ℝ ↦ geometricLength f * s)) (Icc (0:ℝ) 1) = _
140   rw [eVariationOn.comp_eq_of_monotoneOn _ _ hm, scale_image (geometricLength f) (show 0 ≤ geometricLength f from ENNReal.toReal_nonneg)]
141   have hu := arcPath_unitSpeed hf hc
142   have hvar := hu (show (0:ℝ) ∈ Icc 0 (geometricLength f) from ⟨le_rfl, ENNReal.toReal_nonneg⟩)
143     (show geometricLength f ∈ Icc 0 (geometricLength f) from ⟨ENNReal.toReal_nonneg, le_rfl⟩)
144   simpa only [inter_self, NNReal.coe_one, one_mul, sub_zero,
145     geometricLength, ENNReal.ofReal_toReal hf] using hvar
146 
147 end Komorebi.PaperII.ReleaseArcLength

Back to source controls