:: Formalization of Orthogonal Complements of Normed Spaces
:: by Hiroyuki Okazaki
::
:: Received November 28, 2024
:: Copyright (c) 2024-2025 Association of Mizar Users

Lm1: for a, b being Real st 0 < a & ( for e being Real st 0 < e holds
((a + e) ") * a <= b ) holds
1 <= b

proof end;

definition

let V be RealNormSpace;
let W be Subspace of V;

func RSubNormSpace W -> strict RealNormSpace means :Def1: :: DUALSP06:def 1
( RLSStruct(# the carrier of it, the ZeroF of it, the addF of it, the Mult of it #) = RLSStruct(# the carrier of W, the ZeroF of W, the addF of W, the Mult of W #) & the normF of it = the normF of V | the carrier of it );

existence
ex b₁ being strict RealNormSpace st
( RLSStruct(# the carrier of b₁, the ZeroF of b₁, the addF of b₁, the Mult of b₁ #) = RLSStruct(# the carrier of W, the ZeroF of W, the addF of W, the Mult of W #) & the normF of b₁ = the normF of V | the carrier of b₁ )

proof end;

uniqueness
for b₁, b₂ being strict RealNormSpace st RLSStruct(# the carrier of b₁, the ZeroF of b₁, the addF of b₁, the Mult of b₁ #) = RLSStruct(# the carrier of W, the ZeroF of W, the addF of W, the Mult of W #) & the normF of b₁ = the normF of V | the carrier of b₁ & RLSStruct(# the carrier of b₂, the ZeroF of b₂, the addF of b₂, the Mult of b₂ #) = RLSStruct(# the carrier of W, the ZeroF of W, the addF of W, the Mult of W #) & the normF of b₂ = the normF of V | the carrier of b₂ holds
b₁ = b₂ ;

end;

:: deftheorem Def1 defines RSubNormSpace DUALSP06:def 1 :
for V being RealNormSpace
for W being Subspace of V
for b₃ being strict RealNormSpace holds
( b₃ = RSubNormSpace W iff ( RLSStruct(# the carrier of b₃, the ZeroF of b₃, the addF of b₃, the Mult of b₃ #) = RLSStruct(# the carrier of W, the ZeroF of W, the addF of W, the Mult of W #) & the normF of b₃ = the normF of V | the carrier of b₃ ) );

theorem Th1: :: DUALSP06:1

for V being RealNormSpace
for W being Subspace of V holds RSubNormSpace W is SubRealNormSpace of V

proof end;

definition

let V be RealNormSpace;
let x be Point of V;
let y be Point of (DualSp V);

func x .|. y -> Real equals :: DUALSP06:def 2
y . x;

correctness
coherence
y . x is Real;
;

end;

:: deftheorem defines .|. DUALSP06:def 2 :
for V being RealNormSpace
for x being Point of V
for y being Point of (DualSp V) holds x .|. y = y . x;

theorem Th2: :: DUALSP06:2

for V being RealNormSpace
for x being Point of V
for y being Point of (DualSp V) holds |.(x .|. y).| <= ||.y.|| * ||.x.||

proof end;

definition

let V be RealNormSpace;
let x be Point of V;
let y be Point of (DualSp V);

pred x,y are_orthogonal means :: DUALSP06:def 3
x .|. y = 0 ;

end;

:: deftheorem defines are_orthogonal DUALSP06:def 3 :
for V being RealNormSpace
for x being Point of V
for y being Point of (DualSp V) holds
( x,y are_orthogonal iff x .|. y = 0 );

theorem :: DUALSP06:3

for V being RealNormSpace
for x being Point of V
for y, z being Point of (DualSp V) holds x .|. (y + z) = (x .|. y) + (x .|. z) by DUALSP01:29;

theorem :: DUALSP06:4

for V being RealNormSpace
for x being Point of V
for y being Point of (DualSp V)
for a being Real holds x .|. (a * y) = a * (x .|. y) by DUALSP01:30;

theorem Th5: :: DUALSP06:5

for V being RealNormSpace
for x, y being Point of V
for z being Point of (DualSp V) holds (x + y) .|. z = (x .|. z) + (y .|. z)

proof end;

theorem Th6: :: DUALSP06:6

for V being RealNormSpace
for x being Point of V
for y being Point of (DualSp V)
for a being Real holds (a * x) .|. y = a * (x .|. y)

proof end;

theorem :: DUALSP06:7

for V being RealNormSpace
for x being Point of V
for y, z being Point of (DualSp V)
for a, b being Real holds x .|. ((a * y) + (b * z)) = (a * (x .|. y)) + (b * (x .|. z))

proof end;

theorem :: DUALSP06:8

for V being RealNormSpace
for y, z being Point of V
for x being Point of (DualSp V)
for a, b being Real holds ((a * y) + (b * z)) .|. x = (a * (y .|. x)) + (b * (z .|. x))

proof end;

theorem Th9: :: DUALSP06:9

for V being RealNormSpace
for x being Point of V
for y being Point of (DualSp V) holds x .|. (- y) = - (x .|. y)

proof end;

theorem Th10: :: DUALSP06:10

for V being RealNormSpace
for x being Point of V
for y being Point of (DualSp V) holds (- x) .|. y = - (x .|. y)

proof end;

theorem :: DUALSP06:11

for V being RealNormSpace
for x being Point of V
for y being Point of (DualSp V) holds (- x) .|. (- y) = x .|. y

proof end;

theorem Th12: :: DUALSP06:12

for V being RealNormSpace
for x being Point of V
for y, z being Point of (DualSp V) holds x .|. (y - z) = (x .|. y) - (x .|. z)

proof end;

theorem Th13: :: DUALSP06:13

for V being RealNormSpace
for y, z being Point of V
for x being Point of (DualSp V) holds (y - z) .|. x = (y .|. x) - (z .|. x)

proof end;

theorem Th14: :: DUALSP06:14

for V being RealNormSpace
for x being Point of V holds x .|. (0. (DualSp V)) = 0

proof end;

theorem Th15: :: DUALSP06:15

for V being RealNormSpace
for x being Point of (DualSp V) holds (0. V) .|. x = 0

proof end;

definition

let V be RealNormSpace;
let x be Point of V;
let y be Point of (DualSp V);

pred x,y are_parallel means :: DUALSP06:def 4
x .|. y = ||.x.|| * ||.y.||;

end;

:: deftheorem defines are_parallel DUALSP06:def 4 :
for V being RealNormSpace
for x being Point of V
for y being Point of (DualSp V) holds
( x,y are_parallel iff x .|. y = ||.x.|| * ||.y.|| );

definition

let V be RealNormSpace;
let W be Subspace of V;

func Ort_Comp W -> strict Subspace of DualSp V means :Def5: :: DUALSP06:def 5
the carrier of it = { v where v is VECTOR of (DualSp V) : for w being VECTOR of V st w in W holds
w,v are_orthogonal } ;

existence
ex b₁ being strict Subspace of DualSp V st the carrier of b₁ = { v where v is VECTOR of (DualSp V) : for w being VECTOR of V st w in W holds
w,v are_orthogonal }

proof end;

uniqueness
for b₁, b₂ being strict Subspace of DualSp V st the carrier of b₁ = { v where v is VECTOR of (DualSp V) : for w being VECTOR of V st w in W holds
w,v are_orthogonal } & the carrier of b₂ = { v where v is VECTOR of (DualSp V) : for w being VECTOR of V st w in W holds
w,v are_orthogonal } holds
b₁ = b₂ by RLSUB_1:30;

end;

:: deftheorem Def5 defines Ort_Comp DUALSP06:def 5 :
for V being RealNormSpace
for W being Subspace of V
for b₃ being strict Subspace of DualSp V holds
( b₃ = Ort_Comp W iff the carrier of b₃ = { v where v is VECTOR of (DualSp V) : for w being VECTOR of V st w in W holds
w,v are_orthogonal } );

definition

let V be RealNormSpace;
let W be Subspace of DualSp V;

func Ort_Comp W -> strict Subspace of V means :Def6: :: DUALSP06:def 6
the carrier of it = { v where v is VECTOR of V : for w being VECTOR of (DualSp V) st w in W holds
v,w are_orthogonal } ;

existence
ex b₁ being strict Subspace of V st the carrier of b₁ = { v where v is VECTOR of V : for w being VECTOR of (DualSp V) st w in W holds
v,w are_orthogonal }

proof end;

uniqueness
for b₁, b₂ being strict Subspace of V st the carrier of b₁ = { v where v is VECTOR of V : for w being VECTOR of (DualSp V) st w in W holds
v,w are_orthogonal } & the carrier of b₂ = { v where v is VECTOR of V : for w being VECTOR of (DualSp V) st w in W holds
v,w are_orthogonal } holds
b₁ = b₂ by RLSUB_1:30;

end;

:: deftheorem Def6 defines Ort_Comp DUALSP06:def 6 :
for V being RealNormSpace
for W being Subspace of DualSp V
for b₃ being strict Subspace of V holds
( b₃ = Ort_Comp W iff the carrier of b₃ = { v where v is VECTOR of V : for w being VECTOR of (DualSp V) st w in W holds
v,w are_orthogonal } );

theorem Th16: :: DUALSP06:16

for V being RealNormSpace
for M being Subspace of V
for v being VECTOR of (DualSp V)
for m being VECTOR of V st v in Ort_Comp M & m in M holds
m .|. v = 0

proof end;

theorem :: DUALSP06:17

for V being RealNormSpace
for M being Subspace of DualSp V
for v being VECTOR of V
for m being VECTOR of (DualSp V) st v in Ort_Comp M & m in M holds
v .|. m = 0

proof end;

theorem Th18: :: DUALSP06:18

for X being RealNormSpace
for x being Point of X
for M being non empty Subspace of X holds { ||.(x - m).|| where m is Point of X : m in M } is non empty real-membered bounded_below set

proof end;

theorem Th19: :: DUALSP06:19

for X being RealNormSpace
for x being Point of X
for M being non empty Subspace of X holds { (x .|. y) where y is Point of (DualSp X) : ( y in Ort_Comp M & ||.y.|| <= 1 ) } is non empty real-membered bounded_above set

proof end;

theorem Th20: :: DUALSP06:20

for X being RealNormSpace
for x being Point of X
for M being non empty Subspace of X
for F, K being FinSequence of the carrier of X
for G being FinSequence of REAL st len G = len F & len K = len F & ( for i being Nat st i in dom F holds
F . i in x + M ) & ( for i being Nat st i in dom K holds
K . i = (G /. i) * (F /. i) ) holds
Sum K in { ((a * x) + m) where a is Real, m is Point of X : m in M }

proof end;

theorem Th21: :: DUALSP06:21

for V being RealNormSpace
for x being Point of V
for M being non empty Subspace of V st not x in M holds
ex L being non empty real-membered bounded_below set ex U being non empty real-membered bounded_above set st
( L = { ||.(x - m).|| where m is Point of V : m in M } & U = { (x .|. y) where y is Point of (DualSp V) : ( y in Ort_Comp M & ||.y.|| <= 1 ) } & inf L = sup U & sup U in U & ( 0 < inf L implies ex v being Point of (DualSp V) st
( ||.v.|| = 1 & v in Ort_Comp M & x .|. v = inf L ) ) & ( for m0 being Point of V st m0 in M & ||.(x - m0).|| = inf L holds
for v being Point of (DualSp V) st ||.v.|| = 1 & v in Ort_Comp M & x .|. v = inf L holds
x - m0,v are_parallel ) )

proof end;

theorem :: DUALSP06:22

for V being RealNormSpace
for x, m0 being Point of V
for M being non empty Subspace of V st not x in M & m0 in M holds
( ( for m being Point of V st m in M holds
||.(x - m0).|| <= ||.(x - m).|| ) iff ex p being Point of (DualSp V) st
( p in Ort_Comp M & p <> 0. (DualSp V) & x - m0,p are_parallel ) )

proof end;

theorem Th23: :: DUALSP06:23

for X being RealNormSpace
for x being Point of (DualSp X)
for M being non empty Subspace of X holds { ||.(x - m).|| where m is Point of (DualSp X) : m in Ort_Comp M } is non empty real-membered bounded_below set

proof end;

theorem Th24: :: DUALSP06:24

for X being RealNormSpace
for x being Point of (DualSp X)
for M being non empty Subspace of X holds { (y .|. x) where y is Point of X : ( y in M & ||.y.|| <= 1 ) } is non empty real-membered bounded_above set

proof end;

theorem :: DUALSP06:25

for V being RealNormSpace
for x being Point of (DualSp V)
for M being non empty Subspace of V
for SM being SubRealNormSpace of V st SM = RSubNormSpace M holds
ex L being non empty real-membered bounded_below set ex U being non empty real-membered bounded_above set st
( L = { ||.(x - m).|| where m is Point of (DualSp V) : m in Ort_Comp M } & U = { (y .|. x) where y is Point of V : ( y in M & ||.y.|| <= 1 ) } & ex m0 being Point of (DualSp V) ex fx being Lipschitzian linear-Functional of V ex xM being Point of (DualSp SM) st
( x = fx & xM = fx | the carrier of SM & m0 in Ort_Comp M & ||.(x - m0).|| = inf L & inf L in L & ||.(x - m0).|| = ||.xM.|| & ( for y being Point of V st ||.y.|| = 1 & y in M & fx . y = ||.(x - m0).|| holds
y,x - m0 are_parallel ) ) )

proof end;