OAI/Geometry/IntegralFillings/Main.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpIntegralFillings.Optimality.sphereArea_pos line 22
2. lemma OAI.SharpIntegralFillings.Optimality.fillingCoefficient_pos line 25
3. lemma OAI.SharpIntegralFillings.Optimality.sharp_ball_identity line 29
4. lemma OAI.SharpIntegralFillings.Optimality.sharp_ball_bound line 49
5. theorem OAI.SharpIntegralFillings.coefficient_optimal line 60

   Distinct definitions of this name: ComparatorChallenges/FillingCoefficient.lean:120 (same statement text; different proof or body). Qualify references as OAI.SharpIntegralFillings.coefficient_optimal@path.