ReleaseCycleCauchy.lean

1 import KomorebiVerification.PaperII.ReleaseCycleDixon
2 import KomorebiVerification.PaperII.ReleaseCycleDSlope
3 import KomorebiVerification.PaperII.ReleaseCycleDecay
4 import Mathlib.Analysis.Complex.Liouville
5 
6 set_option autoImplicit false
7 noncomputable section
8 namespace Komorebi.PaperII.ReleaseCycleCauchy
9 open Set MeasureTheory Filter
10 open scoped Topology BigOperators
11 open Komorebi.PaperII.ReleaseAnalyticContour
12 open Komorebi.PaperII.ReleaseCycleParameter
13 open Komorebi.PaperII.ReleaseCycleWinding
14 open Komorebi.PaperII.ReleaseCycleDixon
15 open Komorebi.PaperII.ReleaseCycleDSlope
16 
17 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
18 variable [NormedSpace ℝ E] [IsScalarTower ℝ ℂ E] [CompleteSpace E]
19 
20 /-- Dixon's two-cycle continuation. Taking the difference directly avoids
21 introducing a separate reversed-cycle representation. -/
22 def pairDixon (Γ Δ : IntegralCycle) (f : ℂ → E) (U : Set ℂ) (w : ℂ) : E :=
23   by
24     classical
25     exact if w ∈ U then Γ.lineIntegral (dslope f w) - Δ.lineIntegral (dslope f w)
26       else dixonH2 Γ f w - dixonH2 Δ f w
27 
28 theorem differentiable_pairDixon (Γ Δ : IntegralCycle) {f : ℂ → E} {U : Set ℂ}
29     (hU : IsOpen U) (hf : DifferentiableOn ℂ f U)
30     (hΓ : Γ.trace ⊆ U) (hΔ : Δ.trace ⊆ U)
31     (hnull : ∀ w ∉ U, winding Γ w = winding Δ w)
32     (hmatch : ∀ w ∈ U, w ∉ Γ.trace → w ∉ Δ.trace →
33       winding Γ w = winding Δ w →
34       Γ.lineIntegral (dslope f w) - Δ.lineIntegral (dslope f w) =
35         dixonH2 Γ f w - dixonH2 Δ f w) :
36     Differentiable ℂ (pairDixon Γ Δ f U) := by
37   intro w
38   by_cases hw : w ∈ U
39   · have hd := ((differentiableOn_lineIntegral_dslope Γ hU hf hΓ w hw).differentiableAt
40         (hU.mem_nhds hw)).sub
41         ((differentiableOn_lineIntegral_dslope Δ hU hf hΔ w hw).differentiableAt
42         (hU.mem_nhds hw))
43     apply hd.congr_of_eventuallyEq
44     filter_upwards [hU.mem_nhds hw] with a ha
45     simp [pairDixon, ha]
46   · have hwΓ : w ∉ Γ.trace := fun hz ↦ hw (hΓ hz)
47     have hwΔ : w ∉ Δ.trace := fun hz ↦ hw (hΔ hz)
48     have hcompΓ : ContinuousOn f Γ.trace := hf.continuousOn.mono hΓ
49     have hcompΔ : ContinuousOn f Δ.trace := hf.continuousOn.mono hΔ
50     have hd := (hasDerivAt_dixonH2 Γ hcompΓ hwΓ).differentiableAt.sub
51       (hasDerivAt_dixonH2 Δ hcompΔ hwΔ).differentiableAt
52     apply hd.congr_of_eventuallyEq
53     filter_upwards [winding_eventually_eq Γ hwΓ, winding_eventually_eq Δ hwΔ,
54       (isCompact_trace Γ).isClosed.isOpen_compl.mem_nhds hwΓ,
55       (isCompact_trace Δ).isClosed.isOpen_compl.mem_nhds hwΔ] with a haΓ haΔ haoffΓ haoffΔ
56     unfold pairDixon
57     split_ifs with ha
58     · exact hmatch a ha haoffΓ haoffΔ (haΓ.trans ((hnull w hw).trans haΔ.symm))
59     · rfl
60 
61 /-- Once the independently established pieces are matched, the continuation
62 vanishes by the Banach-valued Liouville theorem. -/
63 theorem pairDixon_eq_zero_of_pieces (Γ Δ : IntegralCycle) {f : ℂ → E} {U : Set ℂ}
64     (hU : IsOpen U) (hf : DifferentiableOn ℂ f U)
65     (hΓ : Γ.trace ⊆ U) (hΔ : Δ.trace ⊆ U)
66     (hnull : ∀ w ∉ U, winding Γ w = winding Δ w)
67     (hmatch : ∀ w ∈ U, w ∉ Γ.trace → w ∉ Δ.trace →
68       winding Γ w = winding Δ w →
69       Γ.lineIntegral (dslope f w) - Δ.lineIntegral (dslope f w) =
70         dixonH2 Γ f w - dixonH2 Δ f w)
71     (hwindΓ : ∀ᶠ w in cocompact ℂ, w ∉ Γ.trace ∧ winding Γ w = 0)
72     (hwindΔ : ∀ᶠ w in cocompact ℂ, w ∉ Δ.trace ∧ winding Δ w = 0)
73     (hdecayΓ : Tendsto (dixonH2 Γ f) (cocompact ℂ) (𝓝 0))
74     (hdecayΔ : Tendsto (dixonH2 Δ f) (cocompact ℂ) (𝓝 0)) :
75     ∀ w, pairDixon Γ Δ f U w = 0 := by
76   have hd := differentiable_pairDixon Γ Δ hU hf hΓ hΔ hnull hmatch
77   have heq : pairDixon Γ Δ f U =ᶠ[cocompact ℂ]
78       fun w ↦ dixonH2 Γ f w - dixonH2 Δ f w := by
79     filter_upwards [hwindΓ,hwindΔ] with w hwΓ hwΔ
80     unfold pairDixon
81     split_ifs with hw
82     · exact hmatch w hw hwΓ.1 hwΔ.1 (hwΓ.2.trans hwΔ.2.symm)
83     · rfl
84   have hlim : Tendsto (pairDixon Γ Δ f U) (cocompact ℂ) (𝓝 0) := by
85     have hsub := hdecayΓ.sub hdecayΔ
86     simp only [sub_self] at hsub
87     exact hsub.congr' heq.symm
88   exact fun w ↦ hd.apply_eq_of_tendsto_cocompact w hlim
89 
90 omit [IsScalarTower ℝ ℂ E] [CompleteSpace E] in
91 theorem lineIntegral_congr_on_trace (Γ : IntegralCycle) {f g : ℂ → E}
92     (hfg : EqOn f g Γ.trace) : Γ.lineIntegral f = Γ.lineIntegral g := by
93   unfold IntegralCycle.lineIntegral
94   apply Finset.sum_congr rfl
95   intro i hi
96   apply intervalIntegral.integral_congr
97   intro t ht
98   exact congrArg (fun a : E ↦ Γ.velocity i t • a) (hfg ⟨i,t,ht,rfl⟩)
99 
100 omit [NormedSpace ℝ E] [IsScalarTower ℝ ℂ E] [CompleteSpace E] in
101 /-- Multiplication by the vanishing linear factor removes the divided
102 difference singularity, including on the diagonal itself. -/
103 theorem dslope_twist_eq (f : ℂ → E) {U : Set ℂ} (hU : IsOpen U)
104     (hf : DifferentiableOn ℂ f U) {w : ℂ} (hw : w ∈ U) (z : ℂ) :
105     dslope (fun a ↦ (a-w) • f a) w z = f z := by
106   by_cases hzw : z = w
107   · subst z
108     rw [dslope_same]
109     have hd := ((hasDerivAt_id w).sub_const w).smul
110       ((hf w hw).differentiableAt (hU.mem_nhds hw)).hasDerivAt
111     convert! hd.deriv using 1
112     simp
113   · rw [dslope_of_ne _ hzw]
114     simp [slope_def_module, smul_smul, inv_mul_cancel₀ (sub_ne_zero.mpr hzw)]
115 
116 omit [IsScalarTower ℝ ℂ E] [CompleteSpace E] in
117 theorem lineIntegral_eq_of_twisted_pairDixon_zero (Γ Δ : IntegralCycle)
118     {f : ℂ → E} {U : Set ℂ} (hU : IsOpen U) (hf : DifferentiableOn ℂ f U)
119     {w : ℂ} (hw : w ∈ U)
120     (hzero : pairDixon Γ Δ (fun z ↦ (z-w) • f z) U w = 0) :
121     Γ.lineIntegral f = Δ.lineIntegral f := by
122   have hΓ : Γ.lineIntegral (dslope (fun z ↦ (z-w) • f z) w) = Γ.lineIntegral f :=
123     lineIntegral_congr_on_trace Γ (fun z _ ↦ dslope_twist_eq f hU hf hw z)
124   have hΔ : Δ.lineIntegral (dslope (fun z ↦ (z-w) • f z) w) = Δ.lineIntegral f :=
125     lineIntegral_congr_on_trace Δ (fun z _ ↦ dslope_twist_eq f hU hf hw z)
126   have hz : Γ.lineIntegral (dslope (fun z ↦ (z-w) • f z) w) -
127       Δ.lineIntegral (dslope (fun z ↦ (z-w) • f z) w) = 0 := by
128     simpa [pairDixon, hw] using hzero
129   rw [hΓ, hΔ] at hz
130   exact sub_eq_zero.mp hz
131 
132 /-- The concrete Banach-valued Dixon continuation vanishes. All analytic
133 pieces and all winding inputs are derived from the actual finite cycles. -/
134 theorem pairDixon_eq_zero (Γ Δ : IntegralCycle) {f : ℂ → E} {U : Set ℂ}
135     (hU : IsOpen U) (hf : DifferentiableOn ℂ f U)
136     (hΓ : Γ.trace ⊆ U) (hΔ : Δ.trace ⊆ U)
137     (hnull : ∀ w ∉ U, winding Γ w = winding Δ w) :
138     ∀ w, pairDixon Γ Δ f U w = 0 := by
139   apply pairDixon_eq_zero_of_pieces Γ Δ hU hf hΓ hΔ hnull
140   · intro w hw hwΓ hwΔ hwind
141     exact pairH1H2match Γ Δ (hf.continuousOn.mono hΓ) (hf.continuousOn.mono hΔ)
142       hwΓ hwΔ hwind
143   · filter_upwards [winding_eventually_zero Γ, (isCompact_trace Γ).compl_mem_cocompact]
144       with w hw hoff
145     exact ⟨hoff,hw⟩
146   · filter_upwards [winding_eventually_zero Δ, (isCompact_trace Δ).compl_mem_cocompact]
147       with w hw hoff
148     exact ⟨hoff,hw⟩
149   · exact Komorebi.PaperII.ReleaseCycleDecay.dixonH2_tendsto_zero Γ
150       (hf.continuousOn.mono hΓ)
151   · exact Komorebi.PaperII.ReleaseCycleDecay.dixonH2_tendsto_zero Δ
152       (hf.continuousOn.mono hΔ)
153 
154 /-- General homological Cauchy comparison for arbitrary finite closed curves
155 with integrable velocities and a Banach-valued holomorphic density. Equal
156 winding outside the open domain implies equal genuine cycle integrals. -/
157 theorem lineIntegral_eq_of_winding (Γ Δ : IntegralCycle) {f : ℂ → E} {U : Set ℂ}
158     (hU : IsOpen U) (hf : DifferentiableOn ℂ f U)
159     (hΓ : Γ.trace ⊆ U) (hΔ : Δ.trace ⊆ U)
160     (hnull : ∀ w ∉ U, winding Γ w = winding Δ w) :
161     Γ.lineIntegral f = Δ.lineIntegral f := by
162   by_cases hne : U.Nonempty
163   · obtain ⟨w,hw⟩ := hne
164     have htwist : DifferentiableOn ℂ (fun z ↦ (z-w) • f z) U :=
165       (differentiableOn_id.sub_const w).smul hf
166     exact lineIntegral_eq_of_twisted_pairDixon_zero Γ Δ hU hf hw
167       (pairDixon_eq_zero Γ Δ hU htwist hΓ hΔ hnull w)
168   · have hzero (Λ : IntegralCycle) (hΛ : Λ.trace ⊆ U) : Λ.lineIntegral f = 0 := by
169       apply norm_le_zero_iff.mp
170       have hb := Λ.norm_lineIntegral_le (f := f) 0
171         (fun z hz ↦ (hne ⟨z,hΛ hz⟩).elim)
172       simpa only [mul_zero] using hb
173     rw [hzero Γ hΓ,hzero Δ hΔ]
174 
175 end Komorebi.PaperII.ReleaseCycleCauchy

Back to source controls