ae_eq_zero_of_integral_contDiff_smul_eq_zero

English

If f is locally integrable, g is C^n and depends smoothly on a parameter, then the convolution f ⋆ g is C^n in the parameter and spatial variable.

Русский

Если f локально интегрируемо, g — C^n и гладко зависит от параметра, то свёртка f ⋆ g является C^n по параметру и по пространственной переменной.

LaTeX

$$$$\\text{contDiffOn}_{𝕜} n (p, x) \\mapsto (f⋆[L, μ] g_p)(x) \\in C^n.$$$$

Lean4

/-- If a locally integrable function `f` on a finite-dimensional real vector space has zero integral
when multiplied by any smooth compactly supported function, then `f` vanishes almost everywhere. -/
theorem ae_eq_zero_of_integral_contDiff_smul_eq_zero (hf : LocallyIntegrable f μ)
    (h : ∀ (g : E → ℝ), ContDiff ℝ ∞ g → HasCompactSupport g → ∫ x, g x • f x ∂μ = 0) : ∀ᵐ x ∂μ, f x = 0 :=
  ae_eq_zero_of_integral_smooth_smul_eq_zero 𝓘(ℝ, E) hf (fun g g_diff g_supp ↦ h g g_diff.contDiff g_supp)

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