OAI/MathematicalPhysics/Boltzmann/Compactness/EntropyLocalConstruction.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A strong local solution with the full entropy and moment bounds

  1. theorem OAI.BoltzmannNonuniqueness.uniform_entropyMoment_of_entropy_inequality line 16
  2. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.TightCapFamily.exists_entropy_local_solution line 38