ProjectedGrid.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

A projected prime prefix has mass bounded by its own simplex volume.

def OAI.TotientAsymptotic.projectedPrimeGrid line 16
lemma OAI.TotientAsymptotic.projectedPrimeTuples_subset_grid line 20
lemma OAI.TotientAsymptotic.projectedPrimeGrid_enclosure line 32
lemma OAI.TotientAsymptotic.projected_volume_zero_prefixRegion line 47
theorem OAI.TotientAsymptotic.projectedPrimeGrid_volume_bound line 53

theorem OAI.TotientAsymptotic.projected_prime_mass_bound line 87

Source documentation

Full prime mass, before the independent smooth-cofactor sum.

theorem projected_prime_mass_bound (hford : FordUnitPrimeBoxInput) :
    ∃ C : ℝ, 0 < C ∧ ∀ {x : ℝ} {K : ℕ},
      0 ≤ theta x → 4 ≤ lam*(K : ℝ) → 0 < B x →
      (m x : ℝ)/(B x*rho^(m x)) ≤ 2/lam → 0 < R x K →
      ∀ Q : Finset (Fin (R x K) → ℕ),
      (∀ p ∈ Q, (∀ i, (p i).Prime) ∧ primePrefixCoord p ∈ prefixBandRegion x K ∧
        primePrefixCoord p ∈ enlargedSimplex (R x K) (B x) (xi x 0) (fun i => xi x (i.val+1))) →
      (∑ p ∈ Q, reciprocalShiftWeight p) ≤
        (1+bandPrimeError C (9/10) (K))*
          Real.exp (simplexBoxTail 4 (K))*G x (R x K) := by
…