OAI/NumberTheory/JointDickman/Counting/CountingPeriodicModel.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.countingCandidateWithSeries line 11
2. def OAI.JointDickman.countingSiteWithSeries line 18
3. theorem OAI.JointDickman.countingSiteWithSeries_original line 31
4. theorem OAI.JointDickman.countingCandidateWithSeries_difference line 38
5. theorem OAI.JointDickman.countingSiteWithSeries_difference line 57
6. theorem OAI.JointDickman.countingSiteWithSeries_cut_error line 101
7. theorem OAI.JointDickman.countingSiteModel_periodic_approximation line 151

   Source documentation

   A fixed finite residue function suffices uniformly for all block sizes.

   theorem countingSiteModel_periodic_approximation
       (hMP : PublishedInputs.PrimeProductMertensInput) {R K η ε : ℝ}
       (hR : 0 ≤ R) (hK : 0 ≤ K) (hη : 0 < η) (hε : 0 < ε) :
       ∃ (q : ℕ) (_ : NeZero q) (F : ZMod q → ℝ),
         ∀ (P : MvPolynomial (Fin 4) ℝ) (m : (Fin 4 →₀ ℕ) → ℕ)
           (B L T H M : ℕ) (τ C : ℝ) (c : (Fin 4 →₀ ℕ) → ℕ → ℝ)
           (D : (Fin 4 →₀ ℕ) → ℕ) (σ : ℝ),
           0 < T → 0 < M → independentRootMean B L τ C ≤ R → η*T ≤ H →
           (∀ j : ℕ, H < j → j < T →
             ∀ x y, |countingPrimeKernel P m B j c D T σ x y| ≤ K) →
           ∀ x : Fin M → (auxiliaryPrimes B).powerset,
           kernelCutNorm (realizedSiteKernel
   …

   Mentions: OAI.JointDickman.PublishedInputs.PrimeProductMertensInput, OAI.JointDickman.independentRootMean, OAI.JointDickman.countingPrimeKernel, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.kernelCutNorm, OAI.JointDickman.realizedSiteKernel