OAI/Probability/InvariantIsing/Core/InvariantOrbitLaw.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Joint orbit laws from measure-preserving rotations and pointwise Haar kernels. The proof avoids measurable eigenvector selections.

  1. lemma OAI.InvariantIsing.paired_map_eq_of_comp line 11
  2. lemma OAI.InvariantIsing.map_prod_eq_of_fiber_maps line 21
  3. theorem OAI.InvariantIsing.invariant_joint_orbit_law line 38