OAI/Geometry/Perimeter/Regularity/CoupledConeLink.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RPISingularHarnack.SphericalFrankel.angle_swap line 11
2. lemma OAI.RPISingularHarnack.SphericalFrankel.cross_swap line 13
3. lemma OAI.RPISingularHarnack.SphericalFrankel.traceProduct_swap line 15
4. lemma OAI.RPISingularHarnack.SphericalFrankel.continuous_defect_reverse line 20
5. lemma OAI.RPISingularHarnack.SphericalFrankel.product_frames line 25
6. lemma OAI.RPISingularHarnack.SphericalFrankel.stationary_product_integral line 34
7. lemma OAI.RPISingularHarnack.SphericalFrankel.stationary_gradient_one line 55
8. lemma OAI.RPISingularHarnack.SphericalFrankel.stationary_mixed_one line 81
9. lemma OAI.RPISingularHarnack.SphericalFrankel.coupledStationarity_product line 116
10. lemma OAI.RPISingularHarnack.SphericalFrankel.minimizing_cones_coupledStationarity line 154