ProhibitedDensity.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Density of the actual deleted event, with all finite catalog costs included.

structure OAI.TwoPointCorrelations.ProhibitedPrimeFamily line 13
Source documentation
The arithmetic data used by the prohibited-word argument.
```
structure ProhibitedPrimeFamily (h J M : ℕ) where
…
```
lemma OAI.TwoPointCorrelations.ProhibitedPrimeFamily.prime line 32
lemma OAI.TwoPointCorrelations.ProhibitedPrimeFamily.whole_squarefree line 37
lemma OAI.TwoPointCorrelations.ProhibitedPrimeFamily.support_subset line 44
def OAI.TwoPointCorrelations.ProhibitedPrimeFamily.residueLaw line 55
def OAI.TwoPointCorrelations.ProhibitedPrimeFamily.deletedEvent line 59
lemma OAI.TwoPointCorrelations.ProhibitedPrimeFamily.deletedEvent_iff line 66
Source documentation
The finite-residue event is precisely the manuscript's prohibited-site predicate at any common integer lift of those same coordinates.
```
lemma deletedEvent_iff (s B : ℕ) (x : ↥(F.P ∪ F.Q) → Fin B) (n : ℤ)
    (hn : ∀ p : ↥(F.P ∪ F.Q), (n : ZMod p.val) = ((x p).val : ZMod p.val)) :
    F.deletedEvent s B x ↔ ProhibitedSite h s (fun d q => (d, q) ∈ F.pairs) n := by
…
```
Mentions: OAI.TwoPointCorrelations.ProhibitedSite

theorem OAI.TwoPointCorrelations.ProhibitedPrimeFamily.probability_bound line 75

Source documentation

No code count or numerical assignment sum is left implicit here.

theorem probability_bound (s B H : ℕ)
    (hB : ∀ p ∈ F.P ∪ F.Q, p ≤ B)
    (hVP : 1 ≤ primeHarmonicMass F.P) (hH : 0 < H) (hBone : 1 ≤ B)
    (hlo : ∀ p ∈ F.P, H ≤ p) :
    (F.residueLaw B hB).probability (F.deletedEvent s B) ≤
      badCatalogCost s (s * (J + M)) (primeHarmonicMass F.P) (primeHarmonicMass F.Q) *
        ((H : ℝ)⁻¹ + (1 + Real.log B) / H) := by
…

Mentions: OAI.TwoPointCorrelations.primeHarmonicMass, OAI.TwoPointCorrelations.badCatalogCost

theorem OAI.TwoPointCorrelations.eventually_prohibited_density line 102

Source documentation

The density assertion of q:bad, proved from the actual pair family and independent uniform residues, with the published prime estimates isolated as their numerical mass and scale consequences.

theorem eventually_prohibited_density (C : ℝ) (hC : 0 ≤ C) :
    ∀ᶠ L : ℝ in atTop, ∀ (h s J M B H : ℕ) (F : ProhibitedPrimeFamily h J M)
      (hB : ∀ p ∈ F.P ∪ F.Q, p ≤ B),
      1 ≤ s → (s : ℝ) ≤ L ^ (1 / 10 : ℝ) →
      ((s * (J + M) : ℕ) : ℝ) ≤ C * s * Real.log L →
      1 ≤ primeHarmonicMass F.P →
      primeHarmonicMass F.P ≤ L ^ (2 : ℕ) → primeHarmonicMass F.Q ≤ L ^ (2 : ℕ) →
      Real.exp (L ^ (199 / 200 : ℝ)) ≤ H → 1 ≤ B → (B : ℝ) ≤ Real.exp L →
      (∀ p ∈ F.P, H ≤ p) →
      (F.residueLaw B hB).probability (F.deletedEvent s B) ≤
        Real.exp (-(1 / 2 : ℝ) * L ^ (199 / 200 : ℝ)) := by
…

Mentions: OAI.TwoPointCorrelations.ProhibitedPrimeFamily, OAI.TwoPointCorrelations.primeHarmonicMass