DyadicStepAmplification.lean

1 module
2 public import StepAmplification
3 public import DyadicFourCongruences
4 @[expose] public section
5 noncomputable section
6 set_option autoImplicit false
7 namespace KomorebiPaperIX.DyadicStepAmplification
8 open Mahler DyadicFourCongruences
9 
10 /-- Every power of two in the natural step increases the per-difference precision,
11 up to the previously proved dyadic row cap. Zero step is included. -/
12 theorem normalized_bound (j u k n : ℕ) (hj : j<4) :
13     (2:ℤ_[2])^(min (k*(padicValNat 2 u+1)) n) ∣
14       difference u k (normalizedLift j hj) n := by
15   have H := StepAmplification.repeated_precision 2 (normalizedLift j hj) 1 n u n
16     (fun a => base_step_bound j a n hj) k
17   simpa only [Nat.cast_ofNat,mul_one] using H
18 
19 /-- The displacement strengthening for the original rational normalized Euler coefficients. -/
20 theorem normalized_precision (j u k n : ℕ) (hj : j<4) :
21     GlobalEulerBoundary.precision 2 ((min (k*(padicValNat 2 u+1)) n:ℕ):ℤ)
22       (difference u k (Congruential.coeff 4 j) n) :=
23   StandardWindowPrecision.rational_precision_of_divisibility 2
24     (difference u k (normalizedLift j hj) n) _ (normalized_difference_coe j u k n hj)
25     _ (normalized_bound j u k n hj)
26 
27 /-- Specializing to step u 2^s supplies at least s+1 digits per difference. -/
28 theorem prime_power_step_bound (j u s k n : ℕ) (hj : j<4) :
29     (2:ℤ_[2])^(min (k*(s+1)) n) ∣
30       difference (2^s*u) k (normalizedLift j hj) n := by
31   have H := StepAmplification.repeated_precision 2 (normalizedLift j hj) u n (2^s) n
32     (fun a => DyadicFourCongruences.normalized_bound j u a n hj) k
33   simpa only [Nat.cast_ofNat,padicValNat.prime_pow] using H
34 
35 /-- The higher-address factorial gain remains visible after step amplification. -/
36 theorem unnormalized_factorial_bound (j u k n : ℕ) (hj : j<4) :
37     (2:ℤ_[2])^(min (k*(padicValNat 2 u+1)) n+padicValNat 2 j.factorial) ∣
38       difference u k (unnormalizedLift j hj) n := by
39   have hf : (2:ℤ_[2])^(padicValNat 2 j.factorial) ∣ (j.factorial:ℤ_[2]) := by
40     obtain ⟨c,hc⟩ := pow_padicValNat_dvd (p:=2) (n:=j.factorial)
41     refine ⟨(c:ℤ_[2]), ?_⟩
42     simpa only [Nat.cast_mul,Nat.cast_pow,Nat.cast_ofNat] using congrArg (fun a:ℕ => (a:ℤ_[2])) hc
43   have he : difference u k (unnormalizedLift j hj) n =
44       (j.factorial:ℤ_[2])*difference u k (normalizedLift j hj) n := by
45     exact congrFun (difference_mul_const u k (j.factorial:ℤ_[2]) (normalizedLift j hj)) n
46   rw [he,pow_add]
47   simpa only [mul_comm] using mul_dvd_mul hf (normalized_bound j u k n hj)
48 
49 /-- Strengthened precision stated directly on j! C_(4,j), including its factorial digit. -/
50 theorem unnormalized_factorial_precision (j u k n : ℕ) (hj : j<4) :
51     GlobalEulerBoundary.precision 2
52       ((min (k*(padicValNat 2 u+1)) n+padicValNat 2 j.factorial:ℕ):ℤ)
53       (difference u k (Congruential.unnormalized 4 j) n) :=
54   StandardWindowPrecision.rational_precision_of_divisibility 2
55     (difference u k (unnormalizedLift j hj) n) _ (unnormalized_difference_coe j u k n hj)
56     _ (unnormalized_factorial_bound j u k n hj)
57 
58 end KomorebiPaperIX.DyadicStepAmplification

Back to source controls