OAI/MathematicalPhysics/Boltzmann/Compactness/PeriodicMildApproximation.lean

GitHub source file

73 declarations, 0 contain sorry, 0 declared as axioms

Bounded positive periodic mild states and finite-step continuation

  1. structure OAI.BoltzmannNonuniqueness.WeightedLocalControl.PeriodicMildState line 30
  2. theorem OAI.BoltzmannNonuniqueness.WeightedLocalControl.PeriodicMildState.all_mild line 40
  3. def OAI.BoltzmannNonuniqueness.WeightedLocalControl.PeriodicMildState.restrict line 46
  4. def OAI.BoltzmannNonuniqueness.WeightedLocalControl.PeriodicMildState.initial line 58
  5. theorem OAI.BoltzmannNonuniqueness.WeightedLocalControl.PeriodicMildState.exists_extension line 75
  6. theorem OAI.BoltzmannNonuniqueness.WeightedLocalControl.exists_to_time_of_apriori line 92
  7. theorem OAI.BoltzmannNonuniqueness.WeightedLocalControl.PeriodicMildState.exists_seed_limit line 152
  8. theorem OAI.BoltzmannNonuniqueness.WeightedLocalControl.PeriodicMildState.nearby_seed_exists line 208
  9. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.collisionWindow line 255
  10. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.windowKernel line 258
  11. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.collisionWindow_measurable line 261
  12. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.windowKernel_measurable line 265
  13. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.collisionWindow_bounds line 271
  14. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.windowKernel_bounds line 279
  15. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.windowKernel_scatter line 291
  16. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.windowKernel_particleSwap line 306
  17. def OAI.BoltzmannNonuniqueness.WeightedLocalControl.PeriodicMildState.affineSeed line 339
  18. def OAI.BoltzmannNonuniqueness.WeightedLocalControl.PeriodicMildState.hotPeak line 342
  19. theorem OAI.BoltzmannNonuniqueness.WeightedLocalControl.PeriodicMildState.affineSeed_difference line 347
  20. theorem OAI.BoltzmannNonuniqueness.WeightedLocalControl.PeriodicMildState.exists_cap_limit line 354
  21. theorem OAI.BoltzmannNonuniqueness.WeightedLocalControl.PeriodicMildState.strict_cap_open line 415
  22. theorem OAI.BoltzmannNonuniqueness.PeriodicAveraging.bounded_intervalIntegrable line 498
  23. theorem OAI.BoltzmannNonuniqueness.PeriodicAveraging.primitive_bound line 503
  24. theorem OAI.BoltzmannNonuniqueness.PeriodicAveraging.interval_bound line 521
  25. theorem OAI.BoltzmannNonuniqueness.PeriodicAveraging.test_bound line 535
  26. theorem OAI.BoltzmannNonuniqueness.WeightedLocalControl.PeriodicMildState.select_seed_at_cap line 589
  27. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.rateSum line 672
  28. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.pairRate line 674
  29. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.rateSum_nonneg line 677
  30. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.pairRate_eq line 680
  31. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.pairRate_nonneg line 683
  32. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.pairRate_le_square line 690
  33. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.pairRate_swap_inputs line 702
  34. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.pairRate_swap_outputs line 705
  35. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.pairRate_tendsto line 708
  36. theorem OAI.BoltzmannNonuniqueness.PeriodicAveraging.ac_test_tendsto_zero line 745
  37. theorem OAI.BoltzmannNonuniqueness.PeriodicAveraging.uniformContinuous_test_tendsto_zero line 758
  38. theorem OAI.BoltzmannNonuniqueness.PeriodicAveraging.weakStar_zero line 817
  39. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.fraction_difference_le line 853
  40. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.unit_product_difference line 890
  41. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.rateSum_difference_le line 901
  42. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.pairRate_difference_le line 911
  43. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.pairRate_le_linear line 945
  44. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.regularizedPreRate line 972
  45. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.regularizedPostRate line 978
  46. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.regularizedPreRate_measurable line 982
  47. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.regularizedPostRate_measurable line 988
  48. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.regularizedPostRate_formula line 993
  49. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.regularizedPostRate_scatter line 1011
  50. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.regularizedPreRate_particleSwap line 1017
  51. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.regularizedPreRate_bounds line 1031
  52. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.regularizedPreRate_linear line 1044
  53. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.maxwellian_le_center line 1069
  54. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.maxwellian_lower_on_ball line 1075
  55. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.logRegularizationConstant line 1085
  56. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.log_regularization_bound line 1088
  57. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.regularizedPostRate_particleSwap line 1130
  58. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.integral_regularizedPostRate line 1136
  59. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.integral_regularizedPreRate_swap line 1142
  60. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.integral_regularizedPostRate_swap line 1153
  61. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.integral_regularizedPostRate_scatter line 1164
  62. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.fiberMeasure line 1190
  63. instance OAI.BoltzmannNonuniqueness.PeriodicApproximation.fiberMeasure_finite line 1193
  64. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.gain line 1199
  65. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.loss line 1202
  66. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.gainBound line 1205
  67. def OAI.BoltzmannNonuniqueness.PeriodicApproximation.lossBound line 1207
  68. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.gain_measurable line 1209
  69. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.loss_measurable line 1214
  70. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.pre_fiber_integrable line 1219
  71. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.post_fiber_integrable line 1230
  72. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.gain_bounds line 1241
  73. theorem OAI.BoltzmannNonuniqueness.PeriodicApproximation.loss_bounds line 1251