OAI/MathematicalPhysics/Boltzmann/Compactness/FiniteEntryPhaseBound.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Reachable regions for a fixed finite number of physical gain collisions

  1. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.finiteFlightCone line 18
  2. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.finiteFlightCone_measurable line 22
  3. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.finiteFlightCone_initial line 27
  4. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.markedChild_norm_le line 31
  5. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.finiteFlightCone_parameter_step line 44
  6. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.finiteFlightCone_displacement line 86
  7. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.finiteFlightCone_cold_domain line 94
  8. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.finiteFlightCone_phase_bound line 111
  9. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.finite_velocity_window_bounds line 152
  10. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.phaseBallCore line 184
  11. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.phaseBallCore_measurable line 186
  12. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.finiteFlightCone_window_core line 189
  13. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.exists_phaseBall_cutoff line 201