OAI/Analysis/IrrationalRotation/Rotation/RotationMeasurableLaws.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Invariant233.Rotation.measurableRepresentation_mul line 12
  2. theorem OAI.Invariant233.Rotation.measurableRepresentation_star line 25
  3. theorem OAI.Invariant233.Rotation.measurableRepresentation_eq_iff line 34
  4. theorem OAI.Invariant233.Rotation.vacuumFunctional_measurableRepresentation line 52
  5. theorem OAI.Invariant233.Rotation.lpNorm_le_norm_of_orbit_representation line 69
  6. theorem OAI.Invariant233.Rotation.measurableRepresentation_norm line 96
  7. theorem OAI.Invariant233.Rotation.exists_unique_isometric_mem_algebra_of_memLp_top line 115