begin
set X = {0};
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:28;
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 8;
set f = {[[0,0],P]};
dom {[[0,0],P]} = {[0,0]}
by RELAT_1:9;
then Lm5:
dom {[[0,0],P]} = [:{0},{0}:]
by ZFMISC_1:29;
( rng {[[0,0],P]} = {P} & P in Probabilities Borel_Sets )
by Def1, RELAT_1:9;
then
rng {[[0,0],P]} c= Probabilities Borel_Sets
by ZFMISC_1:31;
then reconsider Y = {[[0,0],P]} as Function of [:{0},{0}:],(Probabilities Borel_Sets) by Lm5, FUNCT_2:def 1, RELSET_1:4;
Lm6:
now ( ( for A1, A2 being Element of Obs QM_Str(# {0},{0},Y #) st ( for s being Element of Sts QM_Str(# {0},{0},Y #) holds Meas (A1,s) = Meas (A2,s) ) holds
A1 = A2 ) & ( for s1, s2 being Element of Sts QM_Str(# {0},{0},Y #) st ( for A being Element of Obs QM_Str(# {0},{0},Y #) holds Meas (A,s1) = Meas (A,s2) ) holds
s1 = s2 ) & ( for s1, s2 being Element of Sts QM_Str(# {0},{0},Y #)
for t being Real st 0 <= t & t <= 1 holds
ex s being Element of Sts QM_Str(# {0},{0},Y #) st
for A being Element of Obs QM_Str(# {0},{0},Y #)
for E being Event of Borel_Sets holds (Meas (A,s)) . E = (t * ((Meas (A,s1)) . E)) + ((1 - t) * ((Meas (A,s2)) . E)) ) )
thus
for
A1,
A2 being
Element of
Obs QM_Str(#
{0},
{0},
Y #) st ( for
s being
Element of
Sts QM_Str(#
{0},
{0},
Y #) holds
Meas (
A1,
s)
= Meas (
A2,
s) ) holds
A1 = A2
( ( for s1, s2 being Element of Sts QM_Str(# {0},{0},Y #) st ( for A being Element of Obs QM_Str(# {0},{0},Y #) holds Meas (A,s1) = Meas (A,s2) ) holds
s1 = s2 ) & ( for s1, s2 being Element of Sts QM_Str(# {0},{0},Y #)
for t being Real st 0 <= t & t <= 1 holds
ex s being Element of Sts QM_Str(# {0},{0},Y #) st
for A being Element of Obs QM_Str(# {0},{0},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(#
{0},
{0},
Y #);
( ( for s being Element of Sts QM_Str(# {0},{0},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(#
{0},
{0},
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(#
{0},
{0},
Y #) st ( for
A being
Element of
Obs QM_Str(#
{0},
{0},
Y #) holds
Meas (
A,
s1)
= Meas (
A,
s2) ) holds
s1 = s2
for s1, s2 being Element of Sts QM_Str(# {0},{0},Y #)
for t being Real st 0 <= t & t <= 1 holds
ex s being Element of Sts QM_Str(# {0},{0},Y #) st
for A being Element of Obs QM_Str(# {0},{0},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(#
{0},
{0},
Y #);
( ( for A being Element of Obs QM_Str(# {0},{0},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(#
{0},
{0},
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(#
{0},
{0},
Y #)
for
t being
Real st
0 <= t &
t <= 1 holds
ex
s being
Element of
Sts QM_Str(#
{0},
{0},
Y #) st
for
A being
Element of
Obs QM_Str(#
{0},
{0},
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(#
{0},
{0},
Y #);
for t being Real st 0 <= t & t <= 1 holds
ex s being Element of Sts QM_Str(# {0},{0},Y #) st
for A being Element of Obs QM_Str(# {0},{0},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(# {0},{0},Y #) st
for A being Element of Obs QM_Str(# {0},{0},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(# {0},{0},Y #) st
for A being Element of Obs QM_Str(# {0},{0},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(# {0},{0},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(#
{0},
{0},
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)) ) ) );
definition
let Q be
Quantum_Mechanics;
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;