OAI/Probability/RadialTransition/CanonicalLimit.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.RadialTransition.(instance at line 12) line 12
2. def OAI.RadialTransition.HasBoxReplication line 16
3. theorem OAI.RadialTransition.boxCost_adjustment line 21
4. theorem OAI.RadialTransition.boxCost_limsup_bound line 38
5. theorem OAI.RadialTransition.tendsto_side_ratio line 99
6. theorem OAI.RadialTransition.boxCost_limit line 110
7. theorem OAI.RadialTransition.boxCost_limit_with_bounds line 188
8. theorem OAI.RadialTransition.finiteCanonical_limit line 231
9. def OAI.RadialTransition.canonicalThermo line 255
10. theorem OAI.RadialTransition.canonicalThermo_spec line 258
11. theorem OAI.RadialTransition.familyCanonicalThermo_spec line 277
12. theorem OAI.RadialTransition.canonicalThermo_concave line 296