OAI/MathematicalPhysics/Boltzmann/Approximation/CapEntropyMoments.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The actual cap shots satisfy the finite entropy-dissipation inequality

  1. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.entropy_dissipation line 29
  2. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.finiteEntropy line 64
  3. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.CapApproximation.entropy_dissipation_extended line 78
  4. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.TightCapFamily.weak_each_time line 119
  5. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.TightCapFamily.exists_mild_limit_with_traces_and_convergence line 149
  6. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.TightCapFamily.exists_mild_limit_with_time_traces line 171
  7. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.TightCapFamily.entropy_mild_limit_of_convergence line 208
  8. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.TightCapFamily.exists_entropy_mild_limit line 257
  9. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.TightCapFamily.exists_energy_conserving_local_solution line 294
  10. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.TightCapFamily.exists_finite_entropy_mild_limit line 344
  11. theorem OAI.BoltzmannNonuniqueness.JetCopyDatum.TightCapFamily.exists_entropy_moment_mild_limit line 391