Grace/Cumulus/Probability/Independence.g17

Open in Workbench Download source

Imports

Conditional

Declarations

Source

1-- Independent events2-- 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.Independence8import Conditional910-- Two events are independent when the probability of both is the product.11predicate IndependentEvents (P A B : Set) :=12  prob(P, A ∩ B) = (prob(P, A):R) * (prob(P, B):R)1314theorem IndependentEvents.product (P A B : Set)15  requires independent : IndependentEvents(P, A, B)16  shows prob(P, A ∩ B) = (prob(P, A):R) * (prob(P, B):R)17proof18  unfold IndependentEvents at independent19  exact independent2021theorem IndependentEvents.intro (P A B : Set)22  requires product : prob(P, A ∩ B) = (prob(P, A):R) * (prob(P, B):R)23  shows IndependentEvents(P, A, B)24proof25  unfold IndependentEvents26  exact product2728theorem IndependentEvents.symmetric (Ω P A B : Set)29  requires space : ProbabilitySpace(Ω, P)30  requires eventA : A ⊆ Ω31  requires eventB : B ⊆ Ω32  requires independent : IndependentEvents(P, A, B)33  shows IndependentEvents(P, B, A)34proof35  have product := IndependentEvents.product with independent36  have realA := prob.real with space, eventA37  have realB := prob.real with space, eventB38  have commute := intersection.commutative at B, A39  have swap := realMulValue.commutative at prob(P, B), prob(P, A)40  unfold IndependentEvents41  rw [commute, product]42  symm43  exact swap4445theorem IndependentEvents.whole_left (Ω P A : Set)46  requires space : ProbabilitySpace(Ω, P)47  requires eventA : A ⊆ Ω48  shows IndependentEvents(P, Ω, A)49proof50  have realA := prob.real with space, eventA51  have same := intersection.eq_right_of_subset at Ω, A with eventA52  have total := prob.whole with space53  unfold IndependentEvents54  rw [same, total]55  ring5657theorem IndependentEvents.whole_right (Ω P A : Set)58  requires space : ProbabilitySpace(Ω, P)59  requires eventA : A ⊆ Ω60  shows IndependentEvents(P, A, Ω)61proof62  have whole := Subset.reflexive at Ω63  have left := IndependentEvents.whole_left with space, eventA64  exact IndependentEvents.symmetric with space, whole, eventA, left6566theorem IndependentEvents.empty_left (Ω P A : Set)67  requires space : ProbabilitySpace(Ω, P)68  requires eventA : A ⊆ Ω69  shows IndependentEvents(P, ∅, A)70proof71  have realA := prob.real with space, eventA72  have same := intersection.left_empty at A73  have empty := prob.empty at P74  unfold IndependentEvents75  rw [same, empty]76  ring7778theorem IndependentEvents.empty_right (Ω P A : Set)79  requires space : ProbabilitySpace(Ω, P)80  requires eventA : A ⊆ Ω81  shows IndependentEvents(P, A, ∅)82proof83  have empty := empty.subset at Ω84  have left := IndependentEvents.empty_left with space, eventA85  exact IndependentEvents.symmetric with space, empty, eventA, left8687theorem IndependentEvents.complement_right (Ω P A B : Set)88  requires space : ProbabilitySpace(Ω, P)89  requires eventA : A ⊆ Ω90  requires eventB : B ⊆ Ω91  requires independent : IndependentEvents(P, A, B)92  shows IndependentEvents(P, A, Ω ∖ B)93proof94  have product := IndependentEvents.product with independent95  have realA := prob.real with space, eventA96  have realB := prob.real with space, eventB97  have same : A ∩ (Ω ∖ B) = A ∖ B98    ext y99    simp100  have split := prob.difference at Ω, P, A, B with space, eventA101  have complement := prob.complement with space, eventB102  unfold IndependentEvents103  rw [same, split, product, complement]104  ring105106theorem IndependentEvents.complement_left (Ω P A B : Set)107  requires space : ProbabilitySpace(Ω, P)108  requires eventA : A ⊆ Ω109  requires eventB : B ⊆ Ω110  requires independent : IndependentEvents(P, A, B)111  shows IndependentEvents(P, Ω ∖ A, B)112proof113  have eventRest : Ω ∖ A ⊆ Ω by simp114  have swapped := IndependentEvents.symmetric with space, eventA, eventB,115      independent116  have complemented := IndependentEvents.complement_right with space, eventB,117      eventA, swapped118  exact IndependentEvents.symmetric with space, eventB, eventRest, complemented119120theorem IndependentEvents.complement_both (Ω P A B : Set)121  requires space : ProbabilitySpace(Ω, P)122  requires eventA : A ⊆ Ω123  requires eventB : B ⊆ Ω124  requires independent : IndependentEvents(P, A, B)125  shows IndependentEvents(P, Ω ∖ A, Ω ∖ B)126proof127  have eventRest : Ω ∖ B ⊆ Ω by simp128  have right := IndependentEvents.complement_right with space, eventA, eventB,129      independent130  exact IndependentEvents.complement_left with space, eventA, eventRest, right131132-- Independence means that conditioning on B does not change the odds of A.133theorem IndependentEvents.condProb (Ω P A B : Set)134  requires space : ProbabilitySpace(Ω, P)135  requires eventA : A ⊆ Ω136  requires eventB : B ⊆ Ω137  requires positive : (0:R) < (prob(P, B):R)138  requires independent : IndependentEvents(P, A, B)139  shows condProb(P, A, B) = prob(P, A)140proof141  have product := IndependentEvents.product with independent142  have realA := prob.real with space, eventA143  have realB := prob.real with space, eventB144  have nonzero := prob.ne_zero_of_positive with space, eventB, positive145  have pull := realDiv.mul_numerator_left at prob(P, A), prob(P, B), prob(P, B)146  have self := realDiv.self at prob(P, B) with nonzero147  have one := realMulValue.one_right at prob(P, A)148  rw [condProb.value, product, pull, self]149  exact one150151theorem IndependentEvents.of_condProb (Ω P A B : Set)152  requires space : ProbabilitySpace(Ω, P)153  requires eventA : A ⊆ Ω154  requires eventB : B ⊆ Ω155  requires positive : (0:R) < (prob(P, B):R)156  requires conditioned : condProb(P, A, B) = prob(P, A)157  shows IndependentEvents(P, A, B)158proof159  have product := condProb.multiplication with space, eventA, eventB, positive160  rw conditioned at product161  exact IndependentEvents.intro with product162163theorem IndependentEvents.of_prob_zero (Ω P A B : Set)164  requires space : ProbabilitySpace(Ω, P)165  requires eventA : A ⊆ Ω166  requires eventB : B ⊆ Ω167  requires zero : prob(P, A) = (0:R)168  shows IndependentEvents(P, A, B)169proof170  have eventMeet : A ∩ B ⊆ Ω by simp171  have realMeet := prob.real with space, eventMeet172  have realA := prob.real with space, eventA173  have realB := prob.real with space, eventB174  have upper := prob.intersection_le_left at Ω, P, A, B with space, eventA175  have lower := prob.nonnegative with space, eventMeet176  have vanishes : prob(P, A ∩ B) = (0:R) by linarith177  unfold IndependentEvents178  rw [vanishes, zero]179  ring180181theorem IndependentEvents.of_prob_one (Ω P A B : Set)182  requires space : ProbabilitySpace(Ω, P)183  requires eventA : A ⊆ Ω184  requires eventB : B ⊆ Ω185  requires one : prob(P, A) = (1:R)186  shows IndependentEvents(P, A, B)187proof188  have eventMeet : A ∩ B ⊆ Ω by simp189  have eventRest : B ∖ A ⊆ Ω by simp190  have innerRest : B ∖ A ⊆ Ω ∖ A by simp191  have eventComplement : Ω ∖ A ⊆ Ω by simp192  have realA := prob.real with space, eventA193  have realMeet := prob.real with space, eventMeet194  have realRest := prob.real with space, eventRest195  have realComplement := prob.real with space, eventComplement196  have realB := prob.real with space, eventB197  have complement := prob.complement with space, eventA198  have bound := prob.monotone with space, eventComplement, innerRest199  have lower := prob.nonnegative with space, eventRest200  have split := prob.difference at Ω, P, B, A with space, eventB201  have commute := intersection.commutative at B, A202  rw commute at split203  have meetValue : prob(P, A ∩ B) = prob(P, B) by linarith204  unfold IndependentEvents205  rw [meetValue, one]206  ring207208theorem IndependentEvents.union_left (Ω P A C B : Set)209  requires space : ProbabilitySpace(Ω, P)210  requires eventA : A ⊆ Ω211  requires eventC : C ⊆ Ω212  requires eventB : B ⊆ Ω213  requires disjoint : Disjoint(A, C)214  requires independentA : IndependentEvents(P, A, B)215  requires independentC : IndependentEvents(P, C, B)216  shows IndependentEvents(P, A ∪ C, B)217proof218  have productA := IndependentEvents.product with independentA219  have productC := IndependentEvents.product with independentC220  have realA := prob.real with space, eventA221  have realC := prob.real with space, eventC222  have realB := prob.real with space, eventB223  have eventMeetA : A ∩ B ⊆ Ω by simp224  have eventMeetC : C ∩ B ⊆ Ω by simp225  have split : (A ∪ C) ∩ B = (A ∩ B) ∪ (C ∩ B)226    ext y227    simp228  have innerC := intersection.subset_left at C, B229  have innerA := intersection.subset_left at A, B230  have disjointRight := Disjoint.of_subset_right with disjoint, innerC231  have disjointMeet := Disjoint.of_subset_left with disjointRight, innerA232  have union := prob.union_disjoint with space, eventMeetA, eventMeetC,233      disjointMeet234  have wholeUnion := prob.union_disjoint with space, eventA, eventC, disjoint235  unfold IndependentEvents236  rw [split, union, productA, productC, wholeUnion]237  ring238239-- Three events, pairwise and mutually.240predicate PairwiseIndependent (P A B C : Set) :=241  IndependentEvents(P, A, B) ∧ IndependentEvents(P, A,242    C) ∧ IndependentEvents(P, B, C)243244predicate MutuallyIndependent (P A B C : Set) :=245  PairwiseIndependent(P, A, B, C) ∧246    prob(P, A ∩ B ∩ C) = ((prob(P, A):R) * (prob(P, B):R)) * (prob(P, C):R)247248theorem PairwiseIndependent.first (P A B C : Set)249  requires pairwise : PairwiseIndependent(P, A, B, C)250  shows IndependentEvents(P, A, B)251proof252  unfold PairwiseIndependent at pairwise253  exact pairwise.left254255theorem PairwiseIndependent.second (P A B C : Set)256  requires pairwise : PairwiseIndependent(P, A, B, C)257  shows IndependentEvents(P, A, C)258proof259  unfold PairwiseIndependent at pairwise260  exact pairwise.right.left261262theorem PairwiseIndependent.third (P A B C : Set)263  requires pairwise : PairwiseIndependent(P, A, B, C)264  shows IndependentEvents(P, B, C)265proof266  unfold PairwiseIndependent at pairwise267  exact pairwise.right.right268269theorem PairwiseIndependent.swap (Ω P A B C : Set)270  requires space : ProbabilitySpace(Ω, P)271  requires eventA : A ⊆ Ω272  requires eventB : B ⊆ Ω273  requires pairwise : PairwiseIndependent(P, A, B, C)274  shows PairwiseIndependent(P, B, A, C)275proof276  have first := PairwiseIndependent.first with pairwise277  have second := PairwiseIndependent.second with pairwise278  have third := PairwiseIndependent.third with pairwise279  have swapped := IndependentEvents.symmetric with space, eventA, eventB, first280  unfold PairwiseIndependent281  refine ⟨swapped, third, second⟩282283theorem MutuallyIndependent.pairwise (P A B C : Set)284  requires mutual : MutuallyIndependent(P, A, B, C)285  shows PairwiseIndependent(P, A, B, C)286proof287  unfold MutuallyIndependent at mutual288  exact mutual.left289290theorem MutuallyIndependent.triple (P A B C : Set)291  requires mutual : MutuallyIndependent(P, A, B, C)292  shows prob(P, A ∩ B ∩ C) = ((prob(P, A):R) * (prob(P, B):R)) * (prob(P, C):R)293proof294  unfold MutuallyIndependent at mutual295  exact mutual.right296297-- Under mutual independence the intersection A ∩ B is independent of C.298theorem MutuallyIndependent.intersection_left (P A B C : Set)299  requires mutual : MutuallyIndependent(P, A, B, C)300  shows IndependentEvents(P, A ∩ B, C)301proof302  have pairwise := MutuallyIndependent.pairwise with mutual303  have first := PairwiseIndependent.first with pairwise304  have productAB := IndependentEvents.product with first305  have triple := MutuallyIndependent.triple with mutual306  unfold IndependentEvents307  rw [triple, productAB]308  rfl309