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.
Cauchy-Schwarz with its equality case, the triangle inequality for , the parallelogram law and polarisation
Statement
Let and let , with the Euclidean inner product and the Euclidean norm as in The Euclidean inner product on . Then:
- Cauchy-Schwarz. with equality if and only if there is a pair of reals with for every .
- is a norm on (A norm on a real vector space, the induced metric, and the dictionary with the metric axioms), for every ; the metric it induces is of as the set of functions , and , , are metrics on it whenever .
- Parallelogram law.
- Polarisation. so the inner product is recovered from the norm it induces.
Clause 1 is a citation, not a new proof. The inequality and its equality case are the published The Cauchy-Schwarz inequality for finite sums, stated there for two lists of reals; all that happens below is that it is read in the vector notation of The Euclidean inner product on . Re-proving it here would put two proofs of one statement in the library.
Statement references
Facts & Assumptions
Given: A natural number and vectors , so that and (The Euclidean inner product on , Finite sums and finite products, by recursion).
Cauchy-Schwarz for finite sums (The Cauchy-Schwarz inequality for finite sums): , with equality if and only if there is with for every ; and the root form .
The inner product is symmetric, bilinear and positive definite, , and exactly when (The Euclidean inner product on , Laws of finite sums and finite products).
Square roots (Square roots exist: a unique with ; the positives are ): every has a unique with , written ; hence and (Integer powers ).
Squaring is monotone on the nonnegatives: for , if and only if , and if and only if (Squaring is monotone on the nonnegatives).
Absolute value (Basic properties of the absolute value, Absolute value in an ordered field): , , and .
The norm axioms (N1), (N2), (N3) (A norm on a real vector space, the induced metric, and the dictionary with the metric axioms), and the fact that for ( as the set of functions , and , , are metrics on it, The Euclidean inner product on clause 6).
Proof
Instantiating [L1] at and gives , with equality exactly when some has for every .
Both and are nonnegative, and their squares are and .
Expanding by bilinearity and symmetry, .
The same expansion at gives .
For a scalar , , so .
Axiom (N1) holds: if and only if , which by positive definiteness says .
Comparing the squares of step 1.2 through step 1.1 and using monotonicity of squaring on the nonnegatives yields , with equality exactly in the proportional case of step 1.1; this is clause 1.
Adding the identities of step 1.3 and step 1.4 gives , which is clause 3.
Subtracting the identity of step 1.4 from that of step 1.3 gives , which is clause 4 after dividing by .
Both and are nonnegative and by step 1.5 have equal squares, so , which is axiom (N2).
By step 2.1 the middle term of step 1.3 satisfies , so .
Both and are nonnegative, so step 3.1 and monotonicity of squaring give , which is axiom (N3).
Steps 2.4, 1.6 and 4.1 are exactly (N1), (N2) and (N3), so is a norm on for every , and for the metric it induces is ; this is clause 2, and with steps 2.1, 2.2 and 2.3 all four clauses are proved.
Remarks
-
Which route to the triangle inequality was taken. The proof above obtains (N3) by expanding and applying Cauchy-Schwarz. The alternative is to quote Minkowski's inequality for finite sums (rational exponent) at the rational exponent , which states the same inequality directly; that route is equally legitimate and is the one Each is a norm on , and the induced metrics are exactly , and of the published metric-spaces page uses for a general exponent. Only one of the two is used here, so no statement is proved twice.
-
Clause 1 holds at , where it reads , and the equality case is then satisfied by every pair , the condition quantifying over no indices. Clause 2 also holds at , the zero space carrying exactly one norm (A norm on a real vector space, the induced metric, and the dictionary with the metric axioms). What is not available at is the metric of as the set of functions , and , , are metrics on it, which is why the last sentence of clause 2 carries .
-
Clauses 3 and 4 are what the companion page uses. The parallelogram law is an identity satisfied by every norm of the form , so a norm violating it is not of that form; that is how the companion page rules out on . Polarisation says the inner product carries no information the norm does not.
Depends on
- The Euclidean inner product $\langle x,y\rangle = \sum_{k<n} x_k y_k$ on $\mathbb{R}^n$
- A norm on a real vector space, the induced metric, and the dictionary with the metric axioms
- The Cauchy-Schwarz inequality for finite sums
- Minkowski's inequality for finite sums (rational exponent)
- Laws of finite sums and finite products
- Finite sums and finite products, by recursion
- Square roots exist: a unique $\sqrt{a} \ge 0$ with $(\sqrt{a})^2 = a$; the positives are $\{x^2 : x \neq 0\}$
- Squaring is monotone on the nonnegatives
- $\mathbb{R}^n$ as the set of functions $n \to \mathbb{R}$, and $d_1$, $d_2$, $d_\infty$ are metrics on it
- Integer powers $a^m$
- Basic properties of the absolute value
- Absolute value in an ordered field
Used by
- Finite checker for rational residual-tube certificates Algorithm
- Finite rejection sampler for a linear combination Algorithm
- A midpoint-quadrature P1 solve has an explicit Strang error budget Corollary
- A positive reaction term restores coercivity without Poincar'e Corollary
- Compact support expands at speed at most c Corollary
- Second-order global bound under symmetric coupling and a cubic defect Corollary
- The fixed-step projected subgradient rate is O(1/√N) Corollary
- ‖·‖₁ on ℝ² violates the parallelogram law, so no symmetric bilinear form induces it Counterexample
- A coercive form need not be symmetric Counterexample
- A smooth map can fail the tangential cone condition Counterexample
- An R-only proximal coordinate rate fails for nonsmooth penalties Counterexample
- Boundary-scale derivative blowup despite bounded ball data Counterexample
- Cyclic exact block minimization can cycle outside the convex separable hypotheses Counterexample
- The Koch curve is a uniform limit of polygonal paths of lengths (4/3)ⁿ but is not rectifiable Counterexample
- x↦-√1-‖x‖₂² has empty subdifferential on the unit-sphere boundary Counterexample
- The subspace Γ of directions along which a series converges absolutely, and its orthogonal complement Γ^⊥ Definition
- Wolfe and strong Wolfe line-search conditions Definition
- A bounded-noise Robbins–Monro scalar root Example
- A mixed-sign vorticity is not a probability for W1 Example
- A poorly aligned start delays the largest Ritz value and requires the start-angle factor Example
- A smooth map with a local tangential cone neighborhood Example
- Bounded noise, compressible truth, and a large nullspace component Example
- Cartan hadamard for hyperbolic space Example
- Lagrange multipliers locate the extrema of a linear functional on a sphere Example
- Norm-bounded robust least squares as an SOCP Example
- The eikonal equation as a viscosity equation at a tip Example
- The Euclidean norm and its square are convex, with a ball of subgradients at zero for the norm Example
- The Pontryagin dual of Euclidean space is Euclidean space Example
- A centered law and its affine dilation have an optimal affine coupling Lemma
- A compact set inside an open set has a uniform neighborhood radius Lemma
- A computed shifted-system residual has a certified upper bound Lemma
- A continuous strongly monotone map of finite-dimensional space is bijective Lemma
- A deterministic threshold-band bound for two Gram sketches Lemma
- A feasible finite-dimensional BPDN problem attains its minimum Lemma
- A feasible strictly convex linear-constrained QP has a unique KKT minimizer with independent active support Lemma
- A finite positive-spanning poll set has a positive uniform angle Lemma
- A finite-grid quantum subgradient from approximate values Lemma
- A finitely generated cone in Euclidean space is closed Lemma
- A Gaussian collocation defect has a high-order weighted endpoint bound Lemma
- A Hessian lower bound gives strong convexity and gradient-gap bounds Lemma
…and 221 more results.
Dependency tree · two levels
61 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
- Cauchy-Schwarz inequality (Wikipedia) (standard reference, not scraped)
- Parallelogram law (Wikipedia) (standard reference, not scraped)
- Polarization identity (Wikipedia) (standard reference, not scraped)
- J. Demmel, MA221 Lecture 3: Vector Norms (standard reference, not scraped)
- G. Zitelli, Math 641 Functional Analysis, Part I (standard reference, not scraped)