OAI/NumberTheory/TotientAsymptotic/OmegaDiscard.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The complete residual factor-count exclusion for universally good tuples.

  1. def OAI.TotientAsymptotic.omegaInternalTuples line 14
  2. def OAI.TotientAsymptotic.FailsWitnessOmega line 18
  3. def OAI.TotientAsymptotic.omegaFailureTuples line 22
  4. lemma OAI.TotientAsymptotic.omegaInternalRemainders_basic line 26
  5. lemma OAI.TotientAsymptotic.omegaInternalTuples_card_le line 33
  6. lemma OAI.TotientAsymptotic.omegaFailureTuples_subset line 49
  7. theorem OAI.TotientAsymptotic.omega_tuple_discard line 61

    Source documentation

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

    theorem omega_tuple_discard (hbox : FordUnitPrimeBoxInput)
    (hren : FordRenewalInput) (hmertens : MertensProductInput) :
    ∃ ε : ℕ → ℝ, Tendsto ε atTop (nhds 0) ∧
      ∀ᶠ H : ℕ in atTop, ∀ᶠ x : ℝ in atTop, ∀ t ≤ x,
        ((omegaFailureTuples 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.omegaFailureTuples, OAI.TotientAsymptotic.G, OAI.TotientAsymptotic.m