OAI/Geometry/Perimeter/Regularity/SupportAffineEstimate.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RPISingularHarnack.normalWindowQuadratic_integrableOn line 12
2. theorem OAI.RPISingularHarnack.normalWindowQuadratic_nonneg line 23
3. theorem OAI.RPISingularHarnack.exists_minimizing_linear_mean_value_constant line 29
4. theorem OAI.RPISingularHarnack.minimizing_affine_error_from_trace line 38
5. theorem OAI.RPISingularHarnack.minimizing_support_taylor_estimate line 85