Grace/Cumulus/Probability/Conditional.g17

Open in Workbench Download source

Imports

Space

Declarations

Source

1-- Conditional probability, the law of total probability, and Bayes' theorem2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Probability.Conditional8import Space910-- The probability of A given B.11def condProb (P A B : Set) : Set := call2(realDiv, prob(P, A ∩ B), prob(P, B))1213theorem condProb.value (P A B : Set)14  shows condProb(P, A, B) = (prob(P, A ∩ B):R) / (prob(P, B):R)15proof16  simp [condProb]1718theorem prob.ne_zero_of_positive (Ω P B : Set)19  requires space : ProbabilitySpace(Ω, P)20  requires event : B ⊆ Ω21  requires positive : (0:R) < (prob(P, B):R)22  shows prob(P, B) ≠ (0:R)23proof24  have realB := prob.real with space, event25  intro zero26  rw zero at positive27  exact realLess.not_self with positive2829theorem prob.positive_of_ne_zero (Ω P B : Set)30  requires space : ProbabilitySpace(Ω, P)31  requires event : B ⊆ Ω32  requires nonzero : prob(P, B) ≠ (0:R)33  shows (0:R) < (prob(P, B):R)34proof35  have realB := prob.real with space, event36  have nonnegative := prob.nonnegative with space, event37  exact Real.positive_of_nonnegative_of_ne_zero with nonnegative, nonzero3839theorem condProb.real (Ω P A B : Set)40  requires space : ProbabilitySpace(Ω, P)41  requires eventA : A ⊆ Ω42  requires eventB : B ⊆ Ω43  shows Real(condProb(P, A, B))44proof45  have eventMeet : A ∩ B ⊆ Ω by simp46  have realMeet := prob.real with space, eventMeet47  have realB := prob.real with space, eventB48  rw condProb.value49  exact realDiv.real at prob(P, A ∩ B), prob(P, B)5051theorem condProb.nonnegative (Ω P A B : Set)52  requires space : ProbabilitySpace(Ω, P)53  requires eventA : A ⊆ Ω54  requires eventB : B ⊆ Ω55  requires positive : (0:R) < (prob(P, B):R)56  shows (0:R) ≤ (condProb(P, A, B):R)57proof58  have eventMeet : A ∩ B ⊆ Ω by simp59  have realMeet := prob.real with space, eventMeet60  have realB := prob.real with space, eventB61  have nonnegativeMeet := prob.nonnegative with space, eventMeet62  have inversePositive := realInvValue.positive at prob(P, B) with positive63  have inverseReal := realInvValue.real at prob(P, B)64  have inverseNonnegative : (0:R) ≤ (realInvValue(prob(P, B)):R) by linarith65  have division := realDiv.eq_mul_inv at prob(P, A ∩ B), prob(P, B)66  have product := realMulValue.nonnegative at prob(P, A ∩ B),67      realInvValue(prob(P, B)) with68    nonnegativeMeet, inverseNonnegative69  rw [condProb.value, division]70  exact product7172theorem condProb.le_one (Ω P A B : Set)73  requires space : ProbabilitySpace(Ω, P)74  requires eventA : A ⊆ Ω75  requires eventB : B ⊆ Ω76  requires positive : (0:R) < (prob(P, B):R)77  shows (condProb(P, A, B):R) ≤ (1:R)78proof79  have eventMeet : A ∩ B ⊆ Ω by simp80  have realMeet := prob.real with space, eventMeet81  have realB := prob.real with space, eventB82  have nonzero := prob.ne_zero_of_positive with space, eventB, positive83  have bound := prob.intersection_le_right at Ω, P, A, B with space, eventB84  have inversePositive := realInvValue.positive at prob(P, B) with positive85  have inverseReal := realInvValue.real at prob(P, B)86  have inverseNonnegative : (0:R) ≤ (realInvValue(prob(P, B)):R) by linarith87  have division := realDiv.eq_mul_inv at prob(P, A ∩ B), prob(P, B)88  have scaled := realLe.mul_right_of_nonnegative at prob(P, A ∩ B), prob(P, B),89    realInvValue(prob(P, B)) with bound, inverseNonnegative90  have inverseLaw := realInvValue.mul_right at prob(P, B) with nonzero91  rw [condProb.value, division]92  rw inverseLaw at scaled93  exact scaled9495theorem condProb.self (Ω P B : Set)96  requires space : ProbabilitySpace(Ω, P)97  requires eventB : B ⊆ Ω98  requires positive : (0:R) < (prob(P, B):R)99  shows condProb(P, B, B) = (1:R)100proof101  have realB := prob.real with space, eventB102  have nonzero := prob.ne_zero_of_positive with space, eventB, positive103  have same := intersection.idempotent at B104  rw [condProb.value, same]105  exact realDiv.self at prob(P, B) with nonzero106107theorem condProb.whole (Ω P B : Set)108  requires space : ProbabilitySpace(Ω, P)109  requires eventB : B ⊆ Ω110  requires positive : (0:R) < (prob(P, B):R)111  shows condProb(P, Ω, B) = (1:R)112proof113  have realB := prob.real with space, eventB114  have nonzero := prob.ne_zero_of_positive with space, eventB, positive115  have same := intersection.eq_right_of_subset at Ω, B with eventB116  rw [condProb.value, same]117  exact realDiv.self at prob(P, B) with nonzero118119theorem condProb.empty (Ω P B : Set)120  requires space : ProbabilitySpace(Ω, P)121  requires eventB : B ⊆ Ω122  shows condProb(P, ∅, B) = (0:R)123proof124  have realB := prob.real with space, eventB125  have same := intersection.left_empty at B126  have empty := prob.empty at P127  rw [condProb.value, same, empty]128  exact realDiv.zero_left at prob(P, B)129130theorem condProb.of_disjoint (Ω P A B : Set)131  requires space : ProbabilitySpace(Ω, P)132  requires eventB : B ⊆ Ω133  requires disjoint : Disjoint(A, B)134  shows condProb(P, A, B) = (0:R)135proof136  have realB := prob.real with space, eventB137  have same : A ∩ B = ∅ := disjoint138  have empty := prob.empty at P139  rw [condProb.value, same, empty]140  exact realDiv.zero_left at prob(P, B)141142-- The multiplication rule.143theorem condProb.multiplication (Ω P A B : Set)144  requires space : ProbabilitySpace(Ω, P)145  requires eventA : A ⊆ Ω146  requires eventB : B ⊆ Ω147  requires positive : (0:R) < (prob(P, B):R)148  shows prob(P, A ∩ B) = (condProb(P, A, B):R) * (prob(P, B):R)149proof150  have eventMeet : A ∩ B ⊆ Ω by simp151  have realMeet := prob.real with space, eventMeet152  have realB := prob.real with space, eventB153  have nonzero := prob.ne_zero_of_positive with space, eventB, positive154  have cancel := realDiv.mul_right at prob(P, A ∩ B), prob(P, B) with nonzero155  rw condProb.value156  symm157  exact cancel158159theorem condProb.of_subset (Ω P A B : Set)160  requires space : ProbabilitySpace(Ω, P)161  requires inner : A ⊆ B162  shows condProb(P, A, B) = (prob(P, A):R) / (prob(P, B):R)163proof164  have same := intersection.eq_left_of_subset at A, B with inner165  rw [condProb.value, same]166  rfl167168theorem condProb.of_superset (Ω P A B : Set)169  requires space : ProbabilitySpace(Ω, P)170  requires eventB : B ⊆ Ω171  requires inner : B ⊆ A172  requires positive : (0:R) < (prob(P, B):R)173  shows condProb(P, A, B) = (1:R)174proof175  have realB := prob.real with space, eventB176  have nonzero := prob.ne_zero_of_positive with space, eventB, positive177  have same := intersection.eq_right_of_subset at A, B with inner178  rw [condProb.value, same]179  exact realDiv.self at prob(P, B) with nonzero180181theorem condProb.monotone (Ω P A C B : Set)182  requires space : ProbabilitySpace(Ω, P)183  requires eventC : C ⊆ Ω184  requires eventB : B ⊆ Ω185  requires inner : A ⊆ C186  requires positive : (0:R) < (prob(P, B):R)187  shows (condProb(P, A, B):R) ≤ (condProb(P, C, B):R)188proof189  have eventMeetC : C ∩ B ⊆ Ω by simp190  have innerMeet : A ∩ B ⊆ C ∩ B by simp191  have eventMeetA := Subset.transitive with innerMeet, eventMeetC192  have realMeetA := prob.real with space, eventMeetA193  have realMeetC := prob.real with space, eventMeetC194  have realB := prob.real with space, eventB195  have bound := prob.monotone with space, eventMeetC, innerMeet196  have inversePositive := realInvValue.positive at prob(P, B) with positive197  have inverseReal := realInvValue.real at prob(P, B)198  have inverseNonnegative : (0:R) ≤ (realInvValue(prob(P, B)):R) by linarith199  have divisionA := realDiv.eq_mul_inv at prob(P, A ∩ B), prob(P, B)200  have divisionC := realDiv.eq_mul_inv at prob(P, C ∩ B), prob(P, B)201  have scaled := realLe.mul_right_of_nonnegative at prob(P, A ∩ B), prob(P,202      C ∩ B),203    realInvValue(prob(P, B)) with bound, inverseNonnegative204  rw [condProb.value, condProb.value, divisionA, divisionC]205  exact scaled206207theorem condProb.union_disjoint (Ω P A C B : Set)208  requires space : ProbabilitySpace(Ω, P)209  requires eventA : A ⊆ Ω210  requires eventC : C ⊆ Ω211  requires eventB : B ⊆ Ω212  requires disjoint : Disjoint(A, C)213  shows condProb(P, A ∪ C, B) = (condProb(P, A, B):R) + (condProb(P, C, B):R)214proof215  have eventMeetA : A ∩ B ⊆ Ω by simp216  have eventMeetC : C ∩ B ⊆ Ω by simp217  have realMeetA := prob.real with space, eventMeetA218  have realMeetC := prob.real with space, eventMeetC219  have realB := prob.real with space, eventB220  have split : (A ∪ C) ∩ B = (A ∩ B) ∪ (C ∩ B)221    ext y222    simp223  have innerC := intersection.subset_left at C, B224  have innerA := intersection.subset_left at A, B225  have disjointRight := Disjoint.of_subset_right with disjoint, innerC226  have disjointMeet := Disjoint.of_subset_left with disjointRight, innerA227  have union := prob.union_disjoint with space, eventMeetA, eventMeetC,228      disjointMeet229  have division := realDiv.add_left at prob(P, A ∩ B), prob(P, C ∩ B), prob(P,230      B)231  rw [condProb.value, condProb.value, condProb.value, split, union]232  exact division233234theorem condProb.complement (Ω P A B : Set)235  requires space : ProbabilitySpace(Ω, P)236  requires eventA : A ⊆ Ω237  requires eventB : B ⊆ Ω238  requires positive : (0:R) < (prob(P, B):R)239  shows condProb(P, Ω ∖ A, B) = (1:R) - (condProb(P, A, B):R)240proof241  have eventMeet : A ∩ B ⊆ Ω by simp242  have eventRest : B ∖ A ⊆ Ω by simp243  have realMeet := prob.real with space, eventMeet244  have realRest := prob.real with space, eventRest245  have realB := prob.real with space, eventB246  have nonzero := prob.ne_zero_of_positive with space, eventB, positive247  have same : (Ω ∖ A) ∩ B = B ∖ A248    ext y249    simp250  have commute := intersection.commutative at B, A251  have split := prob.difference at Ω, P, B, A with space, eventB252  rw commute at split253  have inverseReal := realInvValue.real at prob(P, B)254  have inverseLaw := realInvValue.mul_right at prob(P, B) with nonzero255  have divisionRest := realDiv.eq_mul_inv at prob(P, B ∖ A), prob(P, B)256  have divisionMeet := realDiv.eq_mul_inv at prob(P, A ∩ B), prob(P, B)257  rw [condProb.value, condProb.value, same, divisionRest, divisionMeet, split]258  calc259    ((prob(P, B):R) - (prob(P, A ∩ B):R)) * (realInvValue(prob(P, B)):R) =260        (prob(P, B):R) * (realInvValue(prob(P, B)):R) -261          (prob(P, A ∩ B):R) * (realInvValue(prob(P, B)):R) := by ring262    _ = (1:R) - (prob(P, A ∩ B):R) * (realInvValue(prob(P, B)):R) := by cc263264-- The law of total probability for the partition B, Ω ∖ B.265theorem condProb.total_probability (Ω P A B : Set)266  requires space : ProbabilitySpace(Ω, P)267  requires eventA : A ⊆ Ω268  requires eventB : B ⊆ Ω269  requires positive : (0:R) < (prob(P, B):R)270  requires positiveRest : (0:R) < (prob(P, Ω ∖ B):R)271  shows prob(P, A) = (condProb(P, A, B):R) * (prob(P, B):R) +272    (condProb(P, A, Ω ∖ B):R) * (prob(P, Ω ∖ B):R)273proof274  have eventRest : Ω ∖ B ⊆ Ω by simp275  have eventMeet : A ∩ B ⊆ Ω by simp276  have eventMeetRest : A ∩ (Ω ∖ B) ⊆ Ω by simp277  have split : (A ∩ B) ∪ (A ∩ (Ω ∖ B)) = A278    ext y279    simp280  have innerB := intersection.subset_right at A, B281  have innerRest := intersection.subset_right at A, Ω ∖ B282  have disjointRest := Disjoint.difference_right at Ω, B283  have disjointRight := Disjoint.of_subset_right with disjointRest, innerRest284  have disjointMeet := Disjoint.of_subset_left with disjointRight, innerB285  have union := prob.union_disjoint with space, eventMeet, eventMeetRest,286      disjointMeet287  have first := condProb.multiplication with space, eventA, eventB, positive288  have second := condProb.multiplication with space, eventA, eventRest,289      positiveRest290  rw split at union291  rw [union, first, second]292  rfl293294theorem condProb.bayes (Ω P A B : Set)295  requires space : ProbabilitySpace(Ω, P)296  requires eventA : A ⊆ Ω297  requires eventB : B ⊆ Ω298  requires positiveA : (0:R) < (prob(P, A):R)299  requires positiveB : (0:R) < (prob(P, B):R)300  shows condProb(P, A, B) = ((condProb(P, B, A):R) * (prob(P, A):R)) / (prob(P,301      B):R)302proof303  have commute := intersection.commutative at A, B304  have product := condProb.multiplication with space, eventB, eventA, positiveA305  rw condProb.value306  rw [commute, product]307  rfl308309-- Conditioning on B is again a probability space on Ω: the weight is310-- rescaled on B and vanishes outside it.311def conditionalWeight (Ω P B : Set) : Set :=312  maskedWeight(Ω, B, weightScale(Ω, realInvValue(prob(P, B)), P))313314theorem conditionalWeight.inverse_real (Ω P B : Set)315  requires space : ProbabilitySpace(Ω, P)316  requires eventB : B ⊆ Ω317  shows Real(realInvValue(prob(P, B)))318proof319  have realB := prob.real with space, eventB320  exact realInvValue.real at prob(P, B)321322theorem conditionalWeight.function (Ω P B : Set)323  requires space : ProbabilitySpace(Ω, P)324  requires eventB : B ⊆ Ω325  shows conditionalWeight(Ω, P, B) : Ω → ℝ326proof327  have function := ProbabilitySpace.function with space328  have inverseReal := conditionalWeight.inverse_real with space, eventB329  have scaled := weightScale.function at Ω, realInvValue(prob(P, B)), P with330      function331  unfold conditionalWeight332  exact maskedWeight.function at Ω, B, weightScale(Ω, realInvValue(prob(P, B)),333    P) with334    scaled335336theorem conditionalWeight.inside (Ω P B ω : Set)337  requires space : ProbabilitySpace(Ω, P)338  requires eventB : B ⊆ Ω339  requires point : ω ∈ Ω340  requires inside : ω ∈ B341  shows conditionalWeight(Ω, P, B)(ω) = (realInvValue(prob(P, B)):R) * (P(ω):R)342proof343  have function := ProbabilitySpace.function with space344  have inverseReal := conditionalWeight.inverse_real with space, eventB345  have scaled := weightScale.function at Ω, realInvValue(prob(P, B)), P with346      function347  have mask := maskedWeight.inside at Ω, B, weightScale(Ω, realInvValue(prob(P,348      B)), P),349    ω with scaled, point, inside350  have value := weightScale.value at Ω, realInvValue(prob(P, B)), P, ω with351      function, point352  unfold conditionalWeight353  cc354355theorem conditionalWeight.outside (Ω P B ω : Set)356  requires space : ProbabilitySpace(Ω, P)357  requires eventB : B ⊆ Ω358  requires point : ω ∈ Ω359  requires outside : ¬(ω ∈ B)360  shows conditionalWeight(Ω, P, B)(ω) = (0:R)361proof362  have function := ProbabilitySpace.function with space363  have inverseReal := conditionalWeight.inverse_real with space, eventB364  have scaled := weightScale.function at Ω, realInvValue(prob(P, B)), P with365      function366  have mask := maskedWeight.outside at Ω, B, weightScale(Ω,367      realInvValue(prob(P, B)), P),368    ω with scaled, point, outside369  unfold conditionalWeight370  cc371372theorem conditionalWeight.nonnegative (Ω P B : Set)373  requires space : ProbabilitySpace(Ω, P)374  requires eventB : B ⊆ Ω375  requires positive : (0:R) < (prob(P, B):R)376  shows ∀ ω ∈ Ω, (0:R) ≤ (conditionalWeight(Ω, P, B)(ω):R)377proof378  intros ω point379  have realB := prob.real with space, eventB380  have inverseReal := conditionalWeight.inverse_real with space, eventB381  have inversePositive := realInvValue.positive at prob(P, B) with positive382  have inverseNonnegative : (0:R) ≤ (realInvValue(prob(P, B)):R) by linarith383  have alternatives : ω ∈ B ∨ ¬(ω ∈ B) by tauto384  cases alternatives with inside | outside385  . have value := conditionalWeight.inside with space, eventB, point, inside386    have pointReal := ProbabilitySpace.point_real with space, point387    have pointNonnegative := ProbabilitySpace.point_nonnegative with space,388        point389    rw value390    exact realMulValue.nonnegative at realInvValue(prob(P, B)), P(ω) with391      inverseNonnegative, pointNonnegative392  . have value := conditionalWeight.outside with space, eventB, point, outside393    rw value394    exact realLe.reflexive with realZero.real395396-- Under the conditional weight an event A has probability condProb(A, B).397theorem conditionalWeight.prob (Ω P B A : Set)398  requires space : ProbabilitySpace(Ω, P)399  requires eventB : B ⊆ Ω400  requires eventA : A ⊆ Ω401  shows prob(conditionalWeight(Ω, P, B), A) = condProb(P, A, B)402proof403  have function := ProbabilitySpace.function with space404  have finiteA := ProbabilitySpace.event_finite with space, eventA405  have inverseReal := conditionalWeight.inverse_real with space, eventB406  have scaled := weightScale.function at Ω, realInvValue(prob(P, B)), P with407      function408  have eventMeet : A ∩ B ⊆ Ω by simp409  have finiteMeet := ProbabilitySpace.event_finite with space, eventMeet410  have realMeet := prob.real with space, eventMeet411  have realB := prob.real with space, eventB412  have masked := realSetSum.masked_intersection at A, B, Ω,413    weightScale(Ω, realInvValue(prob(P, B)), P) with finiteA, scaled, eventA414  have scale := realSetSum.scale at A ∩ B, Ω, P, realInvValue(prob(P, B)) with415    finiteMeet, function, eventMeet416  have division := realDiv.eq_mul_inv at prob(P, A ∩ B), prob(P, B)417  have commute := realMulValue.commutative at realInvValue(prob(P, B)), prob(P,418      A ∩ B)419  have meetValue := prob.value at P, A ∩ B420  rw [prob.value, condProb.value, division]421  unfold conditionalWeight422  cc423424theorem conditionalWeight.total (Ω P B : Set)425  requires space : ProbabilitySpace(Ω, P)426  requires eventB : B ⊆ Ω427  requires positive : (0:R) < (prob(P, B):R)428  shows realSetSum(Ω, conditionalWeight(Ω, P, B)) = (1:R)429proof430  have whole := Subset.reflexive at Ω431  have conditioned := conditionalWeight.prob with space, eventB, whole432  have one := condProb.whole with space, eventB, positive433  rw prob.value at conditioned434  rw conditioned435  exact one436437theorem conditionalWeight.space (Ω P B : Set)438  requires space : ProbabilitySpace(Ω, P)439  requires eventB : B ⊆ Ω440  requires positive : (0:R) < (prob(P, B):R)441  shows ProbabilitySpace(Ω, conditionalWeight(Ω, P, B))442proof443  have finite := ProbabilitySpace.finite with space444  have function := conditionalWeight.function with space, eventB445  have nonnegative := conditionalWeight.nonnegative with space, eventB, positive446  have total := conditionalWeight.total with space, eventB, positive447  exact ProbabilitySpace.intro with finite, function, nonnegative, total448