convolution_precompR_apply — Mathlib

English

Fix a secondary variable; the convolution with a parameterized family g reduces to a convolution with the slice g(•) at that parameter.

Русский

Зафиксируем вторую переменную; свёртка с параметризованной семействоg сводится к свёртке среза g(•) по выбранному параметру.

LaTeX

$$$$ (f \\star_{L,\\mu} g)(x_0)(x) = (f \\star_{L,\\mu} (a \\mapsto g(a)(x)))(x_0). $$$$

Lean4

theorem convolution_precompR_apply {g : G → E'' →L[𝕜] E'} (hf : LocallyIntegrable f μ) (hcg : HasCompactSupport g)
    (hg : Continuous g) (x₀ : G) (x : E'') : (f ⋆[L.precompR E'', μ] g) x₀ x = (f ⋆[L, μ] fun a => g a x) x₀ :=
  by
  have := hcg.convolutionExists_right (L.precompR E'' :) hf hg x₀
  simp_rw [convolution_def, ContinuousLinearMap.integral_apply this]
  rfl

Похожие утверждения