OAI/MathematicalPhysics/Boltzmann/Compactness/EntropyUniformIntegrability.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Joint value and velocity truncation controlled by absolute entropy

  1. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.entropyGauge line 18
  2. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.entropyTruncation line 21
  3. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.entropyGauge_measurable line 24
  4. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.entropyTruncation_measurable line 28
  5. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.entropyGauge_nonneg line 34
  6. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.entropyGauge_ge_density line 38
  7. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.entropyTruncation_bounds line 46
  8. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.entropyTruncation_support line 54
  9. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.entropyTruncation_error line 59
  10. theorem OAI.BoltzmannNonuniqueness.scalarRelativeEntropy_truncation_perturbation_le line 103
  11. theorem OAI.BoltzmannNonuniqueness.entropy_truncation_perturbation_tendsto line 116
  12. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.integrable_of_entropyGauge line 172
  13. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.entropyTruncation_integrable line 179
  14. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.entropyTruncation_L1_bound line 186
  15. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.entropyTruncation_uniformIntegrable line 203
  16. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.exists_entropyTruncation_radius line 246
  17. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.uniformIntegrable_of_entropyGauge line 257
  18. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.unifTight_of_entropyGauge line 272