SquarefreeIntervalMass.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The squarefree interval estimate with an absolute Mertens error.

lemma OAI.TotientAsymptotic.prime_interval_upper_bounded_error line 10

theorem OAI.TotientAsymptotic.squarefree_interval_allocation_bound line 23

Source documentation

Unlike the general multiplicity bound, the application’s squarefree product needs no relation between the number of slots and the lower cutoff.

theorem squarefree_interval_allocation_bound : ∃ D : ℝ,0 < D ∧
    ∀ (k : ℕ) (U V I : ℝ),1 ≤ k → 2 ≤ U → U ≤ V →
    (k:ℝ)*(B V-B U+D) ≤ I → ∀ Q : Finset (PairedFactors k),
    (∀ f ∈ Q,0 < pairedProduct f ∧ pairedProduct f=∏ j,f.2 j) →
    (∀ f ∈ Q,Squarefree (pairedProduct f)) →
    (∀ f ∈ Q,((pairedProduct f).primeFactorsList.length:ℝ) ≤ I) →
    (∀ f ∈ Q,∀ p ∈ (pairedProduct f).primeFactorsList,U < (p:ℝ) ∧ (p:ℝ) ≤ V) →
    (∑ f ∈ Q,(pairedProduct f:ℝ)⁻¹) ≤ Real.exp (I*(Real.log k+1)) := by
…

Mentions: OAI.TotientAsymptotic.D, OAI.TotientAsymptotic.V, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.PairedFactors, OAI.TotientAsymptotic.pairedProduct