OAI/MeasureTheory/Falconer/Angular/CircleRotation.lean
12 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.PlanarFalconer.periodic_sourceAngle_valueline 9 - def
OAI.PlanarFalconer.sourceCircleRotateline 20 - theorem
OAI.PlanarFalconer.sourceCircleRotate_compline 23 - theorem
OAI.PlanarFalconer.sourceCircleRotate_distline 28 - theorem
OAI.PlanarFalconer.sourceCircleRotate_isometryline 39 - theorem
OAI.PlanarFalconer.sourceCircleRotate_addline 42 - theorem
OAI.PlanarFalconer.sourceCircleRotate_zeroline 48 - def
OAI.PlanarFalconer.sourceCircleRotationline 51 - theorem
OAI.PlanarFalconer.sourceCircleRotate_integralline 59 - theorem
OAI.PlanarFalconer.sourceCircleRotate_derivline 72 - theorem
OAI.PlanarFalconer.sourceCircleRotate_contDiffline 78 - theorem
OAI.PlanarFalconer.sourceCircleRotate_tsupportline 83