SupportedPrimePrior.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Bounds on the support of the original harmonic prime priors

theorem OAI.Ostmann.primeSubsetPrior_log_lower line 10

theorem OAI.Ostmann.primeSubsetPrior_le_exp_of_support line 16

Source documentation

The ambient sample space can include smaller primes in other roles.

theorem primeSubsetPrior_le_exp_of_support (P Q : Finset ℕ) (H T : ℝ)
    (hmass : (∑ q ∈ Q, (q : ℝ)⁻¹)⁻¹ ≤ Real.exp H)
    (hQ : ∀ q ∈ Q, Real.exp T ≤ (q : ℝ)) (p : P) :
    primeSubsetPrior P Q p ≤ Real.exp (H - T) := by
…

Mentions: OAI.Ostmann.primeSubsetPrior

theorem OAI.Ostmann.primeSubsetPrior_le_one line 26
theorem OAI.Ostmann.prime_mul_primeSubsetPrior_le line 33
Source documentation
The compensated internal prior pays only its original normalizer.
```
theorem prime_mul_primeSubsetPrior_le (P Q : Finset ℕ) (p : P) :
    (p : ℝ) * primeSubsetPrior P Q p ≤ (∑ q ∈ Q, (q : ℝ)⁻¹)⁻¹ := by
…
```
Mentions: OAI.Ostmann.primeSubsetPrior

theorem OAI.Ostmann.selected_cell_mass_scale line 47

Source documentation

The rich-cell lower bound has the polynomial normalizer required in the prime comparison, at every shell scale bounded by exp (K * L).

theorem selected_cell_mass_scale (c K L B mass : ℝ) (hc : 0 < c)
    (hK : 0 ≤ K) (hL : 1 ≤ L) (hB : 0 < B) (hBupper : B ≤ Real.exp (K * L))
    (hmass : c / B ≤ mass) :
    1 ≤ K + c⁻¹ + 1 ∧
      Real.exp (-(K + c⁻¹ + 1) * L) ≤ mass ∧
      mass⁻¹ ≤ Real.exp ((K + c⁻¹ + 1) * L) := by
…