Products of primitives of integrable functions

If two functions are primitives of integrable functions on [0, T], their product is the primitive of the product-rule expression. This is the one-dimensional calculus used to differentiate the mollified cross pairing in lem:pv-serrin-uniqueness.

theorem ESS.serrin_primitive_product {T : ℝ} {F G f g : ℝ → ℝ} (hf : MeasureTheory.IntegrableOn f (Set.Ioo 0 T) MeasureTheory.volume) (hg : MeasureTheory.IntegrableOn g (Set.Ioo 0 T) MeasureTheory.volume) (hF : ∀ t ∈ Set.Icc 0 T, F t = F 0 + ∫ (τ : ℝ) in 0..t, f τ) (hG : ∀ t ∈ Set.Icc 0 T, G t = G 0 + ∫ (τ : ℝ) in 0..t, g τ) {t : ℝ} (ht : t ∈ Set.Icc 0 T) : F t * G t = F 0 * G 0 + ∫ (τ : ℝ) in 0..t, f τ * G τ + F τ * g τ

The product of two primitives of integrable functions on (0, T) is the primitive of f G + F g, from the value at time zero.