OAI/Probability/RadialTransition/ThermodynamicLimit.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RadialTransition.separated_box_limit line 14
  2. theorem OAI.RadialTransition.grandPressure_exists line 65
  3. theorem OAI.RadialTransition.exists_bounded_fill line 88
  4. theorem OAI.RadialTransition.exists_integer_adjustment line 132
  5. theorem OAI.RadialTransition.sum_changed_cost line 196
  6. theorem OAI.RadialTransition.finiteCanonical_replication line 217
  7. theorem OAI.RadialTransition.finiteCanonical_adjustment line 248
  8. def OAI.RadialTransition.thermodynamicFilter line 269
  9. theorem OAI.RadialTransition.thermodynamicFilter_side line 273
  10. theorem OAI.RadialTransition.thermodynamicFilter_density line 277
  11. theorem OAI.RadialTransition.floor_density_tendsto line 282
  12. theorem OAI.RadialTransition.floor_tendsto_thermodynamicFilter line 287
  13. theorem OAI.RadialTransition.thermodynamicFilter_neBot line 294