OAI/Probability/InvariantIsing/Fields/SimpleFieldData.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

A simple random field is represented using only its positive-mass values.

  1. def OAI.InvariantIsing.simpleFieldIndex line 16

    Distinct definitions of this name: ComparatorChallenges/InvariantIsing.lean:176 (different declaration text). Qualify references as OAI.InvariantIsing.simpleFieldIndex@path.

  2. lemma OAI.InvariantIsing.measurable_simpleFieldIndex line 19
  3. def OAI.InvariantIsing.simpleFieldWeight line 22

    Distinct definitions of this name: ComparatorChallenges/InvariantIsing.lean:179 (different declaration text). Qualify references as OAI.InvariantIsing.simpleFieldWeight@path.

  4. abbrev OAI.InvariantIsing.SimpleFieldPositive line 25

    Distinct definitions of this name: ComparatorChallenges/InvariantIsing.lean:182 (different declaration text). Qualify references as OAI.InvariantIsing.SimpleFieldPositive@path.

  5. lemma OAI.InvariantIsing.simpleFieldWeight_sum line 28
  6. instance OAI.InvariantIsing.simpleFieldPositive_nonempty line 32
  7. def OAI.InvariantIsing.simpleFieldPositiveIndex line 37
  8. lemma OAI.InvariantIsing.measurable_simpleFieldPositiveIndex line 41
  9. def OAI.InvariantIsing.simpleFieldValue line 45

    Distinct definitions of this name: ComparatorChallenges/InvariantIsing.lean:185 (different declaration text). Qualify references as OAI.InvariantIsing.simpleFieldValue@path.

  10. lemma OAI.InvariantIsing.simpleFieldPositiveIndex_weight line 50
  11. lemma OAI.InvariantIsing.simpleFieldPositiveIndex_ae line 55
  12. lemma OAI.InvariantIsing.simpleField_law line 63
  13. lemma OAI.InvariantIsing.simpleField_integrable line 74