OAI/MathematicalPhysics/Boltzmann/Jets/ThermalStripeIdentity.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Weak averaging after the Gaussian thermal mixture

  1. def OAI.BoltzmannNonuniqueness.JetGeometry.thermalStripeCentered line 18
  2. theorem OAI.BoltzmannNonuniqueness.JetGeometry.thermalStripeCentered_bound line 22
  3. theorem OAI.BoltzmannNonuniqueness.JetGeometry.thermalStripeCentered_measurable line 26
  4. theorem OAI.BoltzmannNonuniqueness.JetGeometry.thermalStripeCentered_weakStar line 35
  5. theorem OAI.BoltzmannNonuniqueness.JetGeometry.stripe_dilated_indicator line 91
  6. theorem OAI.BoltzmannNonuniqueness.JetGeometry.thermalStripeCentered_eq line 102