CauchySchwarzStarter

Cauchy–Schwarz in every finite dimension

Open in Workbench View on GitHub

1-- Cauchy–Schwarz in every finite dimension2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module CauchySchwarzStarter8import Grace.Cumulus.LinearAlgebra910theorem cauchy_schwarz (u v : Set, n : Nat)11  requires sequenceU : RealSequence(u)12  requires sequenceV : RealSequence(v)13  shows (dotProduct(u, v, n):R) * (dotProduct(u, v, n):R) ≤14    (squaredNorm(u, n):R) * (squaredNorm(v, n):R)15proof16  exact dotProduct.cauchy_schwarz at u, v, n with *1718theorem equality_for_scalar_multiples (v : Set, C : Real, n : Nat)19  requires sequence : RealSequence(v)20  shows (dotProduct(mulSequence(constantSequence(C), v), v, n):R) *21      (dotProduct(mulSequence(constantSequence(C), v), v, n):R) =22    (squaredNorm(mulSequence(constantSequence(C), v), n):R) * (squaredNorm(v, n):R)23proof24  exact dotProduct.cauchy_schwarz_scalar_equality at v, C, n with *2526-- The zero-vector alternative is essential, including at dimension zero.27theorem equality_characterization (u v : Set, n : Nat)28  requires sequenceU : RealSequence(u)29  requires sequenceV : RealSequence(v)30  shows (dotProduct(u, v, n):R) * (dotProduct(u, v, n):R) =31      (squaredNorm(u, n):R) * (squaredNorm(v, n):R) ↔32    (squaredNorm(v, n) = (0:R) ∨33      (∃ C ∈ ℝ, (∀ i ∈ ℕ, i < n → u[i] = C * (v[i]:R))))34proof35  exact dotProduct.cauchy_schwarz_equality_iff at u, v, n with *3637theorem zero_norm_means_zero_coordinates (u : Set, n : Nat)38  requires sequence : RealSequence(u)39  shows squaredNorm(u, n) = (0:R) ↔ (∀ i ∈ ℕ, i < n → u[i] = (0:R))40proof41  exact squaredNorm.eq_zero_iff at u, n with *42