Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedverified 2026-09-23 (gpt-6-sol)
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.

Complex translation, convolution, approximate identities, and mollification

Statement

Assume countable choice, let n≥1, and use Lebesgue measure on Rn. Translation τhf(x)=f(x−h) is an isometry of complex Lp for 1≤p≤∞ and depends norm-continuously on h for p<∞.

For complex K∈L1 and f∈Lp, the convolution (K∗f)(x)=∫K(y)f(x−y) dy exists absolutely a.e., defines a measurable class independent of representatives, and satisfies ∥K∗f∥p≤∥K∥1∥f∥p.

If Kε∈L1(Rn;C) satisfy ∫Kε=1,M:=sup⁡ε>0∥Kε∥1<∞,∫∣y∣≥δ∣Kε(y)∣ dy⟶0(δ>0), then Kε∗f→f in Lp for p<∞, and uniformly for f∈C0(Rn;C). For fixed K∈L1, K∗f∈C0 when f∈C0. These assertions allow complex and sign-changing kernels. In particular Kε(x)=ε−nK(x/ε) is such an approximate identity whenever K∈L1 and ∫K=1.

If ρ∈Cc∞(Rn;R) has mass one, ρε(x)=ε−nρ(x/ε), and f is complex locally integrable, then ρε∗f is smooth and ∂α(ρε∗f)=(∂αρε)∗f. A compactly supported input gives a compactly supported output. No general L∞ translation-continuity or approximate-identity convergence is asserted.

Facts & Assumptions

Given: Countable choice, Euclidean dimension n≥1, and the kernels and inputs in the statement; limits of kernels are as ε↓0.

[F1]

Measurability, local integrability and smoothness have their componentwise meanings (Complex Lp classes and Euclidean test-function conventions).

[F2]

Complex norms have component bounds, Hölder and the triangle inequality (Complex Holder, Minkowski, and the quotient norm).

[F3]

Under countable choice real translations are norm-continuous for finite p (∥τhf−f∥p→0 in Lp(Rn) as h→0, for 1≤p<∞).

[F5]

On sigma-finite spaces and for finite p, the norm of a nonnegative integral envelope is bounded by the integral of the section norms (Minkowski's integral inequality).

[F21]

On sigma-finite product spaces, Tonelli makes the integral of a jointly measurable nonnegative function over one variable measurable in the other (Tonelli's theorem for nonnegative measurable functions on a sigma-finite product).

[F6]

Under countable choice a completion-measurable real function has a base-measurable a.e.-equal representative (A function measurable for a completion is almost everywhere equal to one measurable for the original sigma-algebra).

[F7]

Borel representatives give jointly Borel convolution integrands (Borel representatives make the convolution integrand Borel measurable).

[F8]
[F9]

Under countable choice dilation by c scales measure by the factor |c|^n; reflection preserves measure (For a nonzero real c, dilation by c multiplies Lebesgue outer measure by ∣c∣n, and reflection in the origin preserves it).

[F11]

An integrable majorant permits passing a.e. limits through integrals (Dominated convergence).

[F12]

A real smooth compactly supported mollifier differentiates by differentiating the kernel on locally integrable inputs (Convolution with a mollifier is smooth, and derivatives pass under the integral sign).

[F13]

For Borel L1 inputs, the convolution support lies in the closure of their support sum (The support of a convolution lies in the closure of the support sumset).

[F14]

Countable choice selects one element from each member of a natural-number-indexed family of nonempty sets (The Axiom of Countable Choice (ACω)).

[F15]

Complex integrals are linear (The Lebesgue integral is linear on L1(μ)).

[F16]

The modulus of a complex integral is bounded by the integral of the modulus (The modulus of an integral is bounded by the integral of the modulus).

[F18]

Continuous functions on compact metric spaces are uniformly continuous (Heine-Cantor: a continuous map from a compact metric space to any metric space is uniformly continuous).

[F19]

Proof

technique · Use real norm and measurability suppliers, then estimate the complex error by an absolute integral envelope
1.1F1F2F3F8

Write f=u+iv. Translation invariance F8 gives ∫∣f(x−h)∣p dx=∫∣f(x)∣p dx for finite p: first substitute translated level sets for a nonnegative simple function, then take the supremum defining its nonnegative integral. For infinity the sets {∣f(⋅−h)∣>a} have the same measure as {∣f∣>a}, so the essential bounds coincide. Null disagreement sets also translate to null sets, so translations act on classes. For finite p, F3 and F2 give ∥τhf−f∥p≤∥τhu−u∥p+∥τhv−v∥p→0. The isometry gives continuity at every h0 from ∥τhf−τh0f∥p=∥τh−h0f−f∥p.

1.2F1F11F16F17F18F19

A complex f∈C0 is bounded: its components are bounded on a sufficiently large closed ball by F17 and F19 and are small outside by definition. It is uniformly continuous: for a given η>0, take R with ∣f(x)∣<η/2 for ∣x∣>R and use F18 on the closed ball of radius R+2 to choose 0<δ<1 making differences below η there. If ∣x−z∣<δ, either both points are in that ball or both have radius greater than R, in which case their values differ by less than η. This proves uniform continuity. Hence K∗f exists everywhere and ∣(K∗f)(x+z)−(K∗f)(x)∣≤∥K∥1sup⁡w∣f(w+z)−f(w)∣→0. As ∣x∣→∞, f(x−y)→0 for fixed y, dominated by the integrable function ∥f∥∞∣K(y)∣; F11 gives (K∗f)(x)→0. Thus K∗f∈C0.

1.3F9F11given

For a fixed K∈L1 of integral one, substitution y=x/ε using F9 gives ∫Kε=∫K=1, ∥Kε∥1=∥K∥1, and ∫∣x∣≥δ∣Kε(x)∣ dx=∫∣y∣≥δ/ε∣K(y)∣ dy→0 by F11, dominated by ∣K∣. Thus scaled integrable mass-one kernels satisfy all three conditions, whether or not they are nonnegative.

1.4F1F8F9F11F12F15F17F19

For locally integrable f=u+iv, F1 gives locally integrable real components. Apply F12 to each with the real kernel ρε. By F15 their recombination gives all ordered partial derivatives, equal to the integrals with the corresponding kernel derivatives. To check their continuity explicitly, fix x0 and a closed unit ball of x-values about it. The y-supports of ∂αρε(x−y) for those x-values lie in a fixed closed bounded ball Q, compact by F17. The derivative of the kernel is globally bounded, say by Cα, by F19 on a ball containing its compact support. Thus the integrands are dominated by Cα∣f∣1Q, integrable by local integrability. As x→x0 their pointwise limits are the integrands at x0, so F11 gives continuity of every derivative integral. The change of variables between the two convolution orders follows from F8–F9. Hence the convolution is smooth with the stated formula.

2.1F2F5F6F7F14F16F20F21step 1.1given

Under the given countable-choice hypothesis F14, F6 applied to each component supplies Borel representatives of K,f; any infinite component values in the base representative occur on a Borel null set and can be set to zero there. F7 makes (x,y)↦K(y)f(x−y) jointly Borel. Both Euclidean factors are sigma-finite, covered by the finite-measure boxes of F20. For p<∞, apply F5 to F(x,y)=K(y)f(x−y): step 1.1 gives ∥F(⋅,y)∥p=∣K(y)∣∥f∥p, so the envelope A(x)=∫∣F(x,y)∣ dy belongs to Lp and ∥A∥p≤∥K∥1∥f∥p. For p=∞, modify the Borel representative of f on the Borel null set where ∣f∣>∥f∥∞, setting it to zero. Then A(x)≤∥f∥∞∥K∥1 for every x. By F21, A and the positive and negative parts of the real and imaginary integrands have measurable section integrals. Where A(x)<∞, their finite differences define a measurable complex integral with modulus at most A(x) by F16; set it to zero on the measurable exceptional set. These bounds prove absolute a.e. existence, measurability and the sharp Lp norm estimate independently of real Young.

2.2F15F16step 1.2given

For f∈C0, put ωf(δ)=sup⁡∣y∣<δ,x∣f(x−y)−f(x)∣. Step 1.2 gives ωf(δ)→0. Taking pointwise absolute values in the normalized error integral and then the supremum gives ∥Kε∗f−f∥sup≤Mωf(δ)+2∥f∥sup∫∣y∣≥δ∣Kε(y)∣ dy. First send ε↓0, then δ↓0. This proves the uniform assertion by a direct supremum estimate.

3.1F8F9F10step 2.1

For any other measurable representatives let NK,Nf be their measurable null disagreement sets. For each fixed x, the integrands coincide outside NK∪(x−Nf), a measurable null set by F8–F9. The same is true of their absolute values, so absolute integrability holds for either pair exactly when it holds for the other. At those points F10 gives equal integrals. Thus the measurable class in step 2.1 is representative-independent throughout L1 times Lp, without restricting both inputs to L1.

3.2F2F5F7F15F16F20step 1.1step 2.1

For finite p, normalization and F15 give Kε∗f−f=∫Kε(y)(f(⋅−y)−f(⋅)) dy a.e. Its absolute value is bounded by the envelope with integrand ∣Kε(y)∣∣f(x−y)−f(x)∣ by F16. This integrand is measurable by F7 applied to Borel representatives and ordinary products. Its section norm is ∣Kε(y)∣∥τyf−f∥p, measurable by step 1.1 and bounded by 2∥f∥p∣Kε(y)∣, which is integrable. Euclidean Lebesgue measure is sigma-finite, since [−j,j]n for positive integers j cover it and have finite measure (2j)n by F20. Therefore F5 applies and gives ∥Kε∗f−f∥p≤∫∣Kε(y)∣∥τyf−f∥p dy.

4.1step 1.1step 3.2given

For any η>0, step 1.1 gives δ>0 with ∥τyf−f∥p<η whenever ∣y∣<δ. Splitting the last integral yields ∥Kε∗f−f∥p≤Mη+2∥f∥p∫∣y∣≥δ∣Kε(y)∣ dy. The tail tends to zero, so the limit superior is at most Mη. Let η↓0 to obtain convergence. No separate normalization of the real and imaginary kernel parts has been used.

5.1F13F17step 3.1step 1.4∎

If the locally integrable input has compact support S, then ∫∣f∣=∫S∣f∣<∞. A Borel representative can be made zero outside the closed set S while preserving its class by step 3.1. F13 gives output support inside S+supp⁡ρε‾. Both input supports are bounded, so this closed sum closure is bounded and hence compact by F17. The smooth output has closed support inside it, therefore compact support. Zero input or zero convolution yields the empty support; neither requires a nonempty support choice. All estimates above apply at p=1; the only general infinity assertion is the isometry and Young bound, with uniform approximation restricted to C0.

Depends on

Used by

Dependency tree · two levels

141 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