HarmonicTuplePointBound.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Counterpart point probabilities from the original prime-cell lower endpoints

theorem OAI.Ostmann.primeSubsetPrior_le_lower_endpoint line 10

theorem OAI.Ostmann.harmonicTuple_point_le line 22

Source documentation

The entire ordered tuple has its reciprocal-product scale and exact harmonic normalizer, with no dependence on the matching permutation.

theorem harmonicTuple_point_le {H : Type*} [Fintype H]
    (P : Finset ℕ) (Q : H → Finset ℕ) (lo : H → ℝ)
    (hlo : ∀ h, 0 < lo h) (hcell : ∀ h p, p ∈ Q h → lo h ≤ (p : ℝ))
    (x : H → P) :
    (∏ h, primeSubsetPrior P (Q h) (x h)) ≤
      (∏ h, (∑ q ∈ Q h, (q : ℝ)⁻¹)⁻¹) * (∏ h, lo h)⁻¹ := by
…

Mentions: OAI.Ostmann.primeSubsetPrior