Alphabeta MathHow 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.
A definite quadratic form has a uniform signed bound on the Euclidean unit sphere
Statement
Let and let be a positive definite quadratic form on . Then some satisfies whenever . For a negative definite , some satisfies on the same sphere.
Facts & Assumptions
Given: A definite quadratic form on with .
The Euclidean norm is continuous, and a continuous map has closed preimages of closed sets (The finite and reverse triangle inequalities for a norm; and for every norm on satisfies and is Lipschitz, hence continuous, for , Metric continuity characterisations, with countable choice for the sequential converse).
Heine--Borel says that a closed bounded Euclidean subset is compact (Heine-Borel in : with the Euclidean metric a subset of is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line).
A continuous real function on a nonempty compact metric space attains its extrema (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value).
Proof
The unit sphere is nonempty because it contains , closed by [L1], and bounded since it lies in the radius-two ball about zero.
It is compact by [L2].
The finite coordinate formula for makes it continuous; [L3] therefore gives a point where attains its minimum and maximum on the sphere.
In the positive definite case the attained minimum is positive, and in the negative definite case the attained maximum is negative, by the definition of definiteness.
Taking to be the positive minimum or the negative maximum gives the asserted uniform signed bounds.
Depends on
- Positive definite, negative definite, semidefinite, and indefinite quadratic forms
- The Euclidean inner product $\langle x,y\rangle = \sum_{k<n} x_k y_k$ on $\mathbb{R}^n$
- Laws of finite sums and finite products
- Triangle inequality for finite sums
- The finite and reverse triangle inequalities for a norm; and for $n \ge 1$ every norm $N$ on $\mathbb{R}^n$ satisfies $N(x) \le C\lVert x\rVert_1$ and is Lipschitz, hence continuous, for $d_2$
- Metric continuity characterisations, with countable choice for the sequential converse
- The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement
- Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space
- The standard list $e : n \to F^{n}$ with $e_i(i) = 1_F$ and $e_i(j) = 0_F$ for $j \ne i$ is an ordered basis of $F^{n}$; hence $\dim_F F^{n} = n$, and $F^{0}$ is the zero space with basis $\varnothing$ and dimension $0$
- Heine-Borel in $\mathbb{R}^n$: with the Euclidean metric a subset of $\mathbb{R}^n$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line
- A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value
Used by
Dependency tree · two levels
91 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
- Analysis, Convexity, and Optimization (standard reference, not scraped)