OAI/MathematicalPhysics/Boltzmann/Branching/IntegralSurvival.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A lower bound for an integrable source with bounded loss

  1. theorem OAI.BoltzmannNonuniqueness.IntegralSurvival.lower_bound line 14

    Source documentation

    The integrating factor gives survival even when the source inequality holds only a.e.

    theorem lower_bound {z : ℝ → ℝ} {a C T : ℝ} (hT : 0 ≤ T)
    (hi : IntervalIntegrable z volume 0 T)
    (hb : ∀ᵐ t, t ∈ Icc 0 T → -C * (a + ColdGronwall.primitive z t) ≤ z t) :
    ∀ t ∈ Icc 0 T, Real.exp (-C*t)*a ≤ a + ColdGronwall.primitive z t := by
…

    Mentions: OAI.BoltzmannNonuniqueness.ColdGronwall.primitive