OAI/Geometry/TranslativeCovering/CapCost.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CapCost.rate line 24
2. def OAI.CapCost.intensity line 26
3. instance OAI.CapCost.intensity_finite line 29
4. instance OAI.CapCost.intensity_null line 31
5. lemma OAI.CapCost.intensity_real line 34
6. lemma OAI.CapCost.cap_real_pos line 41
7. lemma OAI.CapCost.halfcap_real_pos line 45
8. lemma OAI.CapCost.intensity_cap line 49
9. lemma OAI.CapCost.log_decrease line 60
10. lemma OAI.CapCost.clipped_cost line 83
11. lemma OAI.CapCost.raw_upper line 102