OAI/Geometry/Perimeter/Regularity/EllipticC1Parts.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RPISingularHarnack.scalar_compact_integration_parts_C1 line 9
2. theorem OAI.RPISingularHarnack.integral_mul_divergence_eq_neg_inner_gradient_C1 line 31
3. theorem OAI.RPISingularHarnack.gradient_continuous_C1 line 66
4. theorem OAI.RPISingularHarnack.C1_gradient_curl_pairing_zero line 70