OAI/Geometry/IntegralFillings/Optimality/Calibration.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpIntegralFillings.Optimality.ambientCoord line 14
2. def OAI.SharpIntegralFillings.Optimality.unitCoord line 15
3. lemma OAI.SharpIntegralFillings.Optimality.ambientCoord_lipschitz line 17
4. lemma OAI.SharpIntegralFillings.Optimality.unitCoord_lipschitz line 25
5. lemma OAI.SharpIntegralFillings.Optimality.unitCoord_bound line 30
6. lemma OAI.SharpIntegralFillings.Optimality.unitCoord_boundedLip line 34
7. lemma OAI.SharpIntegralFillings.Optimality.ballChart_jacobian_coords line 37
8. lemma OAI.SharpIntegralFillings.Optimality.innerBallCurrent_coords line 55
9. lemma OAI.SharpIntegralFillings.Optimality.omega_pos line 94
10. lemma OAI.SharpIntegralFillings.Optimality.ball_volume_scaling line 98
11. lemma OAI.SharpIntegralFillings.Optimality.abs_apply_le_mass line 105