FullPrimeGrid.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The actual full prime tuples are controlled by one enlarged-simplex volume, with the discrete cofactor kept separate.

def OAI.TotientAsymptotic.fullPrimeGrid line 17
lemma OAI.TotientAsymptotic.fullPrimeTuples_subset_grid line 21
lemma OAI.TotientAsymptotic.fullPrimeGrid_enclosure line 44
lemma OAI.TotientAsymptotic.volume_zero_prefixRegion line 58
theorem OAI.TotientAsymptotic.fullPrimeGrid_volume_bound line 64
theorem OAI.TotientAsymptotic.full_prime_mass_bound line 96
Source documentation
Full prime mass, before the independent smooth-cofactor sum.
```
theorem full_prime_mass_bound (hford : FordUnitPrimeBoxInput) :
    ∃ C : ℝ, 0 < C ∧ ∀ {x : ℝ} {H : ℕ},
      0 ≤ theta x → 4 ≤ lam*(P H : ℝ) → 0 < B x →
      (m x : ℝ)/(B x*rho^(m x)) ≤ 2/lam → 0 < L x H →
      (∑ p ∈ fullPrimeTuples x H, reciprocalShiftWeight p) ≤
        (1+bandPrimeError C (9/10) (P H))*
          Real.exp (simplexBoxTail 4 (P H))*G x (L x H) := by
…
```
Mentions: OAI.TotientAsymptotic.FordUnitPrimeBoxInput, OAI.TotientAsymptotic.theta, OAI.TotientAsymptotic.lam, OAI.TotientAsymptotic.P, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.rho, OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.fullPrimeTuples, OAI.TotientAsymptotic.reciprocalShiftWeight, OAI.TotientAsymptotic.bandPrimeError, OAI.TotientAsymptotic.simplexBoxTail, OAI.TotientAsymptotic.G