DyadicSharpTower.lean

1 module
2 
3 public import DyadicReconstruction
4 public import Mathlib.NumberTheory.Bernoulli
5 public import Mathlib.RingTheory.PowerSeries.Derivative
6 
7 @[expose] public section
8 noncomputable section
9 set_option autoImplicit false
10 
11 namespace KomorebiPaperIX.DyadicSharpTower
12 
13 open PowerSeries OddPower KomorebiPaperIX.Dyadic KomorebiPaperIX.DyadicSeries
14 
15 def cothNormalized : PowerSeries ℚ := rescale 2 (bernoulliPowerSeries ℚ) + X
16 
17 theorem expAt_derivative (a : ℚ) : derivative ℚ (expAt a) = C a * expAt a := by
18   ext n
19   rw [coeff_derivative, expAt_coeff, coeff_C_mul, expAt_coeff]
20   rw [Nat.factorial_succ, pow_succ]
21   push_cast
22   field_simp
23 
24 theorem sinh_derivative : derivative ℚ (sinhAt 1) = coshAt 1 := by
25   simp only [sinhAt, coshAt, Derivation.leibniz, map_sub, derivative_C,
26     smul_eq_mul, mul_zero, add_zero, expAt_derivative, map_one, map_neg]
27   ring
28 
29 theorem cosh_derivative : derivative ℚ (coshAt 1) = sinhAt 1 := by
30   simp only [sinhAt, coshAt, Derivation.leibniz, map_add, derivative_C,
31     smul_eq_mul, mul_zero, add_zero, expAt_derivative, map_one, map_neg]
32   ring
33 
34 theorem hyperbolic_identity : coshAt 1 ^ 2 - sinhAt 1 ^ 2 = 1 := by
35   have hp : expAt 1 * expAt (-1) = 1 := by rw [expAt_mul]; norm_num
36   have hc : C (1/2:ℚ) * C (1/2) * 4 = (1:PowerSeries ℚ) := by
37     have h := congrArg (C (R:=ℚ)) (show (1/2:ℚ)*(1/2)*4=1 by norm_num)
38     simpa only [map_mul, map_ofNat, map_one] using h
39   unfold coshAt sinhAt
40   calc
41     _ = (C (1/2) * C (1/2) * 4) * (expAt 1 * expAt (-1)) := by ring
42     _ = 1 := by rw [hp, hc, mul_one]
43 
44 theorem coth_times_sinh : cothNormalized * sinhAt 1 = X * coshAt 1 := by
45   have hb := congrArg (rescale (2:ℚ)) (bernoulliPowerSeries_mul_exp_sub_one ℚ)
46   simp only [map_mul, map_sub, map_one, rescale_X] at hb
47   change rescale 2 (bernoulliPowerSeries ℚ) * (expAt 2 - 1) = C 2 * X at hb
48   have hp : expAt 2 * expAt (-1) = expAt 1 := by rw [expAt_mul]; norm_num
49   have hh := congrArg (fun f : PowerSeries ℚ => f * expAt (-1)) hb
50   unfold cothNormalized sinhAt coshAt
51   simp only [mul_sub, sub_mul, mul_one, mul_assoc, hp] at hh
52   calc
53     _ = C (1/2) * (rescale 2 (bernoulliPowerSeries ℚ) * expAt 1 -
54       rescale 2 (bernoulliPowerSeries ℚ) * expAt (-1)) +
55       X * C (1/2) * (expAt 1 - expAt (-1)) := by ring
56     _ = _ := by rw [hh]; norm_num only [map_ofNat]; ring
57 
58 theorem inverse_eq_coth_derivative :
59     inverseSeries = cothNormalized - X * derivative ℚ cothNormalized := by
60   have hd := congrArg (derivative ℚ) coth_times_sinh
61   simp only [Derivation.leibniz, sinh_derivative, cosh_derivative, derivative_X,
62     smul_eq_mul, mul_one] at hd
63   have hprod : (cothNormalized - X * derivative ℚ cothNormalized) * sinhAt 1 ^ 2 = X^2 := by
64     linear_combination (sinhAt 1 + X * coshAt 1) * coth_times_sinh -
65       X * sinhAt 1 * hd + X^2 * hyperbolic_identity
66   have hnonzero : sinhAt 1 ^ 2 ≠ 0 := by
67     intro h
68     have hh := beta_original_generating_function
69     rw [h, mul_zero] at hh
70     exact (pow_ne_zero 2 PowerSeries.X_ne_zero) hh.symm
71   exact mul_right_cancel₀ hnonzero (beta_original_generating_function.trans hprod.symm)
72 
73 theorem beta_bernoulli (m : ℕ) (hm : 0 < m) :
74     beta m = -(2^(2*m) * (2*(m:ℚ)-1) * bernoulli (2*m)) / (2*m).factorial := by
75   have h := congrArg (coeff (2*m)) inverse_eq_coth_derivative
76   rw [inverse_even_coefficient, map_sub] at h
77   have hcoef : coeff (2*m) cothNormalized = 2^(2*m) * bernoulli (2*m) / (2*m).factorial := by
78     simp [cothNormalized, coeff_rescale, bernoulliPowerSeries,
79       coeff_X, show 2*m ≠ 1 by omega, mul_div_assoc]
80   have hderiv : coeff (2*m) (X * derivative ℚ cothNormalized) =
81       (2*m:ℚ) * coeff (2*m) cothNormalized := by
82     obtain ⟨k,hk⟩ := Nat.exists_eq_succ_of_ne_zero (by omega : 2*m ≠ 0)
83     have hkq : (2*m:ℚ) = k+1 := by exact_mod_cast hk
84     rw [hk, coeff_succ_X_mul, coeff_derivative, hkq]
85     ring
86   rw [hderiv, hcoef] at h
87   rw [h]
88   ring
89 
90 def kappa (m : ℕ) : ℚ := beta m * 2^(2*m) * (2*m).factorial
91 
92 theorem kappa_bernoulli (m : ℕ) (hm : 0 < m) :
93     kappa m = -(2^(4*m) * (2*(m:ℚ)-1) * bernoulli (2*m)) := by
94   rw [kappa, beta_bernoulli m hm]
95   have hfac : ((2*m).factorial:ℚ) ≠ 0 := by positivity
96   rw [show 4*m=2*m+2*m by omega, pow_add]
97   field_simp
98 
99 theorem odd_factor_valuation (m : ℕ) (hm : 0 < m) :
100     padicValRat 2 (2*(m:ℚ)-1) = 0 := by
101   have he : (2*(m:ℚ)-1) = ((2*m-1:ℕ):ℚ) := by
102     rw [Nat.cast_sub (by omega)]; push_cast; rfl
103   rw [he, padicValRat.of_nat, padicValNat.eq_zero_of_not_dvd (by omega)]
104   rfl
105 
106 theorem bernoulli_dyadic_valuation (m : ℕ) (hm : 0 < m) :
107     padicValRat 2 (bernoulli (2*m)) = -1 :=
108   Bernoulli.padicValRat_bernoulli hm (by norm_num)
109 
110 theorem bernoulli_even_nonzero (m : ℕ) (hm : 0 < m) : bernoulli (2*m) ≠ 0 := by
111   intro h
112   have hv := bernoulli_dyadic_valuation m hm
113   rw [h] at hv
114   norm_num at hv
115 
116 /-- Exact valuation of the genuine weighted inverse coefficient, for every positive depth. -/
117 theorem kappa_valuation (m : ℕ) (hm : 0 < m) :
118     padicValRat 2 (kappa m) = 4*(m:ℤ)-1 := by
119   have ho : 2*(m:ℚ)-1 ≠ 0 := by
120     have hmq : (1:ℚ) ≤ m := by exact_mod_cast hm
121     linarith
122   have ht : padicValRat 2 (2:ℚ) = 1 := padicValRat.self (by decide : 1 < 2)
123   rw [kappa_bernoulli m hm, padicValRat.neg,
124     padicValRat.mul (mul_ne_zero (by positivity) ho) (bernoulli_even_nonzero m hm),
125     padicValRat.mul (by positivity) ho, odd_factor_valuation m hm,
126     bernoulli_dyadic_valuation m hm, padicValRat.pow, ht]
127   push_cast
128   ring
129 
130 theorem kappa_nonzero (m : ℕ) (hm : 0 < m) : kappa m ≠ 0 := by
131   intro h
132   have hv := kappa_valuation m hm
133   rw [h] at hv
134   norm_num at hv
135   omega
136 
137 def kappaPadic (m : ℕ) : ℤ_[2] := betaPadic m * 2^(2*m) * (2*m).factorial
138 
139 theorem kappaPadic_coe (m : ℕ) : (kappaPadic m : ℚ_[2]) = (kappa m : ℚ_[2]) := by
140   simp only [kappaPadic, kappa, PadicInt.coe_mul, PadicInt.coe_pow, PadicInt.coe_natCast,
141     betaPadic_coe, Rat.cast_mul, Rat.cast_pow, Rat.cast_ofNat, Rat.cast_natCast]
142   rfl
143 
144 theorem kappaPadic_norm (m : ℕ) (hm : 0 < m) :
145     ‖kappaPadic m‖ = (2:ℝ)^(-(4*(m:ℤ)-1)) := by
146   rw [PadicInt.norm_def, kappaPadic_coe, Padic.eq_padicNorm,
147     padicNorm.eq_zpow_of_nonzero (kappa_nonzero m hm), kappa_valuation m hm]
148   push_cast
149   rfl
150 
151 theorem kappaPadic_divisible (m : ℕ) (hm : 0 < m) :
152     (2:ℤ_[2])^(4*m-1) ∣ kappaPadic m := by
153   rw [← Ideal.mem_span_singleton]
154   apply (PadicInt.norm_le_pow_iff_mem_span_pow (p:=2) (kappaPadic m) (4*m-1)).mp
155   rw [kappaPadic_norm m hm]
156   have hc : ((4*m-1:ℕ):ℤ) = 4*(m:ℤ)-1 := by
157     rw [Nat.cast_sub (by omega)]; push_cast; rfl
158   rw [hc]
159   norm_num
160 
161 open KomorebiPaperIX.DyadicReconstruction
162 
163 theorem summand_kappa (n m : ℕ) :
164     summand n m = kappa m * ((2*n).choose (2*m):ℚ) * sourceEven (n-m) := by
165   rw [summand, Nat.descFactorial_eq_factorial_mul_choose, kappa]
166   push_cast
167   ring
168 
169 theorem summandPadic_kappa (n m : ℕ) :
170     summandPadic n m = kappaPadic m * ((2*n).choose (2*m):ℤ_[2]) * sourcePadic (n-m) := by
171   rw [summandPadic, Nat.descFactorial_eq_factorial_mul_choose, kappaPadic]
172   push_cast
173   ring
174 
175 /-- The exact dyadic coefficient valuation yields four powers of two per omitted level. -/
176 theorem dyadic_supercongruence_sharp (n M : ℕ) :
177     (2:ℤ_[2])^(4*M+3) ∣ (EulerCoefficients.eulerEven n:ℤ_[2]) - truncationPadic n M := by
178   rw [dyadic_reconstruction_padic, truncationPadic, ← OddEuler.filter_range_le]
179   classical
180   rw [← Finset.sum_filter_add_sum_filter_not (Finset.range (n+1)) (fun m => m ≤ M)
181     (summandPadic n), add_sub_cancel_left]
182   apply Finset.dvd_sum
183   intro m hm
184   obtain ⟨_, hm⟩ := Finset.mem_filter.mp hm
185   have hpos : 0 < m := by omega
186   have hpow : (2:ℤ_[2])^(4*M+3) ∣ (2:ℤ_[2])^(4*m-1) := pow_dvd_pow 2 (by omega)
187   rw [summandPadic_kappa]
188   exact dvd_mul_of_dvd_left (dvd_mul_of_dvd_left
189     (hpow.trans (kappaPadic_divisible m hpos)) _) _
190 
191 /-- The first omitted row has just one nonzero omitted term. -/
192 theorem first_omitted_error (M : ℕ) :
193     (EulerCoefficients.eulerEven (M+1):ℚ) - truncation (M+1) M = kappa (M+1) := by
194   rw [truncation, min_eq_left (by omega), dyadic_reconstruction, Finset.sum_range_succ,
195     add_sub_cancel_left, summand_kappa, Nat.choose_self, Nat.sub_self]
196   norm_num [sourceEven]
197 
198 /-- Hence the exponent 4M+3 cannot be increased uniformly in the Euler row. -/
199 theorem first_omitted_error_valuation (M : ℕ) :
200     padicValRat 2 ((EulerCoefficients.eulerEven (M+1):ℚ) - truncation (M+1) M) =
201       4*(M:ℤ)+3 := by
202   rw [first_omitted_error, kappa_valuation (M+1) (by omega)]
203   push_cast
204   ring
205 
206 /-- Exact row-dependent precision of each nonzero positive-depth term. -/
207 theorem summand_valuation (n m : ℕ) (hm : 0 < m) (hmn : m ≤ n) :
208     padicValRat 2 (summand n m) =
209       4*(m:ℤ)-1 + (padicValNat 2 ((2*n).choose (2*m)):ℤ) := by
210   have hc : (((2*n).choose (2*m)):ℚ) ≠ 0 := by
211     exact_mod_cast Nat.ne_of_gt (Nat.choose_pos (by omega : 2*m ≤ 2*n))
212   rw [summand_kappa,
213     padicValRat.mul (mul_ne_zero (kappa_nonzero m hm) hc) (source_nonzero (n-m)),
214     padicValRat.mul (kappa_nonzero m hm) hc,
215     kappa_valuation m hm, source_valuation, padicValRat.of_nat, add_zero]
216 
217 /-- The binomial factor contributes additional row-specific powers of two. -/
218 theorem summandPadic_divisible (n m : ℕ) (hm : 0 < m) :
219     (2:ℤ_[2])^(4*m-1 + padicValNat 2 ((2*n).choose (2*m))) ∣ summandPadic n m := by
220   have hc : (2:ℤ_[2])^(padicValNat 2 ((2*n).choose (2*m))) ∣
221       (((2*n).choose (2*m)):ℤ_[2]) := by
222     have hnat : 2^(padicValNat 2 ((2*n).choose (2*m))) ∣ (2*n).choose (2*m) :=
223       (padicValNat_dvd_iff _ _).mpr (Or.inr le_rfl)
224     obtain ⟨z,hz⟩ := hnat
225     refine ⟨(z:ℤ_[2]), ?_⟩
226     exact_mod_cast hz
227   rw [summandPadic_kappa, pow_add]
228   exact dvd_mul_of_dvd_left (mul_dvd_mul (kappaPadic_divisible m hm) hc) _
229 
230 /-- Any lower bound on the explicit omitted row weights is a valid tail precision. -/
231 theorem dyadic_supercongruence_row_weight (n M L : ℕ)
232     (hL : ∀ m, M < m → m ≤ n → L ≤ 4*m-1 + padicValNat 2 ((2*n).choose (2*m))) :
233     (2:ℤ_[2])^L ∣ (EulerCoefficients.eulerEven n:ℤ_[2]) - truncationPadic n M := by
234   rw [dyadic_reconstruction_padic, truncationPadic, ← OddEuler.filter_range_le]
235   classical
236   rw [← Finset.sum_filter_add_sum_filter_not (Finset.range (n+1)) (fun m => m ≤ M)
237     (summandPadic n), add_sub_cancel_left]
238   apply Finset.dvd_sum
239   intro m hm
240   obtain ⟨hn,hm⟩ := Finset.mem_filter.mp hm
241   have hmn : m ≤ n := by simpa only [Finset.mem_range, Nat.lt_succ_iff] using hn
242   have hmm : M < m := by omega
243   exact (pow_dvd_pow (2:ℤ_[2]) (hL m hmm hmn)).trans
244     (summandPadic_divisible n m (by omega))
245 
246 end KomorebiPaperIX.DyadicSharpTower

Back to source controls