SmoothCellDeletion.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The nongiant smooth cell prior with the prescribed finite deletions

theorem OAI.Ostmann.smoothCell_atom_le line 10

theorem OAI.Ostmann.smoothCell_deletion_loss line 33

Source documentation

Deleting a fixed finite set loses at most its cardinality times the largest reciprocal prime in the cell, including boundary zero weights.

theorem smoothCell_deletion_loss (P E : Finset ℕ) (φ : ℝ → ℝ) (G : ℝ)
    (hφ : ∀ x, φ x ≤ 1) (hout : ∀ x, 1 ≤ |x| → φ x = 0) :
    smoothGiantMass P φ G - (E.card : ℝ) * Real.exp (1 - G) ≤
      smoothGiantMass (P \ E) φ G := by
…

Mentions: OAI.Ostmann.smoothGiantMass

def OAI.Ostmann.deletedSmoothCellPrior line 55
theorem OAI.Ostmann.deletedSmoothCellPrior_nonneg line 60
theorem OAI.Ostmann.deletedSmoothCellPrior_mass line 67
theorem OAI.Ostmann.prime_mul_deletedSmoothCellPrior_le line 88
Source documentation
The cancellation estimate needed for repeated internal samples applies to the exact smooth cell law, not just the hard harmonic prior.
```
theorem prime_mul_deletedSmoothCellPrior_le (P E : Finset ℕ)
    (hP : ∀ p ∈ P, p.Prime) (φ : ℝ → ℝ) (G : ℝ)
    (hφ : ∀ x, φ x ≤ 1) (p : P) :
    (p : ℝ) * deletedSmoothCellPrior P E φ G p ≤
      Real.exp (smoothGiantLogNormalizer (P \ E) φ G) := by
…
```
Mentions: OAI.Ostmann.deletedSmoothCellPrior, OAI.Ostmann.smoothGiantLogNormalizer
theorem OAI.Ostmann.deletedSmoothCellPrior_support line 105
theorem OAI.Ostmann.deletedSmoothCellPrior_log_lower line 116

theorem OAI.Ostmann.deletedSmoothCellPrior_le_exp line 128

Source documentation

The exact smooth law supplies the same small-atom scale required by the repeated-prime and internal arithmetic bounds.

theorem deletedSmoothCellPrior_le_exp (P E : Finset ℕ)
    (hP : ∀ p ∈ P, p.Prime) (φ : ℝ → ℝ) (G H : ℝ)
    (hφ : ∀ x, φ x ≤ 1) (hout : ∀ x, 1 ≤ |x| → φ x = 0)
    (hH : smoothGiantLogNormalizer (P \ E) φ G ≤ H) (p : P) :
    deletedSmoothCellPrior P E φ G p ≤ Real.exp (H - (G - 1)) := by
…

Mentions: OAI.Ostmann.smoothGiantLogNormalizer, OAI.Ostmann.deletedSmoothCellPrior