OAI/Probability/InvariantIsing/Gaussian/IndexedGaussianMaximum.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The finite maximum comparison with an arbitrary nonempty Gaussian coordinate set.

  1. def OAI.InvariantIsing.indexedGaussianMaximum line 12
  2. lemma OAI.InvariantIsing.measurable_indexedGaussianMaximum line 15
  3. lemma OAI.InvariantIsing.indexedGaussianMaximum_reindex line 23
  4. theorem OAI.InvariantIsing.indexed_gaussian_maximum_comparison line 47