OAI/MeasureTheory/Falconer/Angular/AngularDifferentialBounds.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.PlanarFalconer.AngularDifferentialExpr.smooth_finiteline 12 - theorem
OAI.PlanarFalconer.AngularDifferentialExpr.derivative_boundline 16 - theorem
OAI.PlanarFalconer.AngularDifferentialExpr.derivative_bound_of_order_leline 59 - theorem
OAI.PlanarFalconer.AngularDifferentialExpr.iteratedDeriv_tsupportline 69 - theorem
OAI.PlanarFalconer.AngularDifferentialExpr.apply_tsupportline 75