English
The left-parameter differentiability result asserts smoothness in the parameter after suitable reductions.
Русский
Результат дифференцируемости слева по параметру обеспечивает гладкость по параметру после надлежащих редукций.
LaTeX
$$$$D_{p}(g_p⋆f)(x) = (D_p g(p, \\cdot) ⋆ f)(x).$$$$
Lean4
/-- The integral over `Ioi 0` of a forward convolution of two functions is equal to the product
of their integrals over this set. (Compare `integral_convolution` for the two-sided convolution.) -/
theorem integral_posConvolution [CompleteSpace E] [CompleteSpace E'] [CompleteSpace F] {μ ν : Measure ℝ} [SFinite μ]
[SFinite ν] [IsAddRightInvariant μ] [NoAtoms ν] {f : ℝ → E} {g : ℝ → E'} (hf : IntegrableOn f (Ioi 0) ν)
(hg : IntegrableOn g (Ioi 0) μ) (L : E →L[ℝ] E' →L[ℝ] F) :
∫ x : ℝ in Ioi 0, ∫ t : ℝ in 0..x, L (f t) (g (x - t)) ∂ν ∂μ =
L (∫ x : ℝ in Ioi 0, f x ∂ν) (∫ x : ℝ in Ioi 0, g x ∂μ) :=
by
rw [← integrable_indicator_iff measurableSet_Ioi] at hf hg
simp_rw [← integral_indicator measurableSet_Ioi]
convert integral_convolution L hf hg using 4 with x
apply posConvolution_eq_convolution_indicator
