OAI/NumberTheory/TotientAsymptotic/PrimeGrid.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TotientAsymptotic.unitPrimeBox_disjoint line 12
2. def OAI.TotientAsymptotic.primeBoxTuples line 29
3. def OAI.TotientAsymptotic.reciprocalShiftWeight line 32
4. lemma OAI.TotientAsymptotic.reciprocalShiftWeight_nonneg line 35
5. lemma OAI.TotientAsymptotic.prime_box_mass line 38
6. lemma OAI.TotientAsymptotic.primeBoxTuples_disjoint line 55
7. def OAI.TotientAsymptotic.gridPrimeTuples line 64
8. def OAI.TotientAsymptotic.gridPrimeMass line 67
9. lemma OAI.TotientAsymptotic.gridPrimeMass_eq line 70
10. theorem OAI.TotientAsymptotic.grid_prime_mass_error line 79

    Source documentation

    The arithmetic mass of disjoint prime boxes differs from their total unit volume by a relative error controlled uniformly by the lowest coordinate.

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

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

11. theorem OAI.TotientAsymptotic.grid_prime_mass_error_of_sum line 111

    Source documentation

    A coordinate-dependent error budget avoids a dimension factor when the lower band endpoints grow geometrically towards the front of the prefix.

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

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