OAI/MathematicalPhysics/Boltzmann/Compactness/SelectedRemainderMeasure.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Velocity measurability and measure domination for the actual selected remainder

  1. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.selectedRemainderDensity_measurable_velocity line 17
  2. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.rescaled_cold_measure_majorant line 39