Grace/Cumulus/Probability/Space.g17

Open in Workbench Download source

Imports

SetSum · Real.AbsoluteValue

Declarations

• ProbabilitySpace predicate
• prob def
• prob.value theorem derivation
• ProbabilitySpace.intro theorem derivation
• ProbabilitySpace.finite theorem derivation
• ProbabilitySpace.function theorem derivation
• ProbabilitySpace.nonnegative theorem derivation
• ProbabilitySpace.total theorem derivation
• ProbabilitySpace.event_finite theorem derivation
• ProbabilitySpace.point_real theorem derivation
• ProbabilitySpace.point_nonnegative theorem derivation
• prob.real theorem derivation
• prob.empty theorem derivation
• prob.whole theorem derivation
• prob.nonnegative theorem derivation
• prob.monotone theorem derivation
• prob.le_one theorem derivation
• prob.union_disjoint theorem derivation
• prob.difference_subset theorem derivation
• prob.complement theorem derivation
• prob.singleton theorem derivation
• prob.zero_of_pointwise theorem derivation
• prob.insert theorem derivation
• prob.remove theorem derivation
• prob.inclusion_exclusion theorem derivation
• prob.union theorem derivation
• prob.union_le theorem derivation
• prob.union_three_le theorem derivation
• prob.intersection_le_left theorem derivation
• prob.intersection_le_right theorem derivation
• prob.difference theorem derivation
• prob.difference_le theorem derivation
• prob.point_le theorem derivation
• ProbabilitySpace.point_le_one theorem derivation
• prob.disjoint_le_one theorem derivation
• prob.complement_zero_iff theorem derivation
• prob.union_disjoint_three theorem derivation
• prob.subset_zero theorem derivation
• prob.superset_one theorem derivation

Source

1-- Finite probability spaces and the probability of an event2-- 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.Space8import SetSum9import Real.AbsoluteValue1011-- A finite probability space: a finite sample space Ω with nonnegative12-- weights P(ω) that sum to one.13predicate ProbabilitySpace (Ω P : Set) :=14  Finite(Ω) ∧ FunctionBetween(P, Ω, ℝ) ∧15    (∀ ω ∈ Ω, (0:R) ≤ (P(ω):R)) ∧ realSetSum(Ω, P) = (1:R)1617-- The probability of an event A ⊆ Ω is the total weight of its points.18def prob (P A : Set) : Set := realSetSum(A, P)1920theorem prob.value (P A : Set)21  shows prob(P, A) = realSetSum(A, P)22proof23  simp [prob]2425theorem ProbabilitySpace.intro (Ω P : Set)26  requires finite : Finite(Ω)27  requires function : P : Ω → ℝ28  requires nonnegative : ∀ ω ∈ Ω, (0:R) ≤ (P(ω):R)29  requires total : realSetSum(Ω, P) = (1:R)30  shows ProbabilitySpace(Ω, P)31proof32  unfold ProbabilitySpace33  refine ⟨finite, function, nonnegative, total⟩3435theorem ProbabilitySpace.finite (Ω P : Set)36  requires space : ProbabilitySpace(Ω, P)37  shows Finite(Ω)38proof39  unfold ProbabilitySpace at space40  exact space.left4142theorem ProbabilitySpace.function (Ω P : Set)43  requires space : ProbabilitySpace(Ω, P)44  shows P : Ω → ℝ45proof46  unfold ProbabilitySpace at space47  exact space.right.left4849theorem ProbabilitySpace.nonnegative (Ω P : Set)50  requires space : ProbabilitySpace(Ω, P)51  shows ∀ ω ∈ Ω, (0:R) ≤ (P(ω):R)52proof53  unfold ProbabilitySpace at space54  exact space.right.right.left5556theorem ProbabilitySpace.total (Ω P : Set)57  requires space : ProbabilitySpace(Ω, P)58  shows realSetSum(Ω, P) = (1:R)59proof60  unfold ProbabilitySpace at space61  exact space.right.right.right6263theorem ProbabilitySpace.event_finite (Ω P A : Set)64  requires space : ProbabilitySpace(Ω, P)65  requires event : A ⊆ Ω66  shows Finite(A)67proof68  have finite := ProbabilitySpace.finite with space69  exact Finite.subset with finite, event7071theorem ProbabilitySpace.point_real (Ω P ω : Set)72  requires space : ProbabilitySpace(Ω, P)73  requires point : ω ∈ Ω74  shows Real(P(ω))75proof76  have function := ProbabilitySpace.function with space77  exact FunctionBetween.apply_closed with function, point7879theorem ProbabilitySpace.point_nonnegative (Ω P ω : Set)80  requires space : ProbabilitySpace(Ω, P)81  requires point : ω ∈ Ω82  shows (0:R) ≤ (P(ω):R)83proof84  have nonnegative := ProbabilitySpace.nonnegative with space85  exact nonnegative with ω, point8687theorem prob.real (Ω P A : Set)88  requires space : ProbabilitySpace(Ω, P)89  requires event : A ⊆ Ω90  shows Real(prob(P, A))91proof92  have function := ProbabilitySpace.function with space93  have finite := ProbabilitySpace.event_finite with space, event94  have sum := realSetSum.real with finite, function, event95  rw prob.value96  exact sum9798theorem prob.empty (P : Set)99  shows prob(P, ∅) = (0:R)100proof101  rw prob.value102  exact realSetSum.empty at P103104theorem prob.whole (Ω P : Set)105  requires space : ProbabilitySpace(Ω, P)106  shows prob(P, Ω) = (1:R)107proof108  rw prob.value109  exact ProbabilitySpace.total with space110111theorem prob.nonnegative (Ω P A : Set)112  requires space : ProbabilitySpace(Ω, P)113  requires event : A ⊆ Ω114  shows (0:R) ≤ (prob(P, A):R)115proof116  have function := ProbabilitySpace.function with space117  have nonnegative := ProbabilitySpace.nonnegative with space118  have finite := ProbabilitySpace.event_finite with space, event119  have bounds : ∀ x ∈ A, (0:R) ≤ (P(x):R)120    intros x hx121    have member := event with x, hx122    exact nonnegative with x, member123  have sum := realSetSum.nonnegative with finite, function, event, bounds124  rw prob.value125  exact sum126127theorem prob.monotone (Ω P A B : Set)128  requires space : ProbabilitySpace(Ω, P)129  requires eventB : B ⊆ Ω130  requires inner : A ⊆ B131  shows (prob(P, A):R) ≤ (prob(P, B):R)132proof133  have function := ProbabilitySpace.function with space134  have nonnegative := ProbabilitySpace.nonnegative with space135  have finite := ProbabilitySpace.event_finite with space, eventB136  have bounds : ∀ x ∈ B, (0:R) ≤ (P(x):R)137    intros x hx138    have member := eventB with x, hx139    exact nonnegative with x, member140  have sum := realSetSum.subset_le with finite, function, eventB, inner, bounds141  rw [prob.value, prob.value]142  exact sum143144theorem prob.le_one (Ω P A : Set)145  requires space : ProbabilitySpace(Ω, P)146  requires event : A ⊆ Ω147  shows (prob(P, A):R) ≤ (1:R)148proof149  have whole := Subset.reflexive at Ω150  have bound := prob.monotone with space, whole, event151  have total := prob.whole with space152  rwa total at bound153154theorem prob.union_disjoint (Ω P A B : Set)155  requires space : ProbabilitySpace(Ω, P)156  requires eventA : A ⊆ Ω157  requires eventB : B ⊆ Ω158  requires disjoint : Disjoint(A, B)159  shows prob(P, A ∪ B) = (prob(P, A):R) + (prob(P, B):R)160proof161  have function := ProbabilitySpace.function with space162  have finiteA := ProbabilitySpace.event_finite with space, eventA163  have finiteB := ProbabilitySpace.event_finite with space, eventB164  have sum := realSetSum.union_disjoint with finiteA, finiteB, function,165    eventA, eventB, disjoint166  rw [prob.value, prob.value, prob.value]167  exact sum168169theorem prob.difference_subset (Ω P A B : Set)170  requires space : ProbabilitySpace(Ω, P)171  requires eventA : A ⊆ Ω172  requires inner : B ⊆ A173  shows prob(P, A ∖ B) = (prob(P, A):R) - (prob(P, B):R)174proof175  have function := ProbabilitySpace.function with space176  have finiteA := ProbabilitySpace.event_finite with space, eventA177  have split := realSetSum.difference with finiteA, function, eventA, inner178  have rest := difference.subset_left at A, B179  have eventRest := Subset.transitive with rest, eventA180  have eventB := Subset.transitive with inner, eventA181  have finiteB := Finite.subset with finiteA, inner182  have finiteRest := Finite.subset with finiteA, rest183  have realA := realSetSum.real with finiteA, function, eventA184  have realB := realSetSum.real with finiteB, function, eventB185  have realRest := realSetSum.real with finiteRest, function, eventRest186  rw [prob.value, prob.value, prob.value]187  linarith188189theorem prob.complement (Ω P A : Set)190  requires space : ProbabilitySpace(Ω, P)191  requires event : A ⊆ Ω192  shows prob(P, Ω ∖ A) = (1:R) - (prob(P, A):R)193proof194  have whole := Subset.reflexive at Ω195  have difference := prob.difference_subset with space, whole, event196  have total := prob.whole with space197  rwa total at difference198199theorem prob.singleton (Ω P ω : Set)200  requires space : ProbabilitySpace(Ω, P)201  requires point : ω ∈ Ω202  shows prob(P, {ω}) = P(ω)203proof204  have function := ProbabilitySpace.function with space205  rw prob.value206  exact realSetSum.singleton with function, point207208theorem prob.zero_of_pointwise (Ω P A : Set)209  requires space : ProbabilitySpace(Ω, P)210  requires event : A ⊆ Ω211  requires vanishes : ∀ ω ∈ A, P(ω) = (0:R)212  shows prob(P, A) = (0:R)213proof214  have function := ProbabilitySpace.function with space215  have finite := ProbabilitySpace.event_finite with space, event216  rw prob.value217  exact realSetSum.zero with finite, function, event, vanishes218219theorem prob.insert (Ω P A ω : Set)220  requires space : ProbabilitySpace(Ω, P)221  requires event : A ⊆ Ω222  requires point : ω ∈ Ω223  requires fresh : ¬(ω ∈ A)224  shows prob(P, insert(ω, A)) = (prob(P, A):R) + (P(ω):R)225proof226  have function := ProbabilitySpace.function with space227  have finite := ProbabilitySpace.event_finite with space, event228  rw [prob.value, prob.value]229  exact realSetSum.insert with finite, function, event, point, fresh230231theorem prob.remove (Ω P A ω : Set)232  requires space : ProbabilitySpace(Ω, P)233  requires event : A ⊆ Ω234  requires point : ω ∈ A235  shows prob(P, A) = (prob(P, A ∖ {ω}):R) + (P(ω):R)236proof237  have function := ProbabilitySpace.function with space238  have finite := ProbabilitySpace.event_finite with space, event239  rw [prob.value, prob.value]240  exact realSetSum.insert_member with finite, function, event, point241242theorem prob.inclusion_exclusion (Ω P A B : Set)243  requires space : ProbabilitySpace(Ω, P)244  requires eventA : A ⊆ Ω245  requires eventB : B ⊆ Ω246  shows (prob(P, A ∪ B):R) + (prob(P, A ∩ B):R) = (prob(P, A):R) + (prob(P,247      B):R)248proof249  have restSubset := difference.subset_left at B, A250  have meetSubset := intersection.subset_right at A, B251  have meetLeft := intersection.subset_left at A, B252  have eventRest := Subset.transitive with restSubset, eventB253  have eventMeet := Subset.transitive with meetSubset, eventB254  have disjointRest := Disjoint.difference_right at B, A255  have disjointMeet := Disjoint.of_subset_left with disjointRest, meetLeft256  have unionSplit : A ∪ (B ∖ A) = A ∪ B257    ext y258    simp259  have meetSplit : (A ∩ B) ∪ (B ∖ A) = B260    ext y261    simp262  have first := prob.union_disjoint with space, eventA, eventRest, disjointRest263  have second := prob.union_disjoint with space, eventMeet, eventRest,264      disjointMeet265  rw unionSplit at first266  rw meetSplit at second267  have realA := prob.real with space, eventA268  have realB := prob.real with space, eventB269  have realMeet := prob.real with space, eventMeet270  have realRest := prob.real with space, eventRest271  have realUnion : Real(prob(P, A ∪ B))272    have eventUnion : A ∪ B ⊆ Ω by simp273    exact prob.real with space, eventUnion274  linarith275276theorem prob.union (Ω P A B : Set)277  requires space : ProbabilitySpace(Ω, P)278  requires eventA : A ⊆ Ω279  requires eventB : B ⊆ Ω280  shows prob(P, A ∪ B) = ((prob(P, A):R) + (prob(P, B):R)) - (prob(P, A ∩ B):R)281proof282  have identity := prob.inclusion_exclusion with space, eventA, eventB283  have eventUnion : A ∪ B ⊆ Ω by simp284  have eventMeet : A ∩ B ⊆ Ω by simp285  have realA := prob.real with space, eventA286  have realB := prob.real with space, eventB287  have realMeet := prob.real with space, eventMeet288  have realUnion := prob.real with space, eventUnion289  linarith290291theorem prob.union_le (Ω P A B : Set)292  requires space : ProbabilitySpace(Ω, P)293  requires eventA : A ⊆ Ω294  requires eventB : B ⊆ Ω295  shows (prob(P, A ∪ B):R) ≤ (prob(P, A):R) + (prob(P, B):R)296proof297  have identity := prob.inclusion_exclusion with space, eventA, eventB298  have eventUnion : A ∪ B ⊆ Ω by simp299  have eventMeet : A ∩ B ⊆ Ω by simp300  have realA := prob.real with space, eventA301  have realB := prob.real with space, eventB302  have realMeet := prob.real with space, eventMeet303  have realUnion := prob.real with space, eventUnion304  have nonnegative := prob.nonnegative with space, eventMeet305  linarith306307theorem prob.union_three_le (Ω P A B C : Set)308  requires space : ProbabilitySpace(Ω, P)309  requires eventA : A ⊆ Ω310  requires eventB : B ⊆ Ω311  requires eventC : C ⊆ Ω312  shows (prob(P, A ∪ B ∪ C):R) ≤313    ((prob(P, A):R) + (prob(P, B):R)) + (prob(P, C):R)314proof315  have eventUnion : A ∪ B ⊆ Ω by simp316  have first := prob.union_le with space, eventUnion, eventC317  have second := prob.union_le with space, eventA, eventB318  have eventAll : A ∪ B ∪ C ⊆ Ω by simp319  have realA := prob.real with space, eventA320  have realB := prob.real with space, eventB321  have realC := prob.real with space, eventC322  have realUnion := prob.real with space, eventUnion323  have realAll := prob.real with space, eventAll324  linarith325326theorem prob.intersection_le_left (Ω P A B : Set)327  requires space : ProbabilitySpace(Ω, P)328  requires eventA : A ⊆ Ω329  shows (prob(P, A ∩ B):R) ≤ (prob(P, A):R)330proof331  have inner := intersection.subset_left at A, B332  exact prob.monotone with space, eventA, inner333334theorem prob.intersection_le_right (Ω P A B : Set)335  requires space : ProbabilitySpace(Ω, P)336  requires eventB : B ⊆ Ω337  shows (prob(P, A ∩ B):R) ≤ (prob(P, B):R)338proof339  have inner := intersection.subset_right at A, B340  exact prob.monotone with space, eventB, inner341342theorem prob.difference (Ω P A B : Set)343  requires space : ProbabilitySpace(Ω, P)344  requires eventA : A ⊆ Ω345  shows prob(P, A ∖ B) = (prob(P, A):R) - (prob(P, A ∩ B):R)346proof347  have inner := intersection.subset_left at A, B348  have split := prob.difference_subset with space, eventA, inner349  have same := difference.of_intersection at A, B350  rwa same at split351352theorem prob.difference_le (Ω P A B : Set)353  requires space : ProbabilitySpace(Ω, P)354  requires eventA : A ⊆ Ω355  shows (prob(P, A ∖ B):R) ≤ (prob(P, A):R)356proof357  have inner := difference.subset_left at A, B358  exact prob.monotone with space, eventA, inner359360theorem prob.point_le (Ω P A ω : Set)361  requires space : ProbabilitySpace(Ω, P)362  requires event : A ⊆ Ω363  requires point : ω ∈ A364  shows (P(ω):R) ≤ (prob(P, A):R)365proof366  have member := event with ω, point367  have inner : {ω} ⊆ A by simp368  have bound := prob.monotone with space, event, inner369  have singleton := prob.singleton with space, member370  rwa singleton at bound371372theorem ProbabilitySpace.point_le_one (Ω P ω : Set)373  requires space : ProbabilitySpace(Ω, P)374  requires point : ω ∈ Ω375  shows (P(ω):R) ≤ (1:R)376proof377  have whole := Subset.reflexive at Ω378  have bound := prob.point_le with space, whole, point379  have total := prob.whole with space380  rwa total at bound381382theorem prob.disjoint_le_one (Ω P A B : Set)383  requires space : ProbabilitySpace(Ω, P)384  requires eventA : A ⊆ Ω385  requires eventB : B ⊆ Ω386  requires disjoint : Disjoint(A, B)387  shows (prob(P, A):R) + (prob(P, B):R) ≤ (1:R)388proof389  have union := prob.union_disjoint with space, eventA, eventB, disjoint390  have eventUnion : A ∪ B ⊆ Ω by simp391  have bound := prob.le_one with space, eventUnion392  rwa union at bound393394theorem prob.complement_zero_iff (Ω P A : Set)395  requires space : ProbabilitySpace(Ω, P)396  requires event : A ⊆ Ω397  shows prob(P, Ω ∖ A) = (0:R) ↔ prob(P, A) = (1:R)398proof399  have complement := prob.complement with space, event400  have realA := prob.real with space, event401  have eventRest := difference.subset_left at Ω, A402  have realRest := prob.real with space, eventRest403  constructor404  . intro zero405    linarith406  . intro one407    linarith408409theorem prob.union_disjoint_three (Ω P A B C : Set)410  requires space : ProbabilitySpace(Ω, P)411  requires eventA : A ⊆ Ω412  requires eventB : B ⊆ Ω413  requires eventC : C ⊆ Ω414  requires disjointAB : Disjoint(A, B)415  requires disjointAC : Disjoint(A, C)416  requires disjointBC : Disjoint(B, C)417  shows prob(P, A ∪ B ∪ C) =418    ((prob(P, A):R) + (prob(P, B):R)) + (prob(P, C):R)419proof420  have eventUnion : A ∪ B ⊆ Ω by simp421  have disjointUnion := Disjoint.union2_iff.backward at A, B, C with422    ⟨disjointAC, disjointBC⟩423  have first := prob.union_disjoint with space, eventUnion, eventC,424      disjointUnion425  have second := prob.union_disjoint with space, eventA, eventB, disjointAB426  rw [first, second]427  rfl428429theorem prob.subset_zero (Ω P A B : Set)430  requires space : ProbabilitySpace(Ω, P)431  requires eventA : A ⊆ Ω432  requires inner : B ⊆ A433  requires zero : prob(P, A) = (0:R)434  shows prob(P, B) = (0:R)435proof436  have eventB := Subset.transitive with inner, eventA437  have realA := prob.real with space, eventA438  have realB := prob.real with space, eventB439  have upper := prob.monotone with space, eventA, inner440  have lower := prob.nonnegative with space, eventB441  linarith442443theorem prob.superset_one (Ω P A B : Set)444  requires space : ProbabilitySpace(Ω, P)445  requires eventB : B ⊆ Ω446  requires inner : A ⊆ B447  requires one : prob(P, A) = (1:R)448  shows prob(P, B) = (1:R)449proof450  have eventA := Subset.transitive with inner, eventB451  have realA := prob.real with space, eventA452  have realB := prob.real with space, eventB453  have lower := prob.monotone with space, eventB, inner454  have upper := prob.le_one with space, eventB455  linarith456