FiniteHierarchyDense.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.DilutedSpinGlass.atomicProbability_reindex line 10
lemma OAI.DilutedSpinGlass.continuous_atomicProbability_atoms line 19

lemma OAI.DilutedSpinGlass.finite_atomic_dense line 28

Source documentation

Finite laws supported on any dense set are weakly dense.

lemma finite_atomic_dense {X : Type} [MetricSpace X] [SeparableSpace X]
    [MeasurableSpace X] [BorelSpace X] (D : Set X) (hD : Dense D) :
    Dense {μ : ProbabilityMeasure X | ∃ (n : ℕ) (x : Fin n → X) (w : AtomicWeights (Fin n)),
      (∀ i,x i ∈ D) ∧ μ = atomicProbability x w} := by
…

Mentions: OAI.DilutedSpinGlass.AtomicWeights, OAI.DilutedSpinGlass.atomicProbability

def OAI.DilutedSpinGlass.FiniteHierarchy line 62
Source documentation
Genuine finitely branching laws at every level, not an altered trial class.
```
def FiniteHierarchy : (r : ℕ) → Hierarchy r → Prop
  | 0,_ => True
  | r+1,μ => ∃ (n : ℕ) (x : Fin n → Hierarchy r) (w : AtomicWeights (Fin n)),
      (∀ i,FiniteHierarchy r (x i)) ∧ μ = atomicProbability x w
```
Mentions: OAI.DilutedSpinGlass.Hierarchy, OAI.DilutedSpinGlass.AtomicWeights, OAI.DilutedSpinGlass.atomicProbability
lemma OAI.DilutedSpinGlass.finiteHierarchy_dense line 67