begin
:: deftheorem Def1 defines Probabilities QMAX_1:def 1 :
for X being non empty set
for S being SigmaField of X
for b3 being set holds
( b3 = Probabilities S iff for x being set holds
( x in b3 iff x is Probability of S ) );
:: deftheorem defines Obs QMAX_1:def 2 :
for Q being QM_Str holds Obs Q = the Observables of Q;
:: deftheorem defines Sts QMAX_1:def 3 :
for Q being QM_Str holds Sts Q = the FStates of Q;
:: deftheorem defines Meas QMAX_1:def 4 :
for Q being QM_Str
for A1 being Element of Obs Q
for s being Element of Sts Q holds Meas A1,s = the Quantum_Probability of Q . [A1,s];
reconsider X = {0 } as non empty set ;
consider P being Function of Borel_Sets ,REAL such that
Lm1:
for D being Subset of REAL st D in Borel_Sets holds
( ( 0 in D implies P . D = 1 ) & ( not 0 in D implies P . D = 0 ) )
by PROB_1:60;
Lm2:
for A being Event of Borel_Sets holds 0 <= P . A
Lm3:
P . REAL = 1
Lm4:
for A, B being Event of Borel_Sets st A misses B holds
P . (A \/ B) = (P . A) + (P . B)
for ASeq being SetSequence of Borel_Sets st ASeq is non-ascending holds
( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) )
then reconsider P = P as Probability of Borel_Sets by Lm2, Lm3, Lm4, PROB_1:def 13;
reconsider f = {[[0 ,0 ],P]} as Function by GRFUNC_1:15;
dom f = {[0 ,0 ]}
by RELAT_1:23;
then Lm5:
dom f = [:X,X:]
by ZFMISC_1:35;
( rng f = {P} & P in Probabilities Borel_Sets )
by Def1, RELAT_1:23;
then
rng f c= Probabilities Borel_Sets
by ZFMISC_1:37;
then reconsider Y = f as Function of [:X,X:],(Probabilities Borel_Sets ) by Lm5, FUNCT_2:def 1, RELSET_1:11;
Lm6:
now
thus
for
A1,
A2 being
Element of
Obs QM_Str(#
X,
X,
Y #) st ( for
s being
Element of
Sts QM_Str(#
X,
X,
Y #) holds
Meas A1,
s = Meas A2,
s ) holds
A1 = A2
( ( for s1, s2 being Element of Sts QM_Str(# X,X,Y #) st ( for A being Element of Obs QM_Str(# X,X,Y #) holds Meas A,s1 = Meas A,s2 ) holds
s1 = s2 ) & ( for s1, s2 being Element of Sts QM_Str(# X,X,Y #)
for t being Real st 0 <= t & t <= 1 holds
ex s being Element of Sts QM_Str(# X,X,Y #) st
for A being Element of Obs QM_Str(# X,X,Y #)
for E being Event of Borel_Sets holds (Meas A,s) . E = (t * ((Meas A,s1) . E)) + ((1 - t) * ((Meas A,s2) . E)) ) )
proof
let A1,
A2 be
Element of
Obs QM_Str(#
X,
X,
Y #);
( ( for s being Element of Sts QM_Str(# X,X,Y #) holds Meas A1,s = Meas A2,s ) implies A1 = A2 )
A1 = 0
by TARSKI:def 1;
hence
( ( for
s being
Element of
Sts QM_Str(#
X,
X,
Y #) holds
Meas A1,
s = Meas A2,
s ) implies
A1 = A2 )
by TARSKI:def 1;
verum
end;
thus
for
s1,
s2 being
Element of
Sts QM_Str(#
X,
X,
Y #) st ( for
A being
Element of
Obs QM_Str(#
X,
X,
Y #) holds
Meas A,
s1 = Meas A,
s2 ) holds
s1 = s2
for s1, s2 being Element of Sts QM_Str(# X,X,Y #)
for t being Real st 0 <= t & t <= 1 holds
ex s being Element of Sts QM_Str(# X,X,Y #) st
for A being Element of Obs QM_Str(# X,X,Y #)
for E being Event of Borel_Sets holds (Meas A,s) . E = (t * ((Meas A,s1) . E)) + ((1 - t) * ((Meas A,s2) . E))
proof
let s1,
s2 be
Element of
Sts QM_Str(#
X,
X,
Y #);
( ( for A being Element of Obs QM_Str(# X,X,Y #) holds Meas A,s1 = Meas A,s2 ) implies s1 = s2 )
s1 = 0
by TARSKI:def 1;
hence
( ( for
A being
Element of
Obs QM_Str(#
X,
X,
Y #) holds
Meas A,
s1 = Meas A,
s2 ) implies
s1 = s2 )
by TARSKI:def 1;
verum
end;
thus
for
s1,
s2 being
Element of
Sts QM_Str(#
X,
X,
Y #)
for
t being
Real st
0 <= t &
t <= 1 holds
ex
s being
Element of
Sts QM_Str(#
X,
X,
Y #) st
for
A being
Element of
Obs QM_Str(#
X,
X,
Y #)
for
E being
Event of
Borel_Sets holds
(Meas A,s) . E = (t * ((Meas A,s1) . E)) + ((1 - t) * ((Meas A,s2) . E))
verum
proof
let s1,
s2 be
Element of
Sts QM_Str(#
X,
X,
Y #);
for t being Real st 0 <= t & t <= 1 holds
ex s being Element of Sts QM_Str(# X,X,Y #) st
for A being Element of Obs QM_Str(# X,X,Y #)
for E being Event of Borel_Sets holds (Meas A,s) . E = (t * ((Meas A,s1) . E)) + ((1 - t) * ((Meas A,s2) . E))let t be
Real;
( 0 <= t & t <= 1 implies ex s being Element of Sts QM_Str(# X,X,Y #) st
for A being Element of Obs QM_Str(# X,X,Y #)
for E being Event of Borel_Sets holds (Meas A,s) . E = (t * ((Meas A,s1) . E)) + ((1 - t) * ((Meas A,s2) . E)) )
assume
(
0 <= t &
t <= 1 )
;
ex s being Element of Sts QM_Str(# X,X,Y #) st
for A being Element of Obs QM_Str(# X,X,Y #)
for E being Event of Borel_Sets holds (Meas A,s) . E = (t * ((Meas A,s1) . E)) + ((1 - t) * ((Meas A,s2) . E))
take
s2
;
for A being Element of Obs QM_Str(# X,X,Y #)
for E being Event of Borel_Sets holds (Meas A,s2) . E = (t * ((Meas A,s1) . E)) + ((1 - t) * ((Meas A,s2) . E))
let A be
Element of
Obs QM_Str(#
X,
X,
Y #);
for E being Event of Borel_Sets holds (Meas A,s2) . E = (t * ((Meas A,s1) . E)) + ((1 - t) * ((Meas A,s2) . E))let E be
Event of
Borel_Sets ;
(Meas A,s2) . E = (t * ((Meas A,s1) . E)) + ((1 - t) * ((Meas A,s2) . E))
(
s1 = 0 &
s2 = 0 )
by TARSKI:def 1;
hence
(Meas A,s2) . E = (t * ((Meas A,s1) . E)) + ((1 - t) * ((Meas A,s2) . E))
;
verum
end;
end;
definition
let IT be
QM_Str ;
attr IT is
Quantum_Mechanics-like means :
Def5:
( ( for
A1,
A2 being
Element of
Obs IT st ( for
s being
Element of
Sts IT holds
Meas A1,
s = Meas A2,
s ) holds
A1 = A2 ) & ( for
s1,
s2 being
Element of
Sts IT st ( for
A being
Element of
Obs IT holds
Meas A,
s1 = Meas A,
s2 ) holds
s1 = s2 ) & ( for
s1,
s2 being
Element of
Sts IT for
t being
Real st
0 <= t &
t <= 1 holds
ex
s being
Element of
Sts IT st
for
A being
Element of
Obs IT for
E being
Event of
Borel_Sets holds
(Meas A,s) . E = (t * ((Meas A,s1) . E)) + ((1 - t) * ((Meas A,s2) . E)) ) );
end;
:: deftheorem Def5 defines Quantum_Mechanics-like QMAX_1:def 5 :
for IT being QM_Str holds
( IT is Quantum_Mechanics-like iff ( ( for A1, A2 being Element of Obs IT st ( for s being Element of Sts IT holds Meas A1,s = Meas A2,s ) holds
A1 = A2 ) & ( for s1, s2 being Element of Sts IT st ( for A being Element of Obs IT holds Meas A,s1 = Meas A,s2 ) holds
s1 = s2 ) & ( for s1, s2 being Element of Sts IT
for t being Real st 0 <= t & t <= 1 holds
ex s being Element of Sts IT st
for A being Element of Obs IT
for E being Event of Borel_Sets holds (Meas A,s) . E = (t * ((Meas A,s1) . E)) + ((1 - t) * ((Meas A,s2) . E)) ) ) );
:: deftheorem defines is_an_involution QMAX_1:def 6 :
for X1 being set
for Inv being Function of X1,X1 holds
( Inv is_an_involution iff for x1 being Element of X1 holds Inv . (Inv . x1) = x1 );
:: deftheorem Def7 defines is_a_Quantum_Logic QMAX_1:def 7 :
for W being OrthoRelStr holds
( W is_a_Quantum_Logic iff ( the InternalRel of W partially_orders the carrier of W & the Compl of W is_an_involution & ( for x, y being Element of W st [x,y] in the InternalRel of W holds
[(the Compl of W . y),(the Compl of W . x)] in the InternalRel of W ) ) );
:: deftheorem defines Prop QMAX_1:def 8 :
for Q being Quantum_Mechanics holds Prop Q = [:(Obs Q),Borel_Sets :];
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th16:
:: deftheorem defines 'not' QMAX_1:def 9 :
for Q being Quantum_Mechanics
for p being Element of Prop Q holds 'not' p = [(p `1 ),((p `2 ) ` )];
:: deftheorem Def10 defines |- QMAX_1:def 10 :
for Q being Quantum_Mechanics
for p, q being Element of Prop Q holds
( p |- q iff for s being Element of Sts Q holds (Meas (p `1 ),s) . (p `2 ) <= (Meas (q `1 ),s) . (q `2 ) );
:: deftheorem Def11 defines <==> QMAX_1:def 11 :
for Q being Quantum_Mechanics
for p, q being Element of Prop Q holds
( p <==> q iff ( p |- q & q |- p ) );
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem
canceled;
theorem Th27:
theorem Th28:
:: deftheorem Def12 defines PropRel QMAX_1:def 12 :
for Q being Quantum_Mechanics
for b2 being Equivalence_Relation of (Prop Q) holds
( b2 = PropRel Q iff for p, q being Element of Prop Q holds
( [p,q] in b2 iff p <==> q ) );
theorem
canceled;
theorem Th30:
definition
let Q be
Quantum_Mechanics;
func OrdRel Q -> Relation of
(Class (PropRel Q)) means :
Def13:
for
B,
C being
Subset of
(Prop Q) holds
(
[B,C] in it iff (
B in Class (PropRel Q) &
C in Class (PropRel Q) & ( for
p,
q being
Element of
Prop Q st
p in B &
q in C holds
p |- q ) ) );
existence
ex b1 being Relation of (Class (PropRel Q)) st
for B, C being Subset of (Prop Q) holds
( [B,C] in b1 iff ( B in Class (PropRel Q) & C in Class (PropRel Q) & ( for p, q being Element of Prop Q st p in B & q in C holds
p |- q ) ) )
uniqueness
for b1, b2 being Relation of (Class (PropRel Q)) st ( for B, C being Subset of (Prop Q) holds
( [B,C] in b1 iff ( B in Class (PropRel Q) & C in Class (PropRel Q) & ( for p, q being Element of Prop Q st p in B & q in C holds
p |- q ) ) ) ) & ( for B, C being Subset of (Prop Q) holds
( [B,C] in b2 iff ( B in Class (PropRel Q) & C in Class (PropRel Q) & ( for p, q being Element of Prop Q st p in B & q in C holds
p |- q ) ) ) ) holds
b1 = b2
end;
:: deftheorem Def13 defines OrdRel QMAX_1:def 13 :
for Q being Quantum_Mechanics
for b2 being Relation of (Class (PropRel Q)) holds
( b2 = OrdRel Q iff for B, C being Subset of (Prop Q) holds
( [B,C] in b2 iff ( B in Class (PropRel Q) & C in Class (PropRel Q) & ( for p, q being Element of Prop Q st p in B & q in C holds
p |- q ) ) ) );
theorem
canceled;
theorem Th32:
theorem Th33:
theorem
definition
let Q be
Quantum_Mechanics;
func InvRel Q -> Function of
(Class (PropRel Q)),
(Class (PropRel Q)) means :
Def14:
for
p being
Element of
Prop Q holds
it . (Class (PropRel Q),p) = Class (PropRel Q),
('not' p);
existence
ex b1 being Function of (Class (PropRel Q)),(Class (PropRel Q)) st
for p being Element of Prop Q holds b1 . (Class (PropRel Q),p) = Class (PropRel Q),('not' p)
uniqueness
for b1, b2 being Function of (Class (PropRel Q)),(Class (PropRel Q)) st ( for p being Element of Prop Q holds b1 . (Class (PropRel Q),p) = Class (PropRel Q),('not' p) ) & ( for p being Element of Prop Q holds b2 . (Class (PropRel Q),p) = Class (PropRel Q),('not' p) ) holds
b1 = b2
end;
:: deftheorem Def14 defines InvRel QMAX_1:def 14 :
for Q being Quantum_Mechanics
for b2 being Function of (Class (PropRel Q)),(Class (PropRel Q)) holds
( b2 = InvRel Q iff for p being Element of Prop Q holds b2 . (Class (PropRel Q),p) = Class (PropRel Q),('not' p) );
theorem
canceled;
theorem