OAI/NumberTheory/JointDickman/Amplification/AllLargeHighVanishing.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.allLargeClassError line 12
2. theorem OAI.JointDickman.log_add_one_fifth_div_rpow_tendsto line 15
3. theorem OAI.JointDickman.allLargeClassError_tendsto line 29
4. theorem OAI.JointDickman.all_large_high_class_vanishing line 38

   Source documentation

   All cardinality classes together still have vanishing expected multiplicity. The only loss from summing them is two logarithmic powers.

   theorem all_large_high_class_vanishing
       (hFord : PublishedInputs.FordUpperSieveInput)
       (hM : PublishedInputs.PrimeReciprocalMertensInput)
       {L k : ℕ} (hk : k ∈ Icc 1 L) {g Δ δ ε η : ℝ}
       (hkg : (k : ℝ)/L = g) (hg : 0 < g) (hg1 : g ≤ 1)
       (hΔ : 0 < Δ) (hgap : 2*Δ < g)
       (hδ : 0 < δ) (hδ1 : δ ≤ 1/2) (hε : 0 < ε) (hη : 0 < η) :
       ∃ τ₀ : ℝ, 0 < τ₀ ∧ ∀ τ : ℝ, 0 < τ → τ ≤ τ₀ →
         largeMultiplicityLoss Δ δ τ ε < 4/100 →
         ∃ E : ℕ → ℝ, Tendsto E atTop (𝓝 0) ∧ ∀ᶠ B : ℕ in atTop,
           ∀ (C : ℝ) (A D V : Finset ℕ) (j : ℕ),
             A ⊆ auxiliaryPrimes B → D ⊆ auxiliaryPrimes B → V ⊆ auxiliaryPrimes B →
   …

   Mentions: OAI.JointDickman.PublishedInputs.FordUpperSieveInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.largeMultiplicityLoss, OAI.JointDickman.auxiliaryPrimes