RUSUB_7: Formalization of Orthogonal Decomposition for Hilbert Spaces

:: Formalization of Orthogonal Decomposition for Hilbert Spaces
:: by Hiroyuki Okazaki
::
:: Received December 27, 2022
:: Copyright (c) 2022-2025 Association of Mizar Users

theorem Th1: :: RUSUB_7:1

for X being RealUnitarySpace
for x, y being Point of X
for z, t being Point of (MetricSpaceNorm (RUSp2RNSp X)) st x = z & y = t holds
||.(x - y).|| = dist (z,t)

proof end;

theorem Th2: :: RUSUB_7:2

for X being RealUnitarySpace
for z being Element of (MetricSpaceNorm (RUSp2RNSp X))
for r being Real ex x being Point of X st
( x = z & Ball (z,r) = { y where y is Point of X : ||.(x - y).|| < r } )

proof end;

theorem Th3: :: RUSUB_7:3

for X being RealUnitarySpace
for z being Element of (MetricSpaceNorm (RUSp2RNSp X))
for r being Real ex x being Point of X st
( x = z & cl_Ball (z,r) = { y where y is Point of X : ||.(x - y).|| <= r } )

proof end;

theorem Th4: :: RUSUB_7:4

for X being RealUnitarySpace
for S being sequence of X
for St being sequence of (MetricSpaceNorm (RUSp2RNSp X))
for x being Point of X
for xt being Point of (MetricSpaceNorm (RUSp2RNSp X)) st S = St & x = xt holds
( St is_convergent_in_metrspace_to xt iff for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((S . n) - x).|| < r )

proof end;

theorem Th5: :: RUSUB_7:5

for X being RealUnitarySpace
for S being sequence of X
for St being sequence of (MetricSpaceNorm (RUSp2RNSp X)) st S = St holds
( St is convergent iff S is convergent )

proof end;

theorem Th6: :: RUSUB_7:6

for X being RealUnitarySpace
for S being sequence of X
for St being sequence of (MetricSpaceNorm (RUSp2RNSp X)) st S = St & St is convergent holds
lim St = lim S

proof end;

theorem :: RUSUB_7:7

for X being RealUnitarySpace
for V being Subset of (TopSpaceNorm (RUSp2RNSp X)) holds
( V is open iff for x being Point of X st x in V holds
ex r being Real st
( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V ) )

proof end;

theorem :: RUSUB_7:8

for X being RealUnitarySpace
for x being Point of X
for r being Real holds { y where y is Point of X : ||.(x - y).|| < r } is open Subset of (TopSpaceNorm (RUSp2RNSp X))

proof end;

theorem :: RUSUB_7:9

for X being RealUnitarySpace
for x being Point of X
for r being Real holds { y where y is Point of X : ||.(x - y).|| <= r } is closed Subset of (TopSpaceNorm (RUSp2RNSp X))

proof end;

theorem Th10: :: RUSUB_7:10

for M being RealUnitarySpace
for X being Subset of (TopSpaceNorm (RUSp2RNSp M))
for x being object holds
( x in Cl X iff ex S being sequence of M st
( ( for n being Nat holds S . n in X ) & S is convergent & lim S = x ) )

proof end;

theorem Th11: :: RUSUB_7:11

for M being RealUnitarySpace
for X being Subset of (TopSpaceNorm (RUSp2RNSp M)) holds
( X is closed iff for S being sequence of M st ( for n being Nat holds S . n in X ) & S is convergent holds
lim S in X )

proof end;

theorem Th12: :: RUSUB_7:12

for S being RealUnitarySpace
for X being Subset of S holds
( X is closed Subset of (TopSpaceNorm (RUSp2RNSp S)) iff for s1 being sequence of S st rng s1 c= X & s1 is convergent holds
lim s1 in X )

proof end;

theorem Th13: :: RUSUB_7:13

for S being RealUnitarySpace
for x being Point of S
for y being Point of (MetricSpaceNorm (RUSp2RNSp S))
for r being Real st x = y holds
Ball (x,r) = Ball (y,r)

proof end;

theorem :: RUSUB_7:14

for S being RealUnitarySpace holds TopSpaceNorm (RUSp2RNSp S) = TopUnitSpace S

proof end;

theorem :: RUSUB_7:15

for S being RealUnitarySpace
for U being Subset of S
for V being Subset of (TopSpaceNorm (RUSp2RNSp S)) st U = V holds
( U is closed iff V is closed )

proof end;

theorem :: RUSUB_7:16

for S being RealUnitarySpace
for U being Subset of S
for V being Subset of (TopSpaceNorm (RUSp2RNSp S)) st U = V holds
( U is open iff V is open )

proof end;

Lm1: for X being RealUnitarySpace
for x being Point of X holds ||.x.|| ^2 = x .|. x

proof end;

Lm2: for X being RealUnitarySpace
for M being Subspace of X
for x, m0 being Point of X st m0 in M & ( for m being Point of X st m in M holds
||.(x - m0).|| <= ||.(x - m).|| ) holds
for m being Point of X st m in M holds
(x - m0) .|. m = 0

proof end;

theorem Th17: :: RUSUB_7:17

for X being RealUnitarySpace
for M being Subspace of X
for x, m0 being Point of X st m0 in M holds
( ( for m being Point of X st m in M holds
||.(x - m0).|| <= ||.(x - m).|| ) iff for m being Point of X st m in M holds
(x - m0) .|. m = 0 )

proof end;

theorem :: RUSUB_7:18

for X being RealUnitarySpace
for M being Subspace of X
for x, m1, m2 being Point of X st m1 in M & m2 in M & ( for m being Point of X st m in M holds
||.(x - m1).|| <= ||.(x - m).|| ) & ( for m being Point of X st m in M holds
||.(x - m2).|| <= ||.(x - m).|| ) holds
m1 = m2

proof end;

theorem Th19: :: RUSUB_7:19

for X being RealHilbertSpace
for M being Subspace of X
for x being Point of X st the carrier of M is closed Subset of (TopSpaceNorm (RUSp2RNSp X)) holds
ex m0 being Point of X st
( m0 in M & ( for m being Point of X st m in M holds
||.(x - m0).|| <= ||.(x - m).|| ) )

proof end;

definition

let X be RealUnitarySpace;
let M be Subset of X;

func Ort_CompSet M -> non empty Subset of X means :Def1: :: RUSUB_7:def 1
for x being Point of X holds
( x in it iff for y being Point of X st y in M holds
y .|. x = 0 );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines Ort_CompSet RUSUB_7:def 1 :

theorem :: RUSUB_7:20

for X being RealUnitarySpace
for M being Subset of X holds Ort_CompSet M is linearly-closed

proof end;

Lm3: for X being RealUnitarySpace
for M being Subset of X holds Ort_CompSet M = { v where v is VECTOR of X : for w being VECTOR of X st w in M holds
w,v are_orthogonal }

proof end;

Lm4: for X being RealUnitarySpace
for M being Subspace of X
for N being non empty Subset of X st N = the carrier of M holds
Ort_CompSet N = { v where v is VECTOR of X : for w being VECTOR of X st w in M holds
w,v are_orthogonal }

proof end;

Lm5: for X being RealUnitarySpace
for M being non empty Subset of X
for H being strict Subspace of X holds
( H = Ort_Comp M iff the carrier of H = Ort_CompSet M )

proof end;

theorem Th21: :: RUSUB_7:21

for X being RealUnitarySpace
for M being non empty Subset of X
for seq being sequence of X st rng seq c= the carrier of (Ort_Comp M) & seq is convergent holds
lim seq in the carrier of (Ort_Comp M)

proof end;

theorem Th22: :: RUSUB_7:22

for S being RealUnitarySpace
for M being non empty Subset of S
for L being Subset of S st L = the carrier of (Ort_Comp M) holds
L is closed Subset of (TopSpaceNorm (RUSp2RNSp S))

proof end;

Lm6: for X being RealUnitarySpace
for M being Subspace of X
for H being strict Subspace of X holds
( H = Ort_Comp M iff ex N being non empty Subset of X st
( N = the carrier of M & H = Ort_Comp N ) )

proof end;

theorem Th23: :: RUSUB_7:23

for X being RealUnitarySpace
for M being non empty Subset of X holds M is Subset of (Ort_Comp (Ort_Comp M))

proof end;

theorem Th24: :: RUSUB_7:24

for X being RealUnitarySpace
for S, T being non empty Subset of X st S c= T holds
Ort_Comp T is Subspace of Ort_Comp S

proof end;

theorem Th25: :: RUSUB_7:25

for X being RealHilbertSpace
for M being Subspace of X st X is strict & the carrier of M is closed Subset of (TopSpaceNorm (RUSp2RNSp X)) holds
X is_the_direct_sum_of M, Ort_Comp M

proof end;

theorem Th26: :: RUSUB_7:26

for X being RealHilbertSpace
for M being strict Subspace of X st X is strict & the carrier of M is closed Subset of (TopSpaceNorm (RUSp2RNSp X)) holds
M = Ort_Comp (Ort_Comp M)

proof end;

theorem Th27: :: RUSUB_7:27

for X being RealUnitarySpace
for M being Subspace of X
for K being Subset of X
for L being Subset of (TopSpaceNorm (RUSp2RNSp X)) st the carrier of M = L & K = Cl L holds
K is linearly-closed

proof end;

Lm7: for X being RealHilbertSpace
for M, L being non empty Subset of X
for TL being Subset of (TopSpaceNorm (RUSp2RNSp X)) st X is strict & L = the carrier of (Lin M) & TL = L holds
the carrier of (Ort_Comp (Ort_Comp M)) = Cl TL

proof end;

theorem :: RUSUB_7:28

for X being RealHilbertSpace
for M being non empty Subset of X st X is strict holds
( the carrier of (Ort_Comp (Ort_Comp M)) is closed Subset of (TopSpaceNorm (RUSp2RNSp X)) & ex L being Subset of (TopSpaceNorm (RUSp2RNSp X)) st
( L = the carrier of (Lin M) & the carrier of (Ort_Comp (Ort_Comp M)) = Cl L ) & Lin M is Subspace of Ort_Comp (Ort_Comp M) )

proof end;

theorem :: RUSUB_7:29

for X being RealHilbertSpace
for K being strict Subspace of X
for M being non empty Subset of X st X is strict & the carrier of K is closed Subset of (TopSpaceNorm (RUSp2RNSp X)) & Lin M is Subspace of K holds
Ort_Comp (Ort_Comp M) is Subspace of K

proof end;