ReleaseCycleDecay.lean

1 import KomorebiVerification.PaperII.ReleaseCycleParameter
2 import Mathlib.Analysis.Complex.Liouville
3 
4 set_option autoImplicit false
5 noncomputable section
6 
7 namespace Komorebi.PaperII.ReleaseCycleDecay
8 open Set Filter
9 open scoped Topology
10 open Komorebi.PaperII.ReleaseAnalyticContour
11 open Komorebi.PaperII.ReleaseCycleParameter
12 
13 theorem norm_gt_mem_cocompact (R : ℝ) :
14     {w : ℂ | R < ‖w‖} ∈ Filter.cocompact ℂ :=
15   Filter.mem_cocompact.mpr ⟨Metric.closedBall 0 R, isCompact_closedBall 0 R,
16     fun _ hw => by simpa using hw⟩
17 
18 /-- A reciprocal norm bound implies convergence to zero in a normed target. -/
19 theorem tendsto_zero_of_norm_bound
20     {E : Type*} [NormedAddCommGroup E] {g : ℂ → E} {R C : ℝ}
21     (hbound : ∀ w, R < ‖w‖ → ‖g w‖ ≤ C / (‖w‖ - R)) :
22     Tendsto g (Filter.cocompact ℂ) (𝓝 0) := by
23   rw [Metric.tendsto_nhds]
24   intro ε hε
25   simp only [dist_zero_right]
26   filter_upwards [norm_gt_mem_cocompact (max R (R + C / ε))] with w hw
27   have hRw : R < ‖w‖ := lt_of_le_of_lt (le_max_left _ _) hw
28   calc
29     ‖g w‖ ≤ C / (‖w‖ - R) := hbound w hRw
30     _ < ε := by
31       rw [div_lt_iff₀ (sub_pos.mpr hRw)]
32       have h2 : C / ε < ‖w‖ - R := by
33         linarith [lt_of_le_of_lt (le_max_right _ _) hw]
34       rw [div_lt_iff₀ hε] at h2
35       linarith [mul_comm ε (‖w‖ - R)]
36 
37 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
38   [NormedSpace ℝ E]
39 
40 /-- The concrete reciprocal estimate for the actual finite-cycle transform. -/
41 theorem norm_cauchyTransform_le (Γ : IntegralCycle) {f : ℂ → E} (R M : ℝ)
42     (_hM : 0 ≤ M) (hR : ∀ z ∈ Γ.trace, ‖z‖ ≤ R)
43     (hf : ∀ z ∈ Γ.trace, ‖f z‖ ≤ M) {w : ℂ} (hw : R < ‖w‖) :
44     ‖Γ.lineIntegral (fun z => (z-w)⁻¹ • f z)‖ ≤
45       Γ.length * ((‖w‖-R)⁻¹ * M) := by
46   apply Γ.norm_lineIntegral_le
47   intro z hz
48   rw [norm_smul, norm_inv]
49   apply mul_le_mul
50   · apply inv_anti₀ (sub_pos.mpr hw)
51     have htri := norm_sub_norm_le w z
52     rw [norm_sub_rev] at htri
53     linarith [hR z hz]
54   · exact hf z hz
55   · exact norm_nonneg _
56   · positivity
57 
58 /-- Decay of the Banach-valued Cauchy transform of a finite cycle. -/
59 theorem dixonH2_tendsto_zero_of_bounds (Γ : IntegralCycle) {f : ℂ → E}
60     {R M : ℝ} (hM : 0 ≤ M) (hR : ∀ z ∈ Γ.trace, ‖z‖ ≤ R)
61     (hf : ∀ z ∈ Γ.trace, ‖f z‖ ≤ M) :
62     Tendsto (fun w => Γ.lineIntegral (fun z => (z-w)⁻¹ • f z)) (Filter.cocompact ℂ) (𝓝 0) := by
63   apply tendsto_zero_of_norm_bound (R := R) (C := Γ.length * M)
64   intro w hw
65   calc
66     ‖Γ.lineIntegral (fun z => (z-w)⁻¹ • f z)‖ ≤ Γ.length * ((‖w‖ - R)⁻¹ * M) :=
67       norm_cauchyTransform_le Γ R M hM hR hf hw
68     _ = Γ.length * M / (‖w‖ - R) := by ring
69 
70 /-- Continuous densities need no additional bound hypotheses: compactness of the
71 actual cycle trace supplies both bounds used in the decay estimate. -/
72 theorem dixonH2_tendsto_zero (Γ : IntegralCycle) {f : ℂ → E}
73     (hf : ContinuousOn f Γ.trace) :
74     Tendsto (fun w => Γ.lineIntegral (fun z => (z-w)⁻¹ • f z)) (Filter.cocompact ℂ) (𝓝 0) := by
75   obtain ⟨R, hR⟩ := (isCompact_trace Γ).bddAbove_image continuousOn_id.norm
76   obtain ⟨M, hM⟩ := (isCompact_trace Γ).bddAbove_image hf.norm
77   exact dixonH2_tendsto_zero_of_bounds Γ (R := R) (M := max M 0)
78     (le_max_right _ _) (fun z hz => hR (mem_image_of_mem _ hz))
79     (fun z hz => le_max_of_le_left (hM (mem_image_of_mem _ hz)))
80 
81 end Komorebi.PaperII.ReleaseCycleDecay

Back to source controls