ReleaseCyclePrimitive.lean

1 import KomorebiVerification.PaperII.ReleaseRectifiable
2 import Mathlib.Analysis.Complex.CauchyIntegral
3 import Mathlib.Analysis.Calculus.ContDiff.RCLike
4 import Mathlib.Topology.Algebra.MetricSpace.Lipschitz
5 
6 set_option autoImplicit false
7 noncomputable section
8 
9 namespace Komorebi.PaperII.ReleaseCyclePrimitive
10 open MeasureTheory Set Filter
11 open scoped Topology BigOperators
12 open Komorebi.PaperII.ReleaseAnalyticContour
13 
14 theorem isCompact_trace (Γ : IntegralCycle) : IsCompact Γ.trace := by
15   have heq : Γ.trace = ⋃ i : Fin Γ.count, Γ.curve i '' uIcc (0:ℝ) 1 := by
16     ext z
17     simp [IntegralCycle.trace]
18   rw [heq]
19   exact isCompact_iUnion fun i ↦ isCompact_uIcc.image_of_continuousOn (Γ.continuousOn_curve i)
20 
21 /-- The integral primitive of an integrable complex function is absolutely
22 continuous, obtained from the two real coordinate primitives. -/
23 theorem ac_complex_primitive {g : ℝ → ℂ} (hg : IntervalIntegrable g volume 0 1) :
24     AbsolutelyContinuousOnInterval (fun s : ℝ ↦ ∫ t : ℝ in 0..s, g t) 0 1 := by
25   have hr : IntervalIntegrable (fun t ↦ (g t).re) volume 0 1 :=
26     ⟨Complex.reCLM.integrable_comp hg.1, Complex.reCLM.integrable_comp hg.2⟩
27   have hi : IntervalIntegrable (fun t ↦ (g t).im) volume 0 1 :=
28     ⟨Complex.imCLM.integrable_comp hg.1, Complex.imCLM.integrable_comp hg.2⟩
29   have har := Complex.ofRealCLM.lipschitzWith.comp_absolutelyContinuousOnInterval
30     (hr.absolutelyContinuousOnInterval_intervalIntegral (c := 0) (by simp))
31   have hai := Complex.ofRealCLM.lipschitzWith.comp_absolutelyContinuousOnInterval
32     (hi.absolutelyContinuousOnInterval_intervalIntegral (c := 0) (by simp))
33   apply (har.add (hai.const_smul Complex.I)).congr
34   intro s hs
35   have hint := hg.mono_set (uIcc_subset_uIcc_left hs)
36   have hreal := Complex.reCLM.intervalIntegral_comp_comm hint
37   have himag := Complex.imCLM.intervalIntegral_comp_comm hint
38   apply Complex.ext <;> simp_all [Function.comp_def, smul_eq_mul]
39 
40 theorem ac_curve (Γ : IntegralCycle) (i : Fin Γ.count) :
41     AbsolutelyContinuousOnInterval (Γ.curve i) 0 1 := by
42   have hconst : AbsolutelyContinuousOnInterval (fun _ : ℝ ↦ Γ.base i) 0 1 :=
43     (show LipschitzWith 0 (fun _ : ℝ ↦ Γ.base i) from LipschitzWith.const _).lipschitzOnWith.absolutelyContinuousOnInterval
44   exact hconst.add (ac_complex_primitive (Γ.velocity_integrable i))
45 
46 theorem ae_hasDerivAt_curve (Γ : IntegralCycle) (i : Fin Γ.count) :
47     ∀ᵐ s : ℝ, s ∈ uIcc (0:ℝ) 1 → HasDerivAt (Γ.curve i) (Γ.velocity i s) s := by
48   filter_upwards [(Γ.velocity_integrable i).ae_hasDerivAt_integral] with s hs hmem
49   exact (hs hmem 0 left_mem_uIcc).const_add (Γ.base i)
50 
51 theorem lipschitzOn_trace_of_holomorphic (Γ : IntegralCycle) {U : Set ℂ}
52     (hU : IsOpen U) (hΓ : Γ.trace ⊆ U) {F : ℂ → ℂ}
53     (hF : DifferentiableOn ℂ F U) : ∃ K, LipschitzOnWith K F Γ.trace := by
54   apply LocallyLipschitzOn.exists_lipschitzOnWith_of_compact (isCompact_trace Γ)
55   intro z hz
56   have hc : ContDiffAt ℂ 1 F z :=
57     (hF.contDiffOn hU z (hΓ hz)).contDiffAt (hU.mem_nhds (hΓ hz))
58   obtain ⟨K, t, ht, hKt⟩ := hc.exists_lipschitzOnWith
59   exact ⟨K, t, mem_nhdsWithin_of_mem_nhds ht, hKt⟩
60 
61 theorem integral_deriv_curve_eq_sub (Γ : IntegralCycle) {U : Set ℂ}
62     (hU : IsOpen U) (hΓ : Γ.trace ⊆ U) {F : ℂ → ℂ}
63     (hF : DifferentiableOn ℂ F U) (i : Fin Γ.count) :
64     (∫ s : ℝ in (0:ℝ)..1, Γ.velocity i s • deriv F (Γ.curve i s)) =
65       F (Γ.curve i 1) - F (Γ.curve i 0) := by
66   have hderiv : ContinuousOn (deriv F) Γ.trace :=
67     (hF.deriv hU).continuousOn.mono hΓ
68   have hint := Γ.integrable_lineIntegrand hderiv i
69   obtain ⟨K, hK⟩ := lipschitzOn_trace_of_holomorphic Γ hU hΓ hF
70   have hcomp : AbsolutelyContinuousOnInterval (F ∘ Γ.curve i) 0 1 :=
71     hK.comp_absolutelyContinuousOnInterval (fun s hs ↦ ⟨i,s,hs,rfl⟩) (ac_curve Γ i)
72   let g : ℝ → ℂ := fun s ↦ F (Γ.curve i s) -
73     ∫ t : ℝ in 0..s, Γ.velocity i t • deriv F (Γ.curve i t)
74   have hg : AbsolutelyContinuousOnInterval g 0 1 :=
75     hcomp.sub (ac_complex_primitive hint)
76   have hg0 : ∀ᵐ s : ℝ, s ∈ uIcc (0:ℝ) 1 → HasDerivAt g 0 s := by
77     filter_upwards [ae_hasDerivAt_curve Γ i, hint.ae_hasDerivAt_integral] with s hs ht hmem
78     have hFs := ((hF (Γ.curve i s) (hΓ ⟨i,s,hmem,rfl⟩)).differentiableAt
79       (hU.mem_nhds (hΓ ⟨i,s,hmem,rfl⟩))).hasDerivAt
80     have hchain := hFs.scomp s (hs hmem)
81     convert! hchain.sub (ht hmem 0 left_mem_uIcc) using 1
82     simp
83   obtain ⟨C, hC⟩ := hg.const_of_ae_hasDerivAt_zero hg0
84   have ha := hC 0 left_mem_uIcc
85   have hb := hC 1 right_mem_uIcc
86   dsimp [g] at ha hb
87   simp only [intervalIntegral.integral_same, sub_zero] at ha
88   rw [← ha] at hb
89   apply eq_sub_iff_add_eq.mpr
90   simpa only [smul_eq_mul, add_comm] using (sub_eq_iff_eq_add.mp hb).symm
91 
92 end Komorebi.PaperII.ReleaseCyclePrimitive
93 
94 namespace Komorebi.PaperII.ReleaseAnalyticContour.IntegralCycle
95 open Set
96 open Komorebi.PaperII.ReleaseCyclePrimitive
97 open scoped BigOperators
98 
99 /-- A holomorphic derivative integrates to zero over every actual finite
100 integrable-velocity closed cycle. No C1 condition is imposed on its curves. -/
101 theorem lineIntegral_deriv_eq_zero (Γ : IntegralCycle) {U : Set ℂ}
102     (hU : IsOpen U) (hΓ : Γ.trace ⊆ U) {F : ℂ → ℂ}
103     (hF : DifferentiableOn ℂ F U) : Γ.lineIntegral (deriv F) = 0 := by
104   unfold lineIntegral
105   apply Finset.sum_eq_zero
106   intro i hi
107   rw [integral_deriv_curve_eq_sub Γ hU hΓ hF i, Γ.curve_one, Γ.curve_zero, sub_self]
108 
109 end Komorebi.PaperII.ReleaseAnalyticContour.IntegralCycle

Back to source controls