TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-09

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 complex $L^{2}$ pairing is well-defined and satisfies Cauchy–Schwarz

Statement

On every measure space the pairing $⟨ f, g ⟩ = \int f \overline{g}$ on complex $L^{2}$ is representative-independent, linear in the first variable, conjugate-linear in the second, conjugate symmetric and positive definite, with $⟨ f, f ⟩ = ∥ f ∥_{2}^{2}$ . Moreover, $∣ ⟨ f, g ⟩ ∣ \leq ∥ f ∥_{2} ∥ g ∥_{2} .$ If $g \neq 0$ as a class, equality holds iff $f = c g$ a.e. for some $c \in C$ . If $g = 0$ , equality holds for every $f$ .

For each finite $m \geq 0$ , the same conclusions hold on tuples $F = (f_{j})_{j < m}$ , with pairing $B (F, G) = \sum_{j < m} ⟨ f_{j}, g_{j} ⟩$ and $∥ F ∥^{2} = \sum_{j < m} ∥ f_{j} ∥_{2}^{2}$ . For $G \neq 0$ , equality means $f_{j} = c g_{j}$ a.e. for every $j$ , with one common scalar $c$ .

Facts & Assumptions

Given: A measure space and complex $L^{2}$ classes; for the tuple assertion a fixed finite tuple length $m \geq 0$ .

[F1]

The representative expression is $\int f \overline{g}$ (The complex $L^{2}$ pairing on equivalence classes).

[F2]

Hölder gives integrability of $L^{2}$ products; the quotient norm vanishes exactly on the zero class (Complex Holder, Minkowski, and the quotient norm).

[F3]

Complex integration is linear on integrable functions (The Lebesgue integral is linear on $L^{1} (μ)$ ).

[F4]

A.e.-equal integrable functions have equal integrals (Two integrable functions are equal almost everywhere exactly when all of their indefinite integrals agree).

[F5]

A nonnegative integral is zero iff its integrand is zero a.e. (A nonnegative measurable function has integral $0$ exactly when it vanishes almost everywhere).

[F6]

Conjugation distributes over sums and products, and $z \overline{z} = ∣ z ∣^{2}$ (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive).

[F7]

The complex integral is the integral of the real part plus i times the integral of the imaginary part (Integrable real and complex functions, and their integrals).

Proof

technique · Verify the form directly and expand the squared distance to a scalar multiple

1.1

F2 makes $f \overline{g}$ integrable. Replacing $f, g$ by a.e.-equal representatives changes their product only on the union of the two measurable null disagreement sets. F4 therefore leaves the integral in F1 unchanged. This proves representative independence.

F1F2F4

1.2

For an integrable $h = u + i v$ , F7 gives $\int \overline{h} = \int u - i \int v = \overline{\int h}$ . Hence F6 implies $⟨ g, f ⟩ = \overline{⟨ f, g ⟩}$ . F3 applied to $(a f + b k) \overline{g}$ gives $⟨ a f + b k, g ⟩ = a ⟨ f, g ⟩ + b ⟨ k, g ⟩$ , and applied to $f \overline{a g + b k} = \overline{a} f \overline{g} + \overline{b} f \overline{k}$ gives conjugate-linearity in the second variable. All products are integrable by F2.

F1F2F3F6F7

1.3

F6 gives $⟨ f, f ⟩ = \int ∣ f ∣^{2} = ∥ f ∥_{2}^{2} \geq 0$ . By F5 this number is zero iff $∣ f ∣^{2} = 0$ a.e., which is equivalent to $f = 0$ as a class. Thus the form is positive definite and its norm is exactly the modulus $L^{2}$ norm.

F1F2F5F6

2.1

For $g \neq 0$ put $a = ⟨ f, g ⟩$ , $b = ∥ g ∥_{2}^{2} > 0$ and $c = a / b$ . Sesquilinearity yields $∥ f - c g ∥_{2}^{2} = ∥ f ∥_{2}^{2} - \overline{c} a - c \overline{a} + ∣ c ∣^{2} b = ∥ f ∥_{2}^{2} - ∣ a ∣^{2} / b$ . Nonnegativity proves $∣ a ∣^{2} \leq ∥ f ∥_{2}^{2} b$ , hence Cauchy–Schwarz. Equality implies $∥ f - c g ∥_{2} = 0$ , so $f = c g$ a.e. Conversely, if $f = d g$ a.e., then $⟨ f, g ⟩ = d b$ and $∥ f ∥_{2} = ∣ d ∣ ∥ g ∥_{2}$ , giving equality. For $g = 0$ , both sides of the inequality are zero for every $f$ .

F2step 1.2step 1.3

3.1

Finite summation preserves the linearity and symmetry identities. Also $B (F, F) = \sum_{j < m} ∥ f_{j} ∥_{2}^{2} \geq 0$ , and a finite sum of nonnegative reals is zero iff every summand is zero; step 1.3 then gives definiteness. For $G \neq 0$ , set $c = B (F, G) / B (G, G)$ . Expanding the finite sum using step 1.2 gives $∥ F - c G ∥^{2} = ∥ F ∥^{2} - ∣ B (F, G) ∣^{2} / ∥ G ∥^{2}$ . Nonnegativity gives $∣ B (F, G) ∣ \leq ∥ F ∥ ∥ G ∥$ . The expansion $∥ F + G ∥^{2} = ∥ F ∥^{2} + 2 Re B (F, G) + ∥ G ∥^{2} \leq (∥ F ∥ + ∥ G ∥)^{2}$ gives the triangle inequality; scalar homogeneity follows by scaling each squared component norm. Thus this square root is indeed a norm. As above, equality in Cauchy–Schwarz is equivalent to each $f_{j} - c g_{j}$ having norm zero, with this same $c$ for all $j$ ; conversely a common scalar multiple gives equality by homogeneity. For $G = 0$ both sides are zero. If $m = 0$ , the tuple space has just its zero element and all sums are zero, so the same axioms and zero case apply.

F2step 1.2step 1.3step 2.1∎

Depends on

Used by

Cited to discharge well-definedness by The complex L² pairing on equivalence classes.

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

Gerald Teschl, Topics in Real and Functional Analysis (standard reference, not scraped)

The complex L2L2 pairing is well-defined and satisfies Cauchy–Schwarz