BranchingDimension.lean

1 import PaperX.Singular
2 import Mathlib.Analysis.SpecialFunctions.Log.Basic
3 import Mathlib.Analysis.SpecificLimits.Basic
4 
5 /-! The manuscript's branching dimension is a finite-level counting exponent.
6 It is not the cardinality or dimension of the set of infinite compatible roots. -/
7 set_option autoImplicit false
8 namespace PaperX.BranchingDimension
9 open Filter Topology
10 
11 theorem ceil_ratio_bounds (m e : ℕ) (he : 0 < e) :
12     (m : ℝ) / e ≤ (m ⌈/⌉ e : ℕ) ∧
13     ((m ⌈/⌉ e : ℕ) : ℝ) ≤ (m : ℝ) / e + 1 := by
14   have heR : 0 < (e : ℝ) := by exact_mod_cast he
15   have hl : m ≤ e * (m ⌈/⌉ e) := le_smul_ceilDiv he
16   have hu : e * (m ⌈/⌉ e) ≤ m+e := by
17     have H := Nat.div_mul_le_self (m+e-1) e
18     rw [Nat.ceilDiv_eq_add_pred_div]
19     nlinarith [Nat.sub_le (m+e) 1]
20   have hlR : (m : ℝ) ≤ (e : ℝ) * (m ⌈/⌉ e : ℕ) := by exact_mod_cast hl
21   have huR : (e : ℝ) * (m ⌈/⌉ e : ℕ) ≤ (m : ℝ)+e := by exact_mod_cast hu
22   constructor
23   · exact (div_le_iff₀ heR).mpr (by nlinarith)
24   · calc
25       ((m ⌈/⌉ e : ℕ) : ℝ) ≤ ((m : ℝ)+e)/e :=
26         (le_div_iff₀ heR).mpr (by nlinarith)
27       _ = (m : ℝ)/e+1 := by rw [add_div, div_self (ne_of_gt heR)]
28 
29 theorem ceil_ratio_limit (e : ℕ) (he : 0 < e) :
30     Tendsto (fun m : ℕ => ((m ⌈/⌉ e : ℕ) : ℝ) / m) atTop (𝓝 (1/(e : ℝ))) := by
31   have heR : (e : ℝ) ≠ 0 := by exact_mod_cast Nat.ne_of_gt he
32   have hu : Tendsto (fun m : ℕ => 1/(e : ℝ)+1/(m : ℝ)) atTop (𝓝 (1/(e : ℝ))) := by
33     simpa only [add_zero] using
34       ((tendsto_const_nhds (x := 1/(e : ℝ))).add (tendsto_one_div_atTop_nhds_zero_nat (𝕜 := ℝ)))
35   apply tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds hu
36   · refine eventually_atTop.mpr ⟨1, fun m hm => ?_⟩
37     have hmR : 0 < (m : ℝ) := by exact_mod_cast (by omega : 0 < m)
38     calc
39       1/(e : ℝ) = ((m : ℝ)/e)/m := by field_simp
40       _ ≤ ((m ⌈/⌉ e : ℕ) : ℝ)/m :=
41         div_le_div_of_nonneg_right (ceil_ratio_bounds m e he).1 (le_of_lt hmR)
42   · refine eventually_atTop.mpr ⟨1, fun m hm => ?_⟩
43     have hmR : 0 < (m : ℝ) := by exact_mod_cast (by omega : 0 < m)
44     calc
45       ((m ⌈/⌉ e : ℕ) : ℝ)/m ≤ ((m : ℝ)/e+1)/m :=
46         div_le_div_of_nonneg_right (ceil_ratio_bounds m e he).2 (le_of_lt hmR)
47       _ = 1/(e : ℝ)+1/m := by field_simp
48 
49 /-- The actual logarithmic limit, not merely an estimate from fitted counts. -/
50 theorem power_count_dimension (q e : ℕ) (hq : 1 < q) (he : 0 < e) :
51     Tendsto (fun m : ℕ => Real.log ((q : ℝ)^(m - (m ⌈/⌉ e))) /
52       Real.log (q : ℝ) / m) atTop (𝓝 (1-1/(e : ℝ))) := by
53   have hqR : Real.log (q : ℝ) ≠ 0 := (Real.log_pos (by exact_mod_cast hq)).ne'
54   have h := (tendsto_const_nhds (x := (1 : ℝ))).sub (ceil_ratio_limit e he)
55   apply h.congr'
56   refine eventually_atTop.mpr ⟨1, fun m hm => ?_⟩
57   have hmR : (m : ℝ) ≠ 0 := by exact_mod_cast (by omega : m ≠ 0)
58   dsimp only
59   rw [Real.log_pow, mul_div_cancel_right₀ _ hqR,
60     Nat.cast_sub (PaperX.Singular.ceil_threshold_le m e he)]
61   field_simp
62 
63 variable {O : Type*} [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]
64 variable [Finite (O ⧸ IsLocalRing.maximalIdeal O)]
65 
66 /-- Paper X 6.6, using cardinalities of actual roots over a general finite-residue DVR. -/
67 theorem actual_singular_dimension (e : ℕ) (he : 0 < e) :
68     Tendsto (fun m : ℕ => Real.log (Nat.card (PaperX.Singular.Roots (O := O) m e) : ℝ) /
69       Real.log (Nat.card (O ⧸ IsLocalRing.maximalIdeal O) : ℝ) / m)
70       atTop (𝓝 (1-1/(e : ℝ))) := by
71   convert power_count_dimension (Nat.card (O ⧸ IsLocalRing.maximalIdeal O)) e
72     Finite.one_lt_card he using 1
73   ext m
74   rw [PaperX.Singular.singular_root_count m e he, Nat.cast_pow]
75 
76 end PaperX.BranchingDimension

Back to source controls