OAI/Probability/InvariantIsing/Cavity/CavityMeasurableComplement.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

A global measurable completion of the cavity columns. The rule first tries the prescribed limiting frame and otherwise uses a fixed dense sequence. Near the limit it agrees with the continuous local rule.

  1. def OAI.InvariantIsing.cavityComplementCandidate line 17
  2. def OAI.InvariantIsing.cavityGoodCandidate line 22
  3. lemma OAI.InvariantIsing.continuous_cavityRawComplement line 27
  4. lemma OAI.InvariantIsing.measurableSet_cavityGoodCandidate line 33
  5. lemma OAI.InvariantIsing.cavityGoodCandidate_exists line 39
  6. def OAI.InvariantIsing.cavityComplementChoicePredicate line 56
  7. lemma OAI.InvariantIsing.cavityComplementChoice_exists line 61
  8. def OAI.InvariantIsing.cavitySelectedComplement line 71
  9. lemma OAI.InvariantIsing.measurable_cavitySelectedComplement line 77
  10. lemma OAI.InvariantIsing.cavitySelectedComplement_gram line 98
  11. lemma OAI.InvariantIsing.cavitySelectedComplement_orthogonal line 118
  12. lemma OAI.InvariantIsing.cavitySelectedComplement_eq_local line 124
  13. theorem OAI.InvariantIsing.cavitySelectedComplement_tendsto line 140
  14. lemma OAI.InvariantIsing.cavitySelectedComplement_at_limit line 158
  15. lemma OAI.InvariantIsing.cavitySelectedComplement_continuousAt line 170