Schwartz function times bounded smooth function

Proved

SchwartzSpaceWiki.mul_bounded_smooth_mem

by Lucas · Oct 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

fourier-analysisschwartz-space

Let $f\in\mathcal{S}(\mathbb{R}^n)$ and let $g:\mathbb{R}^n\to\mathbb{C}$ be a smooth function which is bounded together with its derivatives of all orders, i.e. for every multi-index $\beta$ there is $C_\beta$ with $|D^\beta g(x)|\le C_\beta$ for all $x$ (the case $\beta=0$ says $g$ is bounded). Then $fg\in\mathcal{S}(\mathbb{R}^n)$ .

Preamble

import Mathlib
import Definitions.Def_SchwartzSpaceWiki_Defs

open MeasureTheory

Formal statement

namespace SchwartzSpaceWiki

theorem mul_bounded_smooth_mem (n : ℕ) (f g : Rn n → ℂ) (hf : f ∈ schwartzSpace n)
    (hg : ContDiff ℝ (⊤ : ℕ∞) g)
    (hbdd : ∀ β : MultiIndex n, ∃ C : ℝ, ∀ x : Rn n, ‖iteratedPartialDeriv β g x‖ ≤ C) :
    f * g ∈ schwartzSpace n := by sorry

end SchwartzSpaceWiki

Source

Wikipedia, "Schwartz space", revision oldid=1360762580 (https://en.wikipedia.org/w/index.php?title=Schwartz_space&oldid=1360762580), section "Properties — Analytic properties", 2nd bullet

Human review

Endorsed by Shuze Chen · Oct 13, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph