OAI/MathematicalPhysics/Boltzmann/Compactness/PeriodicInitialEntropyLimit.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

The positive iteration preserves the actual velocity support

  1. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.exists_supported_weighted_solution line 27
  2. structure OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution line 76
  3. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.exists_supported_cutoff_solution line 85
  4. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.finiteEntropy line 116
  5. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.initial line 124
  6. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.initialApproximation line 145
  7. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.initialApproximation_measurable line 148
  8. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.initialApproximation_bounds line 154
  9. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.initialApproximation_support line 161
  10. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.initialApproximation_le line 167
  11. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.initialApproximation_tendsto line 175
  12. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.exists_initial_approximation_solution line 183
  13. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.initialApproximation_entropy_le line 202
  14. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.initialApproximation_finiteEntropy line 221
  15. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.initialApproximation_entropy_integral_le line 227
  16. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.initialApproximation_sequence_eventually_eq line 247
  17. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.initialApproximation_L1_tendsto line 256
  18. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.initialApproximation_entropy_tendsto line 272
  19. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.initialApproximation_norm_tendsto line 308
  20. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.initialApproximation_time_local_strong line 325
  21. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.initialEntropyCoefficient line 372
  22. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.initialEntropyCoefficient_nonneg line 374
  23. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.relativeEntropy_density_bound line 378
  24. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.initialApproximation_relativeEntropy_le line 398
  25. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.kineticSource line 431
  26. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.kineticSource_eq line 435
  27. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.kineticSource_measurable line 438
  28. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.initialApproximation_test_tendsto line 459
  29. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.rateMultiplier_measurable line 495
  30. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.rateMultiplier_pos line 501
  31. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.rateMultiplier_tendsto line 509
  32. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.source line 537
  33. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.source_measurable line 540
  34. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.source_bounded line 548
  35. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.source_path_integrable line 561
  36. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.along_eq_damped line 570
  37. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.tested_path line 588
  38. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.characteristic_integral line 607
  39. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.collisionOperator_test_integrable line 630
  40. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.nonnegative_entropy_production_bound line 640
  41. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.collision_path_integrable line 686
  42. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.entropy_path_balance line 700
  43. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.positiveProduction line 739
  44. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.positiveProduction_nonneg line 745
  45. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.positiveProduction_identity line 751
  46. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.gaussian_entropy_dissipation_bound line 776
  47. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.renormalized_path_balance line 818
  48. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.BoundedCutoffSolution.renormalized_tested_path line 839
  49. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.extendedProduction line 887
  50. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.extendedDissipation line 893
  51. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.positiveProduction_formula line 898
  52. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.ofReal_positiveProduction line 911
  53. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.ofReal_integral_positiveProduction line 926
  54. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.normalizedRateExcess line 952
  55. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.normalizedRateExcess_measurable line 957
  56. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.normalizedRateExcess_bound line 969
  57. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.normalizedRateExcess_integral_bound line 994
  58. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.gaussianShift_tendsto line 1023
  59. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.extendedDissipation_gaussian_le_liminf line 1029
  60. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.normalizer line 1089
  61. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.normalizer_measurable line 1091
  62. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.normalizer_ge_one line 1097
  63. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.normalizer_pos line 1101
  64. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.normalizedRates_integrable line 1104
  65. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.normalizedRateExcess_integrable line 1127
  66. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.normalizedGainExcess line 1150
  67. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.normalizedRateExcess_marginal_ae line 1153
  68. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.normalizedGainExcess_integral_bound line 1173
  69. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.initialApproximation_linear_moment_tendsto line 1209
  70. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.initialApproximation_relativeEntropy_tendsto line 1250