ReleaseCycleWinding.lean

1 import KomorebiVerification.PaperII.ReleaseCycleParameter
2 import KomorebiVerification.PaperII.ReleaseCycleDecay
3 import ReleaseCyclePrimitive
4 import Mathlib.Analysis.Complex.HasPrimitives
5 
6 set_option autoImplicit false
7 set_option backward.isDefEq.respectTransparency false
8 set_option maxHeartbeats 1000000
9 noncomputable section
10 namespace Komorebi.PaperII.ReleaseCycleWinding
11 open Set MeasureTheory Filter
12 open scoped Topology
13 open Komorebi.PaperII.ReleaseAnalyticContour
14 open Komorebi.PaperII.ReleaseCycleParameter
15 
16 /-- Winding defined by the actual finite cycle integral, off the trace. -/
17 def winding (Γ : IntegralCycle) (w : ℂ) : ℂ :=
18   (2 * (Real.pi : ℂ) * Complex.I)⁻¹ *
19     Γ.lineIntegral (fun z => (z - w)⁻¹)
20 
21 theorem hasDerivAt_inverse_kernel (z w : ℂ) (hzw : z - w ≠ 0) :
22     HasDerivAt (fun a : ℂ => (z - a)⁻¹) (((z - w)^2)⁻¹) w := by
23   convert! ((hasDerivAt_const w z).sub (hasDerivAt_id w)).inv hzw using 1
24   simp
25 
26 theorem hasDerivAt_kernelIntegral (Γ : IntegralCycle) {w : ℂ} (hw : w ∉ Γ.trace) :
27     HasDerivAt (fun a => Γ.lineIntegral (fun z => (z - a)⁻¹))
28       (Γ.lineIntegral (fun z => ((z - w)^2)⁻¹)) w := by
29   obtain ⟨ε, hε, haway⟩ := exists_ball_away_trace Γ hw
30   have hne : ∀ a ∈ Metric.ball w ε, ∀ z ∈ Γ.trace, z - a ≠ 0 := by
31     intro a ha z hz hzero
32     have := haway z hz a ha
33     rw [hzero, norm_zero] at this
34     linarith
35   refine hasDerivAt_lineIntegral Γ
36     (f := fun a z => (z-a)⁻¹) (f' := fun a z => ((z-a)^2)⁻¹)
37     (s := Metric.ball w ε) (Metric.ball_mem_nhds w hε)
38     ?_ ?_ ?_ ((ε^2)⁻¹) ?_
39   · intro a ha
40     exact (continuousOn_id.sub continuousOn_const).inv₀ fun z hz => hne a ha z hz
41   · exact ((continuousOn_id.sub continuousOn_const).pow 2).inv₀
42       fun z hz => pow_ne_zero 2 (hne w (Metric.mem_ball_self hε) z hz)
43   · intro a ha z hz
44     exact hasDerivAt_inverse_kernel z a (hne a ha z hz)
45   · intro a ha z hz
46     simp only [norm_inv, norm_pow]
47     apply inv_anti₀ (by positivity)
48     nlinarith [haway z hz a ha, norm_nonneg (z-a)]
49 
50 theorem hasDerivAt_winding (Γ : IntegralCycle) {w : ℂ} (hw : w ∉ Γ.trace) :
51     HasDerivAt (winding Γ)
52       ((2 * (Real.pi : ℂ) * Complex.I)⁻¹ *
53         Γ.lineIntegral (fun z => ((z - w)^2)⁻¹)) w := by
54   exact (hasDerivAt_kernelIntegral Γ hw).const_mul _
55 
56 theorem hasDerivAt_inverse_primitive (z w : ℂ) (hzw : z - w ≠ 0) :
57     HasDerivAt (fun a : ℂ => -(a-w)⁻¹) (((z-w)^2)⁻¹) z := by
58   convert! (((hasDerivAt_id z).sub_const w).inv hzw).neg using 1
59   simp only [id_eq]
60   ring
61 
62 theorem integral_inverseSquare_eq_zero (Γ : IntegralCycle) {w : ℂ}
63     (hw : w ∉ Γ.trace) : Γ.lineIntegral (fun z => ((z-w)^2)⁻¹) = 0 := by
64   have htrace : Γ.trace ⊆ {w}ᶜ := by
65     intro z hz
66     simpa only [mem_compl_iff, mem_singleton_iff] using ne_of_mem_of_not_mem hz hw
67   have hF : DifferentiableOn ℂ (fun z : ℂ => -(z-w)⁻¹) {w}ᶜ := by
68     intro z hz
69     exact (hasDerivAt_inverse_primitive z w (sub_ne_zero.mpr hz)).differentiableAt.differentiableWithinAt
70   have hzero := Γ.lineIntegral_deriv_eq_zero isOpen_compl_singleton htrace hF
71   rw [← hzero]
72   unfold IntegralCycle.lineIntegral
73   apply Finset.sum_congr rfl
74   intro i hi
75   apply intervalIntegral.integral_congr
76   intro t ht
77   change Γ.velocity i t • ((Γ.curve i t-w)^2)⁻¹ =
78     Γ.velocity i t • deriv (fun z : ℂ => -(z-w)⁻¹) (Γ.curve i t)
79   have hz : Γ.curve i t ∈ Γ.trace := ⟨i,t,ht,rfl⟩
80   exact congrArg (fun q : ℂ => Γ.velocity i t • q)
81     (hasDerivAt_inverse_primitive _ w
82       (sub_ne_zero.mpr (ne_of_mem_of_not_mem hz hw))).deriv.symm
83 
84 theorem hasDerivAt_winding_zero (Γ : IntegralCycle) {w : ℂ} (hw : w ∉ Γ.trace) :
85     HasDerivAt (winding Γ) 0 w := by
86   simpa only [integral_inverseSquare_eq_zero Γ hw, mul_zero] using hasDerivAt_winding Γ hw
87 
88 /-- Winding is locally constant off the trace for arbitrary integrable
89 velocities. The proof uses the scalar primitive FTC, not winding integrality. -/
90 theorem winding_eventually_eq (Γ : IntegralCycle) {w : ℂ} (hw : w ∉ Γ.trace) :
91     ∀ᶠ a in 𝓝 w, winding Γ a = winding Γ w := by
92   obtain ⟨ε, hε, haway⟩ := exists_ball_away_trace Γ hw
93   have hoff : ∀ a ∈ Metric.ball w ε, a ∉ Γ.trace := by
94     intro a ha hz
95     have := haway a hz a ha
96     simp only [sub_self, norm_zero] at this
97     linarith
98   filter_upwards [Metric.ball_mem_nhds w hε] with a ha
99   exact Metric.isOpen_ball.is_const_of_deriv_eq_zero (convex_ball w ε).isPreconnected
100     (fun z hz => (hasDerivAt_winding_zero Γ (hoff z hz)).differentiableAt.differentiableWithinAt)
101     (fun z hz => (hasDerivAt_winding_zero Γ (hoff z hz)).deriv)
102     ha (Metric.mem_ball_self hε)
103 
104 theorem lineIntegral_eq_zero_of_holomorphic_ball (Γ : IntegralCycle) {f : ℂ → ℂ}
105     {c : ℂ} {R : ℝ} (htrace : Γ.trace ⊆ Metric.ball c R)
106     (hf : DifferentiableOn ℂ f (Metric.ball c R)) : Γ.lineIntegral f = 0 := by
107   obtain ⟨F,hF⟩ := hf.isExactOn_ball
108   have hFdif : DifferentiableOn ℂ F (Metric.ball c R) :=
109     fun z hz => (hF z hz).differentiableAt.differentiableWithinAt
110   have hzero := Γ.lineIntegral_deriv_eq_zero Metric.isOpen_ball htrace hFdif
111   rw [← hzero]
112   unfold IntegralCycle.lineIntegral
113   apply Finset.sum_congr rfl
114   intro i hi
115   apply intervalIntegral.integral_congr
116   intro t ht
117   exact congrArg (fun q : ℂ => Γ.velocity i t • q)
118     (hF _ (htrace ⟨i,t,ht,rfl⟩)).deriv.symm
119 
120 /-- The actual winding integral vanishes sufficiently far from the compact trace. -/
121 theorem winding_eq_zero_of_far (Γ : IntegralCycle) {R : ℝ}
122     (htrace : Γ.trace ⊆ Metric.ball 0 R) {w : ℂ} (hw : R ≤ ‖w‖) : winding Γ w = 0 := by
123   have hzero : Γ.lineIntegral (fun z => (z-w)⁻¹) = 0 := by
124     apply lineIntegral_eq_zero_of_holomorphic_ball Γ htrace
125     intro z hz
126     have hzw : z-w ≠ 0 := by
127       apply sub_ne_zero.mpr
128       intro heq
129       subst w
130       simp only [Metric.mem_ball, dist_zero_right] at hz
131       linarith
132     exact (((hasDerivAt_id z).sub_const w).inv hzw).differentiableAt.differentiableWithinAt
133   simp only [winding,hzero,mul_zero]
134 
135 theorem winding_eventually_zero (Γ : IntegralCycle) :
136     ∀ᶠ w in cocompact ℂ, winding Γ w = 0 := by
137   obtain ⟨R,hR⟩ := (isCompact_trace Γ).bddAbove_image continuousOn_id.norm
138   have htrace : Γ.trace ⊆ Metric.ball 0 (R+1) := by
139     intro z hz
140     simp only [Metric.mem_ball,dist_zero_right]
141     exact lt_of_le_of_lt (hR (mem_image_of_mem _ hz)) (lt_add_one R)
142   filter_upwards [Komorebi.PaperII.ReleaseCycleDecay.norm_gt_mem_cocompact (R+1)] with w hw
143   exact winding_eq_zero_of_far Γ htrace hw.le
144 
145 end Komorebi.PaperII.ReleaseCycleWinding

Back to source controls