OAI/MathematicalPhysics/Boltzmann/Branching/DampedCollisionHistories.lean

GitHub source file

76 declarations, 0 contain sorry, 0 declared as axioms

Time-uniform contraction estimates for the positive damped integral

  1. theorem OAI.BoltzmannNonuniqueness.PositiveIntegral.exponential_integral line 17
  2. theorem OAI.BoltzmannNonuniqueness.PositiveIntegral.value_damped_bound line 33
  3. theorem OAI.BoltzmannNonuniqueness.PositiveIntegral.value_damped_difference line 56
  4. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.holdingWeight line 100
  5. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedReferenceWeight line 103
  6. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedParameterDensity line 106
  7. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedMediumParameterDensity line 109
  8. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.holdingWeight_measurable line 116
  9. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedParameterDensity_measurable line 119
  10. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedMediumParameterDensity_measurable line 133
  11. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.holdingWeight_le line 171
  12. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.rate_add_holding_le line 195
  13. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.nearby_damped_parameter_bounds line 207
  14. theorem OAI.BoltzmannNonuniqueness.PositiveIntegral.exists_damped_fixed_point line 271
  15. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedWordDensity line 330
  16. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedMediumWordDensity line 335
  17. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.DampedWordCoefficientClose line 341
  18. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.damped_word_weight_comparison line 350
  19. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.damped_word_coefficients_close line 387
  20. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedMediumCollision line 427
  21. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedMediumCollision_sFinite line 431
  22. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedMediumCollision_apply line 441
  23. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedMediumCollision_lintegral line 447
  24. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedMediumCollision_projection line 461
  25. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedMediumStateCollision line 486
  26. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedMediumStateCollision_sFinite line 492
  27. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedMediumStateCollision_lintegral line 497
  28. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedReferenceWeight_measurable line 523
  29. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedReference_integral line 527
  30. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.damped_eventHistory_marked_succ line 550
  31. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedReferenceParameterDensity line 586
  32. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedReferenceParameterDensity_measurable line 589
  33. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.damped_reference_parameter_integral line 594
  34. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.damped_eventHistory_parameter_succ line 619
  35. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.damped_eventHistory_marked_parameter_succ line 641
  36. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.holdingWeight_ne_top line 673
  37. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedParameterDensity_ne_top line 679
  38. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedParameterDensity_zero line 690
  39. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedWordDensity_measurable line 694
  40. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedWord_integral line 706
  41. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedParameterDensity_zero_of_outside line 755
  42. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.goodReferenceWord_of_damped_density_ne_zero line 763
  43. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedMediumWordDensity_measurable line 776
  44. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedMediumBlockIntegrand line 806
  45. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedHistoryPerturbationError line 813
  46. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.damped_medium_word_integrand_bound line 817
  47. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.damped_medium_word_integral_lower line 853
  48. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedMediumParameterDensity_ne_top line 889
  49. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedMediumEventDensity line 899
  50. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedMediumEventDensity_measurable line 903
  51. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedMediumEventKernel line 907
  52. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedMediumEventKernel_isSFinite line 912
  53. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedMediumEventKernel_lintegral line 923
  54. instance OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedMediumEventKernel_pow_isSFinite line 939
  55. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.damped_medium_parameter_integral line 967
  56. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedMediumEventKernel_physical_lintegral line 1000
  57. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedBoundedWordDensity line 1051
  58. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedBoundedWordDensity_measurable line 1060
  59. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedBoundedWordDensity_eq line 1079
  60. def OAI.BoltzmannNonuniqueness.Published.dampedCharacter line 1123
  61. theorem OAI.BoltzmannNonuniqueness.Published.dampedCharacter_eq line 1126
  62. theorem OAI.BoltzmannNonuniqueness.Published.dampedCharacter_integrable line 1133
  63. theorem OAI.BoltzmannNonuniqueness.Published.integral_dampedCharacter line 1139
  64. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedHistoryPerturbationError_continuous line 1162
  65. def OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedFiniteHistoryError line 1166
  66. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedFiniteHistoryError_continuous line 1169
  67. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedFiniteHistoryError_zero line 1176
  68. theorem OAI.BoltzmannNonuniqueness.ReferenceGeometry.dampedFiniteHistoryError_small line 1179
  69. def OAI.BoltzmannNonuniqueness.Published.lineShear line 1202
  70. theorem OAI.BoltzmannNonuniqueness.Published.lineShear_measurePreserving line 1205
  71. def OAI.BoltzmannNonuniqueness.Published.dampedLineResolvent line 1213
  72. theorem OAI.BoltzmannNonuniqueness.Published.dampedLine_integrable line 1216
  73. theorem OAI.BoltzmannNonuniqueness.Published.dampedLineResolvent_integrable line 1222
  74. def OAI.BoltzmannNonuniqueness.Published.fourierLineKernel line 1242
  75. theorem OAI.BoltzmannNonuniqueness.Published.fourierLineKernel_integrable line 1245
  76. theorem OAI.BoltzmannNonuniqueness.Published.fourier_dampedLine_integral line 1257