The Mizar article:

Probability

by
Andrzej Nedzusiak

Received June 1, 1990

Copyright (c) 1990 Association of Mizar Users

MML identifier: PROB_2
[ MML identifier index ]


environ

 vocabulary SEQ_1, PROB_1, ARYTM_3, RELAT_1, SEQ_2, FUNCT_1, ARYTM_1, ORDINAL2,
      ARYTM, ABSVALUE, BOOLE, SUBSET_1, PROB_2;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
      XREAL_0, RELAT_1, REAL_1, FUNCT_1, FUNCT_2, ABSVALUE, SEQ_1, SEQ_2,
      PROB_1, NAT_1;
 constructors REAL_1, ABSVALUE, SEQ_2, PROB_1, NAT_1, MEMBERED, XBOOLE_0;
 clusters SUBSET_1, XREAL_0, RELSET_1, ARYTM_3, MEMBERED, ZFMISC_1, XBOOLE_0,
      NUMBERS, ORDINAL2;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
 definitions PROB_1;
 theorems FUNCT_1, REAL_1, FUNCT_2, ABSVALUE, SEQ_1, SEQ_2, SUBSET_1, PROB_1,
      SQUARE_1, NAT_1, TARSKI, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1;
 schemes FUNCT_1, FUNCT_2, NAT_1;

begin

reserve Omega for non empty set;
reserve m,n,k for Nat;
reserve x,y,z for set;
reserve r,r1,r2,r3 for Real;
reserve seq,seq1 for Real_Sequence;
reserve Sigma for SigmaField of Omega;
reserve ASeq,BSeq for SetSequence of Sigma;
reserve P,P1,P2 for Probability of Sigma;
reserve A, B, C, A1, A2, A3 for Event of Sigma;

canceled 3;

theorem
Th4: for r,r1,r2,r3 st (r <> 0 & r1 <> 0) holds
  (r3/r1 = r2/r iff r3 * r = r2 * r1)
  proof let r,r1,r2,r3; assume that
 A1: r <> 0 and
 A2: r1 <> 0;
  thus r3/r1 = r2/r implies r3 * r = r2 * r1
    proof assume A3: r3/r1 = r2/r;
      r3 * r = r3/r1 * r1 * r by A2,XCMPLX_1:88
          .= r2/r * r * r1 by A3,XCMPLX_1:4
          .= r2 * r1 by A1,XCMPLX_1:88;
    hence thesis;
    end; assume A4: r3 * r = r2 * r1;
    r3/r1 = (r3 * 1)/r1
       .= (r3 * (r * r"))/r1 by A1,XCMPLX_0:def 7
       .= (r2 * r1 * r")/r1 by A4,XCMPLX_1:4
       .= (r2 * r" * r1)/r1 by XCMPLX_1:4
       .= (r2/r * r1)/r1 by XCMPLX_0:def 9
       .= (r2/r * r1) * r1" by XCMPLX_0:def 9
       .= r2/r * (r1 * r1") by XCMPLX_1:4
       .= r2/r * 1 by A2,XCMPLX_0:def 7
       .= r2/r;
  hence thesis;
  end;

theorem
Th5: (seq is convergent & for n holds seq1.n = r - seq.n) implies
  seq1 is convergent & lim seq1 = r - lim seq
  proof assume that
 A1: seq is convergent and
 A2: for n holds seq1.n = r - seq.n;
  consider r1 be real number such that
 A3: for r2 be real number st 0<r2
  ex n st for m st n<=m holds abs(seq.m-r1)<r2 by A1,SEQ_2:def 6;
 A4:now let r2 be real number; assume
      0 < r2; then consider n such that
   A5: for m st n <= m holds abs(seq.m - r1) < r2 by A3;
   A6:now let m such that
      A7: n <= m;
         abs(seq.m - r1) = abs(-(seq.m - r1)) by ABSVALUE:17
                     .= abs(r1 + 0 - seq.m) by XCMPLX_1:143
                     .= abs(r1 + (-r + r) - seq.m) by XCMPLX_0:def 6
                     .= abs(r1 + -r + r - seq.m) by XCMPLX_1:1
                     .= abs(r1 - r + r - seq.m) by XCMPLX_0:def 8
                     .= abs(r1 - r + (r - seq.m)) by XCMPLX_1:29
                     .= abs(seq1.m + - (-(r1 - r))) by A2
                     .= abs(seq1.m - (-(r1 - r))) by XCMPLX_0:def 8
                     .= abs(seq1.m - (r - r1)) by XCMPLX_1:143;
       hence abs(seq1.m - (r - r1)) < r2 by A5,A7;
      end;
    take n; thus
      for m st n <= m holds abs(seq1.m - (r - r1)) < r2 by A6;
    end;
  hence A8: seq1 is convergent by SEQ_2:def 6;
    lim seq = r1 by A1,A3,SEQ_2:def 7;
  hence thesis by A4,A8,SEQ_2:def 7;
  end;

::
:: THEOREMS CONCERNED EVENTS
::
theorem Th6:
  A /\ Omega = A & A /\ ([#] Sigma) = A
  proof
  thus A /\ Omega = A by XBOOLE_1:28;
  hence A /\ ([#] Sigma) = A by PROB_1:def 11;
  end;

scheme SeqExProb{F(Nat) -> set}:
  ex f being Function st dom f = NAT & for n holds f.n = F(n)
   proof
   defpred P[set,set] means ex n st $1 = n & $2 = F(n);
   A1: for x,y,z st x in NAT & P[x,y] & P[x,z] holds y = z;
   A2: for x st x in NAT ex y st P[x,y]
    proof let x; assume x in NAT;
    then reconsider x as Nat;
    take F(x); thus thesis;
    end;
   consider f being Function such that
  A3: dom f = NAT & for x st x in NAT holds P[x,f.x] from FuncEx(A1,A2);
   take f;
       now let n; ex m st n = m & f.n = F(m) by A3;
     hence f.n = F(n);
     end; hence thesis by A3;
   end;

definition let Omega,Sigma,ASeq,n;
  redefine func ASeq.n -> Event of Sigma;
  coherence by PROB_1:57;
end;

definition let Omega,Sigma,ASeq;
  func @Intersection ASeq -> Event of Sigma equals
  :Def1: Intersection ASeq;
 coherence
  proof
     for n holds ASeq.n in Sigma by PROB_1:def 9;
   then Intersection ASeq in Sigma by PROB_1:def 8;
   hence Intersection ASeq is Event of Sigma by PROB_1:def 10;
  end;
end;

canceled 2;

theorem
Th9: ex BSeq st for n holds BSeq.n = ASeq.n /\ B
  proof
  deffunc F(Nat) = ASeq.$1 /\ B;
  consider f being Function such that
 A1: dom f = NAT & for n holds f.n = F(n) from SeqExProb;
     now let m;
      ASeq.m /\ B in bool Omega;
    hence f.m in bool Omega by A1;
   end;
   then for x being set st x in NAT holds f.x in bool Omega;
   then reconsider f as SetSequence of Omega by A1,FUNCT_2:5;
     now let m; ASeq.m /\ B in Sigma by PROB_1:def 10;
   hence f.m in Sigma by A1;
   end;
   then reconsider f as SetSequence of Sigma by PROB_1:def 9;
   take f; thus thesis by A1;
  end;

theorem
Th10: (ASeq is non-increasing &
       for n holds BSeq.n = ASeq.n /\ B) implies BSeq is non-increasing
  proof assume
 A1: ASeq is non-increasing & for n holds BSeq.n = ASeq.n /\ B;
     now let m,n; assume m<=n;
   then ASeq.n c= ASeq.m by A1,PROB_1:def 6;
   then ASeq.n /\ B c= ASeq.m /\ B by XBOOLE_1:26;
   then BSeq.n c= ASeq.m /\ B by A1; hence
     BSeq.n c= BSeq.m by A1;
   end; hence thesis by PROB_1:def 6;
  end;

theorem
Th11: for f being Function of Sigma,REAL holds
       (f*ASeq).n = f.(ASeq.n)
  proof let f be Function of Sigma,REAL;
        n in NAT;
   then n in dom ASeq by FUNCT_2:def 1;
  hence (f*ASeq).n = f.(ASeq.n) by FUNCT_1:23;
  end;

theorem
Th12: (for n holds BSeq.n = ASeq.n /\ B) implies
       (Intersection ASeq) /\ B = Intersection BSeq
  proof assume
 A1: for n holds BSeq.n = ASeq.n /\ B;
 A2: now let x; assume x in (Intersection ASeq) /\ B;
    then A3: x in (Intersection ASeq) & x in B by XBOOLE_0:def 3;
   A4: for n holds x in ASeq.n /\ B
      proof let n; x in ASeq.n & x in B by A3,PROB_1:29;
      hence thesis by XBOOLE_0:def 3;
      end;
      for n holds x in BSeq.n
      proof let n; x in ASeq.n /\ B by A4;
      hence thesis by A1;
      end;
    hence x in (Intersection BSeq) by PROB_1:29;
    end;
      now let x;
    assume A5: x in (Intersection BSeq);
   A6: for n holds x in ASeq.n /\ B
     proof let n; x in BSeq.n by A5,PROB_1:29;
     hence thesis by A1;
     end;
      for n holds (x in ASeq.n & x in B)
     proof let n; x in ASeq.n /\ B by A6;
     hence thesis by XBOOLE_0:def 3;
     end;
    then x in (Intersection ASeq) & x in B by PROB_1:29;
    hence x in (Intersection ASeq) /\ B by XBOOLE_0:def 3;
    end;
   hence thesis by A2,TARSKI:2;
  end;

theorem
Th13: (for A holds P.A = P1.A) implies P = P1
  proof assume
 A1: for A holds P.A = P1.A;
   for x st x in Sigma holds P.x = P1.x
    proof let x; assume x in Sigma;
    then reconsider x as Event of Sigma by PROB_1:48;
      P.x = P1.x by A1;
    hence thesis;
    end;
   hence thesis by FUNCT_2:18;
  end;

theorem
   for ASeq being SetSequence of Omega holds
          ASeq is non-increasing iff for n holds ASeq.(n+1) c= ASeq.n
  proof let ASeq be SetSequence of Omega;
  thus ASeq is non-increasing implies for n holds ASeq.(n+1) c= ASeq.n
   proof assume
   A1: ASeq is non-increasing;
       now let n;
       n <= n+1 by NAT_1:29;
     hence ASeq.(n+1) c= ASeq.n by A1,PROB_1:def 6;
     end;
    hence thesis;
   end; assume
  A2: for n holds ASeq.(n+1) c= ASeq.n;
      now let n,m such that
    A3: n <= m;
    A4: now
        defpred P[Nat] means ASeq.(n+$1) c= ASeq.n;
        A5: P[0];
        A6: for k st P[k] holds P[k+1]
          proof let k such that
          A7: ASeq.(n+k) c= ASeq.n;
             ASeq.(n+k+1) c= ASeq.(n+k) by A2;
           then ASeq.(n+(k+1)) c= ASeq.(n+k) by XCMPLX_1:1;
           hence thesis by A7,XBOOLE_1:1;
          end;
        thus for k holds P[k] from Ind(A5,A6);
        end;
       ex k st m = n + k by A3,NAT_1:28;
    hence ASeq.m c= ASeq.n by A4;
    end;
  hence thesis by PROB_1:def 6;
  end;

theorem
   for ASeq being SetSequence of Omega holds
      ASeq is non-decreasing iff for n holds ASeq.n c= ASeq.(n+1)
  proof let ASeq be SetSequence of Omega;
  thus ASeq is non-decreasing implies for n holds ASeq.n c= ASeq.(n+1)
   proof assume
   A1: ASeq is non-decreasing;
       now let n;
       n <= n+1 by NAT_1:29;
     hence ASeq.n c= ASeq.(n+1) by A1,PROB_1:def 7;
     end;
    hence thesis;
   end; assume
  A2: for n holds ASeq.n c= ASeq.(n+1);
      now let n,m such that
    A3: n <= m;
    A4: now
        defpred P[Nat] means ASeq.n c= ASeq.(n+$1);
        A5: P[0];
        A6: for k st P[k] holds P[k+1]
          proof let k such that
          A7: ASeq.n c= ASeq.(n+k);
             ASeq.(n+k) c= ASeq.(n+k+1) by A2;
           then ASeq.(n+k) c= ASeq.(n+(k+1)) by XCMPLX_1:1;
           hence thesis by A7,XBOOLE_1:1;
          end;
        thus for k holds P[k] from Ind(A5,A6);
        end;
       ex k st m = n + k by A3,NAT_1:28;
    hence ASeq.n c= ASeq.m by A4;
    end;
  hence thesis by PROB_1:def 7;
  end;

theorem
   for ASeq,BSeq being SetSequence of Omega
          st (for n holds ASeq.n = BSeq.n) holds ASeq = BSeq
  proof let ASeq,BSeq be SetSequence of Omega;
  assume for n holds ASeq.n = BSeq.n;
  then A1: for x holds
       x in NAT implies ASeq.x = BSeq.x;
  A2: dom ASeq = NAT by FUNCT_2:def 1;
     dom BSeq = NAT by FUNCT_2:def 1;
  hence thesis by A1,A2,FUNCT_1:9;
  end;

theorem
Th17: for ASeq being SetSequence of Omega holds
    (ASeq is non-increasing iff Complement ASeq is non-decreasing)
  proof let ASeq be SetSequence of Omega;
  thus ASeq is non-increasing implies Complement ASeq is non-decreasing
    proof
     assume A1: ASeq is non-increasing;
        now let n,m; assume
         n <= m;
       then ASeq.m c= ASeq.n by A1,PROB_1:def 6;
       then (ASeq.n)` c= (ASeq.m)` by SUBSET_1:31;
       then (Complement ASeq).n c= (ASeq.m)` by PROB_1:def 4;
       hence (Complement ASeq).n c= (Complement ASeq).m by PROB_1:def 4;
      end;
    hence thesis by PROB_1:def 7;
    end; assume
  A2: Complement ASeq is non-decreasing;
      now let n,m; assume
       n <= m;
     then (Complement ASeq).n c= (Complement ASeq).m by A2,PROB_1:def 7;
     then (ASeq.n)` c= (Complement ASeq).m by PROB_1:def 4;
     then (ASeq.n)` c= (ASeq.m)` by PROB_1:def 4;
     hence ASeq.m c= ASeq.n by SUBSET_1:31;
    end;
  hence thesis by PROB_1:def 6;
  end;

Lm1: for ASeq being SetSequence of Omega holds
           (ASeq is non-decreasing iff Complement ASeq is non-increasing)
  proof let ASeq be SetSequence of Omega;
  thus ASeq is non-decreasing implies Complement ASeq is non-increasing
    proof
     assume A1: ASeq is non-decreasing;
        now let n,m; assume
         n <= m;
       then ASeq.n c= ASeq.m by A1,PROB_1:def 7;
       then (ASeq.m)` c= (ASeq.n)` by SUBSET_1:31;
       then (Complement ASeq).m c= (ASeq.n)` by PROB_1:def 4;
       hence (Complement ASeq).m c= (Complement ASeq).n by PROB_1:def 4;
      end;
    hence thesis by PROB_1:def 6;
    end; assume
  A2: Complement ASeq is non-increasing;
      now let n,m; assume
       n <= m;
     then (Complement ASeq).m c= (Complement ASeq).n by A2,PROB_1:def 6;
     then (ASeq.m)` c= (Complement ASeq).n by PROB_1:def 4;
     then (ASeq.m)` c= (ASeq.n)` by PROB_1:def 4;
     hence ASeq.n c= ASeq.m by SUBSET_1:31;
    end;
  hence thesis by PROB_1:def 7;
  end;

definition let Omega,Sigma,ASeq;
 func @Complement ASeq -> SetSequence of Sigma equals
  :Def2:      Complement ASeq;
  coherence
  proof
     now let n;
     (Complement ASeq).n = (ASeq.n)` by PROB_1:def 4;
   then (Complement ASeq).n is Event of Sigma by PROB_1:50;
   hence (Complement ASeq).n in Sigma by PROB_1:def 10;
   end; hence thesis by PROB_1:def 9;
  end;
end;

definition let F be Function;
attr F is disjoint_valued means
:Def3: x <> y implies F.x misses F.y;
end;

definition let Omega,Sigma,ASeq;
redefine attr ASeq is disjoint_valued means
   for m,n st m <> n holds ASeq.m misses ASeq.n;
 compatibility
  proof
A1:  dom ASeq = NAT by FUNCT_2:def 1;
  thus ASeq is disjoint_valued implies
    for m,n st m <> n holds ASeq.m misses ASeq.n by Def3;
  assume A2:for m,n st m <> n holds ASeq.m misses ASeq.n;
  let x,y; assume A3:x <> y;
  per cases;
  suppose x in dom ASeq & y in dom ASeq;
  hence ASeq.x misses ASeq.y by A1,A2,A3;
  suppose not (x in dom ASeq & y in dom ASeq);
  then ASeq.x = {} or ASeq.y = {} by FUNCT_1:def 4;
  hence ASeq.x misses ASeq.y by XBOOLE_1:65;
  end;
end;

Lm2: for P,ASeq st ASeq is non-decreasing holds
         (P * ASeq is convergent & lim (P * ASeq) = P.Union ASeq)
  proof let P,ASeq such that
 A1: ASeq is non-decreasing;
  reconsider V = Union ASeq as Event of Sigma by PROB_1:58;
  set BSeq = @Complement ASeq;
 A2: BSeq = Complement ASeq by Def2;
 then A3: BSeq is non-increasing by A1,Lm1;
 then A4: P * BSeq is convergent by PROB_1:def 13;
    Intersection BSeq = (Union Complement Complement ASeq)` by A2,PROB_1:def 5
     .= (Union ASeq)` by PROB_1:31
     .= Omega \ Union ASeq by SUBSET_1:def 5
     .= [#] Sigma \ Union ASeq by PROB_1:def 11;
 then A5: P.Intersection BSeq = 1 - P.V by PROB_1:68;
 A6: now let n;
            (P * BSeq).n = P.(BSeq.n) by Th11
          .= P.((ASeq.n)`) by A2,PROB_1:def 4
          .= P.(Omega \ ASeq.n) by SUBSET_1:def 5
          .= P.([#] Sigma \ ASeq.n) by PROB_1:def 11
          .= 1 - P.(ASeq.n) by PROB_1:68
          .= 1 - (P * ASeq).n by Th11
          .= 1 + - (P * ASeq).n by XCMPLX_0:def 8;
      then - (P * ASeq).n = (P * BSeq).n - 1 by XCMPLX_1:26
                         .= - (1 - (P * BSeq).n) by XCMPLX_1:143;
      hence (P * ASeq).n = -(- (1 - (P * BSeq).n))
                        .= 1 - (P * BSeq).n;
     end;
  hence P * ASeq is convergent by A4,Th5;
  thus lim (P * ASeq) = 1 - lim (P * BSeq) by A4,A6,Th5
       .= 1 - (1 - P.V) by A3,A5,PROB_1:def 13
       .= 1 - 1 + P.V by XCMPLX_1:37
       .= P.(Union ASeq);
  end;

::
:: THEOREMS CONCERNED PROBABILITY
::

canceled 2;

theorem
:: Equivalent Definition of Probability
   for P being Function of Sigma,REAL holds
      P is Probability of Sigma iff
     (for A holds 0 <= P.A) &
     (P.Omega = 1) &
     (for A,B st A misses B holds P.(A \/ B) = P.A + P.B) &
     (for ASeq st ASeq is non-decreasing holds
     (P * ASeq is convergent & lim (P * ASeq) = P.Union ASeq))
   proof let P be Function of Sigma,REAL;
     thus P is Probability of Sigma implies
     (for A holds 0 <= P.A) &
     (P.Omega = 1) &
     (for A,B st A misses B holds P.(A \/ B) = P.A + P.B) &
     (for ASeq st ASeq is non-decreasing holds
     (P * ASeq is convergent & lim (P * ASeq) = P.Union ASeq))
                              by Lm2,PROB_1:def 13;
     assume that
   A1: (for A holds 0 <= P.A) &
      (P.Omega = 1) &
      (for A,B st A misses B holds P.(A \/ B) = P.A + P.B) and
   A2: (for ASeq st ASeq is non-decreasing holds
      (P * ASeq is convergent & lim (P * ASeq) = P.Union ASeq));
        (for ASeq st ASeq is non-increasing holds
      (P * ASeq is convergent & lim (P * ASeq) = P.Intersection ASeq))
      proof let ASeq such that
     A3: ASeq is non-increasing;
     A4: for A holds P.(A`) = 1 - P.A
     proof let A;
      reconsider B = A` as Event of Sigma by PROB_1:50;
      A5:A misses B by SUBSET_1:44;
       1 = P.[#]Omega by A1,SUBSET_1:def 4
      .= P.(A \/ B) by SUBSET_1:25
      .= P.A + P.B by A1,A5;
      hence thesis by XCMPLX_1:26;
     end;
        Intersection ASeq = @Intersection ASeq by Def1;
      then reconsider V = Intersection ASeq as Event of Sigma;
     set BSeq = @Complement ASeq;
     A6: BSeq = Complement ASeq by Def2;
     then A7: BSeq is non-decreasing by A3,Th17;
     then A8: P * BSeq is convergent by A2;
        Union BSeq = (Union Complement ASeq)`` by Def2
     .= (Intersection ASeq)` by PROB_1:def 5;
     then A9: P.Union BSeq = 1 - P.V by A4;
     A10: now let n;
            (P * BSeq).n = P.(BSeq.n) by Th11
          .= P.((ASeq.n)`) by A6,PROB_1:def 4
          .= 1 - P.(ASeq.n) by A4
          .= 1 - (P * ASeq).n by Th11
          .= 1 + - (P * ASeq).n by XCMPLX_0:def 8;
      then - (P * ASeq).n = (P * BSeq).n - 1 by XCMPLX_1:26
                         .= - (1 - (P * BSeq).n) by XCMPLX_1:143;
      hence (P * ASeq).n = -(- (1 - (P * BSeq).n))
                        .= 1 - (P * BSeq).n;
     end;
  hence P * ASeq is convergent by A8,Th5;
  thus lim (P * ASeq) = 1 - lim (P * BSeq) by A8,A10,Th5
       .= 1 - (1 - P.V) by A2,A7,A9
       .= 1 - 1 + P.V by XCMPLX_1:37
       .= P.(Intersection ASeq);
      end;
    hence thesis by A1,PROB_1:def 13;
   end;

theorem
   P.(A \/ B \/ C) =
  P.A + P.B + P.C - (P.(A /\ B) + P.(B /\ C) + P.(A /\ C)) + P.(A /\ B /\ C)
  proof
 A1: P.(A \/ B \/ C) = P.(A \/ B) + P.C - P.((A \/ B) /\ C) by PROB_1:74
    .= P.A + P.B - P.(A /\ B) + P.C - P.((A \/ B) /\ C) by PROB_1:74
    .= P.A + P.B + P.C - P.(A /\ B) - P.((A \/ B) /\ C) by XCMPLX_1:29
    .= P.A + P.B + P.C - (P.(A /\ B) + P.((A \/ B) /\ C)) by XCMPLX_1:36;
    P.((A \/ B) /\ C) = P.((A /\ C) \/ (B /\ C)) by XBOOLE_1:23
    .= P.(A /\ C) + P.(B /\ C) - P.((A /\ C) /\ (B /\ C)) by PROB_1:74
    .= P.(A /\ C) + P.(B /\ C) - P.(A /\ ((B /\ C) /\ C)) by XBOOLE_1:16
    .= P.(A /\ C) + P.(B /\ C) - P.(A /\ (B /\ (C /\ C))) by XBOOLE_1:16
    .= P.(B /\ C) + P.(A /\ C) - P.(A /\ B /\ C) by XBOOLE_1:16;
  then P.(A \/ B \/ C) =P.A + P.B + P.C - (P.(A /\ B) + (P.(B /\ C) + P.(A /\
 C) +
                                       - P.(A /\ B /\ C))) by A1,XCMPLX_0:def 8
  .= P.A + P.B + P.C - (P.(A /\ B) + (P.(B /\ C) + P.(A /\ C)) +
                                       - P.(A /\ B /\ C)) by XCMPLX_1:1
  .= P.A + P.B + P.C - (P.(A /\ B) + P.(B /\ C) + P.(A /\ C) +
                                       - P.(A /\ B /\ C)) by XCMPLX_1:1
  .= P.A + P.B + P.C - (P.(A /\ B) + P.(B /\ C) + P.(A /\ C)
                                       - P.(A /\ B /\ C)) by XCMPLX_0:def 8
  .= P.A + P.B + P.C - (P.(A /\ B) + P.(B /\ C) + P.(A /\ C))
                                       + P.(A /\ B /\ C) by XCMPLX_1:37;
  hence thesis;
  end;

theorem
Th22: P.(A \ (A /\ B)) = P.A - P.(A /\ B)
  proof A /\ B c= A by XBOOLE_1:17;
  hence thesis by PROB_1:69;
  end;

theorem
Th23: P.(A /\ B) <= P.B & P.(A /\ B) <= P.A
  proof
A1:  A /\ B c= B by XBOOLE_1:17;
    A /\ B c= A by XBOOLE_1:17;
  hence thesis by A1,PROB_1:70;
  end;

theorem
Th24: C = B` implies P.A = P.(A /\ B) + P.(A /\ C)
  proof
  assume A1: C = B`;
  then B misses C by SUBSET_1:44;
  then A /\ C misses B by XBOOLE_1:74;
 then A2: A /\ B misses A /\ C by XBOOLE_1:74;
    P.A = P.(A /\ Omega) by Th6
     .= P.(A /\ [#]Omega) by SUBSET_1:def 4
     .= P.(A /\ (B \/ C)) by A1,SUBSET_1:25
     .= P.(A /\ B \/ A /\ C) by XBOOLE_1:23
     .= P.(A /\ B) + P.(A /\ C) by A2,PROB_1:def 13;
  hence thesis;
  end;

theorem
Th25: P.A + P.B - 1 <= P.(A /\ B)
  proof
    P.A + P.B - P.(A /\ B) = P.(A \/ B) by PROB_1:74;
  then P.A + P.B - P.(A /\ B) <= 1 by PROB_1:71;
  then P.A + P.B <= P.(A /\ B) + 1 by REAL_1:86;
  hence thesis by REAL_1:86;
  end;

theorem
Th26: P.A = 1 - P.([#] Sigma \ A)
  proof
    P.([#] Sigma \ A) + P.A = 1 by PROB_1:67;
  hence thesis by XCMPLX_1:26;
  end;

theorem
Th27: P.A < 1 iff 0 < P.([#] Sigma \ A)
  proof
  thus P.A < 1 implies 0 < P.([#] Sigma \ A)
    proof assume P.A < 1;
    then 1 - P.([#] Sigma \ A) < 1 by Th26;
    then 1 + - P.([#] Sigma \ A) < 1 by XCMPLX_0:def 8;
    then - P.([#] Sigma \ A) < 1 - 1 by REAL_1:86;
    then 0 < - (- P.([#] Sigma \ A)) by REAL_1:66;
    hence thesis;
    end; assume
    0 < P.([#] Sigma \ A);
  then 0 < 1 - P.A by PROB_1:68;
  then P.A + 0 < 1 by REAL_1:86;
  hence thesis;
  end;

theorem
   P.([#] Sigma \ A) < 1 iff 0 < P.A
  proof
  thus P.([#] Sigma \ A) < 1 implies 0 < P.A
    proof assume P.([#] Sigma \ A) < 1;
    then 1 - P.A < 1 by PROB_1:68;
    then 1 + - P.A < 1 by XCMPLX_0:def 8;
    then - P.A < 1 - 1 by REAL_1:86;
    then 0 < - (- P.A) by REAL_1:66;
    hence thesis;
    end; assume
    0 < P.A;
  then 0 < 1 - P.([#] Sigma \ A) by Th26;
  then P.([#] Sigma \ A) + 0 < 1 by REAL_1:86;
  hence thesis;
  end;

::
:: INDEPENDENCE OF EVENTS
::

definition
  let Omega, Sigma, P, A, B;
  pred A,B are_independent_respect_to P means
 :Def5:  P.(A /\ B) = P.A * P.B;
  let C;
  pred A,B,C are_independent_respect_to P means
 :Def6:  P.(A /\ B /\ C) = P.A * P.B * P.C &
        P.(A /\ B) = P.A * P.B &
        P.(A /\ C) = P.A * P.C &
        P.(B /\ C) = P.B * P.C;
end;

Lm3:A,B are_independent_respect_to P implies
      B,A are_independent_respect_to P
  proof assume A,B are_independent_respect_to P;
  then P.(B /\ A) = P.B * P.A by Def5;
    hence thesis by Def5;
  end;

canceled 2;

theorem
  A,B are_independent_respect_to P iff
      B,A are_independent_respect_to P by Lm3;

theorem
Th32: (A,B,C are_independent_respect_to P iff
     (P.(A /\ B /\ C) = P.A * P.B * P.C &
      A,B are_independent_respect_to P &
      B,C are_independent_respect_to P &
      A,C are_independent_respect_to P))
  proof
  thus A,B,C are_independent_respect_to P implies
       (P.(A /\ B /\ C) = P.A * P.B * P.C &
        A,B are_independent_respect_to P &
        B,C are_independent_respect_to P &
        A,C are_independent_respect_to P)
     proof assume A,B,C are_independent_respect_to P;
    then P.(A /\ B /\ C) = P.A * P.B * P.C &
       P.(A /\ B) = P.A * P.B &
       P.(A /\ C) = P.A * P.C &
       P.(B /\ C) = P.B * P.C by Def6;
     hence thesis by Def5;
     end;
  assume (P.(A /\ B /\ C) = P.A * P.B * P.C &
        A,B are_independent_respect_to P &
        B,C are_independent_respect_to P &
        A,C are_independent_respect_to P);
  then (P.(A /\ B /\ C) = P.A * P.B * P.C &
       P.(A /\ B) = P.A * P.B &
       P.(A /\ C) = P.A * P.C &
       P.(B /\ C) = P.B * P.C) by Def5;
  hence thesis by Def6;
  end;

theorem
   A,B,C are_independent_respect_to P
      implies B,A,C are_independent_respect_to P
  proof
  assume A,B,C are_independent_respect_to P;
 then A1: (P.(A /\ B /\ C) = P.A * P.B * P.C &
      A,B are_independent_respect_to P &
      B,C are_independent_respect_to P &
      A,C are_independent_respect_to P) by Th32;
  then B,A are_independent_respect_to P by Lm3;
  hence thesis by A1,Th32;
  end;

theorem
    A,B,C are_independent_respect_to P
      implies A,C,B are_independent_respect_to P
  proof
  assume A,B,C are_independent_respect_to P;
 then A1: (P.(A /\ B /\ C) = P.A * P.B * P.C &
      A,B are_independent_respect_to P &
      B,C are_independent_respect_to P &
      A,C are_independent_respect_to P) by Th32;
 then A2: P.(A /\ C /\ B) = P.A * P.B * P.C by XBOOLE_1:16
                  .= P.A * P.C * P.B by XCMPLX_1:4;
    C,B are_independent_respect_to P by A1,Lm3;
  hence thesis by A1,A2,Th32;
  end;

theorem
   for E being Event of Sigma st E = {} holds
 A, E are_independent_respect_to P
  proof
  let E be Event of Sigma;
  assume A1: E = {};
    P.(A /\ ({} Sigma)) = P.A * 0 by PROB_1:64
                    .= P.A * P.({} Sigma) by PROB_1:64;
  hence thesis by A1,Def5;
  end;

theorem
   A, [#] Sigma are_independent_respect_to P
  proof
    P.(A /\ ([#] Sigma)) = P.A * 1 by Th6
                   .= P.A * P.([#] Sigma) by PROB_1:66;
  hence thesis by Def5;
  end;

theorem
Th37: for A,B,P st A,B are_independent_respect_to P
  holds A,([#] Sigma \ B) are_independent_respect_to P
  proof let A,B,P;
  assume A,B are_independent_respect_to P;
 then A1: P.(A /\ B) = P.A * P.B by Def5;
    P.(A /\ ([#] Sigma \ B)) = P.(A /\ (Omega \ B)) by PROB_1:def 11
                       .= P.(A /\ B`) by SUBSET_1:def 5
                       .= P.(A \ B) by SUBSET_1:32
                       .= P.(A \ (A /\ B)) by XBOOLE_1:47
                       .= P.A * 1 - P.A * P.B by A1,Th22
                       .= P.A * (1 - P.B) by XCMPLX_1:40
                       .= P.A * P.([#] Sigma \ B) by PROB_1:68;
  hence thesis by Def5;
  end;

theorem
Th38: A,B are_independent_respect_to P implies
  ([#] Sigma \ A),([#] Sigma \ B) are_independent_respect_to P
  proof
  assume A,B are_independent_respect_to P;
  then A,([#] Sigma \ B) are_independent_respect_to P by Th37;
  then ([#] Sigma \ B),A are_independent_respect_to P by Lm3;
  then ([#] Sigma \ B),([#] Sigma \ A) are_independent_respect_to P by Th37;
  hence thesis by Lm3;
  end;

theorem
   for A,B,C,P st (A,B are_independent_respect_to P &
  A,C are_independent_respect_to P & B misses C) holds
  A,B \/ C are_independent_respect_to P
  proof let A,B,C,P; assume
 A1: A,B are_independent_respect_to P &
    A,C are_independent_respect_to P & B misses C;
 then A2: (A /\ B) misses (A /\ C) by XBOOLE_1:76;
    P.(A /\ (B \/ C)) = P.((A /\ B) \/ (A /\ C)) by XBOOLE_1:23
                 .= P.(A /\ B) + P.(A /\ C) by A2,PROB_1:def 13
                 .= P.A * P.B + P.(A /\ C) by A1,Def5
                 .= P.A * P.B + P.A * P.C by A1,Def5
                 .= P.A * (P.B + P.C) by XCMPLX_1:8
                 .= P.A * P.(B \/ C) by A1,PROB_1:def 13;
  hence thesis by Def5;
  end;

theorem
   for P,A,B st (A,B are_independent_respect_to P & P.A < 1 & P.B < 1)
       holds P.(A \/ B) < 1
   proof let P,A,B; assume that
  A1: A,B are_independent_respect_to P and
  A2: P.A < 1 and
  A3: P.B < 1;
  A4: ([#] Sigma \ A),([#] Sigma \ B) are_independent_respect_to P by A1,Th38;
  A5: 0 < P.([#] Sigma \ A) by A2,Th27;
     0 < P.([#] Sigma \ B) by A3,Th27;
  then A6: 0 < P.([#] Sigma \ A) * P.([#] Sigma \ B) by A5,SQUARE_1:21;
  A7: now let r,r1; assume 0 < r1;
      then - r1 < 0 by REAL_1:26,50;
      then r + - r1 < r + 0 by REAL_1:53;
      hence r - r1 < r by XCMPLX_0:def 8;
      end;
     P.(A \/ B) = 1 - P.([#] Sigma \ (A \/ B)) by Th26
            .= 1 - P.(([#] Sigma \ A) /\ ([#] Sigma \ B)) by XBOOLE_1:53
            .= 1 - P.([#] Sigma \ A) * P.([#] Sigma \ B) by A4,Def5;
   hence thesis by A6,A7;
   end;

::
:: CONDITIONAL PROBABILITY
::

definition let Omega,Sigma,P,B;
  assume A1: 0 < P.B;
  func P.|.B -> Probability of Sigma means
  :Def7: for A holds it.A = P.(A /\ B)/P.B;
  existence
  proof
   defpred P[set,set] means ex A,r st (A = $1 & r = $2) &
        r = P.(A /\ B)/P.B;
 A2: for x st x in Sigma ex y st y in REAL & P[x,y]
    proof let x; assume x in Sigma;
     then reconsider x as Event of Sigma by PROB_1:48;
     consider y such that A3: y = P.(x /\ B)/P.B;
     take y;
     thus thesis by A3;
    end;
   consider f being Function of Sigma,REAL such that
  A4: for x st x in Sigma holds P[x,f.x] from FuncEx1(A2);
  A5: for A holds f.A = P.(A /\ B)/P.B
    proof let A; A in Sigma by PROB_1:def 10;
     then ex C,r1 st C = A & r1 = f.A & r1 = P.(C /\ B)/P.B by A4;
    hence thesis;
    end;
     f is Probability of Sigma
    proof
    thus for A holds 0 <= f.A
      proof let A;
        0 <= P.(A /\ B) by PROB_1:def 13;
      then 0 <= P.(A /\ B)/P.B by A1,SQUARE_1:27;
      hence thesis by A5;
      end;
    thus f.Omega = f.([#] Sigma) by PROB_1:def 11
             .= P.(([#] Sigma) /\ B)/P.B by A5
             .= P.B/P.B by Th6
             .= 1 by A1,XCMPLX_1:60;
    thus for A,C st A misses C holds f.(A \/ C) = f.A + f.C
      proof let A,C; assume A misses C;
     then A6: A /\ B misses C /\ B by XBOOLE_1:76;
      thus f.(A \/ C) = P.((A \/ C) /\ B)/P.B by A5
                    .= P.((A /\ B) \/ (C /\ B))/P.B by XBOOLE_1:23
                    .= (P.(A /\ B) + P.(C /\ B))/P.B by A6,PROB_1:def 13
                    .= P.(A /\ B)/P.B + P.(C /\ B)/P.B by XCMPLX_1:63
                    .= P.(A /\ B)/P.B + f.C by A5
                    .= f.A + f.C by A5;
      end;
    thus for ASeq st ASeq is non-increasing holds
     (f*ASeq is convergent & lim (f*ASeq) = f.(Intersection ASeq))
     proof let ASeq such that
    A7: ASeq is non-increasing;
     consider BSeq such that
    A8: for n holds BSeq.n = ASeq.n /\ B by Th9;
    A9: BSeq is non-increasing by A7,A8,Th10;
A10:   dom(f*ASeq) = NAT by FUNCT_2:def 1;
A11:   dom(P*BSeq) = NAT by FUNCT_2:def 1;
       now let n;
      assume n in dom(f*ASeq);
      thus (f*ASeq).n = f.(ASeq.n) by Th11
                       .= P.(ASeq.n /\ B)/P.B by A5
                       .= P.(BSeq.n)/P.B by A8
                       .= (P*BSeq).n/P.B by Th11
                       .= (P.B)" * (P*BSeq).n by XCMPLX_0:def 9;
     end;
    then A12: f*ASeq = (P.B)" (#) (P*BSeq) by A10,A11,SEQ_1:def 6;
    A13: P*BSeq is convergent & lim (P*BSeq) = P.(Intersection BSeq)
                                                         by A9,PROB_1:def 13;
     hence f*ASeq is convergent by A12,SEQ_2:21;
    A14: Intersection BSeq = @Intersection BSeq by Def1;
    A15: Intersection ASeq = @Intersection ASeq by Def1;
     thus lim (f*ASeq) = (P.B)" * P.(@Intersection BSeq) by A12,A13,A14,SEQ_2:
22
                      .= (P.(@Intersection BSeq))/P.B by XCMPLX_0:def 9
                      .= (P.((@Intersection ASeq) /\ B))/P.B
                                                     by A8,A14,A15,Th12
                      .= f.(Intersection ASeq) by A5,A15;
     end;
    end;
  then reconsider f as Probability of Sigma;
  take f;
  thus thesis by A5;
  end;
  uniqueness
  proof let P1,P2; assume that
 A16: for A holds P1.A = P.(A /\ B)/P.B and
 A17: for A holds P2.A = P.(A /\ B)/P.B;
    now let A;
  thus P1.A = P.(A /\ B)/P.B by A16
            .= P2.A by A17;
  end;
  hence thesis by Th13;
  end;
end;

canceled;

theorem
Th42: for P,B,A st 0 < P.B holds P.(A /\ B) = P.|.B.A * P.B
  proof let P,B,A;
  assume A1: 0 < P.B;
  then P.|.B.A * P.B = (P.(A /\ B)/P.B) * P.B by Def7
             .= P.(A /\ B) * (P.B)" * P.B by XCMPLX_0:def 9
             .= P.(A /\ B) * ((P.B)" * P.B) by XCMPLX_1:4
             .= P.(A /\ B) * 1 by A1,XCMPLX_0:def 7
             .= P.(A /\ B);
  hence thesis;
  end;

theorem
   for P,A,B,C st 0 < P.(A /\ B) holds
       P.(A /\ B /\ C) = P.A * P.|.A.B * P.|.(A /\ B).C
   proof let P,A,B,C;
   assume A1: 0 < P.(A /\ B);
  then A2: 0 < P.A by Th23;
     P.(A /\ B /\ C) = P.(B /\ A) * P.|.(A /\ B).C by A1,Th42
                .= P.A * P.|.A.B * P.|.(A /\ B).C by A2,Th42;
   hence thesis;
   end;

theorem
:: Total Probability Rule for Two Events
Th44: for P,A,B,C st (C = B` & 0 < P.B & 0 < P.C ) holds
       P.A = P.|.B.A * P.B + P.|.C.A * P.C
       proof let P,A,B,C; assume that
      A1: C = B` and
      A2: 0 < P.B and
      A3: 0 < P.C;
         P.A = P.(A /\ B) + P.(A /\ C) by A1,Th24
          .= P.|.B.A * P.B + P.(A /\ C) by A2,Th42
          .= P.|.B.A * P.B + P.|.C.A * P.C by A3,Th42;
       hence thesis;
       end;

theorem
:: Total Probability Rule for Three Events
Th45: for P,A,A1,A2,A3 st (A1 misses A2 & A3 = (A1 \/ A2)` &
       0 < P.A1 & 0 < P.A2 & 0 < P.A3) holds
       P.A = (P.|.A1.A * P.A1) + (P.|.A2.A * P.A2) + (P.|.A3.A * P.A3)
  proof let P,A,A1,A2,A3; assume that
 A1: A1 misses A2 and
 A2: A3 = (A1 \/ A2)` and
 A3: 0 < P.A1 and
 A4: 0 < P.A2 and
 A5: 0 < P.A3;
 A6: A /\ A1 misses A /\ A2 by A1,XBOOLE_1:76;
       (A1 \/ A2) misses A3 by A2,SUBSET_1:44;
 then A7: A /\ (A1 \/ A2) misses A /\ A3 by XBOOLE_1:76;
 A8: A1 \/ A2 \/ A3 = [#]Omega by A2,SUBSET_1:25
                 .= Omega by SUBSET_1:def 4;
    (P.|.A1.A * P.A1) + (P.|.A2.A * P.A2) + (P.|.A3.A * P.A3) =
    P.(A /\ A1) + (P.|.A2.A * P.A2) + (P.|.A3.A * P.A3) by A3,Th42
    .= P.(A /\ A1) + P.(A /\ A2) + (P.|.A3.A * P.A3) by A4,Th42
    .= P.(A /\ A1) + P.(A /\ A2) + P.(A /\ A3) by A5,Th42
    .= P.((A /\ A1) \/ (A /\ A2)) + P.(A /\ A3) by A6,PROB_1:def 13
    .= P.(A /\ (A1 \/ A2)) + P.(A /\ A3) by XBOOLE_1:23
    .= P.((A /\ (A1 \/ A2)) \/ (A /\ A3)) by A7,PROB_1:def 13
    .= P.(A /\ Omega) by A8,XBOOLE_1:23
    .= P.A by Th6;
  hence thesis;
  end;

theorem
   for P,A,B st 0 < P.B holds
       (P.|.B.A = P.A iff A,B are_independent_respect_to P)
   proof let P,A,B; assume
  A1: 0 < P.B;
   thus P.|.B.A = P.A implies A,B are_independent_respect_to P
     proof assume P.|.B.A = P.A;
      then P.(A /\ B)/P.B * P.B = P.A * P.B by A1,Def7;
      then P.(A /\ B) = P.A * P.B by A1,XCMPLX_1:88;
      hence thesis by Def5;
     end; assume A,B are_independent_respect_to P;
    then P.(A /\ B) * (P.B)" = P.A * P.B * (P.B)" by Def5;
    then P.(A /\ B) * (P.B)" = P.A * (P.B * (P.B)") by XCMPLX_1:4;
    then P.(A /\ B) * (P.B)" = P.A * 1 by A1,XCMPLX_0:def 7;
    then P.(A /\ B)/P.B = P.A by XCMPLX_0:def 9;
    hence thesis by A1,Def7;
   end;

theorem
   for P,A,B st (0 < P.B & P.B < 1 & P.|.B.A = P.|.([#] Sigma \ B).A) holds
       A,B are_independent_respect_to P
  proof let P,A,B; assume that
 A1: 0 < P.B and
 A2: P.B < 1 and
 A3: P.|.B.A = P.|.([#] Sigma \B).A;
 A4: 0 < P.([#] Sigma \ B) by A2,Th27;
 A5: P.([#] Sigma \ B) <> 0 by A2,Th27;
A6: B`= (Omega \ B) by SUBSET_1:def 5
      .= ([#] Sigma \ B) by PROB_1:def 11;
    P.(A /\ B)/P.B = P.|.([#] Sigma \B).A by A1,A3,Def7;
  then P.(A /\ B)/P.B = P.(A /\ ([#] Sigma \B))/P.([#] Sigma \ B) by A4,Def7;
  then P.(A /\ B) * P.([#] Sigma \ B) = P.(A /\ ([#] Sigma \B)) * P.B by A1,A5,
Th4;
  then P.(A /\ B) * (1 - P.B) = P.(A /\ ([#] Sigma \B)) * P.B by PROB_1:68;
  then P.(A /\ B) * 1 - P.(A /\ B) * P.B = P.(A /\ ([#] Sigma \B)) * P.B
                                                           by XCMPLX_1:40;
  then P.(A /\ B) + - P.(A /\ B) * P.B = P.(A /\ ([#] Sigma \B)) * P.B
                                                           by XCMPLX_0:def 8;
  then P.(A /\ B) = P.(A /\ ([#] Sigma \B)) * P.B -(- P.(A /\ B) * P.B)
                                                           by XCMPLX_1:26
    .= P.(A /\ ([#] Sigma \B)) * P.B + -(- P.(A /\ B) * P.B) by XCMPLX_0:def 8
    .= (P.(A /\ ([#] Sigma \B)) + P.(A /\ B)) * P.B by XCMPLX_1:8
    .= P.A * P.B by A6,Th24;
  hence thesis by Def5;
  end;

theorem
   for P,A,B st 0 < P.B holds (P.A + P.B - 1)/ P.B <= P.|.B.A
  proof let P,A,B such that
 A1: 0 < P.B;
    P.A + P.B - 1 <= P.(A /\ B) by Th25;
  then (P.A + P.B - 1)/P.B <= P.(A /\ B)/P.B by A1,REAL_1:73;
  hence thesis by A1,Def7;
  end;

theorem
Th49: for A,B,P st (0 < P.A & 0 < P.B) holds
  P.|.B.A = P.|.A.B * P.A / P.B
  proof let A,B,P; assume
 A1: 0 < P.A & 0 < P.B;
  hence P.|.A.B * P.A / P.B = P.(A /\ B) / P.B by Th42
                        .= P.|.B.A by A1,Def7;
  end;

theorem
::Bayes' Theorem for Two Events
   for B,A1,A2,P st (0 < P.B & A2 = A1` & 0 < P.A1 & 0 < P.A2) holds
  P.|.B.A1 = (P.|.A1.B * P.A1) / (P.|.A1.B * P.A1 + P.|.A2.B * P.A2) &
   P.|.B.A2 = (P.|.A2.B * P.A2) / (P.|.A1.B * P.A1 + P.|.A2.B * P.A2)
  proof let B,A1,A2,P; assume that
 A1: 0 < P.B and
 A2: A2 = A1` and
 A3: 0 < P.A1 and
 A4: 0 < P.A2;
  thus P.|.A1.B * P.A1 / (P.|.A1.B * P.A1 + P.|.A2.B * P.A2) =
        P.|.A1.B * P.A1 / P.B by A2,A3,A4,Th44
     .= P.|.B.A1 by A1,A3,Th49;
  thus P.|.A2.B * P.A2 / (P.|.A1.B * P.A1 + P.|.A2.B * P.A2) =
        P.|.A2.B * P.A2 / P.B by A2,A3,A4,Th44
     .= P.|.B.A2 by A1,A4,Th49;
  end;

theorem
:: Bayes' Theorem for Three Events
   for B,A1,A2,A3,P st (0<P.B & 0<P.A1 & 0<P.A2 & 0<P.A3 &
                             A1 misses A2 & A3=(A1 \/ A2)`) holds
P.|.B.A1 = (P.|.A1.B * P.A1)/((P.|.A1.B * P.A1 + P.|.A2.B * P.A2) + P.|.
A3.B * P.A3) &
 P.|.B.A2 = (P.|.A2.B * P.A2)/((P.|.A1.B * P.A1 + P.|.A2.B * P.A2) + P.|.
A3.B * P.A3) &
P.|.B.A3 = (P.|.A3.B * P.A3)/((P.|.A1.B * P.A1 + P.|.A2.B * P.A2) + P.|.
A3.B * P.A3)
  proof let B,A1,A2,A3,P; assume that
 A1:  0<P.B and
 A2: 0<P.A1 and
 A3: 0<P.A2 and
 A4: 0<P.A3 and
 A5: A1 misses A2 and
 A6: A3=(A1 \/ A2)`;
   thus (P.|.A1.B * P.A1)/((P.|.A1.B * P.A1 + P.|.A2.B * P.A2) + P.|.
A3.B * P.A3)
       = (P.|.A1.B * P.A1)/P.B by A2,A3,A4,A5,A6,Th45
      .= P.|.B.A1 by A1,A2,Th49;
   thus (P.|.A2.B * P.A2)/((P.|.A1.B * P.A1 + P.|.A2.B * P.A2) + P.|.
A3.B * P.A3)
       = (P.|.A2.B * P.A2)/P.B by A2,A3,A4,A5,A6,Th45
      .= P.|.B.A2 by A1,A3,Th49;
   thus (P.|.A3.B * P.A3)/((P.|.A1.B * P.A1 + P.|.A2.B * P.A2) + P.|.
A3.B * P.A3)
       = (P.|.A3.B * P.A3)/P.B by A2,A3,A4,A5,A6,Th45
      .= P.|.B.A3 by A1,A4,Th49;
  end;

theorem
   for A,B,P st 0 < P.B holds 1 - P.([#] Sigma \ A)/P.B <= P.|.B.A
  proof let A,B,P; assume
 A1: 0 < P.B;
    P.B + P.A - 1 <= P.(A /\ B) by Th25;
  then P.B + (P.A - 1) <= P.(A /\ B) by XCMPLX_1:29;
  then P.B + -(1 - P.A) <= P.(A /\ B) by XCMPLX_1:143;
  then P.B + -P.([#] Sigma \ A) <= P.(A /\ B) by PROB_1:68;
  then (P.B + -P.([#] Sigma \ A))/P.B <= P.(A /\ B)/P.B by A1,REAL_1:73;
  then (P.B + -P.([#] Sigma \ A))/P.B <= P.|.B.A by A1,Def7;
  then (P.B - P.([#] Sigma \ A))/P.B <= P.|.B.A by XCMPLX_0:def 8;
  then P.B/P.B - P.([#] Sigma \ A)/P.B <= P.|.B.A by XCMPLX_1:121;
  hence thesis by A1,XCMPLX_1:60;
  end;

Back to top