OAI/Probability/InvariantIsing/Cavity/CavityPhysicalBase.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Measurable base interaction built from the actual cavity columns.

  1. def OAI.InvariantIsing.cavityColumns line 15
  2. def OAI.InvariantIsing.cavityCompressionGrams line 19
  3. def OAI.InvariantIsing.cavityPhysicalBase line 24
  4. lemma OAI.InvariantIsing.measurable_cavityColumns line 35
  5. lemma OAI.InvariantIsing.measurable_cavityCompressionGrams line 41
  6. lemma OAI.InvariantIsing.measurable_cavityPhysicalBase line 48
  7. lemma OAI.InvariantIsing.cavityCompressionGrams_reservoir line 85
  8. lemma OAI.InvariantIsing.cavityPhysicalBase_reservoir line 94
  9. theorem OAI.InvariantIsing.cavityPhysicalBase_mem_orbit line 123