OAI/Probability/InvariantIsing/Cavity/CavityOrientedCoefficients.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The orientation correction used for physical cavity coordinates preserves the actual random quadratic coefficients, including their concentration event.

  1. lemma OAI.InvariantIsing.measurable_cavityPhysicalFactorBlocks line 17
  2. theorem OAI.InvariantIsing.cavity_orientation_factor_event line 27
  3. theorem OAI.InvariantIsing.cavity_orientation_factor_probability line 45