OAI/NumberTheory/TotientAsymptotic/TupleMassApproximation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Largest-prime summation over the actual finite tuple set, with all weights.

  1. def OAI.TotientAsymptotic.weightedTupleCount line 15
  2. lemma OAI.TotientAsymptotic.weightedTupleCount_eq_fibers line 18
  3. theorem OAI.TotientAsymptotic.weighted_tuple_mass_relative line 34

    Source documentation

    Relative error in largest-prime summation, uniformly over all bounded weights and all endpoints in a fixed interval [a*x,x].

    theorem weighted_tuple_mass_relative (hpnt : PrimeNumberTheoremInput)
    {a : ℝ} (ha : 0 < a) {H : ℕ} (hPH : P H < H) (hP : 1 ≤ P H)
    {ε : ℝ} (hε : 0 < ε) :
    ∀ᶠ x : ℝ in atTop, ∀ t : ℝ, a*x ≤ t → t ≤ x →
      ∀ f : ℝ → ℝ, (∀ r, 0 ≤ f r ∧ f r ≤ 1) →
      |weightedTupleCount x H t f-(t/Real.log x)*M x H f| ≤
        ε*(t/Real.log x)*M x H (fun _ => 1) := by
…

    Mentions: OAI.TotientAsymptotic.PrimeNumberTheoremInput, OAI.TotientAsymptotic.a, OAI.TotientAsymptotic.P, OAI.TotientAsymptotic.weightedTupleCount, OAI.TotientAsymptotic.M

  4. lemma OAI.TotientAsymptotic.weightedTupleCount_one line 72