# 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

Defining theorems for theory 'proveit.linear_algebra.inner_products'
Subsequent end-of-cell assignments will define theorems
'%end theorems' will finalize the definitions

In [3]:
inner_prod_space_is_vec_space = Forall(
K, Forall(H, InClass(H, VecSpaces(K)),
domain=InnerProdSpaces(K)))

inner_prod_space_is_vec_space (conjecture without proof):

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)

rational_vec_set_is_inner_prod_space (conjecture without proof):

In [5]:
real_vec_set_is_inner_prod_space = Forall(
n, InClass(CartExp(Real, n), InnerProdSpaces(Real)),
domain = NaturalPos)

real_vec_set_is_inner_prod_space (conjecture without proof):

In [6]:
complex_vec_set_is_inner_prod_space = Forall(
n, InClass(CartExp(Complex, n), InnerProdSpaces(Complex)),
domain = NaturalPos)

complex_vec_set_is_inner_prod_space (conjecture without proof):

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)

hilbert_space_is_inner_prod_space (conjecture without proof):

In [8]:
hilbert_space_is_vec_space = Forall(
Hspace, InClass(Hspace, VecSpaces(Complex)),
domain=HilbertSpaces)

hilbert_space_is_vec_space (conjecture without proof):

Complex vectors form Hilbert spaces

In [9]:
complex_vec_set_is_hilbert_space = Forall(
n, InClass(CartExp(Complex, n), HilbertSpaces),
domain=NaturalPos)

complex_vec_set_is_hilbert_space (conjecture without proof):

As special cases, number fields are also inner product spaces:

In [10]:
rational_set_is_inner_prod_space = InClass(Rational,
InnerProdSpaces(Rational))

rational_set_is_inner_prod_space (conjecture without proof):

In [11]:
real_set_is_inner_prod_space = InClass(Real,
InnerProdSpaces(Real))

real_set_is_inner_prod_space (conjecture without proof):

In [12]:
complex_set_is_inner_prod_space = InClass(Complex,
InnerProdSpaces(Complex))

complex_set_is_inner_prod_space (conjecture without proof):

In [13]:
complex_set_is_hilbert_space = InClass(Complex, HilbertSpaces)

complex_set_is_hilbert_space (conjecture without proof):

### Inner product linearity properties¶

In [14]:
inner_prod_linearity = Forall(
K, Forall(
H, Forall(
(a, b), Forall(
(x, y, z),
ScalarMult(b, InnerProd(y, z)))),
domain=H),
domain=K),
domain=InnerProdSpaces(K)))

inner_prod_linearity (conjecture without proof):

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)))

inner_prod_conj_sym (conjecture without proof):

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)))

inner_prod_pos_def (conjecture without proof):

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)))

inner_prod_scalar_mult_left (conjecture without proof):

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)))

inner_prod_scalar_mult_right (conjecture without proof):

In [19]:
inner_prod_vec_add_left = Forall(
K, Forall(
H, Forall(
(x, y, z),
domain=H),
domain = InnerProdSpaces(K)))


In [20]:
inner_prod_vec_add_right = Forall(
K, Forall(
H, Forall(
(x, y, 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)))

norm_is_nonneg (conjecture without proof):

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)))

scaled_norm (conjecture without proof):

In [23]:
norm_triangle_ineq = Forall(
K, Forall(H, Forall((x, y), LessEq(Norm(VecAdd(x, y)),
domain=H),
domain=InnerProdSpaces(K)))

norm_triangle_ineq (conjecture without proof):

### 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))

cauchy_schwartz_inequality (conjecture without proof):

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))

cauchy_schwartz_equality (conjecture without proof):

## 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))

ortho_norm_basis_existence (conjecture without proof):

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))

ortho_norm_basis_existence_with_any_vector (conjecture without proof):

### 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)

ortho_projectors_are_idempotent (conjecture without proof):

In [29]:
ortho_projectors_are_hermitian = Forall(
condition=Equals(P, OrthoProj(Hspace, X))),
condition=SubsetEq(X, Hspace)),
domain=HilbertSpaces)

ortho_projectors_are_hermitian (conjecture without proof):

### Normal operators and spectral decomposition¶

In [30]:
spectral_decomposition_as_ortho_ortho_projectors = Forall(
n, Forall(
Hspace, Forall(
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),
).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,
domain=LinMap(Hspace, Hspace),
.with_wrapping(),
domain=LinMap(Hspace, Hspace)
),
domain=HilbertSpaces)

left_polar_decomposition (conjecture without proof):

In [33]:
right_polar_decomposition = Forall(
Hspace, Forall(
A,
Exists(
U,
domain=LinMap(Hspace, Hspace),
.with_wrapping(),
domain=LinMap(Hspace, Hspace)
),
domain=HilbertSpaces)

right_polar_decomposition (conjecture without proof):

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)

schmidt_decomposition (conjecture without proof):

In [35]:
%end theorems

These theorems may now be imported from the theory package: proveit.linear_algebra.inner_products