OAI/Analysis/RieszRectifiability/Flatness/BilateralBeta.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RieszRectifiability.directedBallDeviation line 12
2. def OAI.RieszRectifiability.bilateralPlaneError line 15
3. def OAI.RieszRectifiability.bilateralBeta line 20
4. theorem OAI.RieszRectifiability.directedBallDeviation_bddAbove line 23
5. theorem OAI.RieszRectifiability.directedBallDeviation_nonneg line 31
6. theorem OAI.RieszRectifiability.directedBallDeviation_le line 37
7. theorem OAI.RieszRectifiability.bilateralPlaneError_nonneg line 45
8. theorem OAI.RieszRectifiability.bilateralBeta_nonneg line 51
9. theorem OAI.RieszRectifiability.bilateralBeta_le_planeError line 57
10. theorem OAI.RieszRectifiability.bilateralBeta_lt_of_support_tubes line 67