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.
L two operator conventions for weak mixing
Definition
Let be a closed complex subspace with the first-variable-linear pairing of The complex pairing is well-defined and satisfies Cauchy–Schwarz. All operators below map to and are complex-linear. An operator is bounded if for some finite and all ; its norm is . It is compact if it is bounded and every bounded sequence has a subsequence for which converges in norm to an element of .
An adjoint is a bounded operator satisfying for all . Such an operator, if it exists, is unique: subtract two proposed identities and set equal to the difference of their values at . Positive definiteness makes that difference zero. Existence is not assumed by this definition.
The operator is self-adjoint if for all . It is positive if is real and nonnegative for every . Later positive self-adjoint assertions impose both conditions explicitly.
An isometry preserves the norm; for linear operators it also preserves the pairing. Indeed expansion of gives , and expansion of gives . Applying both identities before and after the isometry proves the assertion. A unitary is a surjective linear isometry.
A linear subspace is invariant for if . Write when for every , and . These conventions allow , and the zero operator. In the zero space the operator norm is zero because the unit ball is . No infinite selection or assertion of an orthonormal basis enters these definitions.
Depends on
Used by
- Closed l two subspaces have orthogonal projections Lemma
- Conjugate transpose kernels give adjoints Lemma
- Hilbert cesaro averages converge to the fixed subspace Lemma
- Nonzero compact kernel operators yield nonzero positive compact k star k Lemma
- Square integrable kernels define bounded compact integral operators Lemma
- The positive norm eigenvalue of a nonzero positive compact self-adjoint operator has a nonzero finite-dimensional eigenspace Lemma
Dependency tree · two levels
8 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
- Axler 8B, 10A, 10C definitions; Example 10.5 (standard reference, not scraped)