convolution_eq_right — Mathlib

English

If g is constant on a ball around x0, then the convolution of φ with g at x0 equals (∫ φ) · g(x0).

Русский

Если функция g константа на окружности радиуса φ.rOut вокруг x0, то конволюция φ ⋆ g в точке x0 равна (∫ φ) · g(x0).

LaTeX

$$$(\\phi \\star g)(x_0) = \\Bigl( \\int_G \\phi \\ d\\mu \\Bigr) \\cdot g(x_0)$ при условии константности g на ball x_0 φ.rOut$$

Lean4

/-- If `φ` is a bump function, compute `(φ ⋆ g) x₀`
if `g` is constant on `Metric.ball x₀ φ.rOut`. -/
theorem convolution_eq_right [HasContDiffBump G] {x₀ : G} (hg : ∀ x ∈ ball x₀ φ.rOut, g x = g x₀) :
    (φ ⋆[lsmul ℝ ℝ, μ] g : G → E') x₀ = integral μ φ • g x₀ := by
  simp_rw [convolution_eq_right' _ φ.support_eq.subset hg, lsmul_apply, integral_smul_const]

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