OAI/MathematicalPhysics/Boltzmann/Compactness/PeriodicJointBudgetLimit.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

The actual global density and normalized pair on one averaging subsequence

  1. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.exists_global_density_pair_with_patch_averages line 33
  2. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalWeakLimit.localized_weak line 69
  3. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalWeakLimit.patch_mass_strong line 99
  4. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.approximatingSolution_energy_le line 161
  5. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.approximatingSolution_truncated_energy_le line 173
  6. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalWeakLimit.truncated_energy_ae_on_window line 197
  7. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalWeakLimit.energy_ae line 217
  8. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.patch_bounds line 246
  9. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.exists_global_density_pair_with_strong_mass line 261
  10. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalWeakLimit.normalizedPair_identified_on_window line 318
  11. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalWeakLimit.lifted_mass_strong_of_patches line 398
  12. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalWeakLimit.mass_strong_of_patches line 432
  13. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.exists_globalWeakLimit_with_strong_mass_pairs line 486
  14. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.exists_globalWeakLimit_with_normalized_pairs line 531
  15. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalWeakLimit.kinetic_entropy_on_window line 571
  16. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalWeakLimit.weightedPair_on_window line 579
  17. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.exists_globalWeakLimit_with_weighted_pairs line 610
  18. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalWeakLimit.weak_linearMoment_on_window line 635
  19. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalWeakLimit.linear_test_tendsto line 660
  20. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.exists_globalWeakLimit_with_normalized_rates line 708
  21. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalWeakLimit.finite_rates_of_pairs line 754
  22. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.exists_globalWeakLimit_with_strong_mass_rates line 804
  23. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalWeakLimit.physical_dissipation_le_liminf line 842
  24. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalWeakLimit.physical_dissipation_bound line 877
  25. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.exists_globalWeakLimit_with_finite_rates line 920
  26. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalWeakLimit.mass_transport_tendsto line 971
  27. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.local_mass_balance line 1012
  28. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.local_mass_equation line 1053
  29. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalWeakLimit.local_mass_equation line 1078
  30. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalWeakLimit.normalized_collision_integrability line 1131
  31. structure OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit line 1171
  32. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.exists_globalCollisionLimit line 1196
  33. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.dissipation_bound line 1202
  34. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.normalized_integrability line 1209
  35. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.GlobalCollisionLimit.averaged_joint_budget line 1241