ReleaseRectifiableCycle.lean

1 import KomorebiVerification.PaperII.ReleaseRectifiable
2 import KomorebiVerification.PaperII.ReleaseArcLength
3 
4 /-! # Constructed integral cycles from continuous rectifiable closed curves
5 The geometric total variation and trace are preserved by the construction.
6 Identification of integral-norm velocity length with geometric total variation,
7 and invariance of classical contour integrals, are separate obligations. -/
8 
9 set_option autoImplicit false
10 noncomputable section
11 namespace Komorebi.PaperII.ReleaseRectifiableCycle
12 open Set
13 open Komorebi.PaperII.ReleaseAnalyticContour
14 open Komorebi.PaperII.ReleaseRectifiable
15 open Komorebi.PaperII.ReleaseArcLength
16 
17 /-- A finite family of genuinely continuous bounded-variation closed paths
18 produces an integral cycle by arclength and coordinatewise differentiation. -/
19 def cycleOfRectifiable (n : ℕ) (f : Fin n → ℝ → ℂ)
20     (hv : ∀ i, BoundedVariationOn (f i) (Icc (0:ℝ) 1))
21     (hc : ∀ i, ContinuousOn (f i) (Icc (0:ℝ) 1))
22     (hclosed : ∀ i, f i 1 = f i 0) : IntegralCycle :=
23   cycleOfLipschitz n (fun i ↦ unitIntervalPath (f i))
24     (fun i ↦ ⟨geometricLength (f i), ENNReal.toReal_nonneg⟩)
25     (fun i ↦ by simpa only [uIcc_of_le (by norm_num : (0:ℝ) ≤ 1)] using
26       unitIntervalPath_lipschitz (hv i) (hc i))
27     (fun i ↦ unitIntervalPath_closed (hv i) (hclosed i))
28 
29 theorem curve_cycleOfRectifiable (n : ℕ) (f : Fin n → ℝ → ℂ)
30     (hv : ∀ i, BoundedVariationOn (f i) (Icc (0:ℝ) 1))
31     (hc : ∀ i, ContinuousOn (f i) (Icc (0:ℝ) 1))
32     (hclosed : ∀ i, f i 1 = f i 0) (i : Fin n) (s : ℝ) (hs : s ∈ Icc (0:ℝ) 1) :
33     (cycleOfRectifiable n f hv hc hclosed).curve i s = unitIntervalPath (f i) s := by
34   apply curve_cycleOfLipschitz
35   simpa only [uIcc_of_le (by norm_num : (0:ℝ) ≤ 1)] using hs
36 
37 /-- Each curve preserves the complete geometric trace. -/
38 theorem image_curve_cycleOfRectifiable (n : ℕ) (f : Fin n → ℝ → ℂ)
39     (hv : ∀ i, BoundedVariationOn (f i) (Icc (0:ℝ) 1))
40     (hc : ∀ i, ContinuousOn (f i) (Icc (0:ℝ) 1))
41     (hclosed : ∀ i, f i 1 = f i 0) (i : Fin n) :
42     (cycleOfRectifiable n f hv hc hclosed).curve i '' Icc (0:ℝ) 1 =
43       f i '' Icc (0:ℝ) 1 := by
44   calc
45     _ = unitIntervalPath (f i) '' Icc (0:ℝ) 1 :=
46       image_congr (fun s hs ↦ curve_cycleOfRectifiable n f hv hc hclosed i s hs)
47     _ = _ := unitIntervalPath_image (hv i) (hc i)
48 
49 /-- The actual integral cycle has the union of the original traces. -/
50 theorem trace_cycleOfRectifiable (n : ℕ) (f : Fin n → ℝ → ℂ)
51     (hv : ∀ i, BoundedVariationOn (f i) (Icc (0:ℝ) 1))
52     (hc : ∀ i, ContinuousOn (f i) (Icc (0:ℝ) 1))
53     (hclosed : ∀ i, f i 1 = f i 0) :
54     (cycleOfRectifiable n f hv hc hclosed).trace =
55       {z | ∃ i : Fin n, z ∈ f i '' Icc (0:ℝ) 1} := by
56   ext z
57   change (∃ i s, s ∈ uIcc (0:ℝ) 1 ∧
58     (cycleOfRectifiable n f hv hc hclosed).curve i s = z) ↔ _
59   simp only [uIcc_of_le (by norm_num : (0:ℝ) ≤ 1)]
60   constructor
61   · rintro ⟨i,s,hs,hz⟩
62     refine ⟨i, ?_⟩
63     rw [← image_curve_cycleOfRectifiable n f hv hc hclosed i]
64     exact ⟨s,hs,hz⟩
65   · rintro ⟨i,hz⟩
66     rw [← image_curve_cycleOfRectifiable n f hv hc hclosed i] at hz
67     obtain ⟨s,hs,hz⟩ := hz
68     exact ⟨i,s,hs,hz⟩
69 
70 /-- Geometric length of every reconstructed curve, expressed as variation,
71 is exactly the original geometric length. This theorem does not identify the
72 separately defined velocity-integral length. -/
73 theorem variation_curve_cycleOfRectifiable (n : ℕ) (f : Fin n → ℝ → ℂ)
74     (hv : ∀ i, BoundedVariationOn (f i) (Icc (0:ℝ) 1))
75     (hc : ∀ i, ContinuousOn (f i) (Icc (0:ℝ) 1))
76     (hclosed : ∀ i, f i 1 = f i 0) (i : Fin n) :
77     eVariationOn ((cycleOfRectifiable n f hv hc hclosed).curve i) (Icc (0:ℝ) 1) =
78       eVariationOn (f i) (Icc (0:ℝ) 1) := by
79   calc
80     _ = eVariationOn (unitIntervalPath (f i)) (Icc (0:ℝ) 1) :=
81       eVariationOn.eq_of_eqOn (fun s hs ↦ curve_cycleOfRectifiable n f hv hc hclosed i s hs)
82     _ = _ := unitIntervalPath_variation (hv i) (hc i)
83 
84 end Komorebi.PaperII.ReleaseRectifiableCycle

Back to source controls