OAI/Combinatorics/KMedian/Geometry/PotentialBounds.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MetricKMedian.PhysicalPotential.B_le_one line 14
2. theorem OAI.MetricKMedian.PhysicalPotential.m_le_one line 19
3. theorem OAI.MetricKMedian.PhysicalPotential.coefficient_bounds line 26
4. theorem OAI.MetricKMedian.PhysicalPotential.cost_le_mass_mul line 34
5. theorem OAI.MetricKMedian.PhysicalPotential.cost_le_radius line 39
6. theorem OAI.MetricKMedian.PhysicalPotential.potential_bounds line 44
7. theorem OAI.MetricKMedian.PhysicalPotential.internal_charge_bound line 61
8. theorem OAI.MetricKMedian.PhysicalPotential.external_charge_bound line 84