OAI/MathematicalPhysics/Boltzmann/Jets/JetBarriers.lean

GitHub source file

106 declarations, 0 contain sorry, 0 declared as axioms

The actual unshifted cold-jet density and its mass bound

  1. abbrev OAI.BoltzmannNonuniqueness.JetPrototype.Space line 28
  2. abbrev OAI.BoltzmannNonuniqueness.JetPrototype.Phase line 29
  3. abbrev OAI.BoltzmannNonuniqueness.JetPrototype.spaceVolume line 31
  4. def OAI.BoltzmannNonuniqueness.JetPrototype.sign line 33
  5. def OAI.BoltzmannNonuniqueness.JetPrototype.center line 35
  6. def OAI.BoltzmannNonuniqueness.JetPrototype.axialAmplitude line 38
  7. def OAI.BoltzmannNonuniqueness.JetPrototype.spatial line 41
  8. def OAI.BoltzmannNonuniqueness.JetPrototype.density line 44
  9. theorem OAI.BoltzmannNonuniqueness.JetPrototype.axialAmplitude_nonneg line 47
  10. theorem OAI.BoltzmannNonuniqueness.JetPrototype.spatial_nonneg line 53
  11. theorem OAI.BoltzmannNonuniqueness.JetPrototype.density_nonneg line 58
  12. theorem OAI.BoltzmannNonuniqueness.JetPrototype.axialAmplitude_integrable line 63
  13. theorem OAI.BoltzmannNonuniqueness.JetPrototype.spatial_integrable line 68
  14. theorem OAI.BoltzmannNonuniqueness.JetPrototype.measurable_spatial line 72
  15. theorem OAI.BoltzmannNonuniqueness.JetPrototype.measurable_center line 79
  16. theorem OAI.BoltzmannNonuniqueness.JetPrototype.measurable_density line 84
  17. theorem OAI.BoltzmannNonuniqueness.JetPrototype.density_velocity_integral line 95
  18. theorem OAI.BoltzmannNonuniqueness.JetPrototype.density_integrable line 100
  19. theorem OAI.BoltzmannNonuniqueness.JetPrototype.density_mass_eq line 117
  20. theorem OAI.BoltzmannNonuniqueness.JetPrototype.density_mass_bound line 130
  21. theorem OAI.BoltzmannNonuniqueness.JetSpatialEntropy.scalar_scaled_integrable line 170
  22. theorem OAI.BoltzmannNonuniqueness.JetSpatialEntropy.scalar_scaled_integral line 178
  23. def OAI.BoltzmannNonuniqueness.JetSpatialEntropy.massConstant line 187
  24. def OAI.BoltzmannNonuniqueness.JetSpatialEntropy.entropyConstant line 189
  25. theorem OAI.BoltzmannNonuniqueness.JetSpatialEntropy.massConstant_nonneg line 191
  26. theorem OAI.BoltzmannNonuniqueness.JetSpatialEntropy.entropyConstant_nonneg line 193
  27. def OAI.BoltzmannNonuniqueness.JetSpatialEntropy.axialMajorant line 196
  28. theorem OAI.BoltzmannNonuniqueness.JetSpatialEntropy.axial_entropy_bound line 199
  29. theorem OAI.BoltzmannNonuniqueness.JetSpatialEntropy.axialMajorant_integrable line 209
  30. theorem OAI.BoltzmannNonuniqueness.JetSpatialEntropy.axial_entropy_integrable line 214
  31. theorem OAI.BoltzmannNonuniqueness.JetSpatialEntropy.axial_entropy_integral line 233
  32. theorem OAI.BoltzmannNonuniqueness.JetSpatialEntropy.spatial_entropy_eq line 250
  33. theorem OAI.BoltzmannNonuniqueness.JetSpatialEntropy.spatial_entropy_integrable line 257
  34. theorem OAI.BoltzmannNonuniqueness.JetSpatialEntropy.spatial_entropy_integral line 263
  35. theorem OAI.BoltzmannNonuniqueness.JetSupport.center_norm line 297
  36. theorem OAI.BoltzmannNonuniqueness.JetSupport.abs_sign line 305
  37. theorem OAI.BoltzmannNonuniqueness.JetSupport.center_norm_bound line 307
  38. theorem OAI.BoltzmannNonuniqueness.JetSupport.density_velocity_bound line 315
  39. theorem OAI.BoltzmannNonuniqueness.JetSupport.density_support_two line 323
  40. theorem OAI.BoltzmannNonuniqueness.JetSupport.initial_spatial_support line 329
  41. theorem OAI.BoltzmannNonuniqueness.JetSupport.transverse_velocity_bound line 343
  42. theorem OAI.BoltzmannNonuniqueness.JetSupport.free_core_transverse line 360

    Source documentation

    A free core remains in the transverse enlargement once t d ≤ δ_s.

    theorem free_core_transverse {t d η s : ℝ} (ht : 0 ≤ t) (hd : 0 < d)
    (hwidth : t * d ≤ enlargementWidth η s) (K α γ : ℝ) (a : Bool)
    {p : JetPrototype.Phase} (hp : JetPrototype.density η K α γ s d a p ≠ 0) :
    p.1.1 + t • transverse p.2 ∈ enlargement η s a := by
…

    Mentions: OAI.BoltzmannNonuniqueness.JetPrototype.Phase, OAI.BoltzmannNonuniqueness.JetPrototype.density

  43. theorem OAI.BoltzmannNonuniqueness.JetSupport.free_core_axial line 370

    Source documentation

    Axial free flight stays inside the manuscript's interval enlargement.

    theorem free_core_axial {t d α : ℝ} (ht : 0 ≤ t) (hd : 0 < d) (hdmax : d ≤ 1 / 64)
    (hα : 0 ≤ α) (hαmax : α ≤ 1 / 4) (η K γ s : ℝ) (a : Bool)
    {p : JetPrototype.Phase} (hp : JetPrototype.density η K α γ s d a p ≠ 0) :
    |p.1.2 + t * axial p.2| ≤ 1 / 8 + 2 * t + 1 / 16 := by
…

    Mentions: OAI.BoltzmannNonuniqueness.JetPrototype.Phase, OAI.BoltzmannNonuniqueness.JetPrototype.density

  44. def OAI.BoltzmannNonuniqueness.JetCoreFlight.axialCenter line 403
  45. def OAI.BoltzmannNonuniqueness.JetCoreFlight.error line 406
  46. theorem OAI.BoltzmannNonuniqueness.JetCoreFlight.norm_sq_error line 409
  47. theorem OAI.BoltzmannNonuniqueness.JetCoreFlight.axial_error_bound line 414
  48. theorem OAI.BoltzmannNonuniqueness.JetCoreFlight.error_le_initial line 423
  49. theorem OAI.BoltzmannNonuniqueness.JetCoreFlight.error_lt_width line 438
  50. theorem OAI.BoltzmannNonuniqueness.JetCoreFlight.transverse_distance_bound line 445
  51. theorem OAI.BoltzmannNonuniqueness.JetCoreFlight.axial_distance_bound line 453
  52. theorem OAI.BoltzmannNonuniqueness.JetCoreFlight.distance_square_bound line 469
  53. def OAI.BoltzmannNonuniqueness.JetBarrier.centerVelocity line 518
  54. def OAI.BoltzmannNonuniqueness.JetBarrier.distanceSquared line 521
  55. def OAI.BoltzmannNonuniqueness.JetBarrier.flight line 525
  56. def OAI.BoltzmannNonuniqueness.JetBarrier.exponent line 528
  57. def OAI.BoltzmannNonuniqueness.JetBarrier.barrier line 532
  58. theorem OAI.BoltzmannNonuniqueness.JetBarrier.spatial_le line 536
  59. theorem OAI.BoltzmannNonuniqueness.JetBarrier.initial_density_bound line 547
  60. theorem OAI.BoltzmannNonuniqueness.JetBarrier.flight_exponent_lower line 557
  61. theorem OAI.BoltzmannNonuniqueness.JetBarrier.barrier_nonneg line 575
  62. theorem OAI.BoltzmannNonuniqueness.JetBarrier.free_core_le_barrier line 581
  63. def OAI.BoltzmannNonuniqueness.JetBarrierCollision.massScale line 620
  64. theorem OAI.BoltzmannNonuniqueness.JetBarrierCollision.massScale_nonneg line 624
  65. theorem OAI.BoltzmannNonuniqueness.JetBarrierCollision.barrier_eq_density line 630
  66. theorem OAI.BoltzmannNonuniqueness.JetBarrierCollision.measurable_velocity line 645
  67. theorem OAI.BoltzmannNonuniqueness.JetBarrierCollision.integrable_gain line 652
  68. theorem OAI.BoltzmannNonuniqueness.JetBarrierCollision.massScale_le line 661
  69. def OAI.BoltzmannNonuniqueness.JetBarrierCollision.frequencyConstant line 680
  70. theorem OAI.BoltzmannNonuniqueness.JetBarrierCollision.frequencyConstant_nonneg line 684
  71. theorem OAI.BoltzmannNonuniqueness.JetBarrierCollision.frequency_bound line 692

    Source documentation

    The constant is independent of the jet label, thermal width and position.

    theorem frequency_bound {K s d t : ℝ} (hK : 0 ≤ K) (hs : 0 < s) (hd : 0 < d)
    (ht : 0 < t) (htmax : t ≤ 1) (η α γ : ℝ) (a : Bool) (x : Space)
    (z : Position) (v : Velocity) :
    frequency (fun p => barrier η K α γ s d t a (x, p.2)) z v ≤
      frequencyConstant * (K / s) * (d + ‖v - centerVelocity α γ s t a x‖) := by
…

    Mentions: OAI.BoltzmannNonuniqueness.Position, OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.frequency, OAI.BoltzmannNonuniqueness.JetBarrierCollision.frequencyConstant

  72. theorem OAI.BoltzmannNonuniqueness.JetBarrierCollision.self_gain line 723

    Source documentation

    The fixed-position barrier is a Maxwellian, so its gain equals its loss.

    theorem self_gain {K s d t : ℝ} (hK : 0 ≤ K) (hs : 0 < s) (hd : 0 < d)
    (htmax : t ≤ 1) (η α γ : ℝ) (a : Bool) (x : Space) (z : Position) (v : Velocity) :
    gain (fun p => barrier η K α γ s d t a (x, p.2)) z v =
      barrier η K α γ s d t a (x, v) *
        frequency (fun p => barrier η K α γ s d t a (x, p.2)) z v := by
…

    Mentions: OAI.BoltzmannNonuniqueness.Position, OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.gain, OAI.BoltzmannNonuniqueness.frequency

  73. theorem OAI.BoltzmannNonuniqueness.JetGaussianEscape.centered_gaussian_le line 766
  74. theorem OAI.BoltzmannNonuniqueness.JetGaussianEscape.gaussian_le_hot line 778
  75. def OAI.BoltzmannNonuniqueness.JetGaussianEscape.constant line 803
  76. theorem OAI.BoltzmannNonuniqueness.JetGaussianEscape.barrier_velocity_decay line 806
  77. theorem OAI.BoltzmannNonuniqueness.JetDistanceDerivative.infDist_comp_derivative_bound line 866
  78. def OAI.BoltzmannNonuniqueness.JetDistanceDerivative.transverseDistance line 879
  79. def OAI.BoltzmannNonuniqueness.JetDistanceDerivative.axialDistance line 882
  80. theorem OAI.BoltzmannNonuniqueness.JetDistanceDerivative.transverse_lipschitz line 885
  81. theorem OAI.BoltzmannNonuniqueness.JetDistanceDerivative.transverse_ae_derivative_bound line 897
  82. theorem OAI.BoltzmannNonuniqueness.JetDistanceDerivative.flightFoot_lipschitzOn line 904
  83. theorem OAI.BoltzmannNonuniqueness.JetDistanceDerivative.axial_ae_differentiable line 913
  84. theorem OAI.BoltzmannNonuniqueness.JetDistanceDerivative.axial_derivative_bound line 921
  85. def OAI.BoltzmannNonuniqueness.JetBarrierLocalMass.massConstant line 948
  86. theorem OAI.BoltzmannNonuniqueness.JetBarrierLocalMass.massConstant_nonneg line 950
  87. theorem OAI.BoltzmannNonuniqueness.JetBarrierLocalMass.measurable_barrier line 955
  88. theorem OAI.BoltzmannNonuniqueness.JetBarrierLocalMass.velocity_integrable line 972
  89. theorem OAI.BoltzmannNonuniqueness.JetBarrierLocalMass.velocity_integral_le line 978
  90. theorem OAI.BoltzmannNonuniqueness.JetBarrierLocalMass.local_integrable line 990
  91. theorem OAI.BoltzmannNonuniqueness.JetBarrierLocalMass.local_integral_le line 1006
  92. theorem OAI.BoltzmannNonuniqueness.JetEscapeGeometry.transverse_distance line 1037
  93. theorem OAI.BoltzmannNonuniqueness.JetEscapeGeometry.axial_distance line 1047
  94. theorem OAI.BoltzmannNonuniqueness.JetEscapeGeometry.width_le line 1068
  95. theorem OAI.BoltzmannNonuniqueness.JetEscapeGeometry.distance_lower_bound line 1078
  96. theorem OAI.BoltzmannNonuniqueness.JetEscapePower.exp_neg_le line 1111
  97. def OAI.BoltzmannNonuniqueness.JetEscapePower.tail line 1122
  98. theorem OAI.BoltzmannNonuniqueness.JetEscapePower.tail_nonneg line 1124
  99. theorem OAI.BoltzmannNonuniqueness.JetEscapePower.tail_bound line 1128
  100. theorem OAI.BoltzmannNonuniqueness.JetEscapePower.summable_tails line 1143
  101. theorem OAI.BoltzmannNonuniqueness.JetEscapePower.sum_bound line 1154
  102. def OAI.BoltzmannNonuniqueness.JetEscapedBarrier.rate line 1186
  103. def OAI.BoltzmannNonuniqueness.JetEscapedBarrier.coefficient line 1188
  104. theorem OAI.BoltzmannNonuniqueness.JetEscapedBarrier.rate_pos line 1190
  105. theorem OAI.BoltzmannNonuniqueness.JetEscapedBarrier.spatial_exponent line 1195
  106. theorem OAI.BoltzmannNonuniqueness.JetEscapedBarrier.barrier_bound line 1209