OAI/Analysis/IrrationalRotation/Rotation/RotationSetProjectionSmallSupport.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.RotationSmallSupport.orbitCutoff_eq_borelSetProjection line 12
2. theorem OAI.Invariant233.Rotation.borelSetProjection_tendsto_apply line 19
3. theorem OAI.Invariant233.Rotation.norm_borelSetProjection_fourierCoordinate line 25
4. theorem OAI.Invariant233.Rotation.tendsto_apply_of_small_borel_boundary line 30