LocalSmoothGiantSelection.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Selecting a complete giant cell inside a prescribed finite window

The averaging family may cover boundary primes several times. Its exact partition weight is retained, so selecting a cell never clips its prime law.

def OAI.Ostmann.logCellFamilyWeight line 15
theorem OAI.Ostmann.logCellFamilyWeight_nonneg line 18
theorem OAI.Ostmann.smoothGiantPrior_real_mean line 22
theorem OAI.Ostmann.local_smoothGiantPrior_exists_positive_mean line 35

theorem OAI.Ostmann.smoothGiant_full_cell_sums line 82

Source documentation

Extra primes of the ambient container have zero weight in the selected cell. Both its normalizer and its numerator therefore equal the complete cell expressions.

theorem smoothGiant_full_cell_sums (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
    (G : ℝ) (hsub : smoothGiantPrimeRange G ⊆ P) (f : ℕ → ℝ) :
    smoothGiantMass P logCellProfile G =
      smoothGiantMass (smoothGiantPrimeRange G) logCellProfile G ∧
    (∑ p ∈ P, (p : ℝ)⁻¹ * logCellProfile (Real.log p - G) * f p) =
      ∑ p ∈ smoothGiantPrimeRange G,
        (p : ℝ)⁻¹ * logCellProfile (Real.log p - G) * f p := by
…

Mentions: OAI.Ostmann.smoothGiantPrimeRange, OAI.Ostmann.smoothGiantMass, OAI.Ostmann.logCellProfile

theorem OAI.Ostmann.complete_smoothGiantPrior_exists_positive_mean line 100

Source documentation

A localized positive mean produces the original full smooth harmonic prior, with no deletion of endpoint primes.

theorem complete_smoothGiantPrior_exists_positive_mean
    (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime) (C : Finset ℤ)
    (hsub : ∀ n ∈ C, smoothGiantPrimeRange n ⊆ P) (f : ℕ → ℝ) (δ : ℝ)
    (hmean : δ * (∑ p ∈ P, (p : ℝ)⁻¹ * logCellFamilyWeight C p) <
      ∑ p ∈ P, (p : ℝ)⁻¹ * logCellFamilyWeight C p * f p) :
    ∃ n ∈ C, 0 < smoothGiantMass (smoothGiantPrimeRange n) logCellProfile n ∧
      δ < ∑ p : smoothGiantPrimeRange n,
        smoothGiantPrior (smoothGiantPrimeRange n) logCellProfile n p * f p := by
…

Mentions: OAI.Ostmann.smoothGiantPrimeRange, OAI.Ostmann.logCellFamilyWeight, OAI.Ostmann.smoothGiantMass, OAI.Ostmann.logCellProfile, OAI.Ostmann.smoothGiantPrior