OAI/MathematicalPhysics/Boltzmann/Compactness/PeriodicFiniteMild.lean

GitHub source file

97 declarations, 0 contain sorry, 0 declared as axioms

Uniform stability of the actual regularized collision integrands

  1. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.pairRate_uniform_difference line 19
  2. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.regularizedPreRate_difference line 32
  3. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.regularizedPostRate_difference line 49
  4. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.rateLipschitz line 70
  5. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.gain_difference line 72
  6. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.loss_difference line 85
  7. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.positiveSource line 98
  8. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.positiveSource_bounds line 101
  9. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.sourceLipschitz line 127
  10. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.positiveSource_measurable line 129
  11. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.positiveSource_difference line 133
  12. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.scaledDensity line 170
  13. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.scaledProfile line 173
  14. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.scaledSource line 176
  15. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.scaledSource_eq line 180
  16. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.scaledDensity_measurable line 184
  17. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.scaledProfile_measurable line 188
  18. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.scaledSource_measurable line 193
  19. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.exp_discount_cancel line 201
  20. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.scaledSource_bounds line 205
  21. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.scaledSource_difference line 228
  22. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.scalingRate line 262
  23. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.dampingRate line 264
  24. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.sourceLipschitz_nonneg line 266
  25. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.scalingRate_pos line 270
  26. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.dampingRate_gt_sourceLipschitz line 276
  27. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.scaledSource_ball line 283
  28. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.exists_weighted_cutoff_solution line 297
  29. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.regularizedPreRate_zero_of_velocity line 335
  30. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.regularizedPostRate_zero_of_velocity line 342
  31. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.gain_zero_of_velocity line 349
  32. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.loss_zero_of_velocity line 356
  33. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.positiveSource_outside line 363
  34. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.attenuation line 382
  35. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.attenuation_nonneg line 384
  36. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.attenuation_le_one line 387
  37. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.attenuation_tendsto line 392
  38. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.rateMultiplier line 400
  39. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.rateMultiplier_bounds line 408
  40. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.regularizedPreRate_factor line 414
  41. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.regularizedPostRate_factor line 423
  42. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.pairBall line 447
  43. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.pairBall_compact line 450
  44. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.regularizedPreRate_zero_of_outside line 454
  45. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.regularizedPreRate_integrable line 464
  46. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.regularizedPostRate_integrable line 480
  47. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.regularizedPreRate_test_integrable line 500
  48. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.regularizedPostRate_test_integrable line 517
  49. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.regularizedPreRate_zero_of_partner line 549
  50. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.regularizedPostRate_zero_of_partner line 555
  51. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.fiberMeasure_eq_restrict line 561
  52. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.loss_eq_full_integral line 567
  53. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.gain_eq_full_integral line 581
  54. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.integral_regularizedPostRate_scatter_right line 610
  55. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.regularized_weak_identity line 621
  56. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.regularized_collision_invariant line 665
  57. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.regularized_test_marginals line 696
  58. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.regularized_test_invariant line 716
  59. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.regularized_mass_balance line 727
  60. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.regularized_energy_balance line 735
  61. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.regularized_momentum_balance line 745
  62. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.integral_jump_post line 774
  63. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.collisionJump_integrable line 785
  64. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.regularized_production_identity line 832
  65. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.regularized_entropy_production_nonneg line 868
  66. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.regularized_relative_production_nonneg line 904
  67. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.regularized_relative_entropy_nonpositive line 911
  68. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.gaussianShift line 947
  69. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.gaussianShift_measurable line 950
  70. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.gaussianShift_pos line 956
  71. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.gaussianShift_difference line 961
  72. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.collisionOperator line 967
  73. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.collisionOperator_measurable line 970
  74. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.collisionOperator_support line 974
  75. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.collisionOperator_gaussian_difference line 978
  76. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.regularizedEntropy_parameter_continuous line 1008
  77. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.regularizedEntropy_uniform_bound line 1017
  78. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.scalarRelativeEntropy_measurable line 1031
  79. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.regularizedEntropy_measurable line 1036
  80. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.regularizedEntropy_integrable line 1042
  81. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.entropy_error_bound line 1082
  82. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.entropyErrorCoefficient line 1100
  83. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.entropy_error_integral line 1104
  84. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.entropy_error_tendsto line 1116
  85. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.velocityRegion line 1138
  86. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.localize line 1140
  87. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.velocityRegion_measurable line 1142
  88. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.localize_measurable line 1145
  89. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.localize_bounds line 1148
  90. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.localize_difference line 1155
  91. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.localized_fixed_point_zero line 1161
  92. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.localized_scaledSource_eq line 1174
  93. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.entropyCompactMajorant line 1199
  94. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.entropyCompactMajorant_integrable line 1202
  95. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.regularizedEntropy_majorant line 1207
  96. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.regularizedEntropy_integral_tendsto line 1226
  97. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.exists_finite_cutoff_mild line 1253