OAI/MathematicalPhysics/Boltzmann/Approximation/SubcapCapLocalAdmissibility.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Finite entropy-dissipation bounds for approximations below the cap

  1. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.Approximation.entropy_dissipation line 19
  2. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.Approximation.finiteEntropy line 54
  3. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.Approximation.entropy_dissipation_extended line 68
  4. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.TightFamily.entropy_mild_limit_of_convergence line 109
  5. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.TightFamily.exists_entropy_mild_limit line 158
  6. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.Approximation.moment_bound line 196
  7. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.CompactFamily.weak_limit_moment line 221
  8. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.TightFamily.exists_entropy_moment_mild_limit line 267
  9. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.BelowCap.TightFamily.exists_admissible_local_solution line 324