OAI/Analysis/IrrationalRotation/Sampling/SamplingCylinderWeak.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Invariant233.SamplingCylinderWeak.tendsto_finiteMeasure_of_piSystem line 13
  2. abbrev OAI.Invariant233.SamplingCylinderWeak.CylinderTest line 42
  3. def OAI.Invariant233.SamplingCylinderWeak.cylinder line 44
  4. theorem OAI.Invariant233.SamplingCylinderWeak.cylinder_empty line 47
  5. theorem OAI.Invariant233.SamplingCylinderWeak.cylinder_union line 52
  6. theorem OAI.Invariant233.SamplingCylinderWeak.cylinder_isOpen line 64
  7. theorem OAI.Invariant233.SamplingCylinderWeak.cylinder_piSystem line 73
  8. theorem OAI.Invariant233.SamplingCylinderWeak.exists_cylinder_nhds_subset line 79
  9. theorem OAI.Invariant233.SamplingCylinderWeak.tendsto_finiteMeasure_of_cylinders line 105
  10. def OAI.Invariant233.SamplingCylinderWeak.cutCoordinates line 125
  11. def OAI.Invariant233.SamplingCylinderWeak.quotientCoordinates line 128
  12. theorem OAI.Invariant233.SamplingCylinderWeak.cutCoordinates_measurable line 131
  13. theorem OAI.Invariant233.SamplingCylinderWeak.quotientCoordinates_continuous line 140
  14. theorem OAI.Invariant233.SamplingCylinderWeak.quotient_cutCoordinates line 144
  15. def OAI.Invariant233.SamplingCylinderWeak.endpointCylinder line 148
  16. theorem OAI.Invariant233.SamplingCylinderWeak.endpointCylinder_measurable line 151
  17. theorem OAI.Invariant233.SamplingCylinderWeak.map_quotient_cut line 155
  18. theorem OAI.Invariant233.SamplingCylinderWeak.tendsto_endpoint_of_cylinders line 164
  19. theorem OAI.Invariant233.SamplingCylinderWeak.weaklyConverges_of_cylinders line 180
  20. theorem OAI.Invariant233.SamplingCylinderWeak.ae_weaklyConverges_of_cylinders line 196
  21. theorem OAI.Invariant233.SamplingCylinderWeak.ae_all_weaklyConverges_of_cylinders line 207
  22. theorem OAI.Invariant233.SamplingCylinderWeak.ae_all_triangular_weaklyConverges_of_cylinders line 217