ReleaseRectifiableRSError.lean

1 import KomorebiVerification.PaperII.ReleaseRectifiableCycle
2 
3 /-! Classical tagged Riemann–Stieltjes integration and its actual velocity representation. -/
4 set_option autoImplicit false
5 noncomputable section
6 namespace Komorebi.PaperII.ReleaseRectifiableRSError
7 
8 open MeasureTheory Set
9 open scoped Topology BigOperators
10 open Komorebi.PaperII.ReleaseRectifiable
11 
12 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
13   [NormedSpace ℝ E] [CompleteSpace E]
14 
15 /-- Exact tagged-sum error on a single interval, using the actual path velocity. -/
16 theorem tagged_increment_sub_integral {f : ℝ → ℂ} {a b τ : ℝ} {H : ℂ → E}
17     (hf : AbsolutelyContinuousOnInterval f a b)
18     (hH : ContinuousOn H (f '' uIcc a b)) :
19     (f b - f a) • H (f τ) -
20         (∫ s : ℝ in a..b, coordinateVelocity f s • H (f s)) =
21       ∫ s : ℝ in a..b, coordinateVelocity f s • (H (f τ) - H (f s)) := by
22   have hv := integrable_coordinateVelocity hf
23   have hcomp : ContinuousOn (fun s ↦ H (f s)) (uIcc a b) :=
24     hH.comp hf.continuousOn (fun s hs ↦ mem_image_of_mem _ hs)
25   have hi := hv.smul_continuousOn hcomp
26   have hc := hv.smul_continuousOn (continuousOn_const (c := H (f τ)))
27   rw [← integral_coordinateVelocity hf, ← intervalIntegral.integral_smul_const,
28     ← intervalIntegral.integral_sub hc hi]
29   apply intervalIntegral.integral_congr
30   intro s hs
31   exact (smul_sub _ _ _).symm
32 
33 /-- Oscillation times integrated speed bounds the genuine tagged-sum error. -/
34 theorem norm_tagged_increment_sub_integral_le {f : ℝ → ℂ} {a b τ ε : ℝ} {H : ℂ → E}
35     (hab : a ≤ b) (hf : AbsolutelyContinuousOnInterval f a b)
36     (hH : ContinuousOn H (f '' uIcc a b))
37     (hosc : ∀ s ∈ Icc a b, ‖H (f τ) - H (f s)‖ ≤ ε) :
38     ‖(f b - f a) • H (f τ) -
39         (∫ s : ℝ in a..b, coordinateVelocity f s • H (f s))‖ ≤
40       (∫ s : ℝ in a..b, ‖coordinateVelocity f s‖) * ε := by
41   rw [tagged_increment_sub_integral hf hH]
42   calc
43     _ ≤ ∫ s : ℝ in a..b, ‖coordinateVelocity f s‖ * ε := by
44       apply intervalIntegral.norm_integral_le_of_norm_le hab
45       · exact Filter.Eventually.of_forall fun s hs ↦ by
46           rw [norm_smul]
47           exact mul_le_mul_of_nonneg_left (hosc s (Ioc_subset_Icc_self hs)) (norm_nonneg _)
48       · exact (integrable_coordinateVelocity hf).norm.mul_const ε
49     _ = _ := intervalIntegral.integral_mul_const _ _
50 
51 /-- Genuine tagged Riemann–Stieltjes contour sum. -/
52 def taggedSum (f : ℝ → ℂ) (H : ℂ → E) (p q : ℕ → ℝ) (n : ℕ) : E :=
53   ∑ j ∈ Finset.range n, (f (p (j+1)) - f (p j)) • H (f (q j))
54 
55 /-- All endpoints of an ordered partition lie in its endpoint interval. -/
56 theorem partition_mem {a b : ℝ} {n : ℕ} {p : ℕ → ℝ}
57     (hp : MonotoneOn p (Iic n)) (hp0 : p 0 = a) (hpn : p n = b)
58     {j : ℕ} (hj : j ≤ n) : p j ∈ uIcc a b := by
59   have ha : a ≤ p j := by rw [← hp0]; exact hp (by simp) hj (Nat.zero_le j)
60   have hb : p j ≤ b := by rw [← hpn]; exact hp hj (by simp) hj
61   exact Icc_subset_uIcc ⟨ha,hb⟩
62 
63 /-- Every finite ordered partition has total tagged-sum error bounded by one
64 common oscillation bound times the actual integral of speed. -/
65 theorem norm_taggedSum_sub_integral_le {f : ℝ → ℂ} {a b ε : ℝ} {H : ℂ → E}
66     (hf : AbsolutelyContinuousOnInterval f a b)
67     (hH : ContinuousOn H (f '' uIcc a b))
68     {n : ℕ} {p q : ℕ → ℝ}
69     (hp : MonotoneOn p (Iic n)) (hp0 : p 0 = a) (hpn : p n = b)
70     (hosc : ∀ j < n, ∀ s ∈ Icc (p j) (p (j+1)), ‖H (f (q j)) - H (f s)‖ ≤ ε) :
71     ‖taggedSum f H p q n - (∫ s : ℝ in a..b, coordinateVelocity f s • H (f s))‖ ≤
72       (∫ s : ℝ in a..b, ‖coordinateVelocity f s‖) * ε := by
73   have hsub (j : ℕ) (hj : j < n) : uIcc (p j) (p (j+1)) ⊆ uIcc a b :=
74     uIcc_subset_uIcc (partition_mem hp hp0 hpn (Nat.le_of_lt hj))
75       (partition_mem hp hp0 hpn (Nat.succ_le_of_lt hj))
76   have hac (j : ℕ) (hj : j < n) := hf.mono (hsub j hj)
77   have hcont (j : ℕ) (hj : j < n) :
78       ContinuousOn H (f '' uIcc (p j) (p (j+1))) :=
79     hH.mono (image_mono (hsub j hj))
80   have hint (j : ℕ) (hj : j < n) :
81       IntervalIntegrable (fun s ↦ coordinateVelocity f s • H (f s)) volume (p j) (p (j+1)) :=
82     (integrable_coordinateVelocity (hac j hj)).smul_continuousOn
83       ((hcont j hj).comp (hac j hj).continuousOn (fun s hs ↦ mem_image_of_mem _ hs))
84   have hsum : (∑ j ∈ Finset.range n,
85       ∫ s : ℝ in p j..p (j+1), coordinateVelocity f s • H (f s)) =
86         ∫ s : ℝ in a..b, coordinateVelocity f s • H (f s) := by
87     simpa only [hp0,hpn] using intervalIntegral.sum_integral_adjacent_intervals hint
88   have hnormsum : (∑ j ∈ Finset.range n,
89       ∫ s : ℝ in p j..p (j+1), ‖coordinateVelocity f s‖) =
90         ∫ s : ℝ in a..b, ‖coordinateVelocity f s‖ := by
91     simpa only [hp0,hpn] using intervalIntegral.sum_integral_adjacent_intervals
92       (fun j hj ↦ (integrable_coordinateVelocity (hac j hj)).norm)
93   calc
94     _ = ‖∑ j ∈ Finset.range n, ((f (p (j+1)) - f (p j)) • H (f (q j)) -
95         ∫ s : ℝ in p j..p (j+1), coordinateVelocity f s • H (f s))‖ := by
96       rw [Finset.sum_sub_distrib, hsum]
97       rfl
98     _ ≤ ∑ j ∈ Finset.range n, ‖(f (p (j+1)) - f (p j)) • H (f (q j)) -
99         ∫ s : ℝ in p j..p (j+1), coordinateVelocity f s • H (f s)‖ := norm_sum_le _ _
100     _ ≤ ∑ j ∈ Finset.range n, (∫ s : ℝ in p j..p (j+1), ‖coordinateVelocity f s‖) * ε := by
101       apply Finset.sum_le_sum
102       intro j hj
103       have hjn := Finset.mem_range.mp hj
104       exact norm_tagged_increment_sub_integral_le
105         (hp (Nat.le_of_lt hjn) (Nat.succ_le_of_lt hjn) (Nat.le_succ j))
106         (hac j hjn) (hcont j hjn) (hosc j hjn)
107     _ = _ := by rw [← Finset.sum_mul, hnormsum]
108 
109 /-- Classical all-tagged-partitions epsilon-delta contour integral predicate.
110 Repeated partition points are allowed and contribute zero. -/
111 def HasTaggedContourIntegral (f : ℝ → ℂ) (H : ℂ → E) (a b : ℝ) (I : E) : Prop :=
112   a ≤ b ∧ ∀ ε : ℝ, 0 < ε → ∃ δ : ℝ, 0 < δ ∧
113     ∀ (n : ℕ) (p q : ℕ → ℝ), MonotoneOn p (Iic n) → p 0 = a → p n = b →
114       (∀ j < n, q j ∈ Icc (p j) (p (j+1))) →
115       (∀ j < n, p (j+1) - p j < δ) → ‖taggedSum f H p q n - I‖ < ε
116 
117 /-- For every absolutely continuous path, every tagged Riemann–Stieltjes sum
118 converges to the genuine Bochner velocity integral.  This is an all-partitions
119 statement, with no Riemann–Stieltjes/velocity equality assumed in its hypotheses. -/
120 theorem hasTaggedContourIntegral_of_absolutelyContinuous {f : ℝ → ℂ} {a b : ℝ} {H : ℂ → E}
121     (hab : a ≤ b) (hf : AbsolutelyContinuousOnInterval f a b)
122     (hH : ContinuousOn H (f '' uIcc a b)) :
123     HasTaggedContourIntegral f H a b
124       (∫ s : ℝ in a..b, coordinateVelocity f s • H (f s)) := by
125   refine ⟨hab, ?_⟩
126   intro ε hε
127   let V : ℝ := ∫ s : ℝ in a..b, ‖coordinateVelocity f s‖
128   have hV : 0 ≤ V := intervalIntegral.integral_nonneg_of_forall hab (fun s ↦ norm_nonneg _)
129   let η : ℝ := ε / (V+1)
130   have hden : 0 < V+1 := by linarith
131   have hη : 0 < η := div_pos hε hden
132   have hsmall : V * η < ε := by
133     have heq : η * (V+1) = ε := div_mul_cancel₀ ε (ne_of_gt hden)
134     nlinarith
135   have hcomp : ContinuousOn (fun s ↦ H (f s)) (uIcc a b) :=
136     hH.comp hf.continuousOn (fun s hs ↦ mem_image_of_mem _ hs)
137   have huc := isCompact_uIcc.uniformContinuousOn_of_continuous hcomp
138   obtain ⟨δ,hδ,hctl⟩ := Metric.uniformContinuousOn_iff.mp huc η hη
139   refine ⟨δ,hδ,?_⟩
140   intro n p q hp hp0 hpn htag hmesh
141   have hosc : ∀ j < n, ∀ s ∈ Icc (p j) (p (j+1)), ‖H (f (q j)) - H (f s)‖ ≤ η := by
142     intro j hj s hs
143     have ht := htag j hj
144     have hsub : uIcc (p j) (p (j+1)) ⊆ uIcc a b :=
145       uIcc_subset_uIcc (partition_mem hp hp0 hpn (Nat.le_of_lt hj))
146         (partition_mem hp hp0 hpn (Nat.succ_le_of_lt hj))
147     have hdist : dist (q j) s < δ := by
148       have hle : dist (q j) s ≤ p (j+1) - p j := by
149         rw [Real.dist_eq, abs_le]
150         constructor <;> linarith [ht.1, ht.2, hs.1, hs.2]
151       exact hle.trans_lt (hmesh j hj)
152     have hlt := hctl (q j) (hsub (Icc_subset_uIcc ht)) s (hsub (Icc_subset_uIcc hs)) hdist
153     have hlt' : ‖H (f (q j)) - H (f s)‖ < η := by
154       simpa only [dist_eq_norm] using hlt
155     exact hlt'.le
156   exact (norm_taggedSum_sub_integral_le hf hH hp hp0 hpn hosc).trans_lt hsmall
157 
158 omit [NormedSpace ℝ E] [CompleteSpace E] in
159 /-- Orientation-preserving continuous monotone reparameterization preserves
160 the classical tagged contour integral, including flat parameter segments. -/
161 theorem HasTaggedContourIntegral.comp_monotone {f g : ℝ → ℂ} {H : ℂ → E}
162     {a b c d : ℝ} {I : E} {φ : ℝ → ℝ}
163     (hI : HasTaggedContourIntegral g H c d I) (hab : a ≤ b)
164     (hφc : ContinuousOn φ (uIcc a b)) (hφm : MonotoneOn φ (uIcc a b))
165     (hφa : φ a = c) (hφb : φ b = d) (hfg : EqOn f (g ∘ φ) (uIcc a b)) :
166     HasTaggedContourIntegral f H a b I := by
167   refine ⟨hab, ?_⟩
168   intro ε hε
169   obtain ⟨δ,hδ,hctl⟩ := hI.2 ε hε
170   have huc := isCompact_uIcc.uniformContinuousOn_of_continuous hφc
171   obtain ⟨η,hη,hφctl⟩ := Metric.uniformContinuousOn_iff.mp huc δ hδ
172   refine ⟨η,hη,?_⟩
173   intro n p q hp hp0 hpn htag hmesh
174   have hpmem (j : ℕ) (hj : j ≤ n) : p j ∈ uIcc a b := partition_mem hp hp0 hpn hj
175   have hqmem (j : ℕ) (hj : j < n) : q j ∈ uIcc a b :=
176     (uIcc_subset_uIcc (hpmem j (Nat.le_of_lt hj)) (hpmem (j+1) (Nat.succ_le_of_lt hj)))
177       (Icc_subset_uIcc (htag j hj))
178   have hp' : MonotoneOn (φ ∘ p) (Iic n) := by
179     intro j hj k hk hjk
180     exact hφm (hpmem j hj) (hpmem k hk) (hp hj hk hjk)
181   have hp0' : (φ ∘ p) 0 = c := by simp only [Function.comp_apply,hp0,hφa]
182   have hpn' : (φ ∘ p) n = d := by simp only [Function.comp_apply,hpn,hφb]
183   have htag' : ∀ j < n, (φ ∘ q) j ∈ Icc ((φ ∘ p) j) ((φ ∘ p) (j+1)) := by
184     intro j hj
185     exact ⟨hφm (hpmem j (Nat.le_of_lt hj)) (hqmem j hj) (htag j hj).1,
186       hφm (hqmem j hj) (hpmem (j+1) (Nat.succ_le_of_lt hj)) (htag j hj).2⟩
187   have hmesh' : ∀ j < n, (φ ∘ p) (j+1) - (φ ∘ p) j < δ := by
188     intro j hj
189     have hpj : p j ≤ p (j+1) := hp (Nat.le_of_lt hj) (Nat.succ_le_of_lt hj) (Nat.le_succ j)
190     have hd : dist (p (j+1)) (p j) < η := by
191       rw [Real.dist_eq, abs_of_nonneg (sub_nonneg.mpr hpj)]
192       exact hmesh j hj
193     have h := hφctl (p (j+1)) (hpmem (j+1) (Nat.succ_le_of_lt hj))
194       (p j) (hpmem j (Nat.le_of_lt hj)) hd
195     have h' : |φ (p (j+1)) - φ (p j)| < δ := by simpa only [Real.dist_eq] using h
196     exact (le_abs_self (φ (p (j+1)) - φ (p j))).trans_lt h' 
197   have hsum : taggedSum f H p q n = taggedSum g H (φ ∘ p) (φ ∘ q) n := by
198     apply Finset.sum_congr rfl
199     intro j hj
200     have hjn := Finset.mem_range.mp hj
201     rw [hfg (hpmem (j+1) (Nat.succ_le_of_lt hjn)), hfg (hpmem j (Nat.le_of_lt hjn)),
202       hfg (hqmem j hjn)]
203     rfl
204   rw [hsum]
205   exact hctl n (φ ∘ p) (φ ∘ q) hp' hp0' hpn' htag' hmesh'
206 
207 open Komorebi.PaperII.ReleaseArcLength
208 
209 /-- Every continuous bounded-variation path has its original classical tagged
210 contour integral identified with the arclength-reconstructed Bochner velocity
211 integral, including the zero-length case. -/
212 theorem hasTaggedContourIntegral_of_rectifiable {f : ℝ → ℂ} {H : ℂ → E}
213     (hv : BoundedVariationOn f (Icc (0:ℝ) 1))
214     (hc : ContinuousOn f (Icc (0:ℝ) 1))
215     (hH : ContinuousOn H (f '' Icc (0:ℝ) 1)) :
216     HasTaggedContourIntegral f H 0 1
217       (∫ s : ℝ in (0:ℝ)..1, coordinateVelocity (unitIntervalPath f) s •
218         H (unitIntervalPath f s)) := by
219   have h01 : (0:ℝ) ≤ 1 := by norm_num
220   have hGU : LipschitzOnWith ⟨geometricLength f, ENNReal.toReal_nonneg⟩
221       (unitIntervalPath f) (uIcc (0:ℝ) 1) := by
222     simpa only [uIcc_of_le h01] using unitIntervalPath_lipschitz hv hc
223   have hHG : ContinuousOn H (unitIntervalPath f '' uIcc (0:ℝ) 1) := by
224     rw [uIcc_of_le h01, unitIntervalPath_image hv hc]
225     exact hH
226   have hG := hasTaggedContourIntegral_of_absolutelyContinuous h01
227     hGU.absolutelyContinuousOnInterval hHG
228   by_cases hL : geometricLength f = 0
229   · have hfg : EqOn f (unitIntervalPath f ∘ id) (uIcc (0:ℝ) 1) := by
230       intro t ht
231       have ht' : t ∈ Icc (0:ℝ) 1 := by simpa only [uIcc_of_le h01] using ht
232       have hmem : arcMap f t ∈ Icc 0 (geometricLength f) := by
233         rw [← arcMap_image hv hc]
234         exact mem_image_of_mem _ ht'
235       have ha : arcMap f t = 0 := by rw [hL] at hmem; exact le_antisymm hmem.2 hmem.1
236       change f t = arcPath f (geometricLength f * t)
237       rw [hL, zero_mul, ← ha]
238       exact (arcPath_recovers hv t ht').symm
239     exact hG.comp_monotone h01 continuous_id.continuousOn (monotone_id.monotoneOn _) rfl rfl hfg
240   · have hLpos : 0 < geometricLength f := lt_of_le_of_ne ENNReal.toReal_nonneg (Ne.symm hL)
241     have hφc : ContinuousOn (fun t ↦ arcMap f t / geometricLength f) (uIcc (0:ℝ) 1) := by
242       simpa only [uIcc_of_le h01] using (arcMap_continuous hv hc).div_const (geometricLength f)
243     have hφm : MonotoneOn (fun t ↦ arcMap f t / geometricLength f) (uIcc (0:ℝ) 1) := by
244       rw [uIcc_of_le h01]
245       intro x hx y hy hxy
246       exact div_le_div_of_nonneg_right (arcMap_monotone hv hx hy hxy) hLpos.le
247     have hφa : arcMap f 0 / geometricLength f = 0 := by simp
248     have hφb : arcMap f 1 / geometricLength f = 1 := by simp [hL]
249     have hfg : EqOn f (unitIntervalPath f ∘ (fun t ↦ arcMap f t / geometricLength f))
250         (uIcc (0:ℝ) 1) := by
251       intro t ht
252       have ht' : t ∈ Icc (0:ℝ) 1 := by simpa only [uIcc_of_le h01] using ht
253       have hscale : geometricLength f * (arcMap f t / geometricLength f) = arcMap f t := by
254         field_simp
255       change f t = arcPath f (geometricLength f * (arcMap f t / geometricLength f))
256       rw [hscale]
257       exact (arcPath_recovers hv t ht').symm
258     exact hG.comp_monotone h01 hφc hφm hφa hφb hfg
259 
260 omit [NormedSpace ℝ E] [CompleteSpace E] in
261 /-- Every positive mesh tolerance admits an honest finite tagged partition.
262 This rules out a vacuous all-partitions integral predicate. -/
263 theorem exists_tagged_partition {a b δ : ℝ} (hab : a ≤ b) (hδ : 0 < δ) :
264     ∃ (n : ℕ) (p q : ℕ → ℝ), MonotoneOn p (Iic n) ∧ p 0 = a ∧ p n = b ∧
265       (∀ j < n, q j ∈ Icc (p j) (p (j+1))) ∧ (∀ j < n, p (j+1) - p j < δ) := by
266   obtain ⟨n,hn⟩ := exists_nat_gt ((b-a)/δ)
267   have hnp : (0:ℝ) < (n:ℝ) := (div_nonneg (sub_nonneg.mpr hab) hδ.le).trans_lt hn
268   have hnz : (n:ℝ) ≠ 0 := ne_of_gt hnp
269   let p : ℕ → ℝ := fun j ↦ a + (b-a) * (j:ℝ) / (n:ℝ)
270   have hp : MonotoneOn p (Iic n) := by
271     intro j hj k hk hjk
272     dsimp [p]
273     gcongr
274   have hp0 : p 0 = a := by simp [p]
275   have hpn : p n = b := by dsimp [p]; field_simp; ring
276   refine ⟨n,p,p,hp,hp0,hpn,?_,?_⟩
277   · intro j hj
278     exact ⟨le_rfl, hp (Nat.le_of_lt hj) (Nat.succ_le_of_lt hj) (Nat.le_succ j)⟩
279   · intro j hj
280     have hstep : p (j+1) - p j = (b-a)/(n:ℝ) := by dsimp [p]; push_cast; ring
281     rw [hstep,div_lt_iff₀ hnp]
282     have hlt := (div_lt_iff₀ hδ).mp hn
283     nlinarith
284 
285 omit [NormedSpace ℝ E] [CompleteSpace E] in
286 /-- Classical tagged contour integrals have a unique value. -/
287 theorem HasTaggedContourIntegral.unique {f : ℝ → ℂ} {H : ℂ → E} {a b : ℝ} {I J : E}
288     (hI : HasTaggedContourIntegral f H a b I) (hJ : HasTaggedContourIntegral f H a b J) : I = J := by
289   apply eq_of_forall_dist_le
290   intro ε hε
291   obtain ⟨δI,hδI,hctlI⟩ := hI.2 (ε/2) (by positivity)
292   obtain ⟨δJ,hδJ,hctlJ⟩ := hJ.2 (ε/2) (by positivity)
293   obtain ⟨n,p,q,hp,hp0,hpn,htag,hmesh⟩ :=
294     exists_tagged_partition hI.1 (lt_min hδI hδJ)
295   have hSI := hctlI n p q hp hp0 hpn htag (fun j hj ↦ (hmesh j hj).trans_le (min_le_left _ _))
296   have hSJ := hctlJ n p q hp hp0 hpn htag (fun j hj ↦ (hmesh j hj).trans_le (min_le_right _ _))
297   have htri := dist_triangle I (taggedSum f H p q n) J
298   have hSI' : dist I (taggedSum f H p q n) < ε/2 := by
299     simpa only [dist_eq_norm,norm_sub_rev] using hSI
300   have hSJ' : dist (taggedSum f H p q n) J < ε/2 := by simpa only [dist_eq_norm] using hSJ
301   linarith
302 
303 /-- The classical contour integral defined by its unique limit of all tagged
304 Riemann–Stieltjes sums; zero is only the undefined-case convention. -/
305 def taggedContourIntegral (f : ℝ → ℂ) (H : ℂ → E) (a b : ℝ) : E := by
306   classical
307   exact if h : ∃ I, HasTaggedContourIntegral f H a b I then Classical.choose h else 0
308 
309 omit [NormedSpace ℝ E] [CompleteSpace E] in
310 /-- A genuine all-tagged-partitions limit identifies the classical integral. -/
311 theorem HasTaggedContourIntegral.taggedContourIntegral_eq {f : ℝ → ℂ} {H : ℂ → E}
312     {a b : ℝ} {I : E} (hI : HasTaggedContourIntegral f H a b I) :
313     taggedContourIntegral f H a b = I := by
314   classical
315   have hex : ∃ J, HasTaggedContourIntegral f H a b J := ⟨I,hI⟩
316   simp only [taggedContourIntegral,dite_eq_left hex]
317   exact (Classical.choose_spec hex).unique hI
318 
319 /-- Original continuous rectifiable contours integrate by the constructed
320 arclength velocity, as a proved comparison of two distinct definitions. -/
321 theorem taggedContourIntegral_eq_velocity_of_rectifiable {f : ℝ → ℂ} {H : ℂ → E}
322     (hv : BoundedVariationOn f (Icc (0:ℝ) 1))
323     (hc : ContinuousOn f (Icc (0:ℝ) 1))
324     (hH : ContinuousOn H (f '' Icc (0:ℝ) 1)) :
325     taggedContourIntegral f H 0 1 =
326       ∫ s : ℝ in (0:ℝ)..1, coordinateVelocity (unitIntervalPath f) s • H (unitIntervalPath f s) :=
327   (hasTaggedContourIntegral_of_rectifiable hv hc hH).taggedContourIntegral_eq
328 
329 open Komorebi.PaperII.ReleaseAnalyticContour
330 open Komorebi.PaperII.ReleaseRectifiableCycle
331 
332 /-- Sum of the original classical rectifiable contour integrals equals the
333 actual constructed IntegralCycle line integral, retaining each occurrence. -/
334 theorem sum_taggedContourIntegral_eq_lineIntegral (n : ℕ) (f : Fin n → ℝ → ℂ)
335     (hv : ∀ i, BoundedVariationOn (f i) (Icc (0:ℝ) 1))
336     (hc : ∀ i, ContinuousOn (f i) (Icc (0:ℝ) 1))
337     (hclosed : ∀ i, f i 1 = f i 0) {H : ℂ → E}
338     (hH : ∀ i, ContinuousOn H (f i '' Icc (0:ℝ) 1)) :
339     (∑ i : Fin n, taggedContourIntegral (f i) H 0 1) =
340       (cycleOfRectifiable n f hv hc hclosed).lineIntegral H := by
341   unfold IntegralCycle.lineIntegral
342   apply Finset.sum_congr rfl
343   intro i hi
344   rw [taggedContourIntegral_eq_velocity_of_rectifiable (hv i) (hc i) (hH i)]
345   change (∫ s : ℝ in (0:ℝ)..1, coordinateVelocity (unitIntervalPath (f i)) s • H (unitIntervalPath (f i) s)) =
346     ∫ s : ℝ in (0:ℝ)..1, coordinateVelocity (unitIntervalPath (f i)) s •
347       H ((cycleOfRectifiable n f hv hc hclosed).curve i s)
348   apply intervalIntegral.integral_congr
349   intro s hs
350   exact congrArg (fun z : ℂ ↦ coordinateVelocity (unitIntervalPath (f i)) s • H z)
351     (curve_cycleOfRectifiable n f hv hc hclosed i s
352       (by simpa only [uIcc_of_le (by norm_num : (0:ℝ) ≤ 1)] using hs)).symm
353 
354 end Komorebi.PaperII.ReleaseRectifiableRSError

Back to source controls