English
If μ is invariant under right translations, then the convolution respects right invariance and convolution_mono_right results hold under right invariance assumptions.
Русский
Если μ сохраняется при правых трансляциях, свёртка сохраняет это свойство и выводы типа convolution_mono_right остаются верными.
LaTeX
$$$\\mathrm{convolution\\_mono\\_right}$ и аналогичные теоремы применимы при правой инвариантности.$$
Lean4
theorem convolution_mono_right_of_nonneg {f g g' : G → ℝ} (hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ)
(hf : ∀ x, 0 ≤ f x) (hg : ∀ x, g x ≤ g' x) (hg' : ∀ x, 0 ≤ g' x) :
(f ⋆[lsmul ℝ ℝ, μ] g) x ≤ (f ⋆[lsmul ℝ ℝ, μ] g') x :=
by
by_cases H : ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ
· exact convolution_mono_right H hfg' hf hg
have : (f ⋆[lsmul ℝ ℝ, μ] g) x = 0 := integral_undef H
rw [this]
exact integral_nonneg fun y => mul_nonneg (hf y) (hg' (x - y))
