Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 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 standard finite product norms are equivalent

Statement

Let n≥1 and let E=∏k<nEk be a finite product of normed spaces, equipped with the three standard product norms of The standard product norms on a finite product of normed spaces. Then for every x∈E, ∥x∥max⁡≤∥x∥2≤∥x∥1≤n∥x∥max⁡. Consequently these three norms are equivalent.

Facts & Assumptions

Given: A natural number n≥1, normed spaces E0,…,En−1, and a point x=(x0,…,xn−1)∈∏k<nEk.

[L1]

The three product norms are ∥x∥max⁡=max⁡k<n∥xk∥, ∥x∥1=∑k<n∥xk∥, and ∥x∥2=(∑k<n∥xk∥2)1/2 (The standard product norms on a finite product of normed spaces).

Proof

technique · direct
1.1L1algebra

For each coordinate, ∥xk∥2 is one of the nonnegative summands in ∑j<n∥xj∥2, so ∥xk∥≤∥x∥2 for every k and therefore ∥x∥max⁡≤∥x∥2.

1.2L1L2

Applying the scalar inequality ∥(ak)∥2≤∥(ak)∥1 from [L2] to the nonnegative real tuple (∥x0∥,…,∥xn−1∥) gives ∥x∥2≤∥x∥1.

1.3L1algebra

Since every coordinate norm is at most ∥x∥max⁡, summing n such bounds gives ∥x∥1≤n∥x∥max⁡.

2.1step 1.1step 1.2step 1.3∎

The three displayed inequalities of steps 1.1, 1.2, and 1.3 are exactly the comparison constants needed for equivalence of the three norms.

Depends on

Used by

Dependency tree · two levels

26 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