OAI/NumberTheory/TotientAsymptotic/GridVolume.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The geometric volumes of the same disjoint boxes used in the prime sum.

  1. def OAI.TotientAsymptotic.unitGridCell line 13
  2. lemma OAI.TotientAsymptotic.measurableSet_unitGridCell line 16
  3. lemma OAI.TotientAsymptotic.volume_unitGridCell line 20
  4. lemma OAI.TotientAsymptotic.unitGridCell_disjoint line 26
  5. def OAI.TotientAsymptotic.gridRegion line 40
  6. lemma OAI.TotientAsymptotic.volume_gridRegion line 43
  7. lemma OAI.TotientAsymptotic.gridRegion_volume_real line 51
  8. theorem OAI.TotientAsymptotic.grid_prime_mass_volume_error line 58

    Source documentation

    A direct arithmetic-to-volume estimate on a finite union of prime boxes. The later shell argument changes this grid region to the witness region.

    theorem grid_prime_mass_volume_error (hford : FordUnitPrimeBoxInput) :
    ∃ C : ℝ, 0 < C ∧ ∀ {N : ℕ} (K : Finset (Fin N → ℕ)) (T : ℝ),
      (∀ m ∈ K, ∀ i, 1 ≤ m i ∧ T ≤ m i) →
      |gridPrimeMass K-(volume (gridRegion K)).toReal| ≤
        (volume (gridRegion K)).toReal*(Real.exp (C*N*Real.exp (-T))-1) := by
…

    Mentions: OAI.TotientAsymptotic.FordUnitPrimeBoxInput, OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.gridPrimeMass, OAI.TotientAsymptotic.gridRegion