OAI/MathematicalPhysics/Boltzmann/Branching/HotQuadraticGain.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

Normalized truncated transverse weights

The positive disk mixture transfers the existing disk kernel expectation bound to the truncated singular density needed by the quadratic hot gain.

  1. def OAI.BoltzmannNonuniqueness.HotDiskEstimate.radiusMass line 29
  2. def OAI.BoltzmannNonuniqueness.HotDiskEstimate.cutoffMass line 31
  3. def OAI.BoltzmannNonuniqueness.HotDiskEstimate.cutoffLaw line 33
  4. theorem OAI.BoltzmannNonuniqueness.HotDiskEstimate.radiusMass_nonneg line 36
  5. theorem OAI.BoltzmannNonuniqueness.HotDiskEstimate.cutoffMass_pos line 41
  6. theorem OAI.BoltzmannNonuniqueness.HotDiskEstimate.mixing_mass line 48
  7. theorem OAI.BoltzmannNonuniqueness.HotDiskEstimate.cutoffLaw_mass line 57
  8. theorem OAI.BoltzmannNonuniqueness.HotDiskEstimate.cutoff_kernel_bound line 73
  9. def OAI.BoltzmannNonuniqueness.HotDiskEstimate.normalizedCutoff line 107
  10. theorem OAI.BoltzmannNonuniqueness.HotDiskEstimate.normalizedCutoff_isProbabilityMeasure line 110
  11. theorem OAI.BoltzmannNonuniqueness.HotDiskEstimate.normalizedCutoff_absolutelyContinuous line 120
  12. theorem OAI.BoltzmannNonuniqueness.HotDiskEstimate.normalizedCutoff_kernel_bound line 127
  13. theorem OAI.BoltzmannNonuniqueness.HotDiskEstimate.normalizedCutoff_geometric_bound line 139

    Source documentation

    The geometric slice estimate applies uniformly to the normalized hot measure.

    theorem normalizedCutoff_geometric_bound {q D R : ℝ}
    (hq₁ : 1 < q) (hq₂ : q < 2) (hD : 0 < D) (hR : 1 ≤ R)
    {v : Transverse} (hv : v ≠ 0) (t : ℝ) (ρ : Measure ℝ) [IsProbabilityMeasure ρ] :
    (∫⁻ p, normalizedBallSlice q v t p.1 p.2 R (-R) R
      ∂(normalizedCutoff q D).prod ρ) ≤ ENNReal.ofReal (geometricTotalConstant q * R ^ 2) :=
…

    Mentions: OAI.BoltzmannNonuniqueness.HotDiskEstimate.normalizedCutoff

  14. def OAI.BoltzmannNonuniqueness.HotChartBalls.intervalLaw line 177
  15. theorem OAI.BoltzmannNonuniqueness.HotChartBalls.intervalLaw_mass line 179
  16. def OAI.BoltzmannNonuniqueness.HotChartBalls.normalizedInterval line 185
  17. theorem OAI.BoltzmannNonuniqueness.HotChartBalls.normalizedInterval_isProbabilityMeasure line 188
  18. def OAI.BoltzmannNonuniqueness.HotChartBalls.rectangleLaw line 194
  19. def OAI.BoltzmannNonuniqueness.HotChartBalls.normalizedRectangle line 197
  20. theorem OAI.BoltzmannNonuniqueness.HotChartBalls.rectangle_eq_smul line 200
  21. theorem OAI.BoltzmannNonuniqueness.HotChartBalls.weight_ball_normalizedRectangle_bound line 217
  22. theorem OAI.BoltzmannNonuniqueness.HotChartBalls.weight_ball_rectangle_bound line 231
  23. def OAI.BoltzmannNonuniqueness.HotChartBalls.massConstant line 243
  24. theorem OAI.BoltzmannNonuniqueness.HotChartBalls.massConstant_pos line 245
  25. theorem OAI.BoltzmannNonuniqueness.HotChartBalls.cutoffMass_le line 248
  26. def OAI.BoltzmannNonuniqueness.HotRectangleDensity.rectangle line 289
  27. def OAI.BoltzmannNonuniqueness.HotRectangleDensity.weight line 292
  28. theorem OAI.BoltzmannNonuniqueness.HotRectangleDensity.measurableSet_rectangle line 295
  29. theorem OAI.BoltzmannNonuniqueness.HotRectangleDensity.measurable_weight line 299
  30. theorem OAI.BoltzmannNonuniqueness.HotRectangleDensity.join_measurePreserving line 302
  31. theorem OAI.BoltzmannNonuniqueness.HotRectangleDensity.join_withDensity line 311
  32. theorem OAI.BoltzmannNonuniqueness.HotRectangleDensity.rectangleLaw_eq_density line 323
  33. theorem OAI.BoltzmannNonuniqueness.HotRectangleDensity.norm_ball_subset_rectangle line 346
  34. def OAI.BoltzmannNonuniqueness.HotMixedGain.mixedMeasure line 379
  35. theorem OAI.BoltzmannNonuniqueness.HotMixedGain.pointwise_bound line 383
  36. theorem OAI.BoltzmannNonuniqueness.HotMixedGain.restricted_bound line 409
  37. def OAI.BoltzmannNonuniqueness.HotMixedGain.core line 437
  38. theorem OAI.BoltzmannNonuniqueness.HotMixedGain.core_bound line 439
  39. theorem OAI.BoltzmannNonuniqueness.HotMixedGain.shell_bound line 457
  40. def OAI.BoltzmannNonuniqueness.HotTotal.shellConstant line 495
  41. theorem OAI.BoltzmannNonuniqueness.HotTotal.geometricTotalConstant_pos line 498
  42. theorem OAI.BoltzmannNonuniqueness.HotTotal.shellConstant_pos line 503
  43. theorem OAI.BoltzmannNonuniqueness.HotTotal.shell_real_bound line 511
  44. theorem OAI.BoltzmannNonuniqueness.HotTotal.mixed_shell_bound line 537
  45. def OAI.BoltzmannNonuniqueness.HotTotal.baseBound line 555
  46. def OAI.BoltzmannNonuniqueness.HotTotal.bound line 559
  47. theorem OAI.BoltzmannNonuniqueness.HotTotal.bound_lt_top line 562
  48. theorem OAI.BoltzmannNonuniqueness.HotTotal.cover line 572
  49. theorem OAI.BoltzmannNonuniqueness.HotTotal.mixed_total_bound line 586
  50. theorem OAI.BoltzmannNonuniqueness.HotApplication.gain_G_eq line 631
  51. theorem OAI.BoltzmannNonuniqueness.HotApplication.quadratic_gain_bound line 643
  52. def OAI.BoltzmannNonuniqueness.HotApplication.realBound line 669
  53. theorem OAI.BoltzmannNonuniqueness.HotApplication.realBound_pos line 672
  54. theorem OAI.BoltzmannNonuniqueness.HotApplication.quadratic_gain_le_constant line 677

    Source documentation

    Manuscript Lemma lem:hot-bound, for the fixed weight exponent m = 100.

    theorem quadratic_gain_le_constant (hcarleman : Published.GPV2009CarlemanInput)
    {q : ℝ} (hq₁ : 1 < q) (hq₂ : q < 2) :
    ∀ᵐ v : Velocity ∂volume,
      nonnegativeGain (fun ξ => ENNReal.ofReal (H q ξ))
        (fun ξ => ENNReal.ofReal (H q ξ)) v ≤ ENNReal.ofReal (realBound q * H q v) := by
…

    Mentions: OAI.BoltzmannNonuniqueness.Published.GPV2009CarlemanInput, OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.nonnegativeGain, OAI.BoltzmannNonuniqueness.HotApplication.realBound

  55. theorem OAI.BoltzmannNonuniqueness.HotRealGain.quadratic_gain line 713
  56. theorem OAI.BoltzmannNonuniqueness.HotRealGain.dominated_gain line 723