English
The left-parametric convolution with parameter also enjoys C^n regularity when transferred to a common universe via ULift, mirroring the right-parameter case.
Русский
Левая параметрическая свёртка с параметром также имеет гладкость C^n при приведении к общей вселенной через ULift, аналогично правому случаю.
LaTeX
$$$$\\text{contDiffOn}_{𝕜} n (p, x) \\mapsto (g_p⋆[L, μ] f)(x) \\in C^n.$$$$
Lean4
/-- If two locally integrable functions on a finite-dimensional real vector space have the same
integral when multiplied by any smooth compactly supported function, then they coincide almost
everywhere. -/
theorem ae_eq_of_integral_contDiff_smul_eq (hf : LocallyIntegrable f μ) (hf' : LocallyIntegrable f' μ)
(h : ∀ (g : E → ℝ), ContDiff ℝ ∞ g → HasCompactSupport g → ∫ x, g x • f x ∂μ = ∫ x, g x • f' x ∂μ) :
∀ᵐ x ∂μ, f x = f' x :=
ae_eq_of_integral_smooth_smul_eq 𝓘(ℝ, E) hf hf' (fun g g_diff g_supp ↦ h g g_diff.contDiff g_supp)
