StrengtheningStatementContract.lean

1 module
2 public import DyadicFourFinalStrengthening
3 public import DyadicSharpTower
4 @[expose] public section
5 set_option autoImplicit false
6 open KomorebiPaperIX
7 
8 example (j u k n : ℕ) (hj : j < 4) :
9     GlobalEulerBoundary.precision 2
10       ((k * (padicValNat 2 u + 1) + padicValNat 2 j.factorial : ℕ) : ℤ)
11       (Mahler.difference u k (Congruential.unnormalized 4 j) n) :=
12   DyadicFourFinalStrengthening.unnormalized_step_precision j u k n hj
13 
14 example (j r n : ℕ) (hj : j < 4) (hr : 0 < r) :
15     GlobalEulerBoundary.precision 2 (r : ℤ)
16       (NishibuchiCompletion.generalizedEuler 4 (by decide) j (4 * n + 2 ^ (r + 1)) -
17        NishibuchiCompletion.generalizedEuler 4 (by decide) j (4 * n)) :=
18   DyadicFourFinalStrengthening.all_rows_period_degree j r n hj hr
19 
20 example (j r n : ℕ) (hj : j < 4) (hj2 : 2 ≤ j) (hr : 2 ≤ r) :
21     GlobalEulerBoundary.precision 2 (r : ℤ)
22       (NishibuchiCompletion.generalizedEuler 4 (by decide) j (4 * n + 2 ^ r) -
23        NishibuchiCompletion.generalizedEuler 4 (by decide) j (4 * n)) :=
24   DyadicFourFinalStrengthening.all_rows_half_period_degree j r n hj hj2 hr
25 
26 example (n M : ℕ) : (2 : ℤ_[2]) ^ (4 * M + 3) ∣
27     (EulerCoefficients.eulerEven n : ℤ_[2]) - DyadicReconstruction.truncationPadic n M :=
28   DyadicSharpTower.dyadic_supercongruence_sharp n M
29 
30 example (M : ℕ) : padicValRat 2
31     ((EulerCoefficients.eulerEven (M + 1) : ℚ) - DyadicReconstruction.truncation (M + 1) M) =
32       (4 * M + 3 : ℕ) :=
33   DyadicSharpTower.first_omitted_error_valuation M

Back to source controls