OAI/MathematicalPhysics/Boltzmann/Jets/JetProfiles.lean

GitHub source file

138 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BoltzmannNonuniqueness.JetGeometry.gapCoefficient line 29
2. def OAI.BoltzmannNonuniqueness.JetGeometry.jetScale line 31
3. def OAI.BoltzmannNonuniqueness.JetGeometry.enlargementWidth line 33
4. def OAI.BoltzmannNonuniqueness.JetGeometry.annularCore line 35
5. def OAI.BoltzmannNonuniqueness.JetGeometry.stripe line 39
6. def OAI.BoltzmannNonuniqueness.JetGeometry.mask line 43
7. def OAI.BoltzmannNonuniqueness.JetGeometry.enlargement line 45
8. theorem OAI.BoltzmannNonuniqueness.JetGeometry.gapCoefficient_pos line 48
9. theorem OAI.BoltzmannNonuniqueness.JetGeometry.gapCoefficient_le line 53
10. theorem OAI.BoltzmannNonuniqueness.JetGeometry.enlargementWidth_pos line 59
11. theorem OAI.BoltzmannNonuniqueness.JetGeometry.enlargement_witness line 65
12. theorem OAI.BoltzmannNonuniqueness.JetGeometry.enlargement_subset_annulus line 73
13. theorem OAI.BoltzmannNonuniqueness.JetGeometry.scale_antitone line 89
14. theorem OAI.BoltzmannNonuniqueness.JetGeometry.outerRadius_eq line 98
15. theorem OAI.BoltzmannNonuniqueness.JetGeometry.ordered_annuli line 106
16. theorem OAI.BoltzmannNonuniqueness.JetGeometry.distinct_scale_disjoint line 112
17. theorem OAI.BoltzmannNonuniqueness.JetGeometry.stripe_distance line 127
18. theorem OAI.BoltzmannNonuniqueness.JetGeometry.opposite_enlargements_disjoint line 145
19. theorem OAI.BoltzmannNonuniqueness.JetGeometry.enlargement_inside_baseBall line 159
20. abbrev OAI.BoltzmannNonuniqueness.JetLattice.Lattice line 188
21. structure OAI.BoltzmannNonuniqueness.JetLattice.Label line 190
22. def OAI.BoltzmannNonuniqueness.JetLattice.transverseShift line 196
23. def OAI.BoltzmannNonuniqueness.JetLattice.axialShift line 199
24. def OAI.BoltzmannNonuniqueness.JetLattice.spatialEnlargement line 201
25. theorem OAI.BoltzmannNonuniqueness.JetLattice.integer_distance line 206
26. theorem OAI.BoltzmannNonuniqueness.JetLattice.distinct_transverse_shifts line 210
27. theorem OAI.BoltzmannNonuniqueness.JetLattice.common_point_transverse_lattice line 219
28. theorem OAI.BoltzmannNonuniqueness.JetLattice.common_point_axial_lattice line 235
29. theorem OAI.BoltzmannNonuniqueness.JetLattice.common_point_lattice line 250
30. theorem OAI.BoltzmannNonuniqueness.JetLattice.common_point_label line 259
31. theorem OAI.BoltzmannNonuniqueness.JetLattice.pairwise_spatialEnlargement line 288

    Source documentation

    The disjointness statement of manuscript Lemma jet:geometry.

    theorem pairwise_spatialEnlargement {s₀ η t : ℝ} (hs₀ : 0 < s₀) (hsmax : s₀ ≤ 1 / 8)
        (hη : 0 < η) (hηmax : η ≤ Real.log 2) (ht : t ≤ 1 / 32) :
        Pairwise (fun i j : Label => Disjoint (spatialEnlargement s₀ η t i)
          (spatialEnlargement s₀ η t j)) := by
    …

    Mentions: OAI.BoltzmannNonuniqueness.JetLattice.Label, OAI.BoltzmannNonuniqueness.JetLattice.spatialEnlargement

32. theorem OAI.BoltzmannNonuniqueness.JetMaskMeasure.measurableSet_stripe line 316
33. theorem OAI.BoltzmannNonuniqueness.JetMaskMeasure.measurableSet_annularCore line 324
34. theorem OAI.BoltzmannNonuniqueness.JetMaskMeasure.measurableSet_mask line 328
35. theorem OAI.BoltzmannNonuniqueness.JetMaskMeasure.mask_subset_ball line 331
36. theorem OAI.BoltzmannNonuniqueness.JetMaskMeasure.mask_finite line 343
37. theorem OAI.BoltzmannNonuniqueness.JetMaskMeasure.mask_area_le line 346
38. theorem OAI.BoltzmannNonuniqueness.JetMaskMeasure.mask_area_uniform line 352
39. theorem OAI.BoltzmannNonuniqueness.JetMaskMeasure.indicator_integrable line 362
40. def OAI.BoltzmannNonuniqueness.JetThermalKernel.bump line 384
41. def OAI.BoltzmannNonuniqueness.JetThermalKernel.J line 386
42. theorem OAI.BoltzmannNonuniqueness.JetThermalKernel.J_nonneg line 388
43. theorem OAI.BoltzmannNonuniqueness.JetThermalKernel.J_smooth line 390
44. theorem OAI.BoltzmannNonuniqueness.JetThermalKernel.J_integrable line 392
45. theorem OAI.BoltzmannNonuniqueness.JetThermalKernel.J_integral line 394
46. theorem OAI.BoltzmannNonuniqueness.JetThermalKernel.J_support line 396
47. theorem OAI.BoltzmannNonuniqueness.JetThermalKernel.J_zero line 398
48. theorem OAI.BoltzmannNonuniqueness.JetThermalKernel.J_compact line 404
49. def OAI.BoltzmannNonuniqueness.JetThermalKernel.bound line 406
50. theorem OAI.BoltzmannNonuniqueness.JetThermalKernel.bound_pos line 408
51. theorem OAI.BoltzmannNonuniqueness.JetThermalKernel.J_le line 410
52. def OAI.BoltzmannNonuniqueness.JetThermalLaw.scaled line 432
53. def OAI.BoltzmannNonuniqueness.JetThermalLaw.density line 435
54. theorem OAI.BoltzmannNonuniqueness.JetThermalLaw.integrable_scaled line 437
55. theorem OAI.BoltzmannNonuniqueness.JetThermalLaw.integral_scaled line 441
56. theorem OAI.BoltzmannNonuniqueness.JetThermalLaw.density_nonneg line 451
57. theorem OAI.BoltzmannNonuniqueness.JetThermalLaw.density_integrable line 454
58. theorem OAI.BoltzmannNonuniqueness.JetThermalLaw.density_mass line 457
59. theorem OAI.BoltzmannNonuniqueness.JetThermalLaw.density_smooth line 460
60. theorem OAI.BoltzmannNonuniqueness.JetThermalLaw.density_zero line 467
61. theorem OAI.BoltzmannNonuniqueness.JetThermalLaw.density_velocity_bound line 474
62. theorem OAI.BoltzmannNonuniqueness.JetThermalLaw.density_le line 481
63. theorem OAI.BoltzmannNonuniqueness.JetThermalLaw.integrable_J_entropy line 485
64. theorem OAI.BoltzmannNonuniqueness.JetThermalLaw.test_error_integrable_le line 517
65. theorem OAI.BoltzmannNonuniqueness.JetThermalLaw.test_integrable line 541
66. theorem OAI.BoltzmannNonuniqueness.JetThermalLaw.test_average_error_le line 556
67. theorem OAI.BoltzmannNonuniqueness.JetThermalLaw.test_average_tendsto line 570
68. theorem OAI.BoltzmannNonuniqueness.JetThermalLaw.test_average_center_error_le line 579
69. theorem OAI.BoltzmannNonuniqueness.JetThermalLaw.test_average_moving_center_tendsto line 589
70. def OAI.BoltzmannNonuniqueness.JetThermalEntropy.entropy line 620
71. theorem OAI.BoltzmannNonuniqueness.JetThermalEntropy.entropy_nonneg line 622
72. theorem OAI.BoltzmannNonuniqueness.JetThermalEntropy.entropy_mul_le line 625
73. theorem OAI.BoltzmannNonuniqueness.JetThermalEntropy.continuous_entropy_comp line 637
74. theorem OAI.BoltzmannNonuniqueness.JetThermalEntropy.density_entropy_bound line 646

    Source documentation

    Pointwise bound with a constant independent of the profile center.

    theorem density_entropy_bound {d : ℝ} (hd : 0 < d) (a v : Velocity) :
        entropy (density d a v) ≤ (3 * |Real.log d|) * density d a v +
          scaled d a (fun w => entropy (J w)) v := by
    …

    Mentions: OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.JetThermalEntropy.entropy

75. def OAI.BoltzmannNonuniqueness.JetThermalEntropy.entropyConstant line 659
76. theorem OAI.BoltzmannNonuniqueness.JetThermalEntropy.entropyConstant_nonneg line 661
77. theorem OAI.BoltzmannNonuniqueness.JetThermalEntropy.density_entropy_integrable line 664
78. theorem OAI.BoltzmannNonuniqueness.JetThermalEntropy.density_entropy_integral line 675
79. def OAI.BoltzmannNonuniqueness.JetAxialWeight.S line 703

    Source documentation

    The manuscript's S(ℓ) = sech² ℓ.

    def S (x : ℝ) : ℝ := (Real.cosh x)⁻¹ ^ 2

80. theorem OAI.BoltzmannNonuniqueness.JetAxialWeight.S_pos line 705
81. theorem OAI.BoltzmannNonuniqueness.JetAxialWeight.S_le_one line 707
82. theorem OAI.BoltzmannNonuniqueness.JetAxialWeight.continuous_S line 713
83. theorem OAI.BoltzmannNonuniqueness.JetAxialWeight.tanh_derivative line 717
84. theorem OAI.BoltzmannNonuniqueness.JetAxialWeight.intervalIntegral_S line 730
85. theorem OAI.BoltzmannNonuniqueness.JetAxialWeight.intervalIntegral_S_le_two line 735
86. theorem OAI.BoltzmannNonuniqueness.JetAxialWeight.integrable_S line 739
87. theorem OAI.BoltzmannNonuniqueness.JetAxialWeight.scaled_derivative line 753
88. theorem OAI.BoltzmannNonuniqueness.JetAxialWeight.scaled_intervalIntegral line 761
89. theorem OAI.BoltzmannNonuniqueness.JetAxialWeight.scaled_intervalIntegral_le line 774
90. theorem OAI.BoltzmannNonuniqueness.JetAxialEntropy.integrable_exp_neg_abs line 799
91. theorem OAI.BoltzmannNonuniqueness.JetAxialEntropy.cosh_lower line 814
92. theorem OAI.BoltzmannNonuniqueness.JetAxialEntropy.cosh_upper line 818
93. theorem OAI.BoltzmannNonuniqueness.JetAxialEntropy.S_exp_bound line 823
94. theorem OAI.BoltzmannNonuniqueness.JetAxialEntropy.log_S_bound line 836
95. theorem OAI.BoltzmannNonuniqueness.JetAxialEntropy.entropy_exp_bound line 846
96. theorem OAI.BoltzmannNonuniqueness.JetAxialEntropy.integrable_axial_entropy line 859
97. theorem OAI.BoltzmannNonuniqueness.JetGeometry.mem_annularCore_dilation line 884
98. theorem OAI.BoltzmannNonuniqueness.JetGeometry.eventually_annularCore_dilation line 895
99. def OAI.BoltzmannNonuniqueness.JetGaussianMoments.kernel line 942
100. theorem OAI.BoltzmannNonuniqueness.JetGaussianMoments.radial_integrable line 944
101. theorem OAI.BoltzmannNonuniqueness.JetGaussianMoments.kernel_integrable line 957
102. theorem OAI.BoltzmannNonuniqueness.JetGaussianMoments.moment_integrable line 960
103. def OAI.BoltzmannNonuniqueness.JetGaussianMoments.mass line 964
104. def OAI.BoltzmannNonuniqueness.JetGaussianMoments.moment line 965
105. theorem OAI.BoltzmannNonuniqueness.JetGaussianMoments.mass_nonneg line 967
106. theorem OAI.BoltzmannNonuniqueness.JetGaussianMoments.moment_nonneg line 968
107. theorem OAI.BoltzmannNonuniqueness.JetGaussianMoments.kernel_le line 971
108. theorem OAI.BoltzmannNonuniqueness.JetGaussianMoments.integral_kernel_le line 975
109. theorem OAI.BoltzmannNonuniqueness.JetGaussianMoments.integral_moment_le line 979
110. theorem OAI.BoltzmannNonuniqueness.JetGaussianMoments.centered_scaled_eq line 985
111. theorem OAI.BoltzmannNonuniqueness.JetGaussianMoments.centered_scaled_integrable line 993
112. theorem OAI.BoltzmannNonuniqueness.JetGaussianMoments.integral_centered_scaled line 998
113. def OAI.BoltzmannNonuniqueness.JetMaskNonempty.first line 1022
114. def OAI.BoltzmannNonuniqueness.JetMaskNonempty.radius line 1024
115. def OAI.BoltzmannNonuniqueness.JetMaskNonempty.point line 1026
116. theorem OAI.BoltzmannNonuniqueness.JetMaskNonempty.first_bounds line 1029
117. theorem OAI.BoltzmannNonuniqueness.JetMaskNonempty.radius_gt line 1034
118. theorem OAI.BoltzmannNonuniqueness.JetMaskNonempty.point_norm line 1039
119. theorem OAI.BoltzmannNonuniqueness.JetMaskNonempty.point_mem line 1051
120. theorem OAI.BoltzmannNonuniqueness.JetMaskNonempty.mask_nonempty line 1072
121. def OAI.BoltzmannNonuniqueness.JetLatticeGaussian.exponential line 1091
122. theorem OAI.BoltzmannNonuniqueness.JetLatticeGaussian.summable_exponential line 1093
123. def OAI.BoltzmannNonuniqueness.JetLatticeGaussian.gaussian line 1101
124. def OAI.BoltzmannNonuniqueness.JetLatticeGaussian.constant line 1104
125. theorem OAI.BoltzmannNonuniqueness.JetLatticeGaussian.pointwise_bound line 1106
126. theorem OAI.BoltzmannNonuniqueness.JetLatticeGaussian.summable_gaussian line 1121
127. theorem OAI.BoltzmannNonuniqueness.JetLatticeGaussian.sum_le line 1126
128. def OAI.BoltzmannNonuniqueness.JetLatticeProduct.coordinates line 1151
129. def OAI.BoltzmannNonuniqueness.JetLatticeProduct.product line 1157
130. theorem OAI.BoltzmannNonuniqueness.JetLatticeProduct.product_nonneg line 1160
131. theorem OAI.BoltzmannNonuniqueness.JetLatticeProduct.product_eq_exp line 1165
132. theorem OAI.BoltzmannNonuniqueness.JetLatticeProduct.sum_eq line 1172
133. theorem OAI.BoltzmannNonuniqueness.JetLatticeProduct.sum_le line 1192
134. def OAI.BoltzmannNonuniqueness.JetGeometry.stripeAtPeriod line 1227
135. theorem OAI.BoltzmannNonuniqueness.JetGeometry.stripe_dilation line 1231
136. theorem OAI.BoltzmannNonuniqueness.JetGeometry.stripe_period_tendsto_zero line 1239
137. theorem OAI.BoltzmannNonuniqueness.JetGeometry.relative_thermal_shift_eq line 1244
138. theorem OAI.BoltzmannNonuniqueness.JetGeometry.relative_thermal_shift_tendsto_zero line 1248