OAI/MathematicalPhysics/Boltzmann/Collision/SheetGain.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

Exponential tilting of cold sheets

These are the transverse density domination and axial moment-tail estimates used in the proof of the uniform sheet gain bound, Section 3.

  1. theorem OAI.BoltzmannNonuniqueness.SheetTails.gaussian_tilt_identity line 26
  2. theorem OAI.BoltzmannNonuniqueness.SheetTails.gaussian_tilt_le line 47

    Source documentation

    The widened transverse Gaussian retains a fixed Gaussian decay factor.

    theorem gaussian_tilt_le {d : ℝ} (hd : 0 < d) (hdmax : d ≤ 1 / 8) (u : Transverse) :
    Real.exp (2 * ‖u‖ ^ 2) * gaussianDensity d u ≤
      4 * Real.exp (-46 * ‖u‖ ^ 2) * gaussianDensity (2 * d) u := by
…
  3. theorem OAI.BoltzmannNonuniqueness.SheetTails.gaussian_tilt_tail_le line 62
  4. theorem OAI.BoltzmannNonuniqueness.SheetTails.integrable_axial_tilt line 72
  5. theorem OAI.BoltzmannNonuniqueness.SheetTails.integral_axial_tilt_le line 81
  6. theorem OAI.BoltzmannNonuniqueness.SheetTails.integral_axial_tilt_tail_le line 90
  7. def OAI.BoltzmannNonuniqueness.SheetMeasures.join line 135

    Source documentation

    Coordinates are ordered transverse, then axial.

    def join : Transverse × ℝ ≃ᵐ Velocity :=
…

    Mentions: OAI.BoltzmannNonuniqueness.Velocity

  8. theorem OAI.BoltzmannNonuniqueness.SheetMeasures.norm_join_sq line 138
  9. def OAI.BoltzmannNonuniqueness.SheetMeasures.transverseLaw line 150
  10. theorem OAI.BoltzmannNonuniqueness.SheetMeasures.transverseLaw_isProbabilityMeasure line 153
  11. def OAI.BoltzmannNonuniqueness.SheetMeasures.sheetLaw line 160
  12. theorem OAI.BoltzmannNonuniqueness.SheetMeasures.sheetLaw_isProbabilityMeasure line 163
  13. structure OAI.BoltzmannNonuniqueness.SheetMeasures.AxialMoment line 170

    Source documentation

    The exact axial hypothesis used throughout the sheet estimates.

    structure AxialMoment (ρ : Measure ℝ) (L : ℝ) : Prop where
…
  14. theorem OAI.BoltzmannNonuniqueness.SheetMeasures.AxialMoment.nonneg line 174
  15. def OAI.BoltzmannNonuniqueness.SheetMeasures.axialTilt line 177
  16. def OAI.BoltzmannNonuniqueness.SheetMeasures.transverseTilt line 180
  17. def OAI.BoltzmannNonuniqueness.SheetMeasures.tiltedSheet line 183
  18. theorem OAI.BoltzmannNonuniqueness.SheetMeasures.axialTilt_mass line 186
  19. theorem OAI.BoltzmannNonuniqueness.SheetMeasures.axialTilt_mass_le line 192
  20. theorem OAI.BoltzmannNonuniqueness.SheetMeasures.axialTilt_finite line 197
  21. def OAI.BoltzmannNonuniqueness.SheetMeasures.normalizeFinite line 202

    Source documentation

    Normalization is defined even for the zero measure, using a harmless atom.

    def normalizeFinite (μ : Measure ℝ) (hμ : μ univ < ∞) : ProbabilityMeasure ℝ :=
…
  22. theorem OAI.BoltzmannNonuniqueness.SheetMeasures.mass_smul_normalizeFinite line 205
  23. def OAI.BoltzmannNonuniqueness.SheetMeasures.axialProbability line 218
  24. theorem OAI.BoltzmannNonuniqueness.SheetMeasures.axialTilt_eq_mass_smul line 221
  25. theorem OAI.BoltzmannNonuniqueness.SheetMeasures.smul_measure_mono line 225
  26. theorem OAI.BoltzmannNonuniqueness.SheetMeasures.axialTilt_le_probability line 231
  27. theorem OAI.BoltzmannNonuniqueness.SheetMeasures.withDensity_map_join line 236
  28. theorem OAI.BoltzmannNonuniqueness.SheetMeasures.tiltedSheet_eq line 249
  29. theorem OAI.BoltzmannNonuniqueness.SheetMeasures.transverseTilt_zero line 259
  30. theorem OAI.BoltzmannNonuniqueness.SheetMeasures.transverseTilt_gaussian line 262
  31. theorem OAI.BoltzmannNonuniqueness.SheetMeasures.transverseTilt_le line 272
  32. theorem OAI.BoltzmannNonuniqueness.SheetMeasures.tiltedSheet_le line 296
  33. theorem OAI.BoltzmannNonuniqueness.SheetMeasures.tiltedSheet_le_probability line 308
  34. theorem OAI.BoltzmannNonuniqueness.SheetMeasures.tiltedSheet_mass_le line 319
  35. def OAI.BoltzmannNonuniqueness.SheetMeasures.axialTail line 326
  36. theorem OAI.BoltzmannNonuniqueness.SheetMeasures.axialTail_mass_le line 329
  37. theorem OAI.BoltzmannNonuniqueness.SheetMeasures.axialTail_finite line 338
  38. def OAI.BoltzmannNonuniqueness.SheetMeasures.axialTailProbability line 342
  39. theorem OAI.BoltzmannNonuniqueness.SheetMeasures.axialTail_eq_mass_smul line 346
  40. theorem OAI.BoltzmannNonuniqueness.SheetMeasures.axialTail_le_probability line 351
  41. theorem OAI.BoltzmannNonuniqueness.SheetMeasures.transverseTilt_finite line 358
  42. theorem OAI.BoltzmannNonuniqueness.SheetMeasures.transverseTilt_tail_le line 365
  43. theorem OAI.BoltzmannNonuniqueness.SheetMeasures.product_tail_le line 393
  44. def OAI.BoltzmannNonuniqueness.SheetMeasures.tailCoefficient line 420

    Source documentation

    The common decay coefficient for the two probability sheets in the tail.

    def tailCoefficient (L u : ℝ) : ℝ≥0∞ :=
…
  45. theorem OAI.BoltzmannNonuniqueness.SheetMeasures.transverse_tail_coefficient_le line 423
  46. theorem OAI.BoltzmannNonuniqueness.SheetMeasures.axial_tail_coefficient line 433
  47. theorem OAI.BoltzmannNonuniqueness.SheetMeasures.tiltedSheet_tail_le line 446

    Source documentation

    The exponentially tilted norm tail is dominated by two probability sheets. The second axial law is the normalized tilted axial tail and may be an atom when the tail vanishes.

    theorem tiltedSheet_tail_le {d L u : ℝ} (hd : 0 ≤ d) (hdmax : d ≤ 1 / 8)
    {ρ : Measure ℝ} [IsProbabilityMeasure ρ] (h : AxialMoment ρ L) (hu : 0 ≤ u) :
    (tiltedSheet d ρ).restrict {p : Velocity | u < ‖p‖} ≤
      tailCoefficient L u •
        (sheetLaw (2 * d) (axialProbability ρ h) +
          sheetLaw (2 * d) (axialTailProbability ρ h (by positivity : 0 ≤ u / 2))) := by
…

    Mentions: OAI.BoltzmannNonuniqueness.SheetMeasures.AxialMoment, OAI.BoltzmannNonuniqueness.SheetMeasures.tiltedSheet, OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.SheetMeasures.tailCoefficient, OAI.BoltzmannNonuniqueness.SheetMeasures.sheetLaw, OAI.BoltzmannNonuniqueness.SheetMeasures.axialProbability, OAI.BoltzmannNonuniqueness.SheetMeasures.axialTailProbability

  48. def OAI.BoltzmannNonuniqueness.SheetGain.ballRegion line 502
  49. def OAI.BoltzmannNonuniqueness.SheetGain.weightRatio line 505
  50. def OAI.BoltzmannNonuniqueness.SheetGain.ballChartFiber line 508
  51. theorem OAI.BoltzmannNonuniqueness.SheetGain.normal_join line 514
  52. theorem OAI.BoltzmannNonuniqueness.SheetGain.slope_join line 519
  53. theorem OAI.BoltzmannNonuniqueness.SheetGain.offset_join line 527
  54. theorem OAI.BoltzmannNonuniqueness.SheetGain.W_eq_transverseWeight line 532
  55. theorem OAI.BoltzmannNonuniqueness.SheetGain.chart_weight_join line 535
  56. theorem OAI.BoltzmannNonuniqueness.SheetGain.chart_ball_join line 543
  57. theorem OAI.BoltzmannNonuniqueness.SheetGain.full_ballLineMass_eq line 553

    Source documentation

    Clipping the axial chart coordinate loses only the null endpoint -R.

    theorem full_ballLineMass_eq {R : ℝ} (hR : 0 ≤ R) (q : ℝ) (e v : Transverse)
    (A B : ℝ) :
    (∫⁻ z : ℝ, ∫⁻ s in ballLineRegion e v (A - B * z) z R,
      ENNReal.ofReal (TransverseLine.lineWeight q e (A - B * z) s)) =
        ballLineMass q e v A B R (-R) R := by
…

    Mentions: OAI.BoltzmannNonuniqueness.TransverseLine.lineWeight

  58. theorem OAI.BoltzmannNonuniqueness.SheetGain.ballChartFiber_le_slice line 572
  59. theorem OAI.BoltzmannNonuniqueness.SheetGain.weight_ball_sheet_bound line 617