OAI/Probability/InvariantIsing/Cavity/CavityHaarSides.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A right-invariant probability has the same inverse law and is left-invariant. In particular the oriented base law supplies the SO Haar hypothesis used by the finite-model concentration estimates.

  1. instance OAI.InvariantIsing.cavityOrthogonal_measurableMul line 16
  2. instance OAI.InvariantIsing.cavitySpecialOrthogonal_measurableMul line 28
  3. instance OAI.InvariantIsing.cavitySpecialOrthogonal_measurableInv line 40
  4. lemma OAI.InvariantIsing.cavity_right_probability_inv_eq line 48
  5. lemma OAI.InvariantIsing.cavity_right_probability_left line 63
  6. lemma OAI.InvariantIsing.cavityOrientedBaseLaw_rightInvariant line 69
  7. lemma OAI.InvariantIsing.cavityOrientedBaseLaw_leftInvariant line 79