HarmonicFamilyBounds.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Numerical bounds for the selected internal and external harmonic laws

theorem OAI.Ostmann.selected_cell_normalizer line 12

Source documentation

The fixed positive cell-mass constant changes the starting threshold, not the coefficient of L in the normalizer.

theorem selected_cell_normalizer (c K L mass : ℝ) (hc : 0 < c)
    (hL : max 1 (-Real.log c) ≤ L)
    (hmass : c / Real.exp (K * L) ≤ mass) :
    0 < mass ∧ mass⁻¹ ≤ Real.exp ((K + 1) * L) := by
…

theorem OAI.Ostmann.selected_harmonic_family_bounds line 35
Source documentation
Rich selected cells supply all the probability and atom bounds used in both original-prime comparisons. Only their actual reciprocal masses and prime ranges are needed.
```
theorem selected_harmonic_family_bounds (c K : ℝ) (hc : 0 < c) (hK : 0 ≤ K) :
    let C := K + 1
…
```

theorem OAI.Ostmann.selected_harmonic_family_tiers line 82

Source documentation

A finite ambient prime set requires tier separation only for the internal tiers which the depth-n sample actually uses.

theorem selected_harmonic_family_tiers (P : Finset ℕ) (B : Type) (n : ℕ)
    (Qμ : ℕ → Finset ℕ) (Qν : B → Finset ℕ) (tier : P → ℕ) (tierB : B → ℕ)
    (hμ : ∀ j, j < n → ∀ q : P, (q : ℕ) ∈ Qμ j → tier q = j)
    (hν : ∀ j (q : P), (q : ℕ) ∈ Qν j → tier q = tierB j) :
    (∀ j, j < n → ∀ q, primeSubsetPrior P (Qμ j) q ≠ 0 → tier q = j) ∧
    (∀ j q, primeSubsetPrior P (Qν j) q ≠ 0 → tier q = tierB j) := by
…

Mentions: OAI.Ostmann.primeSubsetPrior