OAI/MathematicalPhysics/Boltzmann/Jets/GeometricPositiveCompact.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Measurable two-beam coefficients from the actual geometric cold profiles

  1. def OAI.BoltzmannNonuniqueness.GeometricBackground.beamVelocity line 17
  2. def OAI.BoltzmannNonuniqueness.GeometricBackground.beamDensity line 21
  3. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.beamVelocity_measurable line 25
  4. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.beamDensity_measurable line 47
  5. def OAI.BoltzmannNonuniqueness.GeometricBackground.beamCoefficients line 67
  6. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.beamDensity_eq_relative line 78
  7. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.beamMeasure line 104
  8. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.background_eq_beamMeasure line 112
  9. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.ae_not_mesh_circle line 160
  10. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.active_ae_above_cutoff line 172
  11. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.background_eq_beamMeasure_ae line 181
  12. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.beamDensity_nonneg line 194
  13. theorem OAI.BoltzmannNonuniqueness.GeometricBackground.beamDensity_compact_lower line 217