normed_convolution_eq_right — Mathlib

English

If φ is a bump and g is constant on the ball, then φ.normed ⋆ g at x0 equals g(x0).

Русский

Если φ — нормированная бамп-функция и g константна на ball, то φ.normed ⋆ g в точке x0 равно g(x0).

LaTeX

$$$(\\phi.\\mathrm{normed}\\mu \\star g)(x_0) = g(x_0)$ under constant-on-ball condition$$

Lean4

/-- If `φ` is a normed bump function, compute `φ ⋆ g`
if `g` is constant on `Metric.ball x₀ φ.rOut`. -/
theorem normed_convolution_eq_right [IsLocallyFiniteMeasure μ] [μ.IsOpenPosMeasure] {x₀ : G}
    (hg : ∀ x ∈ ball x₀ φ.rOut, g x = g x₀) : (φ.normed μ ⋆[lsmul ℝ ℝ, μ] g : G → E') x₀ = g x₀ :=
  by
  rw [convolution_eq_right' _ φ.support_normed_eq.subset hg]
  exact integral_normed_smul φ μ (g x₀)

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