OAI/MathematicalPhysics/Boltzmann/Approximation/CutoffLipschitz.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.BoltzmannNonuniqueness.CutoffLipschitz.gain_difference line 14
2. def OAI.BoltzmannNonuniqueness.CutoffLipschitz.frequencyConstant line 30
3. theorem OAI.BoltzmannNonuniqueness.CutoffLipschitz.frequencyConstant_nonneg line 32
4. theorem OAI.BoltzmannNonuniqueness.CutoffLipschitz.integrable_dominated line 37
5. theorem OAI.BoltzmannNonuniqueness.CutoffLipschitz.frequency_nonneg line 43
6. theorem OAI.BoltzmannNonuniqueness.CutoffLipschitz.frequency_bound line 48
7. theorem OAI.BoltzmannNonuniqueness.CutoffLipschitz.frequency_difference line 62
8. theorem OAI.BoltzmannNonuniqueness.CutoffLipschitz.loss_difference line 87
9. def OAI.BoltzmannNonuniqueness.CutoffLipschitz.collision line 111
10. theorem OAI.BoltzmannNonuniqueness.CutoffLipschitz.collision_difference line 115

    Source documentation

    The local difference constant for the actual cutoff collision field.

    theorem collision_difference (hcarleman : Published.GPV2009CarlemanInput)
        {q A B D b : ℝ} (hq₁ : 1 < q) (hq₂ : q < 2) (hb : 0 ≤ b)
        (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) :
        ∀ᵐ v : Velocity, |collision b f v - collision b g v| ≤
          (D * (A + B) * (HotApplication.realBound q + frequencyConstant q b)) * H q v := by
    …

    Mentions: OAI.BoltzmannNonuniqueness.Published.GPV2009CarlemanInput, OAI.BoltzmannNonuniqueness.Velocity, OAI.BoltzmannNonuniqueness.CutoffLipschitz.collision, OAI.BoltzmannNonuniqueness.HotApplication.realBound, OAI.BoltzmannNonuniqueness.CutoffLipschitz.frequencyConstant