Grace/Cumulus/LinearAlgebra/CauchySchwarz.g17

Open in Workbench Download source

Imports

FiniteDimensional

Declarations

Source

1-- Cauchy–Schwarz for arbitrary finite-dimensional real vectors2-- 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 Passmore67-- Mathematical source: imandra-ai/imandra-100-theorems, src/cauchy_schwarz.iml.8-- Sequences restricted to n coordinates replace the source's equal-length lists.910module Grace.Cumulus.LinearAlgebra.CauchySchwarz11import FiniteDimensional1213theorem dotProduct.zero_of_squaredNorm_zero (u v : Set, n : Nat)14  requires sequenceU : RealSequence(u)15  requires sequenceV : RealSequence(v)16  shows squaredNorm(v, n) = (0:R) → dotProduct(u, v, n) = (0:R)17proof18  induction n19  | zero =>20    intro zero21    exact dotProduct.zero at u, v22  | succ(k) using ih =>23    intro zero24    have uk := RealSequence.value at u, k with *25    have vk := RealSequence.value at v, k with *26    have nonnegative := squaredNorm.nonnegative at v, k with *27    have squareNonnegative := realMulValue.square_nonnegative at v[k] with *28    rw squaredNorm.succ at zero29    have prefixZero := realAddValue.nonnegative_eq_zero at squaredNorm(v, k), v[k] * v[k] with *30    have squareZero : (v[k]:R) * (v[k]:R) = 031    . rw prefixZero at zero32      simpa [realAddValue.zero_left] using zero33    have valueZero := realMulValue.square_eq_zero_iff.forward at v[k] with *34    have dotZero := ih with prefixZero35    rw [dotProduct.succ, dotZero, valueZero]36    ring3738theorem squaredNorm.scaled_difference (u v : Set, C D : Real, n : Nat)39  requires sequenceU : RealSequence(u)40  requires sequenceV : RealSequence(v)41  shows squaredNorm(subSequence(mulSequence(constantSequence(C), u), mulSequence(constantSequence(D), v)), n) =42    C * C * (squaredNorm(u, n):R) - (2:R) * C * D * (dotProduct(u, v, n):R) + D * D * (squaredNorm(v, n):R)43proof44  have constantC := constantSequence.sequence at C with *45  have constantD := constantSequence.sequence at D with *46  have scaledU := mulSequence.sequence at constantSequence(C), u with *47  have scaledV := mulSequence.sequence at constantSequence(D), v with *48  simp [squaredNorm.sub, squaredNorm.scale, dotProduct.scale_left, dotProduct.scale_right]49  ring5051theorem dotProduct.cauchy_schwarz (u v : Set, n : Nat)52  requires sequenceU : RealSequence(u)53  requires sequenceV : RealSequence(v)54  shows (dotProduct(u, v, n):R) * (dotProduct(u, v, n):R) ≤55    (squaredNorm(u, n):R) * (squaredNorm(v, n):R)56proof57  have normNonnegative := squaredNorm.nonnegative at v, n with *58  have cases : squaredNorm(v, n) = (0:R) ∨ squaredNorm(v, n) ≠ (0:R)59  . tauto60  cases cases with zero | nonzero61  . have dotZero := dotProduct.zero_of_squaredNorm_zero at u, v, n with *62    rw [dotZero, zero]63    simpa [realMulValue.zero_left, realMulValue.zero_right] using realLe.reflexive at realZero with *64  . have positive := Real.positive_of_nonnegative_of_ne_zero with *65    have constantNorm := constantSequence.sequence at squaredNorm(v, n) with *66    have constantDot := constantSequence.sequence at dotProduct(u, v, n) with *67    have scaledU := mulSequence.sequence at constantSequence(squaredNorm(v, n)), u with *68    have scaledV := mulSequence.sequence at constantSequence(dotProduct(u, v, n)), v with *69    have difference := subSequence.sequence at mulSequence(constantSequence(squaredNorm(v, n)), u), mulSequence(constantSequence(dotProduct(u, v, n)), v) with *70    have nonnegative := squaredNorm.nonnegative at subSequence(mulSequence(constantSequence(squaredNorm(v, n)), u), mulSequence(constantSequence(dotProduct(u, v, n)), v)), n with *71    have expansion := squaredNorm.scaled_difference at u, v, squaredNorm(v, n), dotProduct(u, v, n), n with *72    rw expansion at nonnegative73    have rearrange : (squaredNorm(v, n):R) * (squaredNorm(v, n):R) * (squaredNorm(u, n):R) - (2:R) * (squaredNorm(v, n):R) * (dotProduct(u, v, n):R) * (dotProduct(u, v, n):R) + (dotProduct(u, v, n):R) * (dotProduct(u, v, n):R) * (squaredNorm(v, n):R) =74      ((squaredNorm(u, n):R) * (squaredNorm(v, n):R)) * (squaredNorm(v, n):R) - ((dotProduct(u, v, n):R) * (dotProduct(u, v, n):R)) * (squaredNorm(v, n):R)75    . ring76    rw rearrange at nonnegative77    have products := realLe.of_nonnegative_difference with *78    exact realLe.mul_right_cancel_positive with *7980theorem dotProduct.cauchy_schwarz_scalar_equality (v : Set, C : Real, n : Nat)81  requires sequence : RealSequence(v)82  shows (dotProduct(mulSequence(constantSequence(C), v), v, n):R) *83      (dotProduct(mulSequence(constantSequence(C), v), v, n):R) =84    (squaredNorm(mulSequence(constantSequence(C), v), n):R) * (squaredNorm(v, n):R)85proof86  have constants := constantSequence.sequence with *87  have scaled := mulSequence.sequence at constantSequence(C), v with *88  simp [dotProduct.scale_left, squaredNorm.scale]89  unfold squaredNorm90  ring9192-- A zero norm is exactly coordinatewise zero on the observed prefix.93theorem squaredNorm.zero_prefix (u : Set, n : Nat)94  requires sequence : RealSequence(u)95  shows squaredNorm(u, n) = (0:R) → ∀ i ∈ ℕ, i < n → u[i] = (0:R)96proof97  induction n98  | zero =>99    intros zero i member before100    have naturalI := nat.omega.backward with member101    have impossible : i < i102    . arith103    exfalso104    exact Less.irreflexive with naturalI, impossible105  | succ(k) using ih =>106    intros zero i member before107    have naturalI := nat.omega.backward with member108    have uk := RealSequence.value at u, k with *109    have nonnegative := squaredNorm.nonnegative at u, k with *110    have squareNonnegative := realMulValue.square_nonnegative at u[k] with *111    rw squaredNorm.succ at zero112    have prefixZero := realAddValue.nonnegative_eq_zero at squaredNorm(u, k), u[k] * u[k] with *113    have squareZero : (u[k]:R) * (u[k]:R) = 0114    . rw prefixZero at zero115      simpa [realAddValue.zero_left] using zero116    have valueZero := realMulValue.square_eq_zero_iff.forward at u[k] with *117    have included := membership.of_Less at i, succ(k) with *, before118    have alternatives := membership.successor_forward{n := k} with included119    cases alternatives with earlier | equal120    . have smaller := Less.of_membership at i, k with *, earlier121      exact ih with prefixZero, i, member, smaller122    . rw equal123      exact valueZero124125theorem squaredNorm.of_zero_prefix (u : Set, n : Nat)126  requires sequence : RealSequence(u)127  shows (∀ i ∈ ℕ, i < n → u[i] = (0:R)) → squaredNorm(u, n) = (0:R)128proof129  induction n130  | zero =>131    intro coordinates132    unfold squaredNorm133    exact dotProduct.zero at u, u134  | succ(k) using ih =>135    intro coordinates136    have prefix : ∀ i ∈ ℕ, i < k → u[i] = (0:R)137    . intros i member before138      have naturalI := nat.omega.backward with member139      have smaller : i < succ(k)140      . arith141      exact coordinates with i, member, smaller142    have zeroPrefix := ih with prefix143    have memberK := nat.omega.forward at k with *144    have beforeK : k < succ(k)145    . arith146    have zeroLast := coordinates with k, memberK, beforeK147    rw [squaredNorm.succ, zeroPrefix, zeroLast]148    ring149150theorem squaredNorm.eq_zero_iff (u : Set, n : Nat)151  requires sequence : RealSequence(u)152  shows squaredNorm(u, n) = (0:R) ↔ (∀ i ∈ ℕ, i < n → u[i] = (0:R))153proof154  constructor155  . exact squaredNorm.zero_prefix with *156  . exact squaredNorm.of_zero_prefix with *157158theorem squaredNorm.eq_prefix (u v : Set, n : Nat)159  requires sequenceU : RealSequence(u)160  requires sequenceV : RealSequence(v)161  requires coordinates : ∀ i ∈ ℕ, i < n → u[i] = v[i]162  shows squaredNorm(u, n) = squaredNorm(v, n)163proof164  unfold squaredNorm165  exact dotProduct.eq_prefix with *166167theorem dotProduct.cauchy_schwarz_equality_residual (u v : Set, n : Nat)168  requires sequenceU : RealSequence(u)169  requires sequenceV : RealSequence(v)170  requires equality : (dotProduct(u, v, n):R) * (dotProduct(u, v, n):R) =171    (squaredNorm(u, n):R) * (squaredNorm(v, n):R)172  shows squaredNorm(subSequence(mulSequence(constantSequence(squaredNorm(v, n)), u),173    mulSequence(constantSequence(dotProduct(u, v, n)), v)), n) = (0:R)174proof175  rw squaredNorm.scaled_difference176  linear_combination -(squaredNorm(v, n):R) * equality177178theorem dotProduct.cauchy_schwarz_equality_iff (u v : Set, n : Nat)179  requires sequenceU : RealSequence(u)180  requires sequenceV : RealSequence(v)181  shows (dotProduct(u, v, n):R) * (dotProduct(u, v, n):R) =182      (squaredNorm(u, n):R) * (squaredNorm(v, n):R) ↔183    (squaredNorm(v, n) = (0:R) ∨184      (∃ C ∈ ℝ, (∀ i ∈ ℕ, i < n → u[i] = C * (v[i]:R))))185proof186  constructor187  . intro equality188    have alternatives : squaredNorm(v, n) = (0:R) ∨ squaredNorm(v, n) ≠ (0:R)189    . tauto190    cases alternatives with zero | nonzero191    . left192      exact zero193    . right194      have inverseLaw := realInvValue.mul_right with *195      have coefficient := realMulValue.real at dotProduct(u, v, n), realInvValue(squaredNorm(v, n)) with *196      have coefficientMember : dotProduct(u, v, n) * realInvValue(squaredNorm(v, n)) ∈ ℝ197      . settle with Real198      refine ⟨dotProduct(u, v, n) * realInvValue(squaredNorm(v, n)), coefficientMember, _⟩199      intros i member before200      have naturalI := nat.omega.backward with member201      have ui := RealSequence.value at u, i with *202      have vi := RealSequence.value at v, i with *203      have constantNorm := constantSequence.sequence at squaredNorm(v, n) with *204      have constantDot := constantSequence.sequence at dotProduct(u, v, n) with *205      have scaledU := mulSequence.sequence at constantSequence(squaredNorm(v, n)), u with *206      have scaledV := mulSequence.sequence at constantSequence(dotProduct(u, v, n)), v with *207      have difference := subSequence.sequence at mulSequence(constantSequence(squaredNorm(v, n)), u), mulSequence(constantSequence(dotProduct(u, v, n)), v) with *208      have normZero := dotProduct.cauchy_schwarz_equality_residual with *209      have pointZero := squaredNorm.zero_prefix with *, normZero, i, member, before210      have firstValue := RealSequence.value at mulSequence(constantSequence(squaredNorm(v, n)), u), i with *211      have secondValue := RealSequence.value at mulSequence(constantSequence(dotProduct(u, v, n)), v), i with *212      have normValue := RealSequence.value at constantSequence(squaredNorm(v, n)), i with *213      have dotValue := RealSequence.value at constantSequence(dotProduct(u, v, n)), i with *214      simp [subSequence.value, mulSequence.value, constantSequence.value] at pointZero215      linear_combination realInvValue(squaredNorm(v, n)) * pointZero - (u[i]:R) * inverseLaw216  . intro alternatives217    cases alternatives with zero | proportional218    . have dotZero := dotProduct.zero_of_squaredNorm_zero at u, v, n with *, zero219      rw [dotZero, zero]220      ring221    . obtain ⟨C, memberC, coordinates⟩ := proportional222      have realC : Real(C)223      . settle with Real224      have constants := constantSequence.sequence with *225      have scaled := mulSequence.sequence at constantSequence(C), v with *226      have equalPrefix : ∀ i ∈ ℕ, i < n → u[i] = mulSequence(constantSequence(C), v)[i]227      . intros i member before228        have naturalI := nat.omega.backward with member229        have vi := RealSequence.value at v, i with *230        have ci := RealSequence.value at constantSequence(C), i with *231        simp [mulSequence.value, constantSequence.value]232        exact coordinates with i, member, before233      have reflexive : ∀ i ∈ ℕ, i < n → v[i] = v[i]234      . intros i member before235        rfl236      have equalDot := dotProduct.eq_prefix at u, v, mulSequence(constantSequence(C), v), v, n with *237      have equalNorm := squaredNorm.eq_prefix at u, mulSequence(constantSequence(C), v), n with *238      rw [equalDot, equalNorm]239      exact dotProduct.cauchy_schwarz_scalar_equality with *240