OAI/Probability/DilutedSpin/HierarchyBasic.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DilutedSpinGlass.AtomicWeights line 11
  2. def OAI.DilutedSpinGlass.atomicProbability line 13
  3. theorem OAI.DilutedSpinGlass.integral_atomicProbability line 18
  4. theorem OAI.DilutedSpinGlass.continuous_atomicProbability line 27
  5. theorem OAI.DilutedSpinGlass.simple_map_atomic line 41
  6. theorem OAI.DilutedSpinGlass.probability_map_tendsto line 71
  7. theorem OAI.DilutedSpinGlass.probabilityMeasure_separable line 93

    Source documentation

    The missing recursive weak-hierarchy infrastructure: probability laws on separable metric Borel spaces form a separable space for the actual weak topology. The finite approximations are global, not chosen separately by μ.

    theorem probabilityMeasure_separable {X : Type*} [MetricSpace X]
    [SeparableSpace X] [MeasurableSpace X] [BorelSpace X] :
    SeparableSpace (ProbabilityMeasure X) := by
…
  8. theorem OAI.DilutedSpinGlass.hierarchy_properties line 120
  9. instance OAI.DilutedSpinGlass.hierarchyMetrizable line 131
  10. instance OAI.DilutedSpinGlass.hierarchySeparable line 133
  11. instance OAI.DilutedSpinGlass.hierarchySecondCountable line 136
  12. def OAI.DilutedSpinGlass.ReducedTopology.nodes line 150
  13. lemma OAI.DilutedSpinGlass.ReducedTopology.mem_nodes line 153
  14. def OAI.DilutedSpinGlass.ReducedTopology.boundedTopologies line 157
  15. lemma OAI.DilutedSpinGlass.ReducedTopology.node_arity_le_leaf_card line 162
  16. lemma OAI.DilutedSpinGlass.ReducedTopology.mem_boundedTopologies line 169