TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-01

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The support of a convolution lies in the closure of the support sumset

Statement

Let $f, g \in L^{1} (R^{n})$ be represented by Borel functions still denoted $f, g$ . For any complex-valued function $u$ on $R^{n}$ , use the support convention

$supp (u) : = \overline{{x \in R^{n} : u (x) \neq 0}},$

which extends the real-valued definition of The support of a function on $R^{n}$ and its compactly supported Riemann integral. Define $h (x) : = {\begin{cases} \int_{R^{n}} f (x - y) g (y) d y, & if the integral exists, \\ 0, & otherwise . \end{cases}$ Then

$supp (h) \subseteq \overline{supp (f) + supp (g)} .$

Facts & Assumptions

Given: Borel representatives $f, g \in L^{1} (R^{n})$ and the function $h$ defined above.

[L1]

$L^{1}$ convolution exists almost everywhere (If $f, g \in L^{1} (R^{n})$ , then $f * g$ exists almost everywhere, belongs to $L^{1}$ , and $∥ f * g ∥_{1} \leq ∥ f ∥_{1} ∥ g ∥_{1}$ , Convolution of two functions on $R^{n}$ ).

[L2]

Support is defined by the closure of the nonzero set (The support of a function on $R^{n}$ and its compactly supported Riemann integral).

Proof

technique · direct

1.1

Let [L1, L2, given, choose] $x \notin \overline{supp (f) + supp (g)}$ . Choose an open neighborhood $U$ of $x$ disjoint from that closure. For $z \in U$ and $y \in supp (g)$ , one has $z - y \notin supp (f)$ , so $f (z - y) = 0$ ; and if $y \notin supp (g)$ then $g (y) = 0$ . Hence $f (z - y) g (y) = 0$ for every $y$ and every $z \in U$ .

L1L2givenchoose

2.1

Therefore $h (z) = 0$ for every $z \in U$ : by step 1.1 the integrand [L1, L2, step 1.1] vanishes for every $y$ , so the convolution integral exists and equals $0$ at each such $z$ . So $x$ lies outside the support of $h$ in the sense of [L2].

L1L2step 1.1

3.1

Since every point outside [step 2.1] $\overline{supp (f) + supp (g)}$ lies outside $supp (h)$ , the support inclusion follows.

step 2.1∎

Depends on

Used by

Dependency tree · two levels

14 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Walter Rudin, Real and Complex Analysis, 3rd ed. (standard reference, not scraped)