OAI/MathematicalPhysics/Boltzmann/Compactness/PeriodicRenormalizedCompactness.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Weak L1 extraction for the actual global approximation sequence

  1. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.kinetic_entropy_integrable line 20
  2. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.kinetic_entropy_integral_le line 30
  3. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.approximatingSolution_compactness_hypotheses line 42
  4. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.exists_weak_approximation_limit line 58
  5. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.windowKernel_le_physical line 84
  6. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.regularizedPreRate_le_physical line 92
  7. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.loss_le_physical line 102
  8. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.normalizedLoss_uniformIntegrable line 118
  9. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.approximatingSolution_normalizedLoss_uniformIntegrable line 145
  10. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.normalizedGain_uniformIntegrable line 174
  11. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.relativeEntropy_all_times line 205
  12. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.approximatingSolution_relativeEntropy line 213
  13. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.approximatingSolution_spacetimeEntropy_integrable line 220
  14. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.approximatingSolution_spacetimeRelativeEntropy line 229
  15. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.initialEntropyBudget_nonneg line 240
  16. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.approximatingSolution_dissipation_bound line 261
  17. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.approximatingSolution_normalizedSources_uniformIntegrable line 283
  18. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.extendedDissipation_mono_measure line 324
  19. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.earlier_joint_budget line 330
  20. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.approximatingSolution_renormalizedSources_uniformIntegrable line 368
  21. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.approximatingSolution_rational_uniform_L1 line 408
  22. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.approximatingSolution_renormalizedDensity_uniformIntegrable line 438