FARMSAcceptedTheorem · Statement with omitted proof
Pythagoras identity and vector orthogonality
Orthogonality is equivalent to additivity of squared Euclidean norms.
Drineas & Mahoney ↗
Source label: thm:pythagoras
Formal statement. The assumptions and conclusion are explicit; the theorem proof is omitted (sorry).
01 / MATHEMATICAL STATEMENT
Meaning & conditions
Mathematical summary
Orthogonality is equivalent to additivity of squared Euclidean norms.
Assumptions & context
- x and y are real vectors of the same finite dimension.
Source
Drineas & Mahoney. Lectures on randomized numerical linear algebra.
Source label: thm:pythagoras
02 / LEAN REPRESENTATION
Formal statement
Statement with omitted proof. Expand the complete file below to read imports, local definitions and surrounding context.
theorem pythagoras (n : ℕ) (x y : Fin n → ℝ) :
(dotProduct x y = 0 ↔ l2Norm (x + y) ^ 2 = l2Norm x ^ 2 + l2Norm y ^ 2) ∧
(dotProduct x y = 0 ↔ l2Norm (x - y) ^ 2 = l2Norm x ^ 2 + l2Norm y ^ 2) := by
sorry
Complete Lean file and local definitions
import RNLAPhaseB.B3Base
import RNLAPhaseB.Complexity
open MeasureTheory
open scoped Matrix
open scoped Matrix.Norms.L2Operator
open scoped BigOperators
open scoped ENNReal
namespace RNLAPhaseB.DM2017.Pythagoras
/-- dm2017 `thm:pythagoras`: two vectors `x, y ∈ ℝ^n` are orthogonal, i.e. `xᵀ y = 0`,
if and only if `‖x ± y‖₂² = ‖x‖₂² + ‖y‖₂²`.
The symbol `±` is read as the two statements obtained with each sign. Each statement is its
own equivalence with orthogonality. `xᵀ y` is the standard dot product. `‖·‖₂` is the
Euclidean vector 2-norm (`l2Norm` from the frozen base). -/
theorem pythagoras (n : ℕ) (x y : Fin n → ℝ) :
(dotProduct x y = 0 ↔ l2Norm (x + y) ^ 2 = l2Norm x ^ 2 + l2Norm y ^ 2) ∧
(dotProduct x y = 0 ↔ l2Norm (x - y) ^ 2 = l2Norm x ^ 2 + l2Norm y ^ 2) := by
sorry
end RNLAPhaseB.DM2017.Pythagoras
How to read the formalization
- The plus and minus identities are stated as separate equivalences.