English
If the base field is Real and the function values lie in Real, the convolution formula specializes with real multiplication and the integral is taken in Real.
Русский
В частном случае базовое поле Real, значения функций Real, свёртка определяется через умножение и интеграл в Real.
LaTeX
$$$\\mathrm{convolution}\\_{Real}(f,g,L,μ)(x)=\\int t\\, f(t)g(x-t)\\, dμ(t)$$$
Lean4
theorem convolution_mono_right {f g g' : G → ℝ} (hfg : ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ)
(hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ) (hf : ∀ x, 0 ≤ f x) (hg : ∀ x, g x ≤ g' x) :
(f ⋆[lsmul ℝ ℝ, μ] g) x ≤ (f ⋆[lsmul ℝ ℝ, μ] g') x :=
by
apply integral_mono hfg hfg'
simp only [lsmul_apply, Algebra.id.smul_eq_mul]
intro t
apply mul_le_mul_of_nonneg_left (hg _) (hf _)
