OAI/NumberTheory/TotientAsymptotic/UnbandedPrimeGrid.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Prime mass in arbitrary nonnegative prefix regions.

  1. def OAI.TotientAsymptotic.tupleUnitGrid line 12
  2. lemma OAI.TotientAsymptotic.tupleUnitGrid_cell line 15
  3. lemma OAI.TotientAsymptotic.tupleUnitGrid_cover line 22
  4. lemma OAI.TotientAsymptotic.tupleUnitGrid_positive line 31
  5. lemma OAI.TotientAsymptotic.sum_exp_neg_linear_prefix line 37
  6. theorem OAI.TotientAsymptotic.unbanded_prime_mass_bound line 74

    Source documentation

    A linear lower envelope is enough for a dimension-independent prime mass factor; no concentration or band assumption is used.

    theorem unbanded_prime_mass_bound (hford : FordUnitPrimeBoxInput) :
    ∃ C : ℝ, 0 < C ∧ ∀ {N : ℕ} (Q : Finset (Fin N → ℕ)) (c A : ℝ),
      0 < c →
      (∀ p ∈ Q, ∀ i, (p i).Prime ∧ c*(N-i.val:ℕ) ≤ primePrefixCoord p i) →
      ((tupleUnitGrid Q).card:ℝ) ≤ A →
      (∑ p ∈ Q, reciprocalShiftWeight p) ≤ Real.exp (C*(1-Real.exp (-c))⁻¹)*A := by
…

    Mentions: OAI.TotientAsymptotic.FordUnitPrimeBoxInput, OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.primePrefixCoord, OAI.TotientAsymptotic.tupleUnitGrid, OAI.TotientAsymptotic.reciprocalShiftWeight