OAI/MathematicalPhysics/Boltzmann/Collision/TransverseAverage.lean

GitHub source file

81 declarations, 0 contain sorry, 0 declared as axioms

Uniform transverse disk bounds

This proves the translated disk estimate ker:disk-singularity from Section 3. The singular contribution is split at distance R from the origin. Inside, polar integration is explicit; outside, the singularity is at most R⁻ᑫ.

  1. def OAI.BoltzmannNonuniqueness.TransverseDisk.diskConstant line 23
  2. theorem OAI.BoltzmannNonuniqueness.TransverseDisk.diskConstant_pos line 25
  3. theorem OAI.BoltzmannNonuniqueness.TransverseDisk.diskConstant_ge_pi line 29
  4. theorem OAI.BoltzmannNonuniqueness.TransverseDisk.closedDisk_volume_real line 34
  5. theorem OAI.BoltzmannNonuniqueness.TransverseDisk.disk_volume_real line 40
  6. theorem OAI.BoltzmannNonuniqueness.TransverseDisk.integrableOn_singularity_closedDisk line 46
  7. theorem OAI.BoltzmannNonuniqueness.TransverseDisk.integrableOn_singularity_disk line 50
  8. theorem OAI.BoltzmannNonuniqueness.TransverseDisk.integral_singularity_centeredDisk line 55

    Source documentation

    Exact centered disk integral, including the integrable singularity at the origin.

    theorem integral_singularity_centeredDisk {q R : ℝ} (hq : q < 2) (hR : 0 < R) :
    (∫ u in ball (0 : Transverse) R, singularity q u) =
      2 * Real.pi / (2 - q) * R ^ (2 - q) := by
…
  9. theorem OAI.BoltzmannNonuniqueness.TransverseDisk.singularity_split_bound line 89
  10. theorem OAI.BoltzmannNonuniqueness.TransverseDisk.radius_pow_mul line 100
  11. theorem OAI.BoltzmannNonuniqueness.TransverseDisk.integral_singularity_closedDisk_le line 105
  12. theorem OAI.BoltzmannNonuniqueness.TransverseDisk.integrableOn_diskWeight_closedDisk line 134
  13. theorem OAI.BoltzmannNonuniqueness.TransverseDisk.integral_diskWeight_closedDisk_le line 142

    Source documentation

    The uniform translated closed-disk bound from ker:disk-singularity.

    theorem integral_diskWeight_closedDisk_le {q R : ℝ} (hq₁ : 1 < q) (hq₂ : q < 2)
    (hR : 0 < R) (a : Transverse) :
    (∫ u in closedBall a R, 1 + singularity q u) ≤
      diskConstant q * (R ^ 2 + R ^ (2 - q)) := by
…

    Mentions: OAI.BoltzmannNonuniqueness.TransverseDisk.diskConstant

  14. theorem OAI.BoltzmannNonuniqueness.TransverseDisk.integrableOn_diskWeight_disk line 160
  15. theorem OAI.BoltzmannNonuniqueness.TransverseDisk.integral_diskWeight_disk_le line 164
  16. def OAI.BoltzmannNonuniqueness.TransverseLine.quarterTurn line 198
  17. def OAI.BoltzmannNonuniqueness.TransverseLine.line line 200
  18. theorem OAI.BoltzmannNonuniqueness.TransverseLine.inner_quarterTurn line 202
  19. theorem OAI.BoltzmannNonuniqueness.TransverseLine.norm_quarterTurn line 206
  20. theorem OAI.BoltzmannNonuniqueness.TransverseLine.norm_line_sq line 212
  21. theorem OAI.BoltzmannNonuniqueness.TransverseLine.inner_line line 224
  22. theorem OAI.BoltzmannNonuniqueness.TransverseLine.inner_quarterTurn_line line 230
  23. theorem OAI.BoltzmannNonuniqueness.TransverseLine.line_reconstruct line 239

    Source documentation

    The normal and tangential coordinates recover every transverse vector.

    theorem line_reconstruct (e u : Transverse) (he : ‖e‖ = 1) :
    line e (inner ℝ e u) (inner ℝ (quarterTurn e) u) = u := by
…

    Mentions: OAI.BoltzmannNonuniqueness.TransverseLine.line, OAI.BoltzmannNonuniqueness.TransverseLine.quarterTurn

  24. theorem OAI.BoltzmannNonuniqueness.TransverseLine.line_singularity line 253
  25. def OAI.BoltzmannNonuniqueness.TransverseLine.lineWeight line 259
  26. theorem OAI.BoltzmannNonuniqueness.TransverseLine.lineWeight_nonneg line 262
  27. theorem OAI.BoltzmannNonuniqueness.TransverseLine.integrable_line_singularity line 267
  28. theorem OAI.BoltzmannNonuniqueness.TransverseLine.integrableOn_lineWeight line 272
  29. theorem OAI.BoltzmannNonuniqueness.TransverseLine.integral_lineWeight_le line 279

    Source documentation

    The line bound is uniform in the center of the retained segment.

    theorem integral_lineWeight_le {q D R : ℝ} (hq : 1 < q) (hD : D ≠ 0)
    (hR : 0 ≤ R) (e : Transverse) (he : ‖e‖ = 1) (m : ℝ) :
    (∫ s in Icc (m - R) (m + R), lineWeight q e D s) ≤
      2 * R + lineConstant q * |D| ^ (1 - q) := by
…

    Mentions: OAI.BoltzmannNonuniqueness.TransverseLine.lineWeight

  30. theorem OAI.BoltzmannNonuniqueness.TransverseLine.lintegral_lineWeight_le line 300
  31. abbrev OAI.BoltzmannNonuniqueness.TransverseAverage.Circle line 332
  32. def OAI.BoltzmannNonuniqueness.TransverseAverage.circleArea line 334
  33. instance OAI.BoltzmannNonuniqueness.TransverseAverage.circleArea_isFiniteMeasure line 336
  34. def OAI.BoltzmannNonuniqueness.TransverseAverage.unitAxis line 340
  35. theorem OAI.BoltzmannNonuniqueness.TransverseAverage.norm_unitAxis line 342
  36. def OAI.BoltzmannNonuniqueness.TransverseAverage.angular line 345
  37. def OAI.BoltzmannNonuniqueness.TransverseAverage.gaussianPower line 348
  38. def OAI.BoltzmannNonuniqueness.TransverseAverage.radialGaussian line 351
  39. theorem OAI.BoltzmannNonuniqueness.TransverseAverage.radialMeasure_ne_zero line 354
  40. instance OAI.BoltzmannNonuniqueness.TransverseAverage.radialMeasure_neZero line 360
  41. theorem OAI.BoltzmannNonuniqueness.TransverseAverage.circleArea_real_univ line 363
  42. theorem OAI.BoltzmannNonuniqueness.TransverseAverage.integrable_abs_rpow_gaussian line 369
  43. def OAI.BoltzmannNonuniqueness.TransverseAverage.cartesianSplit line 378
  44. theorem OAI.BoltzmannNonuniqueness.TransverseAverage.cartesianSplit_measurePreserving line 381
  45. theorem OAI.BoltzmannNonuniqueness.TransverseAverage.gaussianPower_unitAxis line 385
  46. theorem OAI.BoltzmannNonuniqueness.TransverseAverage.integrable_gaussianPower_unitAxis line 389
  47. theorem OAI.BoltzmannNonuniqueness.TransverseAverage.gaussianPower_rotate line 402
  48. theorem OAI.BoltzmannNonuniqueness.TransverseAverage.integrable_gaussianPower line 416
  49. theorem OAI.BoltzmannNonuniqueness.TransverseAverage.integral_gaussianPower line 423
  50. theorem OAI.BoltzmannNonuniqueness.TransverseAverage.gaussianPower_polar line 429
  51. theorem OAI.BoltzmannNonuniqueness.TransverseAverage.integrable_polar_gaussianPower line 439
  52. theorem OAI.BoltzmannNonuniqueness.TransverseAverage.integrable_angular line 458
  53. theorem OAI.BoltzmannNonuniqueness.TransverseAverage.integrable_radialGaussian line 466
  54. theorem OAI.BoltzmannNonuniqueness.TransverseAverage.integral_radialGaussian_pos line 481
  55. theorem OAI.BoltzmannNonuniqueness.TransverseAverage.gaussian_polar_identity line 495
  56. theorem OAI.BoltzmannNonuniqueness.TransverseAverage.integral_angular_eq line 512
  57. def OAI.BoltzmannNonuniqueness.TransverseAverage.angularMass line 518

    Source documentation

    A finite constant depending only on q, independent of the direction.

    def angularMass (q : ℝ) : ℝ :=
…
  58. theorem OAI.BoltzmannNonuniqueness.TransverseAverage.angularMass_pos line 521
  59. theorem OAI.BoltzmannNonuniqueness.TransverseAverage.integral_one_add_angular line 527
  60. def OAI.BoltzmannNonuniqueness.TransverseAverage.kernel line 535

    Source documentation

    The degree -1 kernel in ker:transverse-expectation; its value at zero is zero.

    def kernel (q : ℝ) (e n : Transverse) : ℝ :=
…
  61. theorem OAI.BoltzmannNonuniqueness.TransverseAverage.kernel_nonneg line 538
  62. theorem OAI.BoltzmannNonuniqueness.TransverseAverage.kernel_on_ray line 542
  63. def OAI.BoltzmannNonuniqueness.TransverseAverage.radialCutoff line 549
  64. theorem OAI.BoltzmannNonuniqueness.TransverseAverage.radialCutoff_weight line 552
  65. theorem OAI.BoltzmannNonuniqueness.TransverseAverage.integrable_radialCutoff line 557
  66. theorem OAI.BoltzmannNonuniqueness.TransverseAverage.integral_radialCutoff line 573
  67. theorem OAI.BoltzmannNonuniqueness.TransverseAverage.cutoff_kernel_polar line 589
  68. theorem OAI.BoltzmannNonuniqueness.TransverseAverage.integrableOn_kernel_centeredDisk line 605
  69. theorem OAI.BoltzmannNonuniqueness.TransverseAverage.integral_kernel_centeredDisk line 631

    Source documentation

    The radial Jacobian exactly cancels the inverse-distance factor.

    theorem integral_kernel_centeredDisk {q D : ℝ} (hq : q < 2) (hD : 0 < D)
    (e : Transverse) (he : ‖e‖ = 1) :
    (∫ n in ball (0 : Transverse) D, kernel q e n) = D * angularMass q := by
…

    Mentions: OAI.BoltzmannNonuniqueness.TransverseAverage.kernel, OAI.BoltzmannNonuniqueness.TransverseAverage.angularMass

  70. theorem OAI.BoltzmannNonuniqueness.TransverseAverage.translated_cutoff_eq line 652
  71. theorem OAI.BoltzmannNonuniqueness.TransverseAverage.integrableOn_kernel_translatedDisk line 660
  72. theorem OAI.BoltzmannNonuniqueness.TransverseAverage.integral_kernel_translatedDisk_le line 668
  73. def OAI.BoltzmannNonuniqueness.TransverseAverage.direction line 690
  74. theorem OAI.BoltzmannNonuniqueness.TransverseAverage.norm_direction line 692
  75. theorem OAI.BoltzmannNonuniqueness.TransverseAverage.direction_inner_self line 695
  76. theorem OAI.BoltzmannNonuniqueness.TransverseAverage.kernel_small_shift_le line 701
  77. def OAI.BoltzmannNonuniqueness.TransverseAverage.expectationConstant line 741

    Source documentation

    A single constant works for small disks, large disks, and the atom at zero.

    def expectationConstant (q : ℝ) : ℝ :=
…
  78. theorem OAI.BoltzmannNonuniqueness.TransverseAverage.expectationConstant_pos line 744
  79. theorem OAI.BoltzmannNonuniqueness.TransverseAverage.uniformDisk_expectation_le line 750

    Source documentation

    The uniform disk case of ker:transverse-expectation, with explicit integrability above.

    theorem uniformDisk_expectation_le {q d : ℝ} (hq₁ : 1 < q) (hq₂ : q < 2) (hd : 0 < d)
    {v : Transverse} (hv : v ≠ 0) :
    (∫ p in ball (0 : Transverse) d, kernel q (direction v) (v - p)) / (Real.pi * d ^ 2) ≤
      expectationConstant q / ‖v‖ := by
…

    Mentions: OAI.BoltzmannNonuniqueness.TransverseAverage.kernel, OAI.BoltzmannNonuniqueness.TransverseAverage.direction, OAI.BoltzmannNonuniqueness.TransverseAverage.expectationConstant

  80. theorem OAI.BoltzmannNonuniqueness.TransverseAverage.kernel_at_zero_input line 801
  81. theorem OAI.BoltzmannNonuniqueness.TransverseAverage.atomZero_expectation_le line 808