ReleaseCycleDixon.lean

1 import KomorebiVerification.PaperII.ReleaseCycleWinding
2 import Mathlib.Analysis.Calculus.DSlope
3 import Mathlib.Analysis.Complex.Liouville
4 
5 set_option autoImplicit false
6 set_option backward.isDefEq.respectTransparency false
7 set_option maxHeartbeats 1000000
8 noncomputable section
9 namespace Komorebi.PaperII.ReleaseCycleDixon
10 open Set MeasureTheory Filter
11 open scoped Topology BigOperators
12 open Komorebi.PaperII.ReleaseAnalyticContour
13 open Komorebi.PaperII.ReleaseCycleParameter
14 open Komorebi.PaperII.ReleaseCycleWinding
15 
16 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
17 variable [NormedSpace ℝ E] [IsScalarTower ℝ ℂ E] [CompleteSpace E]
18 
19 def dixonH2 (Γ : IntegralCycle) (f : ℂ → E) (w : ℂ) : E :=
20   Γ.lineIntegral (fun z => (z-w)⁻¹ • f z)
21 
22 omit [IsScalarTower ℝ ℂ E] [CompleteSpace E] in
23 /-- The off-trace half of Dixon's continuation is holomorphic for every
24 continuous Banach-valued density on the actual finite cycle. -/
25 theorem hasDerivAt_dixonH2 (Γ : IntegralCycle) {f : ℂ → E}
26     (hf : ContinuousOn f Γ.trace) {w : ℂ} (hw : w ∉ Γ.trace) :
27     HasDerivAt (dixonH2 Γ f)
28       (Γ.lineIntegral (fun z => ((z-w)^2)⁻¹ • f z)) w := by
29   obtain ⟨ε, hε, haway⟩ := exists_ball_away_trace Γ hw
30   obtain ⟨M, hM⟩ := (isCompact_trace Γ).bddAbove_image hf.norm
31   have hne : ∀ a ∈ Metric.ball w ε, ∀ z ∈ Γ.trace, z - a ≠ 0 := by
32     intro a ha z hz hzero
33     have := haway z hz a ha
34     rw [hzero, norm_zero] at this
35     linarith
36   refine hasDerivAt_lineIntegral Γ
37     (f := fun a z => (z-a)⁻¹ • f z) (f' := fun a z => ((z-a)^2)⁻¹ • f z)
38     (s := Metric.ball w ε)
39     (Metric.ball_mem_nhds w hε) ?_ ?_ ?_ ((ε^2)⁻¹ * max M 0) ?_
40   · intro a ha
41     exact ((continuousOn_id.sub continuousOn_const).inv₀
42       fun z hz => hne a ha z hz).smul hf
43   · exact (((continuousOn_id.sub continuousOn_const).pow 2).inv₀
44       fun z hz => pow_ne_zero 2 (hne w (Metric.mem_ball_self hε) z hz)).smul hf
45   · intro a ha z hz
46     exact (hasDerivAt_inverse_kernel z a (hne a ha z hz)).smul_const (f z)
47   · intro a ha z hz
48     rw [norm_smul]
49     apply mul_le_mul
50     · simp only [norm_inv, norm_pow]
51       apply inv_anti₀ (by positivity)
52       nlinarith [haway z hz a ha, norm_nonneg (z-a)]
53     · exact le_max_of_le_left (hM (mem_image_of_mem _ hz))
54     · exact norm_nonneg _
55     · positivity
56 
57 omit [IsScalarTower ℝ ℂ E] [CompleteSpace E] in
58 /-- Decay bound at infinity in terms of the actual velocity length. -/
59 theorem norm_dixonH2_le (Γ : IntegralCycle) {f : ℂ → E} (R M : ℝ)
60     (_hM : 0 ≤ M) (hR : ∀ z ∈ Γ.trace, ‖z‖ ≤ R)
61     (hf : ∀ z ∈ Γ.trace, ‖f z‖ ≤ M) {w : ℂ} (hw : R < ‖w‖) :
62     ‖dixonH2 Γ f w‖ ≤ Γ.length * ((‖w‖-R)⁻¹ * M) := by
63   apply Γ.norm_lineIntegral_le
64   intro z hz
65   rw [norm_smul, norm_inv]
66   apply mul_le_mul
67   · apply inv_anti₀ (sub_pos.mpr hw)
68     have htri := norm_sub_norm_le w z
69     rw [norm_sub_rev] at htri
70     linarith [hR z hz]
71   · exact hf z hz
72   · exact norm_nonneg _
73   · positivity
74 
75 omit [IsScalarTower ℝ ℂ E] [CompleteSpace E] in
76 theorem lineIntegral_congr (Γ : IntegralCycle) {f g : ℂ → E}
77     (hfg : EqOn f g Γ.trace) : Γ.lineIntegral f = Γ.lineIntegral g := by
78   unfold IntegralCycle.lineIntegral
79   apply Finset.sum_congr rfl
80   intro i hi
81   apply intervalIntegral.integral_congr
82   intro t ht
83   exact congrArg (fun a : E => Γ.velocity i t • a) (hfg ⟨i,t,ht,rfl⟩)
84 
85 /-- The algebraic identity underlying Dixon's continuation. It holds for an
86 arbitrary Banach density continuous on the trace, with no holomorphy hypothesis. -/
87 theorem lineIntegral_dslope_eq_dixonH2_sub (Γ : IntegralCycle) {f : ℂ → E}
88     (hf : ContinuousOn f Γ.trace) {w : ℂ} (hw : w ∉ Γ.trace) :
89     Γ.lineIntegral (dslope f w) = dixonH2 Γ f w -
90       Γ.lineIntegral (fun z => (z-w)⁻¹) • f w := by
91   have hk : ContinuousOn (fun z : ℂ => (z-w)⁻¹) Γ.trace :=
92     (continuousOn_id.sub continuousOn_const).inv₀
93       fun z hz => sub_ne_zero.mpr (ne_of_mem_of_not_mem hz hw)
94   have heq : Γ.lineIntegral (dslope f w) =
95       Γ.lineIntegral (fun z => (z-w)⁻¹ • f z - (z-w)⁻¹ • f w) := by
96     apply lineIntegral_congr Γ
97     intro z hz
98     rw [dslope_of_ne f (ne_of_mem_of_not_mem hz hw), slope_def_module, smul_sub]
99   rw [heq, Γ.lineIntegral_sub (f := fun z => (z-w)⁻¹ • f z)
100     (g := fun z => (z-w)⁻¹ • f w) (hk.smul hf) (hk.smul continuousOn_const)]
101   have hmap := Γ.lineIntegral_map (ContinuousLinearMap.toSpanSingleton ℂ (f w)) hk
102   exact congrArg (fun q : E => dixonH2 Γ f w - q) hmap
103 
104 theorem kernelIntegral_eq_of_winding_eq (Γ Δ : IntegralCycle) {w : ℂ}
105     (hw : winding Γ w = winding Δ w) :
106     Γ.lineIntegral (fun z => (z-w)⁻¹) = Δ.lineIntegral (fun z => (z-w)⁻¹) := by
107   have hc : (2 * (Real.pi : ℂ) * Complex.I)⁻¹ ≠ 0 := by
108     simp [Real.pi_ne_zero]
109   exact (mul_left_cancel₀ hc) hw
110 
111 theorem pairH1H2match (Γ Δ : IntegralCycle) {f : ℂ → E}
112     (hfΓ : ContinuousOn f Γ.trace) (hfΔ : ContinuousOn f Δ.trace)
113     {w : ℂ} (hwΓ : w ∉ Γ.trace) (hwΔ : w ∉ Δ.trace)
114     (hwind : winding Γ w = winding Δ w) :
115     Γ.lineIntegral (dslope f w) - Δ.lineIntegral (dslope f w) =
116       dixonH2 Γ f w - dixonH2 Δ f w := by
117   rw [lineIntegral_dslope_eq_dixonH2_sub Γ hfΓ hwΓ,
118     lineIntegral_dslope_eq_dixonH2_sub Δ hfΔ hwΔ,
119     kernelIntegral_eq_of_winding_eq Γ Δ hwind]
120   abel
121 
122 end Komorebi.PaperII.ReleaseCycleDixon

Back to source controls