FiniteLocalLemmaMeasure.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

structure OAI.QuantitativeVanDerWaerden.FiniteLocalLemma.Probability line 15
Source documentation
A probability on the finite sample space Ω, with the event identities needed by the finite local lemma.
```
structure Probability (Ω : Type uOmega) [Fintype Ω] [DecidableEq Ω] where
…
```
theorem OAI.QuantitativeVanDerWaerden.FiniteLocalLemma.Probability.mass_empty line 27
def OAI.QuantitativeVanDerWaerden.FiniteLocalLemma.Probability.ofWeights line 33
Source documentation
The probability whose mass at each point is its prescribed weight.
```
noncomputable def ofWeights (weight : Ω → ℝ)
    (weight_nonneg : ∀ ω, 0 ≤ weight ω)
    (weight_sum : ∑ ω, weight ω = 1) : Probability Ω where
…
```
Mentions: OAI.QuantitativeVanDerWaerden.FiniteLocalLemma.Probability
theorem OAI.QuantitativeVanDerWaerden.FiniteLocalLemma.Probability.ofWeights_mass line 46