OAI/MathematicalPhysics/Boltzmann/Jets/TorusVelocityWindowAE.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The actual periodic approximations satisfy a spacetime mild identity

  1. theorem OAI.BoltzmannNonuniqueness.TorusFlight.initialDensity_measurable line 21
  2. theorem OAI.BoltzmannNonuniqueness.TorusFlight.spacetime_mild line 30
  3. theorem OAI.BoltzmannNonuniqueness.TorusFlight.flight_measurePreserving_velocity line 74
  4. theorem OAI.BoltzmannNonuniqueness.TorusFlight.along_measurePreserving_velocity line 90
  5. theorem OAI.BoltzmannNonuniqueness.TorusFlight.alongRegroup_measurePreserving line 98
  6. theorem OAI.BoltzmannNonuniqueness.TorusFlight.strong_along_regroup line 105
  7. theorem OAI.BoltzmannNonuniqueness.TorusKineticChart.eLpNorm_liftDensity line 131
  8. theorem OAI.BoltzmannNonuniqueness.TorusKineticChart.cutoff_liftDensity_L1_bound line 138
  9. theorem OAI.BoltzmannNonuniqueness.TorusKineticChart.cutoff_liftDensity_integrable line 158
  10. theorem OAI.BoltzmannNonuniqueness.TorusFlight.flight_snd line 181
  11. theorem OAI.BoltzmannNonuniqueness.TorusFlight.backRegroup_measurePreserving line 183
  12. theorem OAI.BoltzmannNonuniqueness.TorusFlight.weak_along_regroup_local line 196
  13. theorem OAI.BoltzmannNonuniqueness.TorusFlight.uniformIntegrable_along_regroup_local line 208
  14. theorem OAI.BoltzmannNonuniqueness.TorusKineticChart.average_lift_difference_le line 231
  15. theorem OAI.BoltzmannNonuniqueness.ae_timePhase_of_velocity_windows line 270