OAI/MathematicalPhysics/Boltzmann/Jets/GeometricSlice.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

Degenerate slices and nonnegative singular integrals

The line integral through the velocity axis is infinite. Its exceptional transverse parameters form an affine line of two-dimensional measure zero. These results keep that extended value explicit and justify the almost-everywhere scalar estimates, including products with arbitrary axial probability measures.

  1. def OAI.BoltzmannNonuniqueness.GeometricSlice.sliceOffset line 28

    Source documentation

    Signed distance of the transverse collision line from the velocity axis.

    def sliceOffset (v p : Transverse) : ℝ := inner ℝ (direction (v - p)) v
  2. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.measurable_sliceOffset line 30
  3. def OAI.BoltzmannNonuniqueness.GeometricSlice.RegularTransverse line 34
  4. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.sliceOffset_eq_zero_iff line 37
  5. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.regularTransverse_iff line 49
  6. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.measurableSet_regularTransverse line 61
  7. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.volume_sliceOffset_zero line 67

    Source documentation

    The bad transverse parameters lie in a proper affine hyperplane.

    theorem volume_sliceOffset_zero {v : Transverse} (hv : v ≠ 0) :
    volume {p | sliceOffset v p = 0} = 0 := by
…

    Mentions: OAI.BoltzmannNonuniqueness.GeometricSlice.sliceOffset

  8. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.ae_regularTransverse_volume line 86
  9. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.regularTransverse_zero line 97
  10. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.ae_regularTransverse_atom line 102
  11. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.ae_regularTransverse_uniformDisk line 107
  12. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.ae_regularTransverse_gaussian line 111
  13. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.ae_regularTransverse_prod line 116

    Source documentation

    No regularity of the axial law is needed to preserve the exceptional null set.

    theorem ae_regularTransverse_prod {v : Transverse} {μ : Measure Transverse}
    {ρ : Measure ℝ} [SFinite ρ] (hμ : ∀ᵐ p ∂μ, RegularTransverse v p) :
    ∀ᵐ p ∂μ.prod ρ, RegularTransverse v p.1 := by
…

    Mentions: OAI.BoltzmannNonuniqueness.GeometricSlice.RegularTransverse

  14. def OAI.BoltzmannNonuniqueness.GeometricSlice.extendedPower line 124

    Source documentation

    The scalar line singularity retains its infinite value on a zero-distance slice.

    def extendedPower (q x : ℝ) : ℝ≥0∞ :=
…
  15. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.measurable_extendedPower line 127
  16. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.extendedPower_ae_eq line 132
  17. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.lintegral_extendedPower_interval_le line 148

    Source documentation

    The extended-valued scalar integral has the same finite bound as the ordinary integral whenever the nonzero intercept excludes an identically singular slice.

    theorem lintegral_extendedPower_interval_le {q a b A B R : ℝ}
    (hq₁ : 1 < q) (hq₂ : q < 2) (hab : a < b) (hR : 0 < R)
    (ha : -R ≤ a) (hb : b ≤ R) (hA : A ≠ 0) :
    (∫⁻ x in Ioc a b, extendedPower q (A - B * x)) ≤
      ENNReal.ofReal (AxialSlices.scalarConstant (1 - q) *
        (R ^ (q - 1) * (b - a) ^ (2 - q) * |A| ^ (1 - q))) := by
…

    Mentions: OAI.BoltzmannNonuniqueness.GeometricSlice.extendedPower, OAI.BoltzmannNonuniqueness.AxialSlices.scalarConstant

  18. def OAI.BoltzmannNonuniqueness.GeometricSlice.extendedKernel line 163

    Source documentation

    Extended expectation kernel, infinite on degenerate transverse slices.

    def extendedKernel (q : ℝ) (v p : Transverse) : ℝ≥0∞ := by
…
  19. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.measurable_extendedKernel line 167
  20. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.extendedKernel_ae_eq line 175
  21. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.uniformDisk_extendedKernel_lintegral_le line 181
  22. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.atom_extendedKernel_lintegral_le line 197
  23. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.gaussian_extendedKernel_lintegral_le line 204
  24. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.lintegral_lineWeight_le_extended line 212

    Source documentation

    The line estimate with its correct extended value at zero distance.

    theorem lintegral_lineWeight_le_extended {q R : ℝ} (hq : 1 < q) (hR : 0 ≤ R)
    (e : Transverse) (he : ‖e‖ = 1) (D m : ℝ) :
    (∫⁻ s in Icc (m - R) (m + R),
      ENNReal.ofReal (TransverseLine.lineWeight q e D s)) ≤
      ENNReal.ofReal (2 * R) + ENNReal.ofReal (AxialSlices.lineConstant q) * extendedPower q D := by
…

    Mentions: OAI.BoltzmannNonuniqueness.TransverseLine.lineWeight, OAI.BoltzmannNonuniqueness.AxialSlices.lineConstant, OAI.BoltzmannNonuniqueness.GeometricSlice.extendedPower

  25. def OAI.BoltzmannNonuniqueness.GeometricSlice.rectangleLineMass line 228

    Source documentation

    Integration over the coordinate rectangle; this is an explicit upper bound, not a definition of the original ball restriction.

    def rectangleLineMass (q : ℝ) (e : Transverse) (A B m R a b : ℝ) : ℝ≥0∞ :=
…
  26. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.rectangleLineMass_le line 232
  27. def OAI.BoltzmannNonuniqueness.GeometricSlice.ballLineRegion line 265

    Source documentation

    The ball restriction in transverse-line and axial-displacement coordinates.

    def ballLineRegion (e v : Transverse) (D z R : ℝ) : Set ℝ :=
…
  28. def OAI.BoltzmannNonuniqueness.GeometricSlice.ballLineMass line 268
  29. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.inner_quarterTurn_line_sub line 272
  30. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.ballLineRegion_subset_rectangle line 282
  31. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.ballLineMass_le_rectangle line 297
  32. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.ballLineMass_le line 305
  33. def OAI.BoltzmannNonuniqueness.GeometricSlice.transverseWeight line 316
  34. def OAI.BoltzmannNonuniqueness.GeometricSlice.intervalCoefficient line 318
  35. def OAI.BoltzmannNonuniqueness.GeometricSlice.averagingCoefficient line 322
  36. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.transverseWeight_pos line 325
  37. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.intervalCoefficient_pos line 329
  38. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.averagingCoefficient_pos line 336
  39. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.sliceOffset_eq_norm_mul_angle line 342
  40. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.sliceOffset_rpow line 352
  41. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.normalized_sum_bound line 358
  42. def OAI.BoltzmannNonuniqueness.GeometricSlice.normalizedBallSlice line 372

    Source documentation

    The ball-restricted chart integral with factor 1 / (W(v) * ‖v-p‖). Identifying this chart factor with the collision-plane measure is a separate change-of-variables statement. Degenerate parameters retain the value infinity.

    def normalizedBallSlice (q : ℝ) (v : Transverse) (t : ℝ) (p : Transverse)
    (alpha R a b : ℝ) : ℝ≥0∞ := by
…
  43. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.slice_numerator_bound line 381
  44. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.normalizedBallSlice_le line 398

    Source documentation

    A pointwise bound with all singular transverse cases handled in the extended reals.

    theorem normalizedBallSlice_le {q a b R : ℝ}
    (hq₁ : 1 < q) (hq₂ : q < 2) (hab : a < b) (hR : 0 < R)
    (ha : -R ≤ a) (hb : b ≤ R) {v : Transverse} (hv : v ≠ 0)
    (t alpha : ℝ) (p : Transverse) :
    normalizedBallSlice q v t p alpha R a b ≤
      ENNReal.ofReal (averagingCoefficient q R (b - a) ‖v‖) * extendedKernel q v p := by
…

    Mentions: OAI.BoltzmannNonuniqueness.GeometricSlice.normalizedBallSlice, OAI.BoltzmannNonuniqueness.GeometricSlice.averagingCoefficient, OAI.BoltzmannNonuniqueness.GeometricSlice.extendedKernel

  45. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.measurable_ballLineMass line 432
  46. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.measurable_normalizedBallSlice line 476
  47. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.averagingCoefficient_bound line 492
  48. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.normalizedBallSlice_product_bound line 518

    Source documentation

    Averaging over an arbitrary axial probability leaves the uniform transverse bound unchanged. The transverse expectation premise is discharged below for each law.

    theorem normalizedBallSlice_product_bound {q a b R : ℝ}
    (hq₁ : 1 < q) (hq₂ : q < 2) (hab : a < b) (hR : 0 < R)
    (ha : -R ≤ a) (hb : b ≤ R) {v : Transverse} (hv : v ≠ 0)
    (t : ℝ) (μ : Measure Transverse) (ρ : Measure ℝ) [IsProbabilityMeasure ρ]
    (hμ : (∫⁻ p, extendedKernel q v p ∂μ) ≤ ENNReal.ofReal (expectationConstant q / ‖v‖)) :
    (∫⁻ p, normalizedBallSlice q v t p.1 p.2 R a b ∂μ.prod ρ) ≤
      ENNReal.ofReal (expectationConstant q *
        (2 * R * (b - a) + intervalCoefficient q R (b - a))) := by
…

    Mentions: OAI.BoltzmannNonuniqueness.GeometricSlice.extendedKernel, OAI.BoltzmannNonuniqueness.GeometricSlice.normalizedBallSlice, OAI.BoltzmannNonuniqueness.GeometricSlice.intervalCoefficient

  49. def OAI.BoltzmannNonuniqueness.GeometricSlice.geometricConstant line 544
  50. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.geometricConstant_pos line 547
  51. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.geometricConstant_bound line 555
  52. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.gaussian_geometric_interval line 569
  53. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.uniformDisk_geometric_interval line 580
  54. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.atom_geometric_interval line 591
  55. def OAI.BoltzmannNonuniqueness.GeometricSlice.IsDiskOrAtomLaw line 603

    Source documentation

    The component laws permitted in the manuscript's transverse mixtures.

    def IsDiskOrAtomLaw (μ : Measure Transverse) : Prop :=
…
  56. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.isProbabilityMeasure_of_diskOrAtomLaw line 606
  57. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.ae_regularTransverse_of_diskOrAtomLaw line 612
  58. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.extendedKernel_bound_of_diskOrAtomLaw line 619
  59. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.diskAtomMixture_isProbabilityMeasure line 626
  60. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.ae_regularTransverse_diskAtomMixture line 633
  61. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.diskAtomMixture_extendedKernel_bound line 644
  62. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.diskAtomMixture_geometric_interval line 660

    Source documentation

    The geometric interval estimate for every probability mixture of centered uniform disks and the atom at zero, with an arbitrary axial probability law.

    theorem diskAtomMixture_geometric_interval {ι : Type*} [MeasurableSpace ι]
    {q a b R : ℝ} (hq₁ : 1 < q) (hq₂ : q < 2) (hab : a < b) (hR : 0 < R)
    (ha : -R ≤ a) (hb : b ≤ R) {v : Transverse} (hv : v ≠ 0)
    (t : ℝ) (ν : Measure ι) [IsProbabilityMeasure ν] (L : ι → Measure Transverse)
    (hL : Measurable L) (hLaw : ∀ᵐ i ∂ν, IsDiskOrAtomLaw (L i))
    (ρ : Measure ℝ) [IsProbabilityMeasure ρ] :
    (∫⁻ p, normalizedBallSlice q v t p.1 p.2 R a b ∂(ν.bind L).prod ρ) ≤
      ENNReal.ofReal (geometricConstant q *
        (R * (b - a) + R ^ (q - 1) * (b - a) ^ (2 - q))) :=
…

    Mentions: OAI.BoltzmannNonuniqueness.GeometricSlice.IsDiskOrAtomLaw, OAI.BoltzmannNonuniqueness.GeometricSlice.normalizedBallSlice, OAI.BoltzmannNonuniqueness.GeometricSlice.geometricConstant

  63. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.ballLineRegion_eq_empty_of_outside line 673
  64. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.ballLineMass_clip line 683

    Source documentation

    The genuine ball already clips the axial displacement to [-R,R]. The single lower endpoint is removed only on a Lebesgue-null set.

    theorem ballLineMass_clip {R : ℝ} (hR : 0 ≤ R)
    (q : ℝ) (e v : Transverse) (A B a b : ℝ) :
    ballLineMass q e v A B R a b =
      ballLineMass q e v A B R (max (-R) a) (min R b) := by
…

    Mentions: OAI.BoltzmannNonuniqueness.GeometricSlice.ballLineMass

  65. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.normalizedBallSlice_clip line 716
  66. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.geometric_interval_of_kernel_bound line 728

    Source documentation

    The interval estimate for arbitrary axial endpoints, using the actual ball restriction to clip the interval before applying the scalar estimate.

    theorem geometric_interval_of_kernel_bound {q a b R : ℝ}
    (hq₁ : 1 < q) (hq₂ : q < 2) (_hab : a < b) (hR : 0 < R)
    {v : Transverse} (hv : v ≠ 0) (t : ℝ)
    (μ : Measure Transverse) (ρ : Measure ℝ) [IsProbabilityMeasure ρ]
    (hreg : ∀ᵐ p ∂μ, RegularTransverse v p)
    (hμ : (∫⁻ p, extendedKernel q v p ∂μ) ≤ ENNReal.ofReal (expectationConstant q / ‖v‖)) :
    (∫⁻ p, normalizedBallSlice q v t p.1 p.2 R a b ∂μ.prod ρ) ≤
      ENNReal.ofReal (geometricConstant q *
        (R * (b - a) + R ^ (q - 1) * (b - a) ^ (2 - q))) := by
…

    Mentions: OAI.BoltzmannNonuniqueness.GeometricSlice.RegularTransverse, OAI.BoltzmannNonuniqueness.GeometricSlice.extendedKernel, OAI.BoltzmannNonuniqueness.GeometricSlice.normalizedBallSlice, OAI.BoltzmannNonuniqueness.GeometricSlice.geometricConstant

  67. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.gaussian_geometric_interval_any line 765
  68. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.diskAtomMixture_geometric_interval_any line 774
  69. def OAI.BoltzmannNonuniqueness.GeometricSlice.geometricTotalConstant line 787
  70. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.geometric_total_of_kernel_bound line 790

    Source documentation

    Taking the full axial range gives the uniform C_q R² ball estimate.

    theorem geometric_total_of_kernel_bound {q R : ℝ} (hq₁ : 1 < q) (hq₂ : q < 2)
    (hR : 1 ≤ R) {v : Transverse} (hv : v ≠ 0) (t : ℝ)
    (μ : Measure Transverse) (ρ : Measure ℝ) [IsProbabilityMeasure ρ]
    (hreg : ∀ᵐ p ∂μ, RegularTransverse v p)
    (hμ : (∫⁻ p, extendedKernel q v p ∂μ) ≤ ENNReal.ofReal (expectationConstant q / ‖v‖)) :
    (∫⁻ p, normalizedBallSlice q v t p.1 p.2 R (-R) R ∂μ.prod ρ) ≤
      ENNReal.ofReal (geometricTotalConstant q * R ^ 2) := by
…

    Mentions: OAI.BoltzmannNonuniqueness.GeometricSlice.RegularTransverse, OAI.BoltzmannNonuniqueness.GeometricSlice.extendedKernel, OAI.BoltzmannNonuniqueness.GeometricSlice.normalizedBallSlice, OAI.BoltzmannNonuniqueness.GeometricSlice.geometricTotalConstant

  71. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.gaussian_geometric_total line 813
  72. theorem OAI.BoltzmannNonuniqueness.GeometricSlice.diskAtomMixture_geometric_total line 821