OAI/MathematicalPhysics/Boltzmann/Compactness/L1CurveEquality.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Spacetime equality determines a strongly continuous L¹ curve at every time

  1. theorem OAI.BoltzmannNonuniqueness.strong_ae_eq_all_times line 15
  2. theorem OAI.BoltzmannNonuniqueness.MildCollisionSolution.evolution_eq_positive_each_time line 53