LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

Finite-dimensional orthogonal projections are linear and contractive

Statement

Let $V$ be a finite-dimensional real inner-product space, let $W \subseteq V$ be a linear subspace, and let $P_{W} : V \to W$ be the orthogonal projection. Then $P_{W}$ is linear and satisfies $∥ P_{W} x ∥ \leq ∥ x ∥$ for every $x \in V$ . In particular, $P_{W}$ is continuous.

Facts & Assumptions

Given: A finite-dimensional real inner-product space $V$ , a subspace $W$ , its orthogonal projection $P_{W}$ , and vectors $x, y \in V$ .

[F1]

$P_{W} z \in W$ and $z - P_{W} z \in W^{⊥}$ , and this decomposition is unique (The orthogonal projection $P_{W} v$ is the $W$ -component in $V = W \oplus W^{⊥}$ ).

[F2]

$W$ and $W^{⊥}$ are linear subspaces (Linear subspace of a vector space, Orthogonality and the orthogonal complement).

[F3]

If $u ⊥ v$ , then $∥ u + v ∥^{2} = ∥ u ∥^{2} + ∥ v ∥^{2}$ (Pythagoras, the parallelogram identity, and the real and complex polarisation identities).

Proof

1.1F1F2

The vectors $P_{W} x + P_{W} y \in W$ and $(x + y) - (P_{W} x + P_{W} y) = (x - P_{W} x) + (y - P_{W} y) \in W^{⊥}$ form a decomposition of $x + y$ of the type in [F1] by [F2]. Uniqueness in [F1] therefore gives $P_{W} (x + y) = P_{W} x + P_{W} y$ .

2.1F1F2step 1.1

For any scalar $a \in R$ , $a P_{W} x \in W$ and $a x - a P_{W} x = a (x - P_{W} x) \in W^{⊥}$ by [F2]. Uniqueness in [F1] gives $P_{W} (a x) = a P_{W} x$ . Together with step 1.1 this proves linearity.

3.1F1F3step 1.1step 2.1algebra∎

The decomposition $x = P_{W} x + (x - P_{W} x)$ is orthogonal by [F1]. Pythagoras [F3] yields $∥ x ∥^{2} = ∥ P_{W} x ∥^{2} + ∥ x - P_{W} x ∥^{2} \geq ∥ P_{W} x ∥^{2}$ , hence $∥ P_{W} x ∥ \leq ∥ x ∥$ . By linearity, $∥ P_{W} x - P_{W} y ∥ = ∥ P_{W} (x - y) ∥ \leq ∥ x - y ∥$ , so $P_{W}$ is continuous.

Depends on

Used by

Dependency tree · two levels

13 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

Philippe Rigollet and Jan-Christian Hütter, High-Dimensional Statistics: Lecture Notes, Chapter 2, §§7–8 (standard reference, not scraped)
Sylvain Arlot, Model/estimator selection, Lecture on model selection, §§1–2 (standard reference, not scraped)