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.

Schwartz space is Fréchet

Statement

The Schwartz topology is locally convex, metrizable and complete. Set qj=max⁡∣α∣,∣β∣≤jpαβ. A complete translation-invariant metric defining it is d(f,g)=∑j=0∞2−j−1min⁡(1,qj(f−g)). No choice axiom is required.

Facts & Assumptions

Given: The seminorm topology of Schwartz topology and convergence, already verified to be Hausdorff and locally convex.

[F1]

The uniform Cauchy criterion gives uniform limits of real functions (A sequence of real-valued functions converges uniformly if and only if it is uniformly Cauchy).

[F2]

Uniform limits of continuous real functions are continuous (The uniform limit of continuous real-valued functions on a metric space is continuous).

[F4]

Continuous higher mixed partials commute (Continuous mixed partials of order k are invariant under permutations), applied separately to real and imaginary parts.

Proof

technique · direct
1.1givenalgebra

The series converges since its terms are bounded by 2−j−1. Symmetry and translation invariance follow termwise; min⁡(1,a+b)≤min⁡(1,a)+min⁡(1,b) proves the triangle inequality. Vanishing distance forces q0(f−g)=0, hence f=g. To make d(f,0)<ε, choose J with ∑j>J2−j−1<ε/2 and require qJ(f)<ε/2. Conversely, to ensure qJ(f)<η, put η′=min⁡(η/2,1/2) and require d(f,0)<2−J−1η′. Then min⁡(1,qJ(f))<η′<1, as required. Every finite seminorm neighbourhood contains such a qJ ball and each qJ ball is a finite seminorm neighbourhood, proving equality of topologies.

2.1step 1.1F1F2F3F4

Let (fk) be d-Cauchy. The converse estimate in step 1.1 makes it Cauchy in every qJ. Each ∂βfk therefore has a unique uniform complex limit gβ, by applying [F1] to its real and imaginary parts, and this limit is continuous by [F2]. On any fixed coordinate segment x+tej, a≤t≤b with a<b, [F4] gives derivative ∂β+ejfk. Apply [F3] componentwise to these restricted functions: their values converge at a and their derivatives converge uniformly. Consequently ∂jgβ=gβ+ej along every segment. Induction on the length of an ordered derivative now gives f=g0∈C∞ and ∂βf=gβ. Limits are unique specified values, so forming this family requires no choice.

3.1step 2.1step 1.1given∎

Fix α,β and ε>0. The seminorm Cauchy property gives N with ∣xα∂β(fk−fl)(x)∣<ε/2 for every x and k,l≥N. For fixed x,k, let l→∞ using step 2.1. Then pαβ(fk−f)≤ε/2<ε. Taking k=N also shows pαβ(f)≤pαβ(fN)+ε/2<∞. Thus f∈S and fk→f in every seminorm and hence in d. Combined with local convexity, this proves the claimed Fréchet property.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

30 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