OAI/MathematicalPhysics/Boltzmann/Jets/JetPeriodicDatum.lean

GitHub source file

103 declarations, 0 contain sorry, 0 declared as axioms

Integration of spatial weights against the cold thermal kernel

  1. def OAI.BoltzmannNonuniqueness.JetWeightedKernel.weighted line 21
  2. theorem OAI.BoltzmannNonuniqueness.JetWeightedKernel.weighted_nonneg line 24
  3. theorem OAI.BoltzmannNonuniqueness.JetWeightedKernel.weighted_measurable line 29
  4. theorem OAI.BoltzmannNonuniqueness.JetWeightedKernel.weighted_velocity_integral line 38
  5. theorem OAI.BoltzmannNonuniqueness.JetWeightedKernel.weighted_integrable line 44
  6. theorem OAI.BoltzmannNonuniqueness.JetWeightedKernel.weighted_integral line 61
  7. theorem OAI.BoltzmannNonuniqueness.JetPrototypeEntropy.measurable_entropy line 91
  8. def OAI.BoltzmannNonuniqueness.JetPrototypeEntropy.spatialWeight line 95
  9. def OAI.BoltzmannNonuniqueness.JetPrototypeEntropy.majorant line 98
  10. theorem OAI.BoltzmannNonuniqueness.JetPrototypeEntropy.spatialWeight_nonneg line 102
  11. theorem OAI.BoltzmannNonuniqueness.JetPrototypeEntropy.spatialWeight_measurable line 107
  12. theorem OAI.BoltzmannNonuniqueness.JetPrototypeEntropy.spatialWeight_integrable line 112
  13. theorem OAI.BoltzmannNonuniqueness.JetPrototypeEntropy.entropy_le_majorant line 118
  14. theorem OAI.BoltzmannNonuniqueness.JetPrototypeEntropy.majorant_integrable line 131
  15. theorem OAI.BoltzmannNonuniqueness.JetPrototypeEntropy.density_entropy_integrable line 144
  16. theorem OAI.BoltzmannNonuniqueness.JetPrototypeEntropy.density_entropy_integral line 154
  17. def OAI.BoltzmannNonuniqueness.JetEntropyBound.spatialConstant line 205
  18. def OAI.BoltzmannNonuniqueness.JetEntropyBound.constant line 209
  19. theorem OAI.BoltzmannNonuniqueness.JetEntropyBound.spatialConstant_nonneg line 212
  20. theorem OAI.BoltzmannNonuniqueness.JetEntropyBound.constant_nonneg line 219
  21. theorem OAI.BoltzmannNonuniqueness.JetEntropyBound.spatial_mass_bound line 226
  22. theorem OAI.BoltzmannNonuniqueness.JetEntropyBound.spatial_entropy_bound line 233
  23. theorem OAI.BoltzmannNonuniqueness.JetEntropyBound.thermal_log_bound line 273
  24. theorem OAI.BoltzmannNonuniqueness.JetEntropyBound.prototype_entropy_bound line 285

    Source documentation

    The constant depends only on the fixed parameters, and is independent of the annular scale.

    theorem prototype_entropy_bound {η K γ s d₀ : ℝ} (hη : 0 ≤ η) (hηmax : η ≤ Real.log 2)
    (hK : 0 < K) (hγ : 0 < γ) (hs : 0 < s) (hd₀ : 0 < d₀) (α : ℝ) (a : Bool) :
    (∫ p, entropy (density η K α γ s (d₀ * s ^ 10) a p) ∂spaceVolume.prod volume) ≤
      constant K γ d₀ * s ^ 2 * (1 + |Real.log s|) := by
…

    Mentions: OAI.BoltzmannNonuniqueness.JetEntropyBound.constant

  25. theorem OAI.BoltzmannNonuniqueness.JetSpatialBox.mask_norm_le_one line 329
  26. theorem OAI.BoltzmannNonuniqueness.JetSpatialBox.transverse_component line 339
  27. theorem OAI.BoltzmannNonuniqueness.JetSpatialBox.axial_component line 355
  28. def OAI.BoltzmannNonuniqueness.JetSpatialBox.shifted line 376
  29. def OAI.BoltzmannNonuniqueness.JetSpatialBox.gap line 379
  30. theorem OAI.BoltzmannNonuniqueness.JetSpatialBox.coordinate_bound line 381
  31. theorem OAI.BoltzmannNonuniqueness.JetSeries.summable_single_support line 420
  32. theorem OAI.BoltzmannNonuniqueness.JetSeries.entropy_tsum line 430
  33. theorem OAI.BoltzmannNonuniqueness.JetSeries.integrable_nonnegative_series line 443
  34. theorem OAI.BoltzmannNonuniqueness.JetSeries.integral_nonnegative_series line 463
  35. abbrev OAI.BoltzmannNonuniqueness.JetDatum.Index line 490
  36. def OAI.BoltzmannNonuniqueness.JetDatum.term line 492
  37. def OAI.BoltzmannNonuniqueness.JetDatum.datum line 495
  38. theorem OAI.BoltzmannNonuniqueness.JetDatum.term_nonneg line 498
  39. theorem OAI.BoltzmannNonuniqueness.JetDatum.term_integrable line 503
  40. theorem OAI.BoltzmannNonuniqueness.JetDatum.term_entropy_integrable line 509
  41. theorem OAI.BoltzmannNonuniqueness.JetDatum.term_measurable line 515
  42. def OAI.BoltzmannNonuniqueness.JetDatum.label line 518
  43. theorem OAI.BoltzmannNonuniqueness.JetDatum.in_enlargement line 520
  44. theorem OAI.BoltzmannNonuniqueness.JetDatum.term_disjoint line 535
  45. theorem OAI.BoltzmannNonuniqueness.JetDatum.term_summable line 545
  46. theorem OAI.BoltzmannNonuniqueness.JetDatum.entropy_datum line 550
  47. theorem OAI.BoltzmannNonuniqueness.JetDatum.summable_bool_extension line 555
  48. theorem OAI.BoltzmannNonuniqueness.JetDatum.mass_summable line 563
  49. theorem OAI.BoltzmannNonuniqueness.JetDatum.entropy_summable line 574
  50. theorem OAI.BoltzmannNonuniqueness.JetDatum.datum_integrable line 588
  51. theorem OAI.BoltzmannNonuniqueness.JetDatum.datum_entropy_integrable line 595
  52. theorem OAI.BoltzmannNonuniqueness.JetDatumMoments.datum_nonneg line 632
  53. theorem OAI.BoltzmannNonuniqueness.JetDatumMoments.mass_eq_sum line 636
  54. theorem OAI.BoltzmannNonuniqueness.JetDatumMoments.entropy_eq_sum line 643
  55. theorem OAI.BoltzmannNonuniqueness.JetDatumMoments.thermal_width_le line 653
  56. theorem OAI.BoltzmannNonuniqueness.JetDatumMoments.datum_support_two line 665
  57. theorem OAI.BoltzmannNonuniqueness.JetDatumMoments.datum_energy_integrable line 678
  58. theorem OAI.BoltzmannNonuniqueness.JetDatumMoments.datum_entropyMoment_integrable line 694
  59. def OAI.BoltzmannNonuniqueness.JetTruncation.truncated line 725
  60. theorem OAI.BoltzmannNonuniqueness.JetTruncation.truncated_measurable line 728
  61. theorem OAI.BoltzmannNonuniqueness.JetTruncation.truncated_at_nonzero line 737
  62. theorem OAI.BoltzmannNonuniqueness.JetTruncation.truncated_eq_or_zero line 750
  63. theorem OAI.BoltzmannNonuniqueness.JetTruncation.eventually_truncated_eq line 763
  64. theorem OAI.BoltzmannNonuniqueness.JetTruncation.truncated_tendsto line 776
  65. theorem OAI.BoltzmannNonuniqueness.JetFreeTransport.flight_add line 802
  66. theorem OAI.BoltzmannNonuniqueness.JetFreeTransport.flight_zero line 812
  67. theorem OAI.BoltzmannNonuniqueness.JetFreeTransport.flight_neg line 815
  68. theorem OAI.BoltzmannNonuniqueness.JetFreeTransport.neg_flight line 818
  69. def OAI.BoltzmannNonuniqueness.JetFreeTransport.free line 821
  70. theorem OAI.BoltzmannNonuniqueness.JetFreeTransport.free_along line 824
  71. theorem OAI.BoltzmannNonuniqueness.JetFreeTransport.free_nonneg line 828
  72. theorem OAI.BoltzmannNonuniqueness.JetFreeTransport.free_le_barrier line 832
  73. theorem OAI.BoltzmannNonuniqueness.JetFreeTransport.measurable_free line 839
  74. theorem OAI.BoltzmannNonuniqueness.JetFreeTransport.measurable_joint_free line 861
  75. theorem OAI.BoltzmannNonuniqueness.JetFreeTransport.measurable_uncurried_free line 867
  76. theorem OAI.BoltzmannNonuniqueness.JetConvergence.selection_L1_tendsto line 897
  77. theorem OAI.BoltzmannNonuniqueness.JetConvergence.mass_L1_tendsto line 917
  78. theorem OAI.BoltzmannNonuniqueness.JetConvergence.entropy_L1_tendsto line 927
  79. theorem OAI.BoltzmannNonuniqueness.JetConvergence.energy_L1_tendsto line 945
  80. theorem OAI.BoltzmannNonuniqueness.JetLatticeTail.pointwise_bound line 987
  81. theorem OAI.BoltzmannNonuniqueness.JetLatticeTail.sum_bound line 1000
  82. def OAI.BoltzmannNonuniqueness.JetLatticeTail.outside line 1010
  83. theorem OAI.BoltzmannNonuniqueness.JetLatticeTail.escaped_sum_bound line 1013
  84. def OAI.BoltzmannNonuniqueness.JetComparisonCoefficient.coefficient line 1053
  85. theorem OAI.BoltzmannNonuniqueness.JetComparisonCoefficient.coefficient_ge_one line 1055
  86. theorem OAI.BoltzmannNonuniqueness.JetComparisonCoefficient.linear_le_quadratic line 1059
  87. theorem OAI.BoltzmannNonuniqueness.JetComparisonCoefficient.comparison_bound line 1069
  88. def OAI.BoltzmannNonuniqueness.JetBarrierDifferential.spatialTerm line 1098
  89. theorem OAI.BoltzmannNonuniqueness.JetBarrierDifferential.spatialTerm_lower line 1101
  90. theorem OAI.BoltzmannNonuniqueness.JetBarrierDifferential.logarithmic_derivative_lower line 1112
  91. def OAI.BoltzmannNonuniqueness.JetEscapedCopies.halfRate line 1151
  92. theorem OAI.BoltzmannNonuniqueness.JetEscapedCopies.halfRate_large line 1153
  93. theorem OAI.BoltzmannNonuniqueness.JetEscapedCopies.rate_identity line 1161
  94. theorem OAI.BoltzmannNonuniqueness.JetEscapedCopies.copy_sum_bound line 1168
  95. def OAI.BoltzmannNonuniqueness.JetPeriodicDatum.spatialMap line 1233
  96. def OAI.BoltzmannNonuniqueness.JetPeriodicDatum.phaseMap line 1235
  97. def OAI.BoltzmannNonuniqueness.JetPeriodicDatum.pullback line 1237
  98. def OAI.BoltzmannNonuniqueness.JetPeriodicDatum.datum line 1240
  99. theorem OAI.BoltzmannNonuniqueness.JetPeriodicDatum.spatialMap_measurePreserving line 1242
  100. theorem OAI.BoltzmannNonuniqueness.JetPeriodicDatum.phaseMap_measurePreserving line 1249
  101. theorem OAI.BoltzmannNonuniqueness.JetPeriodicDatum.integrable_pullback line 1252
  102. theorem OAI.BoltzmannNonuniqueness.JetPeriodicDatum.finiteEntropy line 1257
  103. theorem OAI.BoltzmannNonuniqueness.JetPeriodicDatum.boundedVelocitySupport line 1267