ReleaseRectifiable.lean

1 import KomorebiVerification.PaperII.ReleaseAnalyticContour
2 import Mathlib.Analysis.ConstantSpeed
3 import Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
4 
5 /-! # Concrete integral representations of rectifiable curves
6 The first bridge constructs velocities from derivatives of the real and
7 imaginary coordinates of an absolutely continuous complex path. No supplied
8 integral representation is assumed. -/
9 
10 set_option autoImplicit false
11 noncomputable section
12 
13 namespace Komorebi.PaperII.ReleaseRectifiable
14 
15 open MeasureTheory Set
16 open scoped Topology
17 open Komorebi.PaperII.ReleaseAnalyticContour
18 
19 /-- Canonical complex velocity obtained from the two real coordinate derivatives. -/
20 def coordinateVelocity (f : ℝ → ℂ) (x : ℝ) : ℂ :=
21   Complex.ofReal (deriv (fun t ↦ (f t).re) x) + Complex.ofReal (deriv (fun t ↦ (f t).im) x) * Complex.I
22 
23 theorem ac_re {f : ℝ → ℂ} {a b : ℝ}
24     (hf : AbsolutelyContinuousOnInterval f a b) :
25     AbsolutelyContinuousOnInterval (fun t ↦ (f t).re) a b :=
26   Complex.reCLM.lipschitzWith.comp_absolutelyContinuousOnInterval hf
27 
28 theorem ac_im {f : ℝ → ℂ} {a b : ℝ}
29     (hf : AbsolutelyContinuousOnInterval f a b) :
30     AbsolutelyContinuousOnInterval (fun t ↦ (f t).im) a b :=
31   Complex.imCLM.lipschitzWith.comp_absolutelyContinuousOnInterval hf
32 
33 theorem integrable_coordinateVelocity {f : ℝ → ℂ} {a b : ℝ}
34     (hf : AbsolutelyContinuousOnInterval f a b) :
35     IntervalIntegrable (coordinateVelocity f) volume a b := by
36   have hr := (ac_re hf).intervalIntegrable_deriv
37   have hi := (ac_im hf).intervalIntegrable_deriv
38   have hr' : IntervalIntegrable (fun x ↦ Complex.ofReal (deriv (fun t ↦ (f t).re) x)) volume a b :=
39     ⟨Complex.ofRealCLM.integrable_comp hr.1, Complex.ofRealCLM.integrable_comp hr.2⟩
40   have hi' : IntervalIntegrable (fun x ↦ Complex.ofReal (deriv (fun t ↦ (f t).im) x)) volume a b :=
41     ⟨Complex.ofRealCLM.integrable_comp hi.1, Complex.ofRealCLM.integrable_comp hi.2⟩
42   exact hr'.add (hi'.mul_const Complex.I)
43 
44 /-- The real-valued absolutely-continuous FTC yields the full complex FTC. -/
45 theorem integral_coordinateVelocity {f : ℝ → ℂ} {a b : ℝ}
46     (hf : AbsolutelyContinuousOnInterval f a b) :
47     (∫ x : ℝ in a..b, coordinateVelocity f x) = f b - f a := by
48   have hr := (ac_re hf).intervalIntegrable_deriv
49   have hi := (ac_im hf).intervalIntegrable_deriv
50   have hr' : IntervalIntegrable (fun x ↦ Complex.ofReal (deriv (fun t ↦ (f t).re) x)) volume a b :=
51     ⟨Complex.ofRealCLM.integrable_comp hr.1, Complex.ofRealCLM.integrable_comp hr.2⟩
52   have hi' : IntervalIntegrable (fun x ↦ Complex.ofReal (deriv (fun t ↦ (f t).im) x)) volume a b :=
53     ⟨Complex.ofRealCLM.integrable_comp hi.1, Complex.ofRealCLM.integrable_comp hi.2⟩
54   unfold coordinateVelocity
55   rw [intervalIntegral.integral_add hr' (hi'.mul_const Complex.I),
56     intervalIntegral.integral_mul_const, intervalIntegral.integral_ofReal,
57     intervalIntegral.integral_ofReal, (ac_re hf).integral_deriv_eq_sub,
58     (ac_im hf).integral_deriv_eq_sub]
59   apply Complex.ext <;> simp
60 
61 /-- Construct the actual IntegralCycle from an arbitrary finite family of
62 closed absolutely continuous paths. -/
63 def cycleOfAbsolutelyContinuous (n : ℕ) (f : Fin n → ℝ → ℂ)
64     (hf : ∀ i, AbsolutelyContinuousOnInterval (f i) 0 1)
65     (hclosed : ∀ i, f i 1 = f i 0) : IntegralCycle where
66   count := n
67   base := fun i ↦ f i 0
68   velocity := fun i ↦ coordinateVelocity (f i)
69   velocity_integrable i := integrable_coordinateVelocity (hf i)
70   closed i := by rw [integral_coordinateVelocity (hf i), hclosed, sub_self]
71 
72 /-- The constructed curve agrees pointwise with the original path throughout
73 the whole closed parameter interval. -/
74 theorem curve_cycleOfAbsolutelyContinuous (n : ℕ) (f : Fin n → ℝ → ℂ)
75     (hf : ∀ i, AbsolutelyContinuousOnInterval (f i) 0 1)
76     (hclosed : ∀ i, f i 1 = f i 0) (i : Fin n) (s : ℝ) (hs : s ∈ uIcc (0:ℝ) 1) :
77     (cycleOfAbsolutelyContinuous n f hf hclosed).curve i s = f i s := by
78   change f i 0 + (∫ r : ℝ in 0..s, coordinateVelocity (f i) r) = f i s
79   rw [integral_coordinateVelocity ((hf i).mono (uIcc_subset_uIcc_left hs))]
80   abel
81 
82 /-- In particular every finite family of closed Lipschitz paths has a
83 constructed integrable-velocity representation, not an assumed certificate. -/
84 def cycleOfLipschitz (n : ℕ) (f : Fin n → ℝ → ℂ) (K : Fin n → NNReal)
85     (hf : ∀ i, LipschitzOnWith (K i) (f i) (uIcc (0:ℝ) 1))
86     (hclosed : ∀ i, f i 1 = f i 0) : IntegralCycle :=
87   cycleOfAbsolutelyContinuous n f (fun i ↦ (hf i).absolutelyContinuousOnInterval) hclosed
88 
89 theorem curve_cycleOfLipschitz (n : ℕ) (f : Fin n → ℝ → ℂ) (K : Fin n → NNReal)
90     (hf : ∀ i, LipschitzOnWith (K i) (f i) (uIcc (0:ℝ) 1))
91     (hclosed : ∀ i, f i 1 = f i 0) (i : Fin n) (s : ℝ) (hs : s ∈ uIcc (0:ℝ) 1) :
92     (cycleOfLipschitz n f K hf hclosed).curve i s = f i s :=
93   curve_cycleOfAbsolutelyContinuous n f _ hclosed i s hs
94 
95 end Komorebi.PaperII.ReleaseRectifiable

Back to source controls