SoftPrimeCellSelection.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Selecting a smooth prime cell from a positive empirical mean

def OAI.Ostmann.smoothPrimeCenters line 11
Source documentation
The integer translates that can occur in a finite prime set.
```
noncomputable def smoothPrimeCenters (P : Finset ℕ) : Finset ℤ :=
…
```
theorem OAI.Ostmann.logCellProfile_zero_off_centers line 14
theorem OAI.Ostmann.smoothPrimeCenters_partition line 27

theorem OAI.Ostmann.smoothPrimeCell_exists line 40

Source documentation

A positive weighted mean selects a positive-mass smooth cell. The test may be unbounded and may change sign; no hard-cell or positivity approximation is used in passing to the original soft prior.

theorem smoothPrimeCell_exists (P : Finset ℕ) (ν f : ℕ → ℝ)
    (hν : ∀ p ∈ P, 0 ≤ ν p) (δ : ℝ)
    (hmean : δ * (∑ p ∈ P, ν p) < ∑ p ∈ P, ν p * f p) :
    ∃ n ∈ smoothPrimeCenters P,
      0 < ∑ p ∈ P, ν p * logCellProfile (Real.log p - n) ∧
      δ * (∑ p ∈ P, ν p * logCellProfile (Real.log p - n)) <
        ∑ p ∈ P, ν p * logCellProfile (Real.log p - n) * f p := by
…

Mentions: OAI.Ostmann.smoothPrimeCenters, OAI.Ostmann.logCellProfile

theorem OAI.Ostmann.smoothGiantPrior_exists_positive_mean line 82

Source documentation

The selected cell uses exactly the manuscript's harmonic smooth prior, including all primes in the ambient support.

theorem smoothGiantPrior_exists_positive_mean (P : Finset ℕ) (f : ℕ → ℝ) (δ : ℝ)
    (hmean : δ * (∑ p ∈ P, (p : ℝ)⁻¹) < ∑ p ∈ P, (p : ℝ)⁻¹ * f p) :
    ∃ n ∈ smoothPrimeCenters P,
      0 < smoothGiantMass P logCellProfile n ∧
      δ < ∑ p : P, smoothGiantPrior P logCellProfile n p * f p := by
…

Mentions: OAI.Ostmann.smoothPrimeCenters, OAI.Ostmann.smoothGiantMass, OAI.Ostmann.logCellProfile, OAI.Ostmann.smoothGiantPrior