OAI/Probability/ContinuumTransition/DensityLimit.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ContinuumTemperature.densityFilter line 12
  2. instance OAI.ContinuumTemperature.densityFilter_countablyGenerated line 15
  3. theorem OAI.ContinuumTemperature.densityFilter_length line 18
  4. theorem OAI.ContinuumTemperature.densityFilter_density line 25
  5. theorem OAI.ContinuumTemperature.tendsto_densityFilter_iff line 29
  6. theorem OAI.ContinuumTemperature.floor_density_tendsto line 36
  7. instance OAI.ContinuumTemperature.densityFilter_neBot line 42
  8. theorem OAI.ContinuumTemperature.tileCount_asymptotic line 45
  9. theorem OAI.ContinuumTemperature.length_inv_cube_tendsto line 52
  10. def OAI.ContinuumTemperature.DensityBounded line 57
  11. def OAI.ContinuumTemperature.HasBoxInequality line 61
  12. theorem OAI.ContinuumTemperature.density_eventually_bounded line 65
  13. theorem OAI.ContinuumTemperature.densityFilter_bounded line 74
  14. theorem OAI.ContinuumTemperature.limsup_box_comparison line 82
  15. theorem OAI.ContinuumTemperature.dilution_tendsto_one line 111
  16. theorem OAI.ContinuumTemperature.exists_density_limit line 127