OAI/NumberTheory/JointDickman/Amplification/SingularSeriesApproximation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.totientSquareSum line 11
2. theorem OAI.JointDickman.totientSquareSum_nonneg line 13
3. theorem OAI.JointDickman.singularSeries_partial_abs_bound line 16
4. theorem OAI.JointDickman.singularSeries_periodic_error line 26
5. theorem OAI.JointDickman.totient_ratio_mean_bound line 46
6. theorem OAI.JointDickman.singularSeries_periodic_mean_error line 54
7. theorem OAI.JointDickman.singularSeries_periodic_approximation line 73

   Source documentation

   The finite period is fixed before the averaging length.

   theorem singularSeries_periodic_approximation
       (hMP : PublishedInputs.PrimeProductMertensInput) {ε : ℝ} (hε : 0 < ε) :
       ∃ (q : ℕ) (_ : NeZero q) (F : ZMod q → ℝ),
         ∀ U : ℕ, (∑ n ∈ Ioc 0 U, |singularSeries n-F (n : ZMod q)|) ≤ ε*U := by
   …

   Mentions: OAI.JointDickman.PublishedInputs.PrimeProductMertensInput, OAI.JointDickman.singularSeries