StepAmplificationExamples.lean

1 module
2 public import DyadicStepAmplification
3 public import ConjectureExamples
4 @[expose] public section
5 noncomputable section
6 set_option autoImplicit false
7 namespace KomorebiPaperIX.StepAmplificationExamples
8 open Mahler Congruential GlobalEulerBoundary
9 
10 theorem actual_second_coefficient : coeff 4 0 2 = 69 := by
11   rw [coefficient_recurrence 4 0 (by decide : 0<2)]
12   norm_num [Finset.sum_range_succ,Nat.choose,ConjectureExamples.four_first_coefficients.1]
13 
14 theorem actual_first_difference : difference 1 1 (coeff 4 0) 1 = 70 := by
15   rw [difference_one,actual_second_coefficient,ConjectureExamples.four_first_coefficients.1]
16   norm_num
17 
18 theorem actual_first_difference_valuation : padicValRat 2 (difference 1 1 (coeff 4 0) 1)=1 := by
19   rw [actual_first_difference]
20   norm_num [padicValRat_def,padicValInt]
21   rw [show (70:ℕ)=2*35 by decide,
22     padicValNat.mul (by decide : (2:ℕ)≠0) (by decide : (35:ℕ)≠0)]
23   norm_num [padicValNat.eq_zero_of_not_dvd]
24 
25 /-- The proved dyadic estimate is exact at this row and address. -/
26 theorem no_uniform_extra_digit : ¬precision 2 2 (difference 1 1 (coeff 4 0) 1) := by
27   intro H
28   rcases H with hz | hv
29   · rw [actual_first_difference] at hz
30     norm_num at hz
31   · rw [actual_first_difference_valuation] at hv
32     omega
33 
34 end KomorebiPaperIX.StepAmplificationExamples

Back to source controls