OAI/Analysis/IrrationalRotation/Spectral/PolarStructure.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InvariantProjection.PolarStructure.countable_finite_drop_values line 14
  2. theorem OAI.InvariantProjection.PolarStructure.ae_countable_range_of_finite_drops line 18
  3. theorem OAI.InvariantProjection.PolarStructure.ae_countable_joint_range line 28
  4. theorem OAI.InvariantProjection.PolarStructure.ae_countable_joint_range_of_measurePreserving line 37
  5. theorem OAI.InvariantProjection.PolarStructure.ae_nonzero_fiber_of_ae_countable_range line 47
  6. theorem OAI.InvariantProjection.PolarStructure.measure_eq_sum_dirac_of_ae_mem_countable line 62
  7. theorem OAI.InvariantProjection.PolarStructure.map_eq_sum_dirac_of_ae_countable_range line 104
  8. theorem OAI.InvariantProjection.PolarStructure.mem_iff_of_eq_of_measurable_comap line 115
  9. theorem OAI.InvariantProjection.PolarStructure.fiber_is_atom_in_comap line 123
  10. theorem OAI.InvariantProjection.PolarStructure.countable_atomic_fiber_partition line 137
  11. theorem OAI.InvariantProjection.PolarStructure.finite_family_atomic_fiber_partition line 153
  12. theorem OAI.InvariantProjection.PolarStructure.not_ae_invariant_of_totalErgodic line 175
  13. theorem OAI.InvariantProjection.PolarStructure.exists_positive_proper_orbit_overlap line 185
  14. theorem OAI.InvariantProjection.PolarStructure.measure_eq_one_of_atom_orbit line 201
  15. theorem OAI.InvariantProjection.PolarStructure.invariant_family_has_no_measure_atoms line 213