ReleaseRectifiableLength.lean

1 import KomorebiVerification.PaperII.ReleaseRectifiableCycle
2 import Mathlib.Analysis.Complex.RealDeriv
3 
4 /-!
5 A geometric upper bound suffices for the
6 paper's contour norm estimate, without assuming the exact length/speed theorem.
7 -/
8 
9 set_option autoImplicit false
10 noncomputable section
11 namespace Komorebi.PaperII.ReleaseRectifiableLength
12 
13 open MeasureTheory Set
14 open scoped Topology BigOperators
15 open Komorebi.PaperII.ReleaseAnalyticContour
16 open Komorebi.PaperII.ReleaseRectifiable
17 open Komorebi.PaperII.ReleaseRectifiableCycle
18 open Komorebi.PaperII.ReleaseArcLength
19 
20 /-- At a point where both real coordinates are differentiable, the coordinate
21 velocity is the genuine derivative of the complex-valued real-variable path. -/
22 theorem hasDerivAt_coordinateVelocity {f : ℝ → ℂ} {x : ℝ}
23     (hr : DifferentiableAt ℝ (fun t ↦ (f t).re) x)
24     (hi : DifferentiableAt ℝ (fun t ↦ (f t).im) x) :
25     HasDerivAt f (coordinateVelocity f x) x := by
26   have h := hr.hasDerivAt.ofReal_comp.add
27     (hi.hasDerivAt.ofReal_comp.mul_const Complex.I)
28   have heq : ((fun y : ℝ ↦ Complex.ofReal (f y).re) +
29       fun y : ℝ ↦ Complex.ofReal (f y).im * Complex.I) = f := by
30     funext y
31     exact Complex.re_add_im (f y)
32   rw [heq] at h
33   exact h
34 
35 /-- The coordinate velocity is bounded by a Lipschitz constant at each interior
36 point.  At a non-differentiability point a missing coordinate derivative is zero
37 by the definition of `deriv`; the one-coordinate bound handles these cases. -/
38 theorem norm_coordinateVelocity_le {f : ℝ → ℂ} {a b x : ℝ} {K : NNReal}
39     (hf : LipschitzOnWith K f (Icc a b)) (hx : x ∈ Ioo a b) :
40     ‖coordinateVelocity f x‖ ≤ (K : ℝ) := by
41   have hs : Icc a b ∈ nhds x := Icc_mem_nhds hx.1 hx.2
42   have hrLip : LipschitzOnWith K (fun t ↦ (f t).re) (Icc a b) := by
43     apply LipschitzOnWith.of_dist_le_mul
44     intro x hx y hy
45     calc
46       dist (f x).re (f y).re = |(f x - f y).re| := by simp [Real.dist_eq]
47       _ ≤ ‖f x - f y‖ := Complex.abs_re_le_norm _
48       _ ≤ (K : ℝ) * dist x y := by simpa only [dist_eq_norm] using hf.dist_le_mul x hx y hy
49   have hiLip : LipschitzOnWith K (fun t ↦ (f t).im) (Icc a b) := by
50     apply LipschitzOnWith.of_dist_le_mul
51     intro x hx y hy
52     calc
53       dist (f x).im (f y).im = |(f x - f y).im| := by simp [Real.dist_eq]
54       _ ≤ ‖f x - f y‖ := Complex.abs_im_le_norm _
55       _ ≤ (K : ℝ) * dist x y := by simpa only [dist_eq_norm] using hf.dist_le_mul x hx y hy
56   by_cases hr : DifferentiableAt ℝ (fun t ↦ (f t).re) x
57   · by_cases hi : DifferentiableAt ℝ (fun t ↦ (f t).im) x
58     · exact (hasDerivAt_coordinateVelocity hr hi).le_of_lipschitzOn hs hf
59     · simp only [coordinateVelocity, deriv_zero_of_not_differentiableAt hi,
60         Complex.ofReal_zero, zero_mul, add_zero, Complex.norm_real]
61       simpa only [Real.norm_eq_abs] using norm_deriv_le_of_lipschitzOn hs hrLip
62   · simp only [coordinateVelocity, deriv_zero_of_not_differentiableAt hr,
63       Complex.ofReal_zero, zero_add, norm_mul, Complex.norm_real, Complex.norm_I, mul_one]
64     simpa only [Real.norm_eq_abs] using norm_deriv_le_of_lipschitzOn hs hiLip
65 
66 /-- The actual velocity-integral length of a Lipschitz path is at most its
67 Lipschitz constant times the parameter interval's length. -/
68 theorem integral_norm_coordinateVelocity_le {f : ℝ → ℂ} {a b : ℝ} {K : NNReal}
69     (hab : a ≤ b) (hf : LipschitzOnWith K f (Icc a b)) :
70     (∫ x : ℝ in a..b, ‖coordinateVelocity f x‖) ≤ (b-a) * (K : ℝ) := by
71   have hac : AbsolutelyContinuousOnInterval f a b := by
72     apply LipschitzOnWith.absolutelyContinuousOnInterval
73     simpa only [uIcc_of_le hab] using hf
74   calc
75     _ ≤ ∫ x : ℝ in a..b, (K : ℝ) := by
76       exact intervalIntegral.integral_mono_on_of_le_Ioo hab
77         (integrable_coordinateVelocity hac).norm intervalIntegrable_const
78         (fun x hx ↦ norm_coordinateVelocity_le hf hx)
79     _ = _ := by simp
80 
81 /-- Arclength reconstruction gives exactly the upper bound needed in the
82 manuscript's length-times-suprema estimate.  No equality of the two notions of
83 length is assumed. -/
84 theorem length_cycleOfRectifiable_le (n : ℕ) (f : Fin n → ℝ → ℂ)
85     (hv : ∀ i, BoundedVariationOn (f i) (Icc (0:ℝ) 1))
86     (hc : ∀ i, ContinuousOn (f i) (Icc (0:ℝ) 1))
87     (hclosed : ∀ i, f i 1 = f i 0) :
88     (cycleOfRectifiable n f hv hc hclosed).length ≤ ∑ i : Fin n, geometricLength (f i) := by
89   apply Finset.sum_le_sum
90   intro i hi
91   change (∫ s : ℝ in (0:ℝ)..1, ‖coordinateVelocity (unitIntervalPath (f i)) s‖) ≤ _
92   have h := integral_norm_coordinateVelocity_le (by norm_num : (0:ℝ) ≤ 1)
93     (unitIntervalPath_lipschitz (hv i) (hc i))
94   change (∫ s : ℝ in (0:ℝ)..1, ‖coordinateVelocity (unitIntervalPath (f i)) s‖) ≤
95     ((1:ℝ) - 0) * geometricLength (f i) at h
96   simpa only [sub_zero, one_mul] using h
97 
98 end Komorebi.PaperII.ReleaseRectifiableLength

Back to source controls