OAI/MathematicalPhysics/Boltzmann/Collision/GaussianEstimates.lean

GitHub source file

99 declarations, 0 contain sorry, 0 declared as axioms

Pointwise Gaussian norm bounds for the fixed-cutoff equation

Detailed balance removes the output Gaussian from the gain. These estimates are for the actual collision integral, with no published-input hypothesis.

  1. def OAI.BoltzmannNonuniqueness.GaussianCutoff.mass line 28
  2. def OAI.BoltzmannNonuniqueness.GaussianCutoff.gainConstant line 30
  3. def OAI.BoltzmannNonuniqueness.GaussianCutoff.lossConstant line 32
  4. theorem OAI.BoltzmannNonuniqueness.GaussianCutoff.constants_nonneg line 34
  5. def OAI.BoltzmannNonuniqueness.GaussianCutoff.integrand line 40
  6. def OAI.BoltzmannNonuniqueness.GaussianCutoff.gain line 45
  7. def OAI.BoltzmannNonuniqueness.GaussianCutoff.frequency line 48
  8. theorem OAI.BoltzmannNonuniqueness.GaussianCutoff.kernel_le line 51
  9. theorem OAI.BoltzmannNonuniqueness.GaussianCutoff.measurable_integrand line 62
  10. theorem OAI.BoltzmannNonuniqueness.GaussianCutoff.measurable_gain line 76
  11. theorem OAI.BoltzmannNonuniqueness.GaussianCutoff.integrand_bound line 82
  12. theorem OAI.BoltzmannNonuniqueness.GaussianCutoff.majorant_integrable line 98
  13. theorem OAI.BoltzmannNonuniqueness.GaussianCutoff.majorant_integral line 104
  14. theorem OAI.BoltzmannNonuniqueness.GaussianCutoff.integrable_gain line 113
  15. theorem OAI.BoltzmannNonuniqueness.GaussianCutoff.gain_bound line 122
  16. theorem OAI.BoltzmannNonuniqueness.GaussianCutoff.gain_nonneg line 131
  17. theorem OAI.BoltzmannNonuniqueness.GaussianCutoff.gain_eq_actual line 139
  18. theorem OAI.BoltzmannNonuniqueness.GaussianCutoff.product_difference line 178
  19. theorem OAI.BoltzmannNonuniqueness.GaussianCutoff.gain_difference line 188
  20. theorem OAI.BoltzmannNonuniqueness.GaussianCutoff.measurable_frequency line 223
  21. theorem OAI.BoltzmannNonuniqueness.GaussianCutoff.frequency_nonneg line 232
  22. theorem OAI.BoltzmannNonuniqueness.GaussianCutoff.frequency_bound line 239
  23. theorem OAI.BoltzmannNonuniqueness.GaussianCutoff.frequency_difference line 258
  24. theorem OAI.BoltzmannNonuniqueness.log_maxwellian line 307
  25. theorem OAI.BoltzmannNonuniqueness.integrable_maxwellian line 314
  26. theorem OAI.BoltzmannNonuniqueness.integrable_maxwellian_phase line 327
  27. theorem OAI.BoltzmannNonuniqueness.relativeEntropyDensity_eq line 330
  28. theorem OAI.BoltzmannNonuniqueness.FiniteEntropyDatum.integrable_relativeEntropy line 339
  29. theorem OAI.BoltzmannNonuniqueness.relativeEntropyDensity_nonneg line 349

    Source documentation

    The scalar relative entropy is nonnegative at every nonnegative density value.

    theorem relativeEntropyDensity_nonneg {a m : ℝ} (ha : 0 ≤ a) (hm : 0 < m) :
    0 ≤ a * Real.log (a / m) - a + m := by
…
  30. theorem OAI.BoltzmannNonuniqueness.relativeEntropy_nonneg line 363
  31. theorem OAI.BoltzmannNonuniqueness.GaussianCutoff.gain_mono line 388
  32. theorem OAI.BoltzmannNonuniqueness.GaussianCutoff.finite_sum_gain_le line 404
  33. theorem OAI.BoltzmannNonuniqueness.GaussianCutoff.gain_tendsto line 437
  34. def OAI.BoltzmannNonuniqueness.GaussianDiskMixture.gaussianDensity line 476
  35. def OAI.BoltzmannNonuniqueness.GaussianDiskMixture.diskDensity line 479
  36. def OAI.BoltzmannNonuniqueness.GaussianDiskMixture.mixingDensity line 482
  37. theorem OAI.BoltzmannNonuniqueness.GaussianDiskMixture.gaussianDensity_nonneg line 485
  38. theorem OAI.BoltzmannNonuniqueness.GaussianDiskMixture.diskDensity_nonneg line 489
  39. theorem OAI.BoltzmannNonuniqueness.GaussianDiskMixture.mixingDensity_nonneg line 495
  40. theorem OAI.BoltzmannNonuniqueness.GaussianDiskMixture.measurable_gaussianDensity line 499
  41. theorem OAI.BoltzmannNonuniqueness.GaussianDiskMixture.measurable_mixingDensity line 503
  42. theorem OAI.BoltzmannNonuniqueness.GaussianDiskMixture.diskDensity_eq_ite line 507
  43. theorem OAI.BoltzmannNonuniqueness.GaussianDiskMixture.measurable_diskDensity line 511
  44. theorem OAI.BoltzmannNonuniqueness.GaussianDiskMixture.integrableOn_mixingDensity line 515
  45. theorem OAI.BoltzmannNonuniqueness.GaussianDiskMixture.integral_gaussian_tail line 526
  46. theorem OAI.BoltzmannNonuniqueness.GaussianDiskMixture.integral_radius_tail line 547
  47. theorem OAI.BoltzmannNonuniqueness.GaussianDiskMixture.integral_radius_cubic line 558
  48. theorem OAI.BoltzmannNonuniqueness.GaussianDiskMixture.integral_mixingDensity line 577
  49. theorem OAI.BoltzmannNonuniqueness.GaussianDiskMixture.layerCake_integrand line 587
  50. theorem OAI.BoltzmannNonuniqueness.GaussianDiskMixture.integrableOn_layerCake line 603
  51. theorem OAI.BoltzmannNonuniqueness.GaussianDiskMixture.density_layerCake line 619

    Source documentation

    Pointwise layer-cake identity, with the positive-radius mixing law normalized below.

    theorem density_layerCake {d : ℝ} (hd : 0 < d) (p : Transverse) :
    (∫ a in Ioi (0 : ℝ), mixingDensity d a * diskDensity a p) = gaussianDensity d p := by
…

    Mentions: OAI.BoltzmannNonuniqueness.GaussianDiskMixture.mixingDensity, OAI.BoltzmannNonuniqueness.GaussianDiskMixture.diskDensity, OAI.BoltzmannNonuniqueness.GaussianDiskMixture.gaussianDensity

  52. theorem OAI.BoltzmannNonuniqueness.GaussianDiskMixture.lintegral_density_layerCake line 628
  53. theorem OAI.BoltzmannNonuniqueness.GaussianDiskMixture.lintegral_mixingDensity line 635
  54. theorem OAI.BoltzmannNonuniqueness.GaussianDiskMixture.lintegral_diskDensity_mul line 642
  55. theorem OAI.BoltzmannNonuniqueness.GaussianDiskMixture.measurable_layerCake line 653
  56. theorem OAI.BoltzmannNonuniqueness.GaussianDiskMixture.lintegral_layerCake_mul line 666
  57. theorem OAI.BoltzmannNonuniqueness.GaussianDiskMixture.lintegral_layerCake_disk line 676
  58. theorem OAI.BoltzmannNonuniqueness.GaussianDiskMixture.lintegral_gaussian_mixture line 686

    Source documentation

    Tonelli's theorem expresses every nonnegative measurable Gaussian expectation as a probability mixture of normalized disk expectations.

    theorem lintegral_gaussian_mixture {d : ℝ} (hd : 0 < d)
    (φ : Transverse → ℝ≥0∞) (hφ : Measurable φ) :
    (∫⁻ p, ENNReal.ofReal (gaussianDensity d p) * φ p) =
      ∫⁻ a in Ioi (0 : ℝ), ENNReal.ofReal (mixingDensity d a) *
        ((ENNReal.ofReal (Real.pi * a ^ 2))⁻¹ * ∫⁻ p in ball (0 : Transverse) a, φ p) := by
…

    Mentions: OAI.BoltzmannNonuniqueness.GaussianDiskMixture.gaussianDensity, OAI.BoltzmannNonuniqueness.GaussianDiskMixture.mixingDensity

  59. theorem OAI.BoltzmannNonuniqueness.GaussianDiskMixture.integrable_diskDensity line 703
  60. theorem OAI.BoltzmannNonuniqueness.GaussianDiskMixture.integral_diskDensity line 706
  61. theorem OAI.BoltzmannNonuniqueness.GaussianDiskMixture.lintegral_diskDensity line 712
  62. theorem OAI.BoltzmannNonuniqueness.GaussianDiskMixture.lintegral_gaussianDensity line 717
  63. def OAI.BoltzmannNonuniqueness.GaussianDiskMixture.gaussianLaw line 731
  64. def OAI.BoltzmannNonuniqueness.GaussianDiskMixture.uniformDiskLaw line 734
  65. def OAI.BoltzmannNonuniqueness.GaussianDiskMixture.mixingRadiusLaw line 737
  66. theorem OAI.BoltzmannNonuniqueness.GaussianDiskMixture.gaussianLaw_isProbabilityMeasure line 740
  67. theorem OAI.BoltzmannNonuniqueness.GaussianDiskMixture.uniformDiskLaw_isProbabilityMeasure line 746
  68. theorem OAI.BoltzmannNonuniqueness.GaussianDiskMixture.mixingRadiusLaw_isProbabilityMeasure line 752
  69. theorem OAI.BoltzmannNonuniqueness.GaussianDiskMixture.uniformDiskLaw_lintegral line 758
  70. theorem OAI.BoltzmannNonuniqueness.GaussianDiskMixture.gaussianLaw_mixture line 771

    Source documentation

    The centered Gaussian law is the probability mixture of normalized disk laws with radius density mixingDensity d on the positive half-line.

    theorem gaussianLaw_mixture {d : ℝ} (hd : 0 < d)
    (φ : Transverse → ℝ≥0∞) (hφ : Measurable φ) :
    (∫⁻ p, φ p ∂gaussianLaw d) =
      ∫⁻ a, (∫⁻ p, φ p ∂uniformDiskLaw a) ∂mixingRadiusLaw d := by
…

    Mentions: OAI.BoltzmannNonuniqueness.GaussianDiskMixture.gaussianLaw, OAI.BoltzmannNonuniqueness.GaussianDiskMixture.uniformDiskLaw, OAI.BoltzmannNonuniqueness.GaussianDiskMixture.mixingRadiusLaw

  71. theorem OAI.BoltzmannNonuniqueness.GaussianDiskMixture.gaussian_kernel_lintegral_le line 792
  72. theorem OAI.BoltzmannNonuniqueness.GaussianDiskMixture.integrable_gaussian_kernel line 826
  73. theorem OAI.BoltzmannNonuniqueness.GaussianDiskMixture.gaussian_kernel_expectation_le line 840
  74. theorem OAI.BoltzmannNonuniqueness.GaussianDiskMixture.gaussianLaw_kernel_lintegral_le line 854
  75. def OAI.BoltzmannNonuniqueness.GaussianSheets.axialLaw line 890

    Source documentation

    The axial image law, with variance parameter as in Mathlib's Gaussian.

    def axialLaw (v : ℝ≥0) (Φ : ℝ → ℝ) : Measure ℝ :=
…
  76. instance OAI.BoltzmannNonuniqueness.GaussianSheets.axialLaw_isProbabilityMeasure line 893
  77. theorem OAI.BoltzmannNonuniqueness.GaussianSheets.axialLaw_univ line 898
  78. theorem OAI.BoltzmannNonuniqueness.GaussianSheets.original_gaussian_density line 901
  79. theorem OAI.BoltzmannNonuniqueness.GaussianSheets.wider_gaussian_density line 908
  80. theorem OAI.BoltzmannNonuniqueness.GaussianSheets.integrable_gaussianReal_iff line 912
  81. theorem OAI.BoltzmannNonuniqueness.GaussianSheets.gaussianPDF_mul_exp_quarter line 922

    Source documentation

    A quadratic exponential changes the centered Gaussian variance by a factor of two.

    theorem gaussianPDF_mul_exp_quarter {v : ℝ≥0} (hv : v ≠ 0) (a : ℝ) :
    gaussianPDFReal 0 v a * Real.exp (a ^ 2 / (4 * (v : ℝ))) =
      Real.sqrt 2 * gaussianPDFReal 0 (2 * v) a := by
…
  82. theorem OAI.BoltzmannNonuniqueness.GaussianSheets.integrable_exp_quarter_gaussian line 940
  83. theorem OAI.BoltzmannNonuniqueness.GaussianSheets.integral_exp_quarter_gaussian line 946
  84. theorem OAI.BoltzmannNonuniqueness.GaussianSheets.exp_image_le line 953
  85. theorem OAI.BoltzmannNonuniqueness.GaussianSheets.integrable_exp_image line 975

    Source documentation

    The Gaussian parameter integrand is genuinely integrable, before taking its image law.

    theorem integrable_exp_image {v : ℝ≥0} (hv : v ≠ 0) (hv₁ : v ≤ 1)
    {A δ : ℝ} (hA : 0 ≤ A) (hδ : 0 ≤ δ) (hδ₁ : δ ≤ 1 / 16)
    {Φ : ℝ → ℝ} (hΦm : Measurable Φ) (hΦ : ∀ a, |Φ a| ≤ A + δ * |a|) :
    Integrable (fun a => Real.exp (8 * (Φ a) ^ 2)) (gaussianReal 0 v) := by
…
  86. theorem OAI.BoltzmannNonuniqueness.GaussianSheets.integral_exp_image_le line 986

    Source documentation

    The constant 2 * exp (16 * A²) works for the original and wider parameter laws.

    theorem integral_exp_image_le {v : ℝ≥0} (hv : v ≠ 0) (hv₁ : v ≤ 1)
    {A δ : ℝ} (hA : 0 ≤ A) (hδ : 0 ≤ δ) (hδ₁ : δ ≤ 1 / 16)
    {Φ : ℝ → ℝ} (hΦm : Measurable Φ) (hΦ : ∀ a, |Φ a| ≤ A + δ * |a|) :
    (∫ a, Real.exp (8 * (Φ a) ^ 2) ∂gaussianReal 0 v) ≤ 2 * Real.exp (16 * A ^ 2) := by
…
  87. theorem OAI.BoltzmannNonuniqueness.GaussianSheets.integrable_axialLaw_exp line 1003
  88. theorem OAI.BoltzmannNonuniqueness.GaussianSheets.integral_axialLaw_exp_le line 1010
  89. theorem OAI.BoltzmannNonuniqueness.GaussianSheets.gaussian_parameter_tail line 1018

    Source documentation

    The parameter-tail estimate widens the Gaussian and extracts its uniform decay factor.

    theorem gaussian_parameter_tail {B : ℝ} (hB : 0 ≤ B) (w : Velocity) :
    {u : Velocity | B < ‖u‖}.indicator (fun u => Real.exp (-‖u‖ ^ 2)) w ≤
      Real.exp (-B ^ 2 / 2) * Real.exp (-‖w‖ ^ 2 / 2) := by
…

    Mentions: OAI.BoltzmannNonuniqueness.Velocity

  90. def OAI.BoltzmannNonuniqueness.GaussianCutoff.source line 1047
  91. theorem OAI.BoltzmannNonuniqueness.GaussianCutoff.measurable_source line 1050
  92. theorem OAI.BoltzmannNonuniqueness.GaussianCutoff.source_bounds line 1055
  93. theorem OAI.BoltzmannNonuniqueness.GaussianCutoff.source_difference line 1074
  94. def OAI.BoltzmannNonuniqueness.GaussianCutoff.coldSource line 1132
  95. theorem OAI.BoltzmannNonuniqueness.GaussianCutoff.measurable_coldSource line 1135
  96. theorem OAI.BoltzmannNonuniqueness.GaussianCutoff.coldSource_bounds line 1140
  97. theorem OAI.BoltzmannNonuniqueness.GaussianCutoff.coldSource_mono line 1160
  98. theorem OAI.BoltzmannNonuniqueness.GaussianCutoff.coldSource_tendsto line 1172
  99. theorem OAI.BoltzmannNonuniqueness.GaussianCutoff.finite_sum_coldSource_le line 1199