CountErrorBoundary.lean

1 import Mathlib.Analysis.PSeries
2 import Mathlib.Analysis.Asymptotics.SpecificAsymptotics
3 import Mathlib.Analysis.SpecialFunctions.Log.Basic
4 import Mathlib.Tactic
5 
6 /-! A qualitative zero-mean counting error does not imply convergence of
7 its Dirichlet series at one. This is a counterexample to that analytic
8 inference, not a statement about the actual arithmetic ray-class errors. -/
9 set_option autoImplicit false
10 noncomputable section
11 namespace PaperX.CountErrorBoundary
12 open Filter Finset
13 open scoped Topology
14 
15 def coefficient (n : ℕ) : ℝ := (Real.log (n : ℝ))⁻¹
16 def weighted (n : ℕ) : ℝ := coefficient n / n
17 
18 theorem coefficient_tendsto_zero : Tendsto coefficient atTop (𝓝 0) := by
19   exact tendsto_inv_atTop_zero.comp
20     (Real.tendsto_log_atTop.comp tendsto_natCast_atTop_atTop)
21 
22 /-- The summatory coefficients have size o(N), expressed as a normalized limit. -/
23 theorem summatory_div_tendsto_zero :
24     Tendsto (fun N : ℕ => (∑ n ∈ range N, coefficient n) / N) atTop (𝓝 0) := by
25   simpa only [div_eq_mul_inv, mul_comm] using coefficient_tendsto_zero.cesaro
26 
27 theorem weighted_eventually_nonneg : 0 ≤ᶠ[atTop] weighted := by
28   filter_upwards [eventually_ge_atTop 2] with n hn
29   have hnr : (1 : ℝ) ≤ n := by exact_mod_cast (show 1 ≤ n by omega)
30   exact div_nonneg (inv_nonneg.mpr (Real.log_nonneg hnr)) (Nat.cast_nonneg n)
31 
32 theorem weighted_eventually_antitone :
33     ∀ᶠ n in atTop, weighted (n + 1) ≤ weighted n := by
34   filter_upwards [eventually_ge_atTop 2] with n hn
35   have hn0 : (0 : ℝ) < n := by exact_mod_cast (show 0 < n by omega)
36   have hn1 : (1 : ℝ) < n := by exact_mod_cast (show 1 < n by omega)
37   have hlog := Real.log_pos hn1
38   have hle : (n : ℝ) ≤ n + 1 := by linarith
39   have hlogle := Real.log_le_log hn0 hle
40   simp only [weighted, coefficient, Nat.cast_add, Nat.cast_one,
41     div_eq_mul_inv, ← mul_inv_rev]
42   apply inv_anti₀
43   · exact mul_pos hn0 hlog
44   · exact mul_le_mul hle hlogle hlog.le (by positivity)
45 
46 theorem condensed_identity (k : ℕ) :
47     Real.log 2 * ((2 : ℝ) ^ k * weighted (2 ^ k)) = (k : ℝ)⁻¹ := by
48   have hlog : Real.log 2 ≠ 0 := ne_of_gt (Real.log_pos (by norm_num))
49   have hpow : (2 : ℝ) ^ k ≠ 0 := pow_ne_zero k (by norm_num)
50   by_cases hk : k = 0
51   · simp [hk, weighted, coefficient]
52   have hkR : (k : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr hk
53   simp only [weighted, coefficient, Nat.cast_pow, Nat.cast_ofNat, Real.log_pow]
54   field_simp
55 
56 /-- Nevertheless the positive Dirichlet series at s=1 is nonsummable. -/
57 theorem weighted_not_summable : ¬ Summable weighted := by
58   intro h
59   have hc := (summable_condensed_iff_of_eventually_nonneg
60     weighted_eventually_nonneg weighted_eventually_antitone).mpr h
61   have hs := hc.mul_left (Real.log 2)
62   exact Real.not_summable_natCast_inv (hs.congr condensed_identity)
63 
64 /-- Therefore normalized summatory convergence alone cannot justify the
65 claimed s=1 convergence for all real coefficient sequences. -/
66 theorem qualitative_counting_does_not_imply_convergence :
67     ¬ (∀ a : ℕ → ℝ,
68       Tendsto (fun N : ℕ => (∑ n ∈ range N, a n) / N) atTop (𝓝 0) →
69       Summable (fun n => a n / n)) := by
70   intro h
71   exact weighted_not_summable (h coefficient summatory_div_tendsto_zero)
72 
73 end PaperX.CountErrorBoundary

Back to source controls