IndicatorLimit.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.AlignedExponentialRadii
6 import KomorebiPaperIV.UniformDominantSectors
7 
8 namespace Komorebi.PaperIV
9 noncomputable section
10 open Set Filter
11 open scoped Topology
12 
13 /-- The finite exponential representation gives the sharp directional bound. -/
14 theorem canonicalSignedDenominator_indicator_upper {N : ℕ} (hN : 0 < N)
15     (θ : ℝ) {r : ℝ} (hr : 0 ≤ r) :
16     ‖canonicalSignedDenominator N ((r : ℂ) * rayDirection θ)‖ ≤ Real.exp (r * signedIndicator N hN θ) := by
17   unfold canonicalSignedDenominator
18   rw [entireSigned_zero_eq_average, norm_mul, norm_inv, Complex.norm_natCast]
19   have hb (i : ℕ) (hi : i ∈ Finset.range N) :
20       ‖Complex.exp (canonicalSignedVertex N i * ((r : ℂ) * rayDirection θ))‖ ≤
21         Real.exp (r * signedIndicator N hN θ) := by
22     rw [Complex.norm_exp]
23     apply Real.exp_le_exp.mpr
24     have he : (canonicalSignedVertex N i * ((r : ℂ) * rayDirection θ)).re =
25         r * signedProjection N θ i := by
26       rw [show canonicalSignedVertex N i * ((r : ℂ) * rayDirection θ) =
27         (r : ℂ) * (canonicalSignedVertex N i * rayDirection θ) by ring, Complex.re_ofReal_mul]
28       rfl
29     rw [he]
30     exact mul_le_mul_of_nonneg_left (signedProjection_le_indicator hN (Finset.mem_range.mp hi) θ) hr
31   calc
32     _ ≤ (N : ℝ)⁻¹ * ∑ i ∈ Finset.range N, ‖Complex.exp (canonicalSignedVertex N i * ((r : ℂ) * rayDirection θ))‖ :=
33       mul_le_mul_of_nonneg_left (norm_sum_le _ _) (by positivity)
34     _ ≤ (N : ℝ)⁻¹ * ∑ _i ∈ Finset.range N, Real.exp (r * signedIndicator N hN θ) :=
35       mul_le_mul_of_nonneg_left (Finset.sum_le_sum hb) (by positivity)
36     _ = _ := by simp [hN.ne']
37 
38 theorem canonicalSignedDenominator_log_indicator_upper {N : ℕ} (hN : 2 ≤ N)
39     (θ : ℝ) {r : ℝ} (hr : 0 < r) :
40     Real.log ‖canonicalSignedDenominator N ((r : ℂ) * rayDirection θ)‖ / r ≤
41       signedIndicator N (by omega) θ := by
42   apply (div_le_iff₀ hr).mpr
43   by_cases hz : canonicalSignedDenominator N ((r : ℂ) * rayDirection θ) = 0
44   · simp only [hz, norm_zero, Real.log_zero]
45     exact mul_nonneg (signedIndicator_nonneg hN θ) hr.le
46   · have h := (Real.log_le_iff_le_exp (norm_pos_iff.mpr hz)).mpr
47       (canonicalSignedDenominator_indicator_upper (show 0 < N by omega) θ hr.le)
48     simpa only [mul_comm] using h
49 
50 theorem canonicalSignedDenominator_real_normalization (N : ℕ) (θ h r : ℝ) :
51     Complex.exp (-((h * r : ℝ) : ℂ)) * canonicalSignedDenominator N ((r : ℂ) * rayDirection θ) =
52       (N : ℂ)⁻¹ * ∑ i ∈ Finset.range N,
53         Complex.exp ((canonicalSignedVertex N i * rayDirection θ - (h : ℂ)) * (r : ℂ)) := by
54   unfold canonicalSignedDenominator
55   rw [entireSigned_zero_eq_average, mul_left_comm]
56   congr 1
57   rw [Finset.mul_sum]
58   apply Finset.sum_congr rfl
59   intro i _
60   rw [← Complex.exp_add]
61   congr 1
62   dsimp [canonicalSignedVertex]
63   push_cast
64   ring
65 
66 /-- The lower indicator sequence exists in every direction, including ties. -/
67 theorem canonicalSignedDenominator_indicator_sequence {N : ℕ} (hN : 0 < N) (θ : ℝ) :
68     ∃ r : ℕ → ℝ, Tendsto r atTop atTop ∧
69       Tendsto (fun n => Real.log ‖canonicalSignedDenominator N ((r n : ℂ) * rayDirection θ)‖ / r n)
70         atTop (𝓝 (signedIndicator N hN θ)) ∧
71       ∀ᶠ n in atTop, canonicalSignedDenominator N ((r n : ℂ) * rayDirection θ) ≠ 0 := by
72   let a : ℕ → ℂ := fun i => canonicalSignedVertex N i * rayDirection θ
73   obtain ⟨k, hk, he⟩ := (Finset.range N).exists_mem_eq_sup' ⟨0, Finset.mem_range.mpr hN⟩ (signedProjection N θ)
74   have hmax : ∀ i ∈ Finset.range N, (a i).re ≤ (a k).re :=
75     fun i hi => (signedProjection_le_indicator hN (Finset.mem_range.mp hi) θ).trans_eq he
76   have ht := finite_unit_exponential_aligned_limit hk
77     (a := a) (fun i _ => by simp [a, norm_canonicalSignedVertex, norm_rayDirection]) hmax
78   let r := alignedRadii (a k).im
79   let c : ℂ := (N : ℂ)⁻¹ * ((Finset.range N).filter (fun i => (a i).re = (a k).re)).card
80   have hcard : 0 < ((Finset.range N).filter (fun i => (a i).re = (a k).re)).card :=
81     Finset.card_pos.mpr ⟨k, Finset.mem_filter.mpr ⟨hk, rfl⟩⟩
82   have hc : c ≠ 0 := mul_ne_zero
83     (inv_ne_zero (by exact_mod_cast hN.ne')) (by exact_mod_cast hcard.ne')
84   have hnorm : Tendsto (fun n => Complex.exp (-(((a k).re * r n : ℝ) : ℂ)) *
85       canonicalSignedDenominator N ((r n : ℂ) * rayDirection θ)) atTop (𝓝 c) := by
86     simpa only [canonicalSignedDenominator_real_normalization] using! ht.const_mul (N : ℂ)⁻¹
87   refine ⟨r, alignedRadii_tendsto _, ?_, ?_⟩
88   · have hslope := log_norm_slope_of_normalized_limit (alignedRadii_tendsto _) hc hnorm
89     have he' : signedIndicator N hN θ = (a k).re := he
90     rw [he']
91     exact hslope
92   · exact (hnorm.eventually_ne hc).mono (fun n hn => (mul_ne_zero_iff.mp hn).2)
93 
94 /-- A sharp upper bound and a convergent lower sequence determine a limsup. -/
95 theorem limsup_eq_of_upper_and_sequence {f : ℝ → ℝ} {h : ℝ} {l : Filter ℝ}
96     (hu : ∀ᶠ r in l, f r ≤ h) {r : ℕ → ℝ}
97     (hr : Tendsto r atTop l) (hf : Tendsto (fun n => f (r n)) atTop (𝓝 h)) :
98     limsup f l = h := by
99   have hleast (b : ℝ) (hb : ∀ᶠ x in l, f x ≤ b) : h ≤ b :=
100     le_of_tendsto hf (hr.eventually hb)
101   exact le_antisymm (limsup_le_of_le ⟨h, hleast⟩ hu) (le_limsup_of_le ⟨h, hu⟩ hleast)
102 
103 /-- The exact indicator equality in Theorem 11.4, with no omitted tie directions. -/
104 theorem canonicalSignedDenominator_indicator {N : ℕ} (hN : 2 ≤ N) (θ : ℝ) :
105     limsup (fun r : ℝ => Real.log ‖canonicalSignedDenominator N ((r : ℂ) * rayDirection θ)‖ / r) atTop =
106       signedIndicator N (by omega) θ := by
107   obtain ⟨r, hr, hf, _⟩ := canonicalSignedDenominator_indicator_sequence (show 0 < N by omega) θ
108   exact limsup_eq_of_upper_and_sequence
109     ((eventually_gt_atTop (0 : ℝ)).mono (fun r hr => canonicalSignedDenominator_log_indicator_upper hN θ hr)) hr hf
110 
111 /-- The same indicator on the classical logarithm domain. This avoids relying
112 on Lean's totalized value of log(0) at zeros along a ray. -/
113 theorem canonicalSignedDenominator_indicator_nonzero_radii {N : ℕ} (hN : 2 ≤ N) (θ : ℝ) :
114     limsup (fun r : ℝ => Real.log ‖canonicalSignedDenominator N ((r : ℂ) * rayDirection θ)‖ / r)
115       (atTop ⊓ principal {r : ℝ | canonicalSignedDenominator N ((r : ℂ) * rayDirection θ) ≠ 0}) =
116       signedIndicator N (by omega) θ := by
117   obtain ⟨r, hr, hf, hn⟩ := canonicalSignedDenominator_indicator_sequence (show 0 < N by omega) θ
118   apply limsup_eq_of_upper_and_sequence _ (tendsto_inf.mpr ⟨hr, tendsto_principal.mpr hn⟩) hf
119   exact ((eventually_gt_atTop (0 : ℝ)).mono
120     (fun r hr => canonicalSignedDenominator_log_indicator_upper hN θ hr)).filter_mono inf_le_left
121 
122 end
123 end Komorebi.PaperIV

Back to source controls