OAI/MathematicalPhysics/Boltzmann/Compactness/KineticEndpointCoordinates.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The four compactness alternatives for kinetic endpoints

  1. theorem OAI.BoltzmannNonuniqueness.kinetic_endpoint_subsequence line 18
  2. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.fromKinetic_continuous line 69
  3. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.nonaxial_of_transverse_ne_zero line 76
  4. theorem OAI.BoltzmannNonuniqueness.FiveGainMap.eventually_velocityWindow line 82