OAI/Geometry/CylinderCovering/Rational/CostActual.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SlopeRational.cost_physicalScale_pos line 16
2. lemma OAI.SlopeRational.cost_physicalScale_sq line 20
3. lemma OAI.SlopeRational.cost_physicalWeight_eq_energy line 25
4. lemma OAI.SlopeRational.cost_normalization line 35
5. lemma OAI.SlopeRational.cost_ceiling_nonneg line 44
6. lemma OAI.SlopeRational.cost_baseDomain_subset line 49
7. lemma OAI.SlopeRational.cost_baseDomain_measurable line 59
8. theorem OAI.SlopeRational.cost_bound_from_domain_area line 63
9. theorem OAI.SlopeRational.weightedCost_expansion_bound line 81
10. theorem OAI.SlopeRational.weightedCost_expansion line 100