begin
:: deftheorem Def1 defines Probabilities QMAX_1:def 1 :
:: deftheorem defines Obs QMAX_1:def 2 :
:: deftheorem defines Sts QMAX_1:def 3 :
:: deftheorem defines Meas QMAX_1:def 4 :
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 :
:: deftheorem Def7 defines is_a_Quantum_Logic QMAX_1:def 7 :
:: deftheorem defines Prop QMAX_1:def 8 :
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 :
:: deftheorem Def10 defines |- QMAX_1:def 10 :
:: deftheorem Def11 defines <==> QMAX_1:def 11 :
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 :
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 :
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 :
theorem
canceled;
theorem