OAI/MathematicalPhysics/Boltzmann/Branching/LateBoxAccessMeasure.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

The expanding boxes used in the finite-horizon growth contradiction

  1. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.lateBox line 22
  2. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.lateBox_measurable line 25
  3. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.physicalBlockTarget_subset_lateBox line 29
  4. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.flight_eventually_lateBox line 40
  5. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.lateBoxCapConstant line 87
  6. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.lateBoxCapConstant_nonneg line 90
  7. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.density_lateBox_bound line 96
  8. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.lateBox_radius_bounds line 159
  9. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.lateBox_geometric_scale line 183
  10. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.lateBox_block_duration line 205
  11. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.lateBox_damping_range line 241
  12. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.lateBox_damping_normalization line 260
  13. theorem OAI.BoltzmannNonuniqueness.GrowthContradiction.next_good_growth_time_in_interval line 282
  14. theorem OAI.BoltzmannNonuniqueness.GrowthContradiction.no_late_ae_growth_with_cap line 297
  15. theorem OAI.BoltzmannNonuniqueness.GrowthContradiction.ae_zero_of_late_growth_cap line 331
  16. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.bounded_flight_lateBox line 365
  17. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.entryVelocityRegion line 398
  18. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.entryVelocityRegion_measurable line 401
  19. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.positive_mass_eventually_lateBox line 405