OAI/MathematicalPhysics/Boltzmann/Compactness/SelectedOriginDeletion.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Uniform first-gain decay along axially escaping bounded-speed flights

  1. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.selected_axial_escape_small line 23
  2. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.selected_small_input_bound line 95
  3. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.selected_small_input_eventually line 118
  4. abbrev OAI.BoltzmannNonuniqueness.ReferenceGeometry.CollisionWord line 166
  5. abbrev OAI.BoltzmannNonuniqueness.ReferenceGeometry.collisionWordMeasurable line 170
  6. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.collisionWordMeasure line 178
  7. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.collisionWordMeasure_sFinite line 182
  8. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.selectedWordState line 190
  9. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.selectedWordDensity line 195
  10. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.selectedWordState_measurable line 201
  11. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.selectedWordDensity_measurable line 214
  12. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.selectedWord_integral line 228
  13. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.selected_scale_deletion line 276
  14. def OAI.BoltzmannNonuniqueness.JetCopyDatum.transverseRetained line 329
  15. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.transverseRetained_measurable line 331
  16. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.selected_successive_thresholds line 334
  17. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.selected_successive_deletion line 373
  18. def OAI.BoltzmannNonuniqueness.JetCopyDatum.velocityWindow line 427
  19. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.velocityWindow_measurable line 429
  20. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.selected_velocity_radii line 432
  21. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.selected_velocity_windows line 456
  22. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.selected_origin_deletion line 510