OAI/NumberTheory/TotientAsymptotic/TupleMassBound.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Tuple counts controlled by arithmetic mass.

  1. lemma OAI.TotientAsymptotic.tupleValue_eq_head line 14
  2. lemma OAI.TotientAsymptotic.basic_prefix_denominator_pos line 21
  3. lemma OAI.TotientAsymptotic.tupleFinset_card_eq_sum_fibers line 27
  4. theorem OAI.TotientAsymptotic.tuple_count_le_mass line 40

    Source documentation

    Uniform at both common endpoints: an arbitrary smaller endpoint can only reduce the largest-prime fibers.

    theorem tuple_count_le_mass : ∀ᶠ x : ℝ in atTop, ∀ H : ℕ, P H ≤ H →
    ∀ t : ℝ, t ≤ x → ( (tupleFinset x H t).card : ℝ) ≤
      (10*x/Real.log x)*M x H (fun _ => 1) := by
…

    Mentions: OAI.TotientAsymptotic.P, OAI.TotientAsymptotic.tupleFinset, OAI.TotientAsymptotic.M