OAI/Probability/InvariantIsing/Gaussian/MPDensitySupport.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Support of the literal MP density, with its zero atom distinguished.

  1. lemma OAI.InvariantIsing.mp_edges_strict line 11
  2. lemma OAI.InvariantIsing.mpDensity_pos line 16
  3. lemma OAI.InvariantIsing.mp_interior_absolutelyContinuous line 21
  4. theorem OAI.InvariantIsing.mp_interval_subset_support line 37