UniformDominantSectors.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.IndicatorGeometry
6 
7 namespace Komorebi.PaperIV
8 noncomputable section
9 open Set Filter
10 open scoped Topology
11 
12 theorem range_erase_nonempty {N : ℕ} (hN : 2 ≤ N) (k : ℕ) :
13     ((Finset.range N).erase k).Nonempty := by
14   by_cases hk : k = 0
15   · exact ⟨1, by simp [hk]; omega⟩
16   · exact ⟨0, by simp [Ne.symm hk]; omega⟩
17 
18 def vertexProjectionGap (N : ℕ) (hN : 2 ≤ N) (k : ℕ) (θ : ℝ) : ℝ :=
19   ((Finset.range N).erase k).inf' (range_erase_nonempty hN k)
20     (fun l => signedProjection N θ k - signedProjection N θ l)
21 
22 def directionSeparation (N : ℕ) (hN : 2 ≤ N) (θ : ℝ) : ℝ :=
23   (Finset.range N).sup' ⟨0, Finset.mem_range.mpr (by omega)⟩
24     (fun k => vertexProjectionGap N hN k θ)
25 
26 theorem continuous_vertexProjectionGap (N : ℕ) (hN : 2 ≤ N) (k : ℕ) :
27     Continuous (vertexProjectionGap N hN k) :=
28   Continuous.finset_inf'_apply _ (fun l _ => (continuous_signedProjection N k).sub (continuous_signedProjection N l))
29 
30 theorem continuous_directionSeparation (N : ℕ) (hN : 2 ≤ N) :
31     Continuous (directionSeparation N hN) :=
32   Continuous.finset_sup'_apply _ (fun k _ => continuous_vertexProjectionGap N hN k)
33 
34 theorem directionSeparation_pos {N : ℕ} (hN : 2 ≤ N) {θ : ℝ}
35     (hθ : ¬signedTieDirection N θ) : 0 < directionSeparation N hN θ := by
36   obtain ⟨k, hk, he⟩ := (Finset.range N).exists_mem_eq_sup'
37     ⟨0, Finset.mem_range.mpr (show 0 < N by omega)⟩ (signedProjection N θ)
38   have hgap : 0 < vertexProjectionGap N hN k θ := by
39     apply (Finset.lt_inf'_iff _).mpr
40     intro l hl
41     apply sub_pos.mpr
42     apply signed_maximizer_strict_of_not_tie (show 0 < N by omega) (norm_rayDirection θ)
43       (fun ht => hθ ((signedTieDirection_iff (by omega) θ).mpr ht)) (Finset.mem_range.mp hk)
44       (fun j hj => (signedProjection_le_indicator (by omega) hj θ).trans_eq he)
45       (Finset.mem_range.mp (Finset.mem_erase.mp hl).2) (Finset.mem_erase.mp hl).1
46   exact hgap.trans_le ((Finset.range N).le_sup' (fun j => vertexProjectionGap N hN j θ) hk)
47 
48 /-- Compactness provides a common strictly positive projection gap. -/
49 theorem compact_directions_uniform_gap {N : ℕ} (hN : 2 ≤ N) {K : Set ℝ}
50     (hK : IsCompact K) (hnt : ∀ θ ∈ K, ¬signedTieDirection N θ) :
51     ∃ δ : ℝ, 0 < δ ∧ ∀ θ ∈ K, ∃ k < N,
52       ∀ l ∈ (Finset.range N).erase k, δ ≤ signedProjection N θ k - signedProjection N θ l := by
53   by_cases hne : K.Nonempty
54   · obtain ⟨θ₀, hθ₀, hmin⟩ := hK.exists_isMinOn hne (continuous_directionSeparation N hN).continuousOn
55     refine ⟨directionSeparation N hN θ₀, directionSeparation_pos hN (hnt θ₀ hθ₀), ?_⟩
56     intro θ hθ
57     obtain ⟨k, hk, he⟩ := (Finset.range N).exists_mem_eq_sup'
58       ⟨0, Finset.mem_range.mpr (show 0 < N by omega)⟩ (fun k => vertexProjectionGap N hN k θ)
59     refine ⟨k, Finset.mem_range.mp hk, fun l hl => ?_⟩
60     have hh : directionSeparation N hN θ₀ ≤ vertexProjectionGap N hN k θ := (hmin hθ).trans_eq he
61     exact hh.trans (((Finset.range N).erase k).inf'_le _ hl)
62   · exact ⟨1, by norm_num, by simp [Set.not_nonempty_iff_eq_empty.mp hne]⟩
63 
64 /-- Explicit uniform error bound for the normalized denominator. -/
65 theorem canonicalSignedDenominator_dominant_error {N k : ℕ} (hN : 0 < N) (hk : k < N)
66     {θ δ r : ℝ} (hr : 0 ≤ r)
67     (hgap : ∀ l ∈ (Finset.range N).erase k, δ ≤ signedProjection N θ k - signedProjection N θ l) :
68     ‖(N : ℂ) * Complex.exp (-(canonicalSignedVertex N k * ((r : ℂ) * rayDirection θ))) *
69       canonicalSignedDenominator N ((r : ℂ) * rayDirection θ) - 1‖ ≤
70       ((N - 1 : ℕ) : ℝ) * Real.exp (-δ * r) := by
71   have he : (N : ℂ) * Complex.exp (-(canonicalSignedVertex N k * ((r : ℂ) * rayDirection θ))) *
72       canonicalSignedDenominator N ((r : ℂ) * rayDirection θ) =
73       Complex.exp (-(canonicalSignedVertex N k * ((r : ℂ) * rayDirection θ))) *
74       ∑ l ∈ Finset.range N, Complex.exp (canonicalSignedVertex N l * ((r : ℂ) * rayDirection θ)) := by
75     unfold canonicalSignedDenominator
76     rw [entireSigned_zero_eq_average]
77     have hn : (N : ℂ) ≠ 0 := by exact_mod_cast hN.ne'
78     dsimp [canonicalSignedVertex]
79     field_simp
80   rw [he]
81   have h := finite_exponential_dominant_bound (a := canonicalSignedVertex N) (u := rayDirection θ) (δ := δ) (Finset.mem_range.mpr hk) hr
82     (fun l hl => by
83       rw [sub_mul, Complex.sub_re]
84       have hh := hgap l hl
85       dsimp [signedProjection] at hh
86       linarith)
87   simpa only [Finset.card_erase_of_mem (Finset.mem_range.mpr hk), Finset.card_range] using h
88 
89 /-- The uniform dominant-sector and eventual zero-free clauses of Theorem 11.4. -/
90 theorem canonicalSignedDenominator_compact_dominant_sectors {N : ℕ} (hN : 2 ≤ N)
91     {K : Set ℝ} (hK : IsCompact K) (hnt : ∀ θ ∈ K, ¬signedTieDirection N θ) :
92     ∃ δ : ℝ, 0 < δ ∧ ∃ R : ℝ, 0 < R ∧ ∀ θ ∈ K, ∃ k < N,
93       ∀ r : ℝ, R ≤ r →
94         ‖(N : ℂ) * Complex.exp (-(canonicalSignedVertex N k * ((r : ℂ) * rayDirection θ))) *
95           canonicalSignedDenominator N ((r : ℂ) * rayDirection θ) - 1‖ ≤
96           ((N - 1 : ℕ) : ℝ) * Real.exp (-δ * r) ∧
97         canonicalSignedDenominator N ((r : ℂ) * rayDirection θ) ≠ 0 := by
98   obtain ⟨δ, hδ, hgap⟩ := compact_directions_uniform_gap hN hK hnt
99   have ht : Tendsto (fun r : ℝ => ((N - 1 : ℕ) : ℝ) * Real.exp (-δ * r)) atTop (𝓝 0) := by
100     simpa only [mul_zero, Function.comp_apply, id_eq, neg_mul] using
101       (Real.tendsto_exp_neg_atTop_nhds_zero.comp (tendsto_id.const_mul_atTop hδ)).const_mul ((N - 1 : ℕ) : ℝ)
102   obtain ⟨R, hR⟩ := eventually_atTop.mp (ht.eventually (eventually_lt_nhds (by norm_num : (0 : ℝ) < 1)))
103   refine ⟨δ, hδ, max 1 R, lt_of_lt_of_le zero_lt_one (le_max_left _ _), fun θ hθ => ?_⟩
104   obtain ⟨k, hk, hkgap⟩ := hgap θ hθ
105   refine ⟨k, hk, fun r hr => ?_⟩
106   have hr0 : 0 ≤ r := le_trans (by norm_num) ((le_max_left _ _).trans hr)
107   have hb := canonicalSignedDenominator_dominant_error (by omega) hk hr0 hkgap
108   refine ⟨hb, fun hz => ?_⟩
109   rw [hz, mul_zero, zero_sub, norm_neg, norm_one] at hb
110   exact (not_lt_of_ge hb) (hR r ((le_max_right _ _).trans hr))
111 
112 end
113 end Komorebi.PaperIV

Back to source controls