OAI/MeasureTheory/Falconer/Angular/InverseCircleArcLength.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PlanarFalconer.periodic_sourceAngle_complex line 10
2. def OAI.PlanarFalconer.inverseCircleOperator line 21
3. theorem OAI.PlanarFalconer.inverseCircleOperator_comp line 24
4. theorem OAI.PlanarFalconer.circle_measurable_of_angular line 31
5. theorem OAI.PlanarFalconer.inverseCircleOperator_measurable line 39
6. theorem OAI.PlanarFalconer.inner_sourceDirection line 44
7. theorem OAI.PlanarFalconer.displacement_has_angle line 50
8. def OAI.PlanarFalconer.sourceInverseCircleIntegral line 60
9. theorem OAI.PlanarFalconer.sourceInverseCircleIntegral_eq line 66