VariableSurvival.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Positive characteristic forcing with an integrable loss frequency

theorem OAI.BoltzmannNonuniqueness.TransportPrimitive.exp_absolutelyContinuous line 10

theorem OAI.BoltzmannNonuniqueness.TransportPrimitive.variable_survival_with_source line 22

Source documentation

The integrating factor keeps the positive forcing when the frequency is only integrable.

theorem variable_survival_with_source {T : ℝ} (hT : 0 ≤ T)
    {u r k g : ℝ → ℝ} (hu : AbsolutelyContinuousOnInterval u 0 T)
    (hk : IntervalIntegrable k volume 0 T) (hg : IntervalIntegrable g volume 0 T)
    (hr : ∀ᵐ t, t ∈ Icc 0 T → HasDerivAt u (r t) t)
    (hb : ∀ᵐ t, t ∈ Icc 0 T → g t-k t*u t ≤ r t) :
    Real.exp (-(∫ t in 0..T, k t))*u 0 +
      (∫ t in 0..T, Real.exp (-((∫ s in 0..T, k s)-(∫ s in 0..t, k s)))*g t) ≤ u T := by
…