AllResidueStepAmplification.lean

1 module
2 public import StepAmplification
3 public import AllResidueEuler
4 @[expose] public section
5 noncomputable section
6 set_option autoImplicit false
7 namespace KomorebiPaperIX.AllResidueStepAmplification
8 open Mahler AllResidueEuler GlobalEulerBoundary
9 variable (p : ℕ) [Fact p.Prime]
10 
11 /-- Step-sensitive ideal divisibility for every actual residue on the divisor branch. -/
12 theorem unnormalized_bound (m j u k n : ℕ)
13     (hm : m∣p-1) (hmpos : 0<m) (hj : j<m*p) :
14     (p:ℤ_[p])^(min (k*(padicValNat p u+1)) (m*n)) ∣
15       difference (u*((p-1)/m)) k (unnormalizedLift p m j hm hmpos hj) n := by
16   exact StepAmplification.repeated_precision p (unnormalizedLift p m j hm hmpos hj)
17     ((p-1)/m) n u (m*n) (fun a => by
18       simpa only [one_mul] using global_unnormalized_bound p m j 1 a n hm hmpos hj) k
19 
20 /-- The bound is on the same original rational coefficients as the completed theorem. -/
21 theorem unnormalized_precision (m j u k n : ℕ)
22     (hm : m∣p-1) (hmpos : 0<m) (hj : j<m*p) :
23     precision p ((min (k*(padicValNat p u+1)) (m*n):ℕ):ℤ)
24       (difference (u*((p-1)/m)) k (Congruential.unnormalized (m*p) j) n) := by
25   apply StandardWindowPrecision.rational_precision_of_divisibility p
26     (difference (u*((p-1)/m)) k (unnormalizedLift p m j hm hmpos hj) n)
27   · change (algebraMap ℤ_[p] ℚ_[p]) (difference _ _ _ _) =
28       (algebraMap ℚ ℚ_[p]) (difference _ _ _ _)
29     rw [←DifferenceFiltration.difference_map,←DifferenceFiltration.difference_map]
30     congr 1
31     funext r
32     exact unnormalizedLift_coe p m j r hm hmpos hj
33   · exact unnormalized_bound p m j u k n hm hmpos hj
34 
35 /-- Normalization on this branch retains the factorial loss already required by the baseline. -/
36 theorem normalized_precision (m j u k n : ℕ)
37     (hm : m∣p-1) (hmpos : 0<m) (hj : j<m*p) :
38     precision p (((min (k*(padicValNat p u+1)) (m*n):ℕ):ℤ)-padicValNat p j.factorial)
39       (difference (u*((p-1)/m)) k (Congruential.coeff (m*p) j) n) :=
40   factorial_loss_transfer p (m*p) j _ k n _
41     (unnormalized_precision p m j u k n hm hmpos hj)
42 
43 end KomorebiPaperIX.AllResidueStepAmplification

Back to source controls