Theorems (or conjectures) for the theory of proveit.linear_algebra.inner_products¶
In [1]:
import proveit
# Prepare this notebook for defining the theorems of a theory:
%theorems_notebook # Keep this at the top following 'import proveit'.
from proveit import ExprRange, Composition
from proveit import n, a, b, i, m, n, v, w, x, y, z, A, B, K, H, M, P, U, X, alpha
from proveit.core_expr_types import (a_i, a_1_to_m, a_1_to_n, b_i, b_1_to_n, x_i, x_1_to_n,
lambda_i)
from proveit.logic import (
And, Forall, Exists, Iff, InSet, Set, SubsetEq, CartExp, InClass, Equals, NotEquals)
from proveit.numbers import zero, one, NaturalPos, Rational, Real, RealNonNeg, Complex, Conjugate
from proveit.numbers import Interval, Add, Mult, Abs, LessEq, greater, Min, sqrd, sqrt
from proveit.linear_algebra import (
VecSpaces, InnerProdSpaces, HilbertSpaces, Hspace, VecAdd, VecZero, VecSum, LinMap, Identity, Commutator,
ScalarMult, InnerProd, Norm, Adj, OrthoProj, Span, OrthoNormBases, Dim, TensorProd)
In [2]:
%begin theorems
In [3]:
inner_prod_space_is_vec_space = Forall(
K, Forall(H, InClass(H, VecSpaces(K)),
domain=InnerProdSpaces(K)))
Number field vector sets are inner product spaces:
In [4]:
rational_vec_set_is_inner_prod_space = Forall(
n, InClass(CartExp(Rational, n), InnerProdSpaces(Rational)),
domain = NaturalPos)
In [5]:
real_vec_set_is_inner_prod_space = Forall(
n, InClass(CartExp(Real, n), InnerProdSpaces(Real)),
domain = NaturalPos)
In [6]:
complex_vec_set_is_inner_prod_space = Forall(
n, InClass(CartExp(Complex, n), InnerProdSpaces(Complex)),
domain = NaturalPos)
Hilbert spaces are inner product spaces and vector spaces
In [7]:
hilbert_space_is_inner_prod_space = Forall(
Hspace, InClass(Hspace, InnerProdSpaces(Complex)),
domain=HilbertSpaces)
In [8]:
hilbert_space_is_vec_space = Forall(
Hspace, InClass(Hspace, VecSpaces(Complex)),
domain=HilbertSpaces)
Complex vectors form Hilbert spaces
In [9]:
complex_vec_set_is_hilbert_space = Forall(
n, InClass(CartExp(Complex, n), HilbertSpaces),
domain=NaturalPos)
As special cases, number fields are also inner product spaces:
In [10]:
rational_set_is_inner_prod_space = InClass(Rational,
InnerProdSpaces(Rational))
In [11]:
real_set_is_inner_prod_space = InClass(Real,
InnerProdSpaces(Real))
In [12]:
complex_set_is_inner_prod_space = InClass(Complex,
InnerProdSpaces(Complex))
In [13]:
complex_set_is_hilbert_space = InClass(Complex, HilbertSpaces)
Inner product linearity properties¶
In [14]:
inner_prod_linearity = Forall(
K, Forall(
H, Forall(
(a, b), Forall(
(x, y, z),
Equals(InnerProd(VecAdd(ScalarMult(a, x), ScalarMult(b, y)), z),
VecAdd(ScalarMult(a, InnerProd(x, z)),
ScalarMult(b, InnerProd(y, z)))),
domain=H),
domain=K),
domain=InnerProdSpaces(K)))
In [15]:
inner_prod_conj_sym = Forall(
K, Forall(
H, Forall(
(x, y), Equals(InnerProd(x, y), Conjugate(InnerProd(y, x))),
domain=H),
domain=InnerProdSpaces(K)))
In [16]:
inner_prod_pos_def = Forall(
K, Forall(
H, Forall(
x, greater(InnerProd(x, x), zero),
domain=H, condition=NotEquals(x, VecZero(H))),
domain=InnerProdSpaces(K)))
In [17]:
inner_prod_scalar_mult_left = Forall(
K, Forall(
H, Forall(
a, Forall(
(x, y),
Equals(InnerProd(ScalarMult(a, x), y),
ScalarMult(a, InnerProd(x, y))),
domain=H),
domain=K),
domain = InnerProdSpaces(K)))
In [18]:
inner_prod_scalar_mult_right = Forall(
K, Forall(
H, Forall(
a, Forall(
(x, y),
Equals(InnerProd(x, ScalarMult(a, y)),
ScalarMult(a, InnerProd(x, y))),
domain=H),
domain=K),
domain = InnerProdSpaces(K)))
In [19]:
inner_prod_vec_add_left = Forall(
K, Forall(
H, Forall(
(x, y, z),
Equals(InnerProd(VecAdd(x, y), z),
VecAdd(InnerProd(x, z), InnerProd(x, z))),
domain=H),
domain = InnerProdSpaces(K)))
In [20]:
inner_prod_vec_add_right = Forall(
K, Forall(
H, Forall(
(x, y, z),
Equals(InnerProd(x, VecAdd(y, z)),
VecAdd(InnerProd(x, y), InnerProd(x, z))),
domain=H),
domain = InnerProdSpaces(K)))
Our specific Norm definition satisfy the properties of an abstract normalization¶
In [21]:
norm_is_nonneg = Forall(
K, Forall(H, Forall(x, InSet(Norm(x), RealNonNeg),
domain=H),
domain=InnerProdSpaces(H)))
In [22]:
scaled_norm = Forall(
K, Forall(H, Forall((alpha, x), Equals(Norm(ScalarMult(alpha, x)),
Mult(Abs(alpha), Norm(x))),
domains=(K, H)),
domain=InnerProdSpaces(K)))
In [23]:
norm_triangle_ineq = Forall(
K, Forall(H, Forall((x, y), LessEq(Norm(VecAdd(x, y)),
Add(Norm(x), Norm(y))),
domain=H),
domain=InnerProdSpaces(K)))
Cauchy-Schwartz inequality¶
In [24]:
cauchy_schwartz_inequality = Forall(
H, Forall(
(v, w),
LessEq(sqrd(Norm(InnerProd(v, w))), Mult(InnerProd(v, v), InnerProd(w, w))),
domain=H),
domain=InnerProdSpaces(Complex))
In [25]:
cauchy_schwartz_equality = Forall(
H, Forall(
(v, w),
Iff(Equals(sqrd(Norm(InnerProd(v, w))), Mult(InnerProd(v, v), InnerProd(w, w))),
InSet(v, Span(Set(w)))),
domain=H),
domain=InnerProdSpaces(Complex))
Gram-Schmidt¶
To-Do: add the Gram-Schmidt construction of an orthonormal basis
In [26]:
# A direct consequence of Gram-Schmidt:
ortho_norm_basis_existence = Forall(
K, Forall(
n, Forall(
H, Exists(
x_1_to_n,
InSet(Set(x_1_to_n), OrthoNormBases(H))),
domain=InnerProdSpaces(K),
condition=Equals(Dim(H), n)).with_wrapping(),
domain=NaturalPos))
In [27]:
# A direct consequence of Gram-Schmidt:
ortho_norm_basis_existence_with_any_vector = Forall(
K, Forall(
n, Forall(
H, Forall(
v, Exists(
x_1_to_n,
And(InSet(v, Set(x_1_to_n)),
InSet(Set(x_1_to_n), OrthoNormBases(H)))
.with_wrap_after_operator()),
domain=H),
domain=InnerProdSpaces(K),
condition=Equals(Dim(H), n)).with_wrapping(),
domain=NaturalPos))
Properties of orthogonal projectors¶
In [28]:
ortho_projectors_are_idempotent = Forall(
Hspace, Forall(X, Forall(P, Equals(sqrd(P), P),
condition=Equals(P, OrthoProj(Hspace, X))),
condition=SubsetEq(X, Hspace)),
domain=HilbertSpaces)
In [29]:
ortho_projectors_are_hermitian = Forall(
Hspace, Forall(X, Forall(P, Equals(Adj(P), P),
condition=Equals(P, OrthoProj(Hspace, X))),
condition=SubsetEq(X, Hspace)),
domain=HilbertSpaces)
Normal operators and spectral decomposition¶
In [30]:
spectral_decomposition_as_ortho_ortho_projectors = Forall(
n, Forall(
Hspace, Forall(
M,
Iff(Equals(Composition(Adj(M), M),
Composition(M, Adj(M))),
Exists(
x_1_to_n, Exists(
a_1_to_n,
Equals(M, VecSum(i, ScalarMult(a_i, OrthoProj(Hspace, Span(Set(x_i)))),
domain=Interval(one, n))),
domain=Complex).with_wrapping(),
condition=InSet(Set(x_1_to_n), OrthoNormBases(Hspace))).with_wrapping())
.with_wrap_after_operator(),
domain=LinMap(Hspace, Hspace)),
domain=HilbertSpaces,
condition=Equals(Dim(Hspace), n)).with_wrapping(),
domain=NaturalPos)
Simultaneous diagonalization¶
In [31]:
simultaneous_diagonalization_as_ortho_projectors = Forall(
n, Forall(
Hspace, Forall(
(A, B),
Iff(Equals(Commutator(A, B), VecZero(LinMap(Hspace, Hspace))),
Exists(
x_1_to_n, Exists(
(a_1_to_n, b_1_to_n),
And(Equals(A, VecSum(i, ScalarMult(a_i, OrthoProj(Hspace, Span(Set(x_i)))),
domain=Interval(one, n))),
Equals(B, VecSum(i, ScalarMult(b_i, OrthoProj(Hspace, Span(Set(x_i)))),
domain=Interval(one, n)))).with_wrap_after_operator(),
domain=Complex).with_wrapping(),
condition=InSet(Set(x_1_to_n), OrthoNormBases(Hspace))).with_wrapping())
.with_wrap_after_operator(),
domain=LinMap(Hspace, Hspace),
conditions=[Equals(Adj(A), A), Equals(Adj(B), B)]
).with_wrapping(),
domain=HilbertSpaces,
condition=Equals(Dim(Hspace), n)).with_wrapping(),
domain=NaturalPos)
The polar decomposition¶
In [32]:
left_polar_decomposition = Forall(
Hspace, Forall(
A,
Exists(
U,
Equals(A, Composition(U, sqrt(Composition(Adj(A), A)))),
domain=LinMap(Hspace, Hspace),
condition=Equals(Composition(Adj(U), U), Identity(Hspace)))
.with_wrapping(),
domain=LinMap(Hspace, Hspace)
),
domain=HilbertSpaces)
In [33]:
right_polar_decomposition = Forall(
Hspace, Forall(
A,
Exists(
U,
Equals(A, Composition(sqrt(Composition(A, Adj(A))), U)),
domain=LinMap(Hspace, Hspace),
condition=Equals(Composition(Adj(U), U), Identity(Hspace)))
.with_wrapping(),
domain=LinMap(Hspace, Hspace)
),
domain=HilbertSpaces)
In [34]:
schmidt_decomposition = Forall(
(m, n), Forall(
(A, B), Forall(
v,
Exists(
a_1_to_m, Exists(
b_1_to_n, Exists(
ExprRange(i, lambda_i, one, Min(m, n)),
Equals(v, VecSum(i, ScalarMult(lambda_i, TensorProd(a_i, b_i)),
domain=Interval(one, Min(m, n)))),
domain=RealNonNeg).with_wrapping(),
condition=InSet(Set(b_1_to_n), OrthoNormBases(B))).with_wrapping(),
condition=InSet(Set(a_1_to_m), OrthoNormBases(A))).with_wrapping(),
domain=TensorProd(A, B)
),
domain=HilbertSpaces,
conditions=[Equals(Dim(A), m), Equals(Dim(B), n)]).with_wrapping(),
domain=NaturalPos)
In [35]:
%end theorems