CharacterPriorMass.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Harmonic mass floors for every original signed character marginal

theorem OAI.Ostmann.eventual_full_character_mass_floor line 14

Source documentation

The bulk has linear mass, the top shell has fixed positive mass, and all remaining selected cells already have the proved exponential mass floor.

theorem eventual_full_character_mass_floor (a b C : ℝ)
    (ha : 0 < a) (hb : 0 < b) (hC : 0 < C) :
    ∀ᶠ L : ℝ in atTop, ∀ (k m : ℕ) (r : Fin k → ℕ) (f : ℕ)
      (Q : Fin (m + 1) → Finset ℕ)
      (R : (v : CharacterCell k) → Fin (characterCellSize r f v) → Finset ℕ),
      b ≤ ∑ p ∈ Q 0, (p : ℝ)⁻¹ →
      (∀ i : Fin m, a * L ≤ ∑ p ∈ Q i.succ, (p : ℝ)⁻¹) →
      (∀ v i, Real.exp (-C * L) ≤ ∑ p ∈ R v i, (p : ℝ)⁻¹) →
      ∀ i, Real.exp (-C * L) ≤
        ∑ p ∈ characterFullPrimeCells m r f Q R i, (p : ℝ)⁻¹ := by
…

Mentions: OAI.Ostmann.CharacterCell, OAI.Ostmann.characterCellSize, OAI.Ostmann.characterFullPrimeCells

theorem OAI.Ostmann.harmonic_mass_inv_le_exp line 41
theorem OAI.Ostmann.harmonic_mass_inv_energy_budget line 47