OAI/MathematicalPhysics/Boltzmann/Branching/BoundedEntropyProduction.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Collision bounds for a finite approximation under its hot majorant

  1. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.bounded_pair_integrable line 22
  2. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.bounded_cutoff_gain line 32
  3. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.bounded_cutoff_loss line 54
  4. def OAI.BoltzmannNonuniqueness.boundedEntropyTest line 91

    Source documentation

    Outside the bounded logarithmic window use the zero test. At a zero density, use the negative endpoint, which recovers the Maxwellian contribution.

    def boundedEntropyTest (n : ℕ) (m u : ℝ) : ℝ :=
…
  5. theorem OAI.BoltzmannNonuniqueness.boundedEntropyTest_bound line 94
  6. theorem OAI.BoltzmannNonuniqueness.entropyDual_boundedEntropyTest_nonneg line 102
  7. theorem OAI.BoltzmannNonuniqueness.entropyDual_boundedEntropyTest_tendsto line 115
  8. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.bounded_log_gainLoss_integrable line 151
  9. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.bounded_positive_entropy_production line 172