OAI/NumberTheory/TwoPoint/Bounds/CrudeHarmonicMass.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Elementary harmonic and padding-weight bounds for the crude enumeration.

  1. lemma OAI.TwoPointCorrelations.primeHarmonicMass_le_one_add_log line 15

    Source documentation

    Enlarging primes to all positive integers already gives enough mass control for the negligible-word estimates.

    lemma primeHarmonicMass_le_one_add_log (P : Finset ℕ) (B : ℕ)
    (hpos : ∀ p ∈ P, 1 ≤ p) (hB : ∀ p ∈ P, p ≤ B) :
    primeHarmonicMass P ≤ 1 + Real.log B := by
…

    Mentions: OAI.TwoPointCorrelations.primeHarmonicMass

  2. lemma OAI.TwoPointCorrelations.primeHarmonicMass_le_one_add_scale line 32
  3. def OAI.TwoPointCorrelations.crudePaddingWeight line 42

    Source documentation

    The actual padding weight u(q)=4^ω(q).

    noncomputable def crudePaddingWeight (q : ℕ) : ℝ := 4 ^ q.primeFactors.card
  4. lemma OAI.TwoPointCorrelations.crudePaddingWeight_le line 44