CountableFullSupport.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.DilutedSpinGlass.exists_countable_full_support line 12
Source documentation
A concrete full-support probability law for every nonempty countable mark dictionary, obtained by pushing forward a geometric law on its enumeration.
```
theorem exists_countable_full_support (I : Type) [Countable I] [Nonempty I]
    [MeasurableSpace I] [MeasurableSingletonClass I] :
    ∃ ν : Measure I, IsProbabilityMeasure ν ∧ ∀ i, 0 < ν.real {i} := by
…
```