OAI/MathematicalPhysics/Boltzmann/Jets/GeometricDampedRetention.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Uniform loss control for the geometric cold family and bounded hot remainder

  1. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.geometric_loss_bound line 28
  2. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.geometric_loss_scale_bound line 132
  3. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.beamMeasure_integral line 236
  4. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.BeamNear.frequency_bound line 246
  5. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.frequency_eq_beamFrequency line 271
  6. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.frequency_le_near_clock line 287
  7. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.join_zero_axis line 317
  8. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.beamVelocity_error line 326
  9. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.selected_scale_error_small line 332
  10. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.beam_density_tolerance line 348
  11. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedMediumCollision_eq_nonzero_marks line 396
  12. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.scaled_retention_eq_actual line 415