OAI/Analysis/IrrationalRotation/Rotation/CircleRawTagEvent.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Invariant233.CircleDigitCoupling.rawLaw_map_endpoint_density line 21
2. lemma OAI.Invariant233.CircleDigitCoupling.rawLaw_map_endpoint_le_ten line 57
3. lemma OAI.Invariant233.CircleDigitCoupling.rawLaw_tag_mass line 71
4. theorem OAI.Invariant233.CircleDigitCoupling.rawLaw_ae_tag_interval line 80
5. theorem OAI.Invariant233.CircleDigitCoupling.concrete_circle_currentBlock_mass line 117