normed_def — Mathlib

English

The normed bump is a smooth function whose L^1-normalization is 1, and it preserves smoothness under differentiation.

Русский

Нормированное bump-распределение — гладкая функция с нормировкой L^1 равной 1, сохраняющая гладкость при дифференцировании.

LaTeX

$$ContDiffBump.normed μ ∈ …$$

Lean4

theorem normed_def {μ : Measure E} (x : E) : f.normed μ x = f x / ∫ x, f x ∂μ :=
  rfl

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