OAI/Geometry/IntegralFillings/Optimality/GoodRadius.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpIntegralFillings.Optimality.exists_le_of_integral_le_ae line 13
2. lemma OAI.SharpIntegralFillings.Optimality.integral_radial_area line 32
3. theorem OAI.SharpIntegralFillings.Optimality.exists_good_inner_ball line 48