OAI/NumberTheory/TotientAsymptotic/IntervalOmegaMoment.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exact multiplicative moments for the number of prime factors in an interval.

  1. def OAI.TotientAsymptotic.intervalOmegaWeight line 11
  2. lemma OAI.TotientAsymptotic.intervalOmegaWeight_nonneg line 22
  3. lemma OAI.TotientAsymptotic.intervalOmegaWeight_prime line 27
  4. lemma OAI.TotientAsymptotic.intervalOmegaWeight_norm line 36
  5. lemma OAI.TotientAsymptotic.interval_omega_moment_product line 45

    Source documentation

    The exact finite Euler product; concentration bounds are proved separately.

    lemma interval_omega_moment_product {a : ℝ} (ha : 0≤a) (ha' : a≤3/2)
    (U T : ℝ) (N : ℕ) (Q : Finset ℕ) (hQ : ∀ n ∈ Q,0<n ∧ n≤N) :
    (∑ n ∈ Q,intervalOmegaWeight a U T n) ≤
      ∏ p ∈ (Finset.Icc 2 N).filter Nat.Prime,
        (1-(if U<(p:ℝ) ∧ (p:ℝ)≤T then a else 1)/(p:ℝ))⁻¹ := by
…

    Mentions: OAI.TotientAsymptotic.a, OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.intervalOmegaWeight