DyadicFourFinalStrengthening.lean

1 module
2 public import DyadicFourAllRows
3 public import StepAmplification
4 public import DyadicFourSharpening
5 @[expose] public section
6 noncomputable section
7 set_option autoImplicit false
8 namespace KomorebiPaperIX.DyadicFourFinalStrengthening
9 open Mahler DyadicFourCongruences
10 
11 /-- Step-sensitive precision at every row, with no saturation cap. -/
12 theorem normalized_step_bound (j u k n : ℕ) (hj : j < 4) :
13     (2 : ℤ_[2]) ^ (k * (padicValNat 2 u + 1)) ∣
14       difference u k (normalizedLift j hj) n := by
15   have H := StepAmplification.repeated_precision 2 (normalizedLift j hj) 1 n u
16     (k * (padicValNat 2 u + 1)) (fun a =>
17       dvd_trans (pow_dvd_pow _ (min_le_left _ _))
18         (DyadicFourAllRows.base_step_bound j a n hj)) k
19   simpa only [Nat.cast_ofNat, mul_one, min_self] using H
20 
21 theorem normalized_step_precision (j u k n : ℕ) (hj : j < 4) :
22     GlobalEulerBoundary.precision 2 ((k * (padicValNat 2 u + 1) : ℕ) : ℤ)
23       (difference u k (Congruential.coeff 4 j) n) :=
24   StandardWindowPrecision.rational_precision_of_divisibility 2
25     (difference u k (normalizedLift j hj) n) _ (normalized_difference_coe j u k n hj)
26     _ (normalized_step_bound j u k n hj)
27 
28 /-- The original coefficients gain their full address-factorial valuation at every row. -/
29 theorem unnormalized_step_bound (j u k n : ℕ) (hj : j < 4) :
30     (2 : ℤ_[2]) ^ (k * (padicValNat 2 u + 1) + padicValNat 2 j.factorial) ∣
31       difference u k (unnormalizedLift j hj) n := by
32   have hf : (2 : ℤ_[2]) ^ (padicValNat 2 j.factorial) ∣ (j.factorial : ℤ_[2]) := by
33     obtain ⟨c, hc⟩ := pow_padicValNat_dvd (p := 2) (n := j.factorial)
34     refine ⟨(c : ℤ_[2]), ?_⟩
35     simpa only [Nat.cast_mul, Nat.cast_pow, Nat.cast_ofNat] using
36       congrArg (fun a : ℕ => (a : ℤ_[2])) hc
37   rw [DyadicFourSharpening.unnormalized_difference_factorial, pow_add]
38   simpa only [mul_comm] using mul_dvd_mul hf (normalized_step_bound j u k n hj)
39 
40 theorem unnormalized_step_precision (j u k n : ℕ) (hj : j < 4) :
41     GlobalEulerBoundary.precision 2
42       ((k * (padicValNat 2 u + 1) + padicValNat 2 j.factorial : ℕ) : ℤ)
43       (difference u k (Congruential.unnormalized 4 j) n) :=
44   StandardWindowPrecision.rational_precision_of_divisibility 2
45     (difference u k (unnormalizedLift j hj) n) _ (unnormalized_difference_coe j u k n hj)
46     _ (unnormalized_step_bound j u k n hj)
47 
48 /-- The normalized dyadic period is valid starting at row zero. -/
49 theorem normalized_period (j r n : ℕ) (hj : j < 4) (hr : 0 < r) :
50     (2 : ℤ_[2]) ^ r ∣ normalizedLift j hj (n + 2 ^ (r - 1)) - normalizedLift j hj n := by
51   have H := PeriodFromDifferences.prime_power_period 2 (normalizedLift j hj) 1 n r hr
52     (fun k => dvd_trans (pow_dvd_pow _ (min_le_left _ _))
53       (DyadicFourAllRows.base_step_bound j k n hj))
54   simpa only [Nat.cast_ofNat, mul_one] using H
55 
56 /-- All four original packets have the conjectured period at every row. -/
57 theorem all_rows_period (j r n : ℕ) (hj : j < 4) (hr : 0 < r) :
58     (2 : ℤ_[2]) ^ r ∣ unnormalizedLift j hj (n + 2 ^ (r - 1)) - unnormalizedLift j hj n := by
59   simpa only [unnormalizedLift, mul_sub] using
60     dvd_mul_of_dvd_right (normalized_period j r n hj hr) (j.factorial : ℤ_[2])
61 
62 theorem all_rows_period_precision (j r n : ℕ) (hj : j < 4) (hr : 0 < r) :
63     GlobalEulerBoundary.precision 2 (r : ℤ)
64       (Congruential.unnormalized 4 j (n + 2 ^ (r - 1)) - Congruential.unnormalized 4 j n) := by
65   apply StandardWindowPrecision.rational_precision_of_divisibility 2
66     (unnormalizedLift j hj (n + 2 ^ (r - 1)) - unnormalizedLift j hj n)
67   · simp only [PadicInt.coe_sub, unnormalizedLift_coe, Rat.cast_sub]
68   · exact all_rows_period j r n hj hr
69 
70 /-- Literal original degree statement, with no lower bound on the packet row. -/
71 theorem all_rows_period_degree (j r n : ℕ) (hj : j < 4) (hr : 0 < r) :
72     GlobalEulerBoundary.precision 2 (r : ℤ)
73       (NishibuchiCompletion.generalizedEuler 4 (by decide) j (4 * n + 2 ^ (r + 1)) -
74        NishibuchiCompletion.generalizedEuler 4 (by decide) j (4 * n)) := by
75   have he : 4 * (n + 2 ^ (r - 1)) = 4 * n + 2 ^ (r + 1) := by
76     have hp : 2 ^ (r + 1) = 2 ^ (r - 1) * 2 ^ 2 := by
77       rw [← pow_add]
78       congr 1
79       omega
80     rw [hp]
81     ring
82   rw [← he, NishibuchiCompletion.generalizedEuler_at_packet,
83     NishibuchiCompletion.generalizedEuler_at_packet]
84   exact all_rows_period_precision j r n hj hr
85 
86 /-- The higher-address half period also starts at row zero. -/
87 theorem all_rows_half_period (j r n : ℕ) (hj : j < 4) (hj2 : 2 ≤ j) (hr : 2 ≤ r) :
88     (2 : ℤ_[2]) ^ r ∣ unnormalizedLift j hj (n + 2 ^ (r - 2)) - unnormalizedLift j hj n := by
89   have h := mul_dvd_mul (DyadicFourSharpening.factorial_even j hj hj2)
90     (normalized_period j (r - 1) n hj (by omega))
91   have he : (2 : ℤ_[2]) * 2 ^ (r - 1) = 2 ^ r := by
92     rw [← pow_succ']
93     congr 1
94     omega
95   have he' : r - 1 - 1 = r - 2 := by omega
96   rw [he, he'] at h
97   simpa only [unnormalizedLift, mul_sub] using h
98 
99 theorem all_rows_half_period_precision (j r n : ℕ) (hj : j < 4)
100     (hj2 : 2 ≤ j) (hr : 2 ≤ r) :
101     GlobalEulerBoundary.precision 2 (r : ℤ)
102       (Congruential.unnormalized 4 j (n + 2 ^ (r - 2)) - Congruential.unnormalized 4 j n) := by
103   apply StandardWindowPrecision.rational_precision_of_divisibility 2
104     (unnormalizedLift j hj (n + 2 ^ (r - 2)) - unnormalizedLift j hj n)
105   · simp only [PadicInt.coe_sub, unnormalizedLift_coe, Rat.cast_sub]
106   · exact all_rows_half_period j r n hj hj2 hr
107 
108 theorem all_rows_half_period_degree (j r n : ℕ) (hj : j < 4)
109     (hj2 : 2 ≤ j) (hr : 2 ≤ r) :
110     GlobalEulerBoundary.precision 2 (r : ℤ)
111       (NishibuchiCompletion.generalizedEuler 4 (by decide) j (4 * n + 2 ^ r) -
112        NishibuchiCompletion.generalizedEuler 4 (by decide) j (4 * n)) := by
113   have he : 4 * (n + 2 ^ (r - 2)) = 4 * n + 2 ^ r := by
114     have hp : 2 ^ r = 2 ^ (r - 2) * 2 ^ 2 := by
115       rw [← pow_add, Nat.sub_add_cancel hr]
116     rw [hp]
117     ring
118   rw [← he, NishibuchiCompletion.generalizedEuler_at_packet,
119     NishibuchiCompletion.generalizedEuler_at_packet]
120   exact all_rows_half_period_precision j r n hj hj2 hr
121 
122 end KomorebiPaperIX.DyadicFourFinalStrengthening

Back to source controls