OAI/NumberTheory/TotientAsymptotic/WitnessGrid.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Uniform prime mass for the boxes occupied by discrete witness tails.

  1. def OAI.TotientAsymptotic.tailBoxIndex line 13
  2. def OAI.TotientAsymptotic.witnessGrid line 16
  3. lemma OAI.TotientAsymptotic.tailVector_mem_box line 19
  4. lemma OAI.TotientAsymptotic.tailPrimeVector_mem_grid line 25
  5. lemma OAI.TotientAsymptotic.tailBoxIndex_lower line 34
  6. lemma OAI.TotientAsymptotic.witnessGrid_exp_sum line 52
  7. theorem OAI.TotientAsymptotic.witnessGrid_prime_mass_bound line 83

    Source documentation

    The entire prime mass of any occupied tail box is bounded by an absolute constant, independent of the number of tail coordinates and witnesses.

    theorem witnessGrid_prime_mass_bound (hford : FordUnitPrimeBoxInput) :
    ∃ C : ℝ, 0 < C ∧ ∀ {H : ℕ} {s : ℝ}, 0 ≤ s → P H ≤ H →
      ∀ W : Finset (TailDatum H), (∀ η ∈ W, IsWitness H s η) →
      ∀ b ∈ witnessGrid W, (∏ i, unitPrimeWeight (b i)) ≤ C := by
…

    Mentions: OAI.TotientAsymptotic.FordUnitPrimeBoxInput, OAI.TotientAsymptotic.P, OAI.TotientAsymptotic.TailDatum, OAI.TotientAsymptotic.IsWitness, OAI.TotientAsymptotic.witnessGrid, OAI.TotientAsymptotic.unitPrimeWeight