OAI/NumberTheory/TotientAsymptotic/PositiveSquareDiscard.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Positive-index squarefree exclusion for every basic witness.

  1. def OAI.TotientAsymptotic.squareInternalTuples line 14
  2. def OAI.TotientAsymptotic.FailsPositiveSquare line 18
  3. def OAI.TotientAsymptotic.positiveSquareFailureTuples line 23
  4. lemma OAI.TotientAsymptotic.squareInternalTuples_card_le line 27
  5. lemma OAI.TotientAsymptotic.positiveSquareFailureTuples_subset line 43
  6. theorem OAI.TotientAsymptotic.positive_square_tuple_discard line 54

    Source documentation

    Every basic witness is covered, without choosing a preferred factorization.

    theorem positive_square_tuple_discard (hbox : FordUnitPrimeBoxInput)
    (hren : FordRenewalInput) (hmertens : MertensProductInput) :
    ∃ ε : ℕ → ℝ, Tendsto ε atTop (nhds 0) ∧
      ∀ᶠ H : ℕ in atTop, ∀ᶠ x : ℝ in atTop, ∀ t ≤ x,
        ((positiveSquareFailureTuples x H t).card : ℝ) ≤ ε H*(x/Real.log x*G x (m x)) := by
…

    Mentions: OAI.TotientAsymptotic.FordUnitPrimeBoxInput, OAI.TotientAsymptotic.FordRenewalInput, OAI.TotientAsymptotic.MertensProductInput, OAI.TotientAsymptotic.positiveSquareFailureTuples, OAI.TotientAsymptotic.G, OAI.TotientAsymptotic.m