Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-12
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 L1 transform is bounded and uniformly continuous

Statement

The map F:L1(Rn;C)→BUC(Rn;C) is complex-linear and sup⁡ξ∣f^(ξ)∣≤∥f∥1. Here n≥1 and BUC means bounded uniformly continuous functions.

Facts & Assumptions

Given: f,g∈L1, complex scalars a,b, and real frequency vectors ξ,h.

[F1]

The integral transform exists at every frequency, is representative independent, and satisfies the pointwise norm bound (The integral transform is representative independent).

[F2]

Dominated convergence applies to complex integrands dominated by one integrable function (Dominated convergence).

[F4]

Integration is complex-linear on L1 (The Lebesgue integral is linear on L1(μ)).

[F6]

The real mean value theorem bounds an increment by a bound for the derivative times the interval length (The mean value theorem, as the case g(x)=x of Cauchy's: for f continuous on [a,b] with a<b and differentiable on (a,b) there is c∈(a,b) with f(b)−f(a)=f′(c)(b−a)), and (sin⁡u)′=cos⁡u, (cos⁡u)′=−sin⁡u (The derivatives of sine and cosine are cosine and minus sine).

Proof

1.1F1F4givenconstruct

Reconstruct first the integral interface used here. Augment any finite disjoint display of a nonnegative simple function by the complement with coefficient 0. Intersections of two augmented displays partition the whole space and have equal coefficients on nonempty cells, so finite additivity and 0⋅(+∞)=0 prove representation independence. Common refinements give simple addition and monotonicity; scalar zero is direct and positive scalars are termwise. Supremum over simple minorants and the sets {uj≥cs}, 0<c<1, give monotone convergence; increasing simple approximations give nonnegative additivity, and positive/negative plus real/imaginary decompositions give finite complex L1 linearity. Thus the integrable functions f(x)e−2πix⋅ξ and g(x)e−2πix⋅ξ have linear combination (af+bg)(x)e−2πix⋅ξ, and integrating gives af+bg^=af^+bg^. The pointwise estimate in F1, with a right side independent of frequency, gives boundedness and the asserted supremum bound.

2.1F1F2F3F4F5F6F7F8step 1.1∎

The preceding MCT also gives Fatou by applying it to inf⁡j≥mvj↑lim inf⁡jvj. If uj→u almost everywhere and ∣uj∣≤g∈L1, Fatou applied to 2g−∣uj−u∣≥0 gives lim sup⁡j∫∣uj−u∣≤0; hence L1 convergence, and the local finite linearity gives convergence of integrals. This proves the exact dominated-convergence clause used below without [F2]'s affected foundation. Factoring the exponentials yields f^(ξ+h)−f^(ξ)=F(f(e−2πix⋅h−1))(ξ). F1 therefore gives the bound ∣f^(ξ+h)−f^(ξ)∣≤I(h), where I(h)=∫∣f(x)∣∣e−2πix⋅h−1∣ dx. For real u, F5--F6 and F8 give ∣sin⁡u∣≤∣u∣, ∣cos⁡u−1∣≤∣u∣, and hence ∣eiu−1∣≤2∣u∣; F5 also bounds this modulus by two. Applying the locally proved dominated convergence to the explicit integer-ball tails, dominated by ∣f∣, choose an integer R≥1 with ∫∣x∣>R∣f∣<ϵ/4. On ∣x∣≤R, F7 gives ∣2πx⋅h∣≤2πR∣h∣, so the single choice δ=ϵ/(8πR(1+∥f∥1)) makes ∣e−2πix⋅h−1∣<ϵ/(2(1+∥f∥1)) whenever ∣h∣<δ. The inside integral is below ϵ/2 and the outside integral below ϵ/2, so I(h)<ϵ. Consequently, for every ϵ>0 there is δ>0 such that ∣h∣<δ implies the difference is below ϵ for every ξ. This is uniform continuity.

Depends on

Dependency tree · 2 levels

Sources