OAI/MathematicalPhysics/Boltzmann/Branching/GainSmoothingError.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.BoltzmannNonuniqueness.GainLipschitz.integrand_difference line 19
2. theorem OAI.BoltzmannNonuniqueness.GainLipschitz.gain_difference line 49
3. theorem OAI.BoltzmannNonuniqueness.GainUpperDifference.integrand_bound line 97
4. theorem OAI.BoltzmannNonuniqueness.GainUpperDifference.cutoff_integrand_bound line 122
5. theorem OAI.BoltzmannNonuniqueness.GainUpperDifference.cutoff_gain_bound line 136

   Source documentation

   Only the positive difference of the two densities enters the upper gain difference.

   theorem cutoff_gain_bound (hcarleman : Published.GPV2009CarlemanInput)
       {q A B D : ℝ} (hq₁ : 1 < q) (hq₂ : q < 2) (hA : 0 ≤ A) (hB : 0 ≤ B) (hD : 0 ≤ D)
       {f g : Velocity → ℝ} (hfm : Measurable f) (hgm : Measurable g)
       (hf : ∀ w, 0 ≤ f w) (hg : ∀ w, 0 ≤ g w)
       (hfB : ∀ w, f w ≤ A * H q w) (hgB : ∀ w, g w ≤ B * H q w)
       (hfg : ∀ w, f w - g w ≤ D * H q w) (b : ℝ) :
       ∀ᵐ v : Velocity,
         CollisionCutoff.gain b f v - CollisionCutoff.gain b g v ≤
           (D * (A + B) * HotApplication.realBound q) * H q v := by
   …

   Mentions: OAI.BoltzmannNonuniqueness.Published.GPV2009CarlemanInput, OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.CollisionCutoff.gain, OAI.BoltzmannNonuniqueness.HotApplication.realBound

6. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.velocitySmooth_eq_outgoing_convolution line 179
7. theorem OAI.BoltzmannNonuniqueness.CollisionCompactness.DoubleGain.localizedGain_uniform_smoothing line 186