VolterraFubini.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Triangular Fubini identity for measurable characteristic sources

This elementary identity allows integration by parts against an integral primitive without assuming the collision source is continuous in time.

theorem OAI.BoltzmannNonuniqueness.TransportPrimitive.integral_mul_primitive line 18

theorem OAI.BoltzmannNonuniqueness.TransportPrimitive.integral_deriv_mul_primitive line 67

Source documentation

Integration by parts with an integrable, possibly discontinuous source.

theorem integral_deriv_mul_primitive {a b : ℝ} (hab : a ≤ b) {h h' g : ℝ → ℝ}
    (hd : ∀ t ∈ Icc a b, HasDerivAt h (h' t) t)
    (hh' : IntervalIntegrable h' volume a b) (hg : IntervalIntegrable g volume a b)
    (hhg : IntervalIntegrable (fun t => h t*g t) volume a b) :
    (∫ s in a..b, h' s * (∫ t in a..s, g t)) =
      h b * (∫ t in a..b, g t) - ∫ t in a..b, h t*g t := by
…