OAI/Analysis/IrrationalRotation/Operators/VectorProjectionNormality.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.vectorTrace_starProjection_re line 17
2. theorem OAI.Invariant233.vectorTrace_starProjection_mono line 25
3. theorem OAI.Invariant233.tendsto_vectorTrace_starProjection_iSup line 37
4. theorem OAI.Invariant233.iSup_vectorTrace_starProjection line 44
5. theorem OAI.Invariant233.tendsto_vectorTrace_starProjection_exhaustion line 58
6. theorem OAI.Invariant233.tendsto_vectorTrace_starProjection_exhaustion_one line 70
7. theorem OAI.Invariant233.starProjection_closure_iSup_mem line 79
8. theorem OAI.Invariant233.vectorTrace_projection_normality line 97