DyadicFourSharpening.lean

1 module
2 public import NishibuchiCompletion
3 @[expose] public section
4 noncomputable section
5 set_option autoImplicit false
6 namespace KomorebiPaperIX.DyadicFourSharpening
7 open Mahler DyadicFourCongruences
8 
9 /-- Addresses two and three have exactly one elementary factorial factor of two. -/
10 theorem factorial_even (j : ℕ) (hj : j < 4) (hj2 : 2 ≤ j) :
11     (2 : ℤ_[2]) ∣ (j.factorial : ℤ_[2]) := by
12   interval_cases j
13   · norm_num
14   · refine ⟨3, ?_⟩
15     norm_num
16 
17 theorem unnormalized_difference_factorial (j u k n : ℕ) (hj : j < 4) :
18     difference u k (unnormalizedLift j hj) n =
19       (j.factorial : ℤ_[2]) * difference u k (normalizedLift j hj) n := by
20   induction k generalizing n with
21   | zero => rfl
22   | succ k ih => rw [difference_succ, ih, ih, difference_succ, mul_sub]
23 
24 /-- The original coefficients at addresses two and three gain one dyadic digit. -/
25 theorem factorial_difference_bound (j u k n : ℕ) (hj : j < 4) (hj2 : 2 ≤ j) :
26     (2 : ℤ_[2]) ^ (1 + min k n) ∣ difference u k (unnormalizedLift j hj) n := by
27   rw [unnormalized_difference_factorial, pow_add, pow_one]
28   exact mul_dvd_mul (factorial_even j hj hj2) (normalized_bound j u k n hj)
29 
30 theorem factorial_difference_precision (j u k n : ℕ) (hj : j < 4) (hj2 : 2 ≤ j) :
31     GlobalEulerBoundary.precision 2 ((1 + min k n : ℕ) : ℤ)
32       (difference u k (Congruential.unnormalized 4 j) n) :=
33   StandardWindowPrecision.rational_precision_of_divisibility 2
34     (difference u k (unnormalizedLift j hj) n) _ (unnormalized_difference_coe j u k n hj)
35     _ (factorial_difference_bound j u k n hj hj2)
36 
37 /-- The period mechanism applies before multiplication by the address factorial. -/
38 theorem normalized_period (j r n : ℕ) (hj : j < 4) (hr : 0 < r) (hn : r ≤ n) :
39     (2 : ℤ_[2]) ^ r ∣ normalizedLift j hj (n + 2 ^ (r - 1)) - normalizedLift j hj n := by
40   have H := PeriodFromDifferences.prime_power_period 2 (normalizedLift j hj) 1 n r hr ?_
41   · simpa only [Nat.cast_ofNat, mul_one] using H
42   · intro k
43     exact dvd_trans (pow_dvd_pow _ (min_le_min_left k hn)) (normalized_bound j 1 k n hj)
44 
45 /-- Half the old packet displacement suffices for addresses two and three.
46 The sufficient starting row improves from r to r-1; no least-period claim. -/
47 theorem half_period (j r n : ℕ) (hj : j < 4) (hj2 : 2 ≤ j)
48     (hr : 2 ≤ r) (hn : r - 1 ≤ n) :
49     (2 : ℤ_[2]) ^ r ∣ unnormalizedLift j hj (n + 2 ^ (r - 2)) - unnormalizedLift j hj n := by
50   have h := mul_dvd_mul (factorial_even j hj hj2)
51     (normalized_period j (r - 1) n hj (by omega) hn)
52   have he : (2 : ℤ_[2]) * 2 ^ (r - 1) = 2 ^ r := by
53     rw [← pow_succ']
54     congr 1
55     omega
56   have he' : r - 1 - 1 = r - 2 := by omega
57   rw [he, he'] at h
58   simpa only [unnormalizedLift, mul_sub] using h
59 
60 theorem half_period_precision (j r n : ℕ) (hj : j < 4) (hj2 : 2 ≤ j)
61     (hr : 2 ≤ r) (hn : r - 1 ≤ n) :
62     GlobalEulerBoundary.precision 2 (r : ℤ)
63       (Congruential.unnormalized 4 j (n + 2 ^ (r - 2)) - Congruential.unnormalized 4 j n) := by
64   apply StandardWindowPrecision.rational_precision_of_divisibility 2
65     (unnormalizedLift j hj (n + 2 ^ (r - 2)) - unnormalizedLift j hj n)
66   · simp only [PadicInt.coe_sub, unnormalizedLift_coe, Rat.cast_sub]
67   · exact half_period j r n hj hj2 hr hn
68 
69 /-- Literal degree displacement 2^r, in place of the original 2^(r+1). -/
70 theorem half_period_degree (j r n : ℕ) (hj : j < 4) (hj2 : 2 ≤ j)
71     (hr : 2 ≤ r) (hn : r - 1 ≤ n) :
72     GlobalEulerBoundary.precision 2 (r : ℤ)
73       (NishibuchiCompletion.generalizedEuler 4 (by decide) j (4 * n + 2 ^ r) -
74        NishibuchiCompletion.generalizedEuler 4 (by decide) j (4 * n)) := by
75   have he : 4 * (n + 2 ^ (r - 2)) = 4 * n + 2 ^ r := by
76     have hp : 2 ^ r = 2 ^ (r - 2) * 2 ^ 2 := by
77       rw [← pow_add, Nat.sub_add_cancel hr]
78     rw [hp]
79     ring
80   rw [← he, NishibuchiCompletion.generalizedEuler_at_packet,
81     NishibuchiCompletion.generalizedEuler_at_packet]
82   exact half_period_precision j r n hj hj2 hr hn
83 
84 /-- At precision one these addresses vanish modulo two at every row. -/
85 theorem all_rows_even (j n : ℕ) (hj : j < 4) (hj2 : 2 ≤ j) :
86     (2 : ℤ_[2]) ∣ unnormalizedLift j hj n :=
87   dvd_mul_of_dvd_left (factorial_even j hj hj2) _
88 
89 end KomorebiPaperIX.DyadicFourSharpening

Back to source controls