OAI/Probability/InvariantIsing/Cavity/CavityCompressionBlocks.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Joint Haar compression limits for the actual measurable cavity block construction. Only continuity at the prescribed limiting stack is used; the completion rule need not be continuous on every frame.

  1. lemma OAI.InvariantIsing.cavityFrame_measurable_integral_eq_haar line 18
  2. def OAI.InvariantIsing.cavityReindexedStack line 38
  3. lemma OAI.InvariantIsing.measurable_cavityReindexedStack line 42
  4. def OAI.InvariantIsing.cavityCompressionBlocks line 52
  5. lemma OAI.InvariantIsing.measurable_cavityCompressionBlocks line 60
  6. theorem OAI.InvariantIsing.cavityCompressionBlocks_tendsto line 73
  7. theorem OAI.InvariantIsing.cavityHaarCompressionBlocks_integral_tendsto line 98