Grace/Cumulus/Probability/RandomVariable.g17

Open in Workbench Download source

Imports

Independence

Declarations

Source

1-- Real random variables and expectation2-- 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.RandomVariable8import Independence910-- Pointwise product of two real-valued functions on the same domain.11defgraph weightMul (Ω w v : Set) (x ∈ Ω) : ℝ := call2(realMul, w(x), v(x))12requires weightsW : w : Ω → ℝ13requires weightsV : v : Ω → ℝ14proof15  have left := FunctionBetween.apply_closed with weightsW, member16  have right := FunctionBetween.apply_closed with weightsV, member17  exact realMulValue.real at w(x), v(x)1819-- Pointwise difference of two real-valued functions on the same domain.20defgraph weightSub (Ω w v : Set) (x ∈ Ω) : ℝ := realSubValue(w(x), v(x))21requires weightsW : w : Ω → ℝ22requires weightsV : v : Ω → ℝ23proof24  have left := FunctionBetween.apply_closed with weightsW, member25  have right := FunctionBetween.apply_closed with weightsV, member26  exact realSubValue.real at w(x), v(x)2728-- The expectation of a random variable X : Ω → ℝ is the P-weighted sum of29-- its values.30def expectation (Ω P X : Set) : Set := realSetSum(Ω, weightMul(Ω, P, X))3132theorem expectation.value (Ω P X : Set)33  shows expectation(Ω, P, X) = realSetSum(Ω, weightMul(Ω, P, X))34proof35  simp [expectation]3637theorem expectation.real (Ω P X : Set)38  requires space : ProbabilitySpace(Ω, P)39  requires random : X : Ω → ℝ40  shows Real(expectation(Ω, P, X))41proof42  have finite := ProbabilitySpace.finite with space43  have function := ProbabilitySpace.function with space44  have whole := Subset.reflexive at Ω45  have product := weightMul.function with function, random46  rw expectation.value47  exact realSetSum.real with finite, product, whole4849theorem expectation.congr (Ω P X Y : Set)50  requires space : ProbabilitySpace(Ω, P)51  requires variableX : X : Ω → ℝ52  requires variableY : Y : Ω → ℝ53  requires values : ∀ ω ∈ Ω, X(ω) = Y(ω)54  shows expectation(Ω, P, X) = expectation(Ω, P, Y)55proof56  have function := ProbabilitySpace.function with space57  have whole := Subset.reflexive at Ω58  have productX := weightMul.function with function, variableX59  have productY := weightMul.function with function, variableY60  have agree : ∀ ω ∈ Ω, weightMul(Ω, P, X)(ω) = weightMul(Ω, P, Y)(ω)61    intros ω point62    have left := weightMul.value at Ω, P, X, ω with function, variableX, point63    have right := weightMul.value at Ω, P, Y, ω with function, variableY, point64    have equal := values with ω, point65    rw [left, right, equal]66    rfl67  rw [expectation.value, expectation.value]68  exact realSetSum.congr with productX, productY, whole, agree6970-- Linearity of expectation.71theorem expectation.add (Ω P X Y : Set)72  requires space : ProbabilitySpace(Ω, P)73  requires variableX : X : Ω → ℝ74  requires variableY : Y : Ω → ℝ75  shows expectation(Ω, P, weightAdd(Ω, X, Y)) =76    (expectation(Ω, P, X):R) + (expectation(Ω, P, Y):R)77proof78  have finite := ProbabilitySpace.finite with space79  have function := ProbabilitySpace.function with space80  have whole := Subset.reflexive at Ω81  have sum := weightAdd.function with variableX, variableY82  have productX := weightMul.function with function, variableX83  have productY := weightMul.function with function, variableY84  have productSum := weightMul.function with function, sum85  have combined := weightAdd.function with productX, productY86  have agree : ∀ ω ∈ Ω, weightMul(Ω, P, weightAdd(Ω, X, Y))(ω) =87      weightAdd(Ω, weightMul(Ω, P, X), weightMul(Ω, P, Y))(ω)88    intros ω point89    have pointReal := ProbabilitySpace.point_real with space, point90    have xReal := FunctionBetween.apply_closed with variableX, point91    have yReal := FunctionBetween.apply_closed with variableY, point92    have left := weightMul.value at Ω, P, weightAdd(Ω, X, Y), ω with function,93        sum, point94    have inner := weightAdd.value at Ω, X, Y, ω with variableX, variableY, point95    have right := weightAdd.value at Ω, weightMul(Ω, P, X), weightMul(Ω, P, Y),96        ω with97      productX, productY, point98    have mulX := weightMul.value at Ω, P, X, ω with function, variableX, point99    have mulY := weightMul.value at Ω, P, Y, ω with function, variableY, point100    rw [left, inner, right, mulX, mulY]101    ring102  have same := realSetSum.congr with productSum, combined, whole, agree103  have split := realSetSum.add with finite, productX, productY, whole104  rw [expectation.value, expectation.value, expectation.value, same, split]105  rfl106107theorem expectation.scale (Ω P X : Set) (c : Real)108  requires space : ProbabilitySpace(Ω, P)109  requires random : X : Ω → ℝ110  shows expectation(Ω, P, weightScale(Ω, c, X)) = c * (expectation(Ω, P, X):R)111proof112  have finite := ProbabilitySpace.finite with space113  have function := ProbabilitySpace.function with space114  have whole := Subset.reflexive at Ω115  have scaled := weightScale.function at Ω, c, X with random116  have product := weightMul.function with function, random117  have productScaled := weightMul.function with function, scaled118  have combined := weightScale.function at Ω, c, weightMul(Ω, P, X) with product119  have agree : ∀ ω ∈ Ω, weightMul(Ω, P, weightScale(Ω, c, X))(ω) =120      weightScale(Ω, c, weightMul(Ω, P, X))(ω)121    intros ω point122    have pointReal := ProbabilitySpace.point_real with space, point123    have xReal := FunctionBetween.apply_closed with random, point124    have left := weightMul.value at Ω, P, weightScale(Ω, c, X), ω with125        function, scaled, point126    have inner := weightScale.value at Ω, c, X, ω with random, point127    have right := weightScale.value at Ω, c, weightMul(Ω, P, X), ω with128        product, point129    have mul := weightMul.value at Ω, P, X, ω with function, random, point130    rw [left, inner, right, mul]131    ring132  have same := realSetSum.congr with productScaled, combined, whole, agree133  have pulled := realSetSum.scale at Ω, Ω, weightMul(Ω, P, X), c with finite,134      product, whole135  rw [expectation.value, expectation.value, same, pulled]136  rfl137138theorem expectation.constant (Ω P : Set) (c : Real)139  requires space : ProbabilitySpace(Ω, P)140  shows expectation(Ω, P, constantFunction(Ω, ℝ, c)) = c141proof142  have finite := ProbabilitySpace.finite with space143  have function := ProbabilitySpace.function with space144  have total := ProbabilitySpace.total with space145  have whole := Subset.reflexive at Ω146  have scalar : c ∈ ℝ by simp [Real]147  have constant := constantFunction.function at Ω, ℝ, c with scalar148  have product := weightMul.function with function, constant149  have scaled := weightScale.function at Ω, c, P with function150  have agree : ∀ ω ∈ Ω, weightMul(Ω, P, constantFunction(Ω, ℝ, c))(ω) =151      weightScale(Ω, c, P)(ω)152    intros ω point153    have pointReal := ProbabilitySpace.point_real with space, point154    have left := weightMul.value at Ω, P, constantFunction(Ω, ℝ, c), ω with155      function, constant, point156    have value := constantFunction.apply at Ω, ℝ, ω, c with point, scalar157    have right := weightScale.value at Ω, c, P, ω with function, point158    rw [left, value, right]159    ring160  have same := realSetSum.congr with product, scaled, whole, agree161  have pulled := realSetSum.scale at Ω, Ω, P, c with finite, function, whole162  rw [expectation.value, same, pulled, total]163  ring164165-- The expectation of an indicator is the probability of its event.166theorem expectation.indicator (Ω P A : Set)167  requires space : ProbabilitySpace(Ω, P)168  requires event : A ⊆ Ω169  shows expectation(Ω, P, realIndicator(Ω, A)) = prob(P, A)170proof171  have finite := ProbabilitySpace.finite with space172  have function := ProbabilitySpace.function with space173  have whole := Subset.reflexive at Ω174  have indicator := realIndicator.function at Ω, A175  have product := weightMul.function with function, indicator176  have masked := maskedWeight.function at Ω, A, P with function177  have agree : ∀ ω ∈ Ω, weightMul(Ω, P, realIndicator(Ω,178      A))(ω) = maskedWeight(Ω, A, P)(ω)179    intros ω point180    have pointReal := ProbabilitySpace.point_real with space, point181    have natural := indicator.natural at A, ω182    have maskReal := realNat.real at indicator(A, ω)183    have left := weightMul.value at Ω, P, realIndicator(Ω, A), ω with function,184        indicator, point185    have inner := realIndicator.value at Ω, A, ω with point186    have right := maskedWeight.value at Ω, A, P, ω with function, point187    rw [left, inner, right]188    ring189  have same := realSetSum.congr with product, masked, whole, agree190  have counted := realSetSum.masked_intersection at Ω, A, Ω, P with finite,191      function, whole192  have meet := intersection.eq_right_of_subset at Ω, A with event193  rw [expectation.value, prob.value, same, counted, meet]194  rfl195196theorem expectation.monotone (Ω P X Y : Set)197  requires space : ProbabilitySpace(Ω, P)198  requires variableX : X : Ω → ℝ199  requires variableY : Y : Ω → ℝ200  requires bounds : ∀ ω ∈ Ω, (X(ω):R) ≤ (Y(ω):R)201  shows (expectation(Ω, P, X):R) ≤ (expectation(Ω, P, Y):R)202proof203  have finite := ProbabilitySpace.finite with space204  have function := ProbabilitySpace.function with space205  have whole := Subset.reflexive at Ω206  have productX := weightMul.function with function, variableX207  have productY := weightMul.function with function, variableY208  have pointwise : ∀ ω ∈ Ω, (weightMul(Ω, P, X)(ω):R) ≤ (weightMul(Ω, P,209      Y)(ω):R)210    intros ω point211    have pointReal := ProbabilitySpace.point_real with space, point212    have pointNonnegative := ProbabilitySpace.point_nonnegative with space,213        point214    have xReal := FunctionBetween.apply_closed with variableX, point215    have yReal := FunctionBetween.apply_closed with variableY, point216    have left := weightMul.value at Ω, P, X, ω with function, variableX, point217    have right := weightMul.value at Ω, P, Y, ω with function, variableY, point218    have bound := bounds with ω, point219    have scaled := realLe.mul_left_of_nonnegative at X(ω), Y(ω), P(ω) with220      bound, pointNonnegative221    rw [left, right]222    exact scaled223  rw [expectation.value, expectation.value]224  exact realSetSum.monotone with finite, productX, productY, whole, pointwise225226theorem expectation.nonnegative (Ω P X : Set)227  requires space : ProbabilitySpace(Ω, P)228  requires random : X : Ω → ℝ229  requires nonnegative : ∀ ω ∈ Ω, (0:R) ≤ (X(ω):R)230  shows (0:R) ≤ (expectation(Ω, P, X):R)231proof232  have finite := ProbabilitySpace.finite with space233  have function := ProbabilitySpace.function with space234  have whole := Subset.reflexive at Ω235  have product := weightMul.function with function, random236  have pointwise : ∀ ω ∈ Ω, (0:R) ≤ (weightMul(Ω, P, X)(ω):R)237    intros ω point238    have pointReal := ProbabilitySpace.point_real with space, point239    have pointNonnegative := ProbabilitySpace.point_nonnegative with space,240        point241    have xReal := FunctionBetween.apply_closed with random, point242    have value := weightMul.value at Ω, P, X, ω with function, random, point243    have bound := nonnegative with ω, point244    have scaled := realMulValue.nonnegative at P(ω), X(ω) with245        pointNonnegative, bound246    rw value247    exact scaled248  rw expectation.value249  exact realSetSum.nonnegative with finite, product, whole, pointwise250251theorem expectation.le_of_bounded (Ω P X : Set) (c : Real)252  requires space : ProbabilitySpace(Ω, P)253  requires random : X : Ω → ℝ254  requires bounded : ∀ ω ∈ Ω, (X(ω):R) ≤ c255  shows (expectation(Ω, P, X):R) ≤ c256proof257  have scalar : c ∈ ℝ by simp [Real]258  have constant := constantFunction.function at Ω, ℝ, c with scalar259  have bounds : ∀ ω ∈ Ω, (X(ω):R) ≤ (constantFunction(Ω, ℝ, c)(ω):R)260    intros ω point261    have value := constantFunction.apply at Ω, ℝ, ω, c with point, scalar262    rw value263    exact bounded with ω, point264  have monotone := expectation.monotone with space, random, constant, bounds265  have expected := expectation.constant at Ω, P, c with space266  rwa expected at monotone267268theorem expectation.ge_of_bounded (Ω P X : Set) (c : Real)269  requires space : ProbabilitySpace(Ω, P)270  requires random : X : Ω → ℝ271  requires bounded : ∀ ω ∈ Ω, c ≤ (X(ω):R)272  shows c ≤ (expectation(Ω, P, X):R)273proof274  have scalar : c ∈ ℝ by simp [Real]275  have constant := constantFunction.function at Ω, ℝ, c with scalar276  have bounds : ∀ ω ∈ Ω, (constantFunction(Ω, ℝ, c)(ω):R) ≤ (X(ω):R)277    intros ω point278    have value := constantFunction.apply at Ω, ℝ, ω, c with point, scalar279    rw value280    exact bounded with ω, point281  have monotone := expectation.monotone with space, constant, random, bounds282  have expected := expectation.constant at Ω, P, c with space283  rwa expected at monotone284285theorem expectation.sub (Ω P X Y : Set)286  requires space : ProbabilitySpace(Ω, P)287  requires variableX : X : Ω → ℝ288  requires variableY : Y : Ω → ℝ289  shows expectation(Ω, P, weightSub(Ω, X, Y)) =290    (expectation(Ω, P, X):R) - (expectation(Ω, P, Y):R)291proof292  have difference := weightSub.function with variableX, variableY293  have restored := weightAdd.function with difference, variableY294  have agree : ∀ ω ∈ Ω, weightAdd(Ω, weightSub(Ω, X, Y), Y)(ω) = X(ω)295    intros ω point296    have xReal := FunctionBetween.apply_closed with variableX, point297    have yReal := FunctionBetween.apply_closed with variableY, point298    have outer := weightAdd.value at Ω, weightSub(Ω, X, Y), Y, ω with299        difference, variableY, point300    have inner := weightSub.value at Ω, X, Y, ω with variableX, variableY, point301    rw [outer, inner]302    ring303  have same := expectation.congr with space, restored, variableX, agree304  have split := expectation.add with space, difference, variableY305  have realX := expectation.real with space, variableX306  have realY := expectation.real with space, variableY307  have realDifference := expectation.real with space, difference308  linarith309310-- The pointwise absolute value of a random random.311defgraph absVariable (Ω X : Set) (x ∈ Ω) : ℝ := abs(X(x))312requires random : X : Ω → ℝ313proof314  have value := FunctionBetween.apply_closed with random, member315  exact abs.real at X(x)316317theorem expectation.abs_le (Ω P X : Set)318  requires space : ProbabilitySpace(Ω, P)319  requires random : X : Ω → ℝ320  shows (abs(expectation(Ω, P, X)):R) ≤ (expectation(Ω, P, absVariable(Ω, X)):R)321proof322  have absolute := absVariable.function with random323  have zeroReal := realZero.real324  have zeros := constantFunction.function at Ω, ℝ, (0:R) with zeroReal325  have negated := weightSub.function with zeros, random326  have realX := expectation.real with space, random327  have realAbs := expectation.real with space, absolute328  have upperBounds : ∀ ω ∈ Ω, (X(ω):R) ≤ (absVariable(Ω, X)(ω):R)329    intros ω point330    have xReal := FunctionBetween.apply_closed with random, point331    have value := absVariable.value at Ω, X, ω with random, point332    rw value333    exact abs.upper at X(ω)334  have lowerBounds : ∀ ω ∈ Ω,335      (weightSub(Ω, constantFunction(Ω, ℝ, (0:R)), X)(ω):R) ≤ (absVariable(Ω,336        X)(ω):R)337    intros ω point338    have xReal := FunctionBetween.apply_closed with random, point339    have absReal := abs.real at X(ω)340    have value := absVariable.value at Ω, X, ω with random, point341    have difference := weightSub.value at Ω, constantFunction(Ω, ℝ, (0:R)), X,342        ω with343      zeros, random, point344    have zero := constantFunction.apply at Ω, ℝ, ω, (0:R) with point, zeroReal345    have negative := abs.upper_neg at X(ω)346    rw [value, difference, zero]347    linarith348  have upper := expectation.monotone with space, random, absolute, upperBounds349  have lower := expectation.monotone with space, negated, absolute, lowerBounds350  have split := expectation.sub with space, zeros, random351  have zeroExpected := expectation.constant at Ω, P, (0:R) with space352  rw [split, zeroExpected] at lower353  have alternatives : (0:R) ≤ (expectation(Ω, P, X):R) ∨354      ¬((0:R) ≤ (expectation(Ω, P, X):R)) by tauto355  cases alternatives with nonnegative | negative356  . have same := abs.of_nonnegative at expectation(Ω, P, X) with nonnegative357    rw same358    exact upper359  . have below := realLess.of_not_le at realZero, expectation(Ω, P, X) with360    negative361    have nonpositive := realLess.implies_le with below362    have same := abs.of_nonpositive at expectation(Ω, P, X) with nonpositive363    rw same364    linarith365366-- The event that X is at least a.367def levelSet (Ω X : Set) (a : Real) : Set := { ω ∈ Ω | a ≤ (X(ω):R) }368369theorem levelSet.subset (Ω X : Set) (a : Real)370  shows levelSet(Ω, X, a) ⊆ Ω371proof372  intros ω member373  have data := levelSet.membership.forward with member374  exact data.left375376-- Markov's inequality.377theorem expectation.markov (Ω P X : Set) (a : Real)378  requires space : ProbabilitySpace(Ω, P)379  requires random : X : Ω → ℝ380  requires nonnegative : ∀ ω ∈ Ω, (0:R) ≤ (X(ω):R)381  requires positive : (0:R) < a382  shows (prob(P, levelSet(Ω, X, a)):R) ≤ (expectation(Ω, P, X):R) / a383proof384  have event := levelSet.subset at Ω, X, a385  have indicator := realIndicator.function at Ω, levelSet(Ω, X, a)386  have scaled := weightScale.function at Ω, a, realIndicator(Ω, levelSet(Ω, X,387      a)) with388    indicator389  have pointwise : ∀ ω ∈ Ω,390      (weightScale(Ω, a, realIndicator(Ω, levelSet(Ω, X, a)))(ω):R) ≤ (X(ω):R)391    intros ω point392    have xReal := FunctionBetween.apply_closed with random, point393    have value := weightScale.value at Ω, a, realIndicator(Ω, levelSet(Ω, X,394        a)), ω with395      indicator, point396    have alternatives : ω ∈ levelSet(Ω, X, a) ∨ ¬(ω ∈ levelSet(Ω, X,397        a)) by tauto398    cases alternatives with inside | outside399    . have one := realIndicator.inside at Ω, levelSet(Ω, X, a), ω with point,400      inside401      have data := levelSet.membership.forward with inside402      have oneMul := realMulValue.one_right at a403      rw [value, one, oneMul]404      exact data.right405    . have zero := realIndicator.outside at Ω, levelSet(Ω, X, a), ω with point,406      outside407      have zeroMul := realMulValue.zero_right at a408      rw [value, zero, zeroMul]409      exact nonnegative with ω, point410  have monotone := expectation.monotone with space, scaled, random, pointwise411  have scale := expectation.scale at Ω, P, realIndicator(Ω, levelSet(Ω, X, a)),412      a with413    space, indicator414  have indicatorValue := expectation.indicator with space, event415  rw [scale, indicatorValue] at monotone416  have realLevel := prob.real with space, event417  have realExpected := expectation.real with space, random418  have inverseReal := realInvValue.real at a419  have inversePositive := realInvValue.positive at a with positive420  have inverseNonnegative : (0:R) ≤ (realInvValue(a):R) by linarith421  have nonzero : a ≠ (0:R)422    intro zero423    rw zero at positive424    exact realLess.not_self with positive425  have inverseLaw := realInvValue.mul_right at a with nonzero426  have scaledBound := realLe.mul_right_of_nonnegative at427    a * (prob(P, levelSet(Ω, X, a)):R), expectation(Ω, P, X),428      realInvValue(a) with429    monotone, inverseNonnegative430  have division := realDiv.eq_mul_inv at expectation(Ω, P, X), a431  have simplify : (a * (prob(P, levelSet(Ω, X, a)):R)) * (realInvValue(a):R) =432      prob(P, levelSet(Ω, X, a))433    calc434      (a * (prob(P, levelSet(Ω, X, a)):R)) * (realInvValue(a):R) =435          (prob(P, levelSet(Ω, X, a)):R) * (a * (realInvValue(a):R)) := by ring436      _ = (prob(P, levelSet(Ω, X, a)):R) * (1:R) := by cc437      _ = prob(P, levelSet(Ω, X, a)) := realMulValue.one_right at prob(P,438        levelSet(Ω, X, a))439  rw simplify at scaledBound440  rw division441  exact scaledBound442443theorem expectation.indicator_complement (Ω P A : Set)444  requires space : ProbabilitySpace(Ω, P)445  requires event : A ⊆ Ω446  shows expectation(Ω, P, realIndicator(Ω, Ω ∖ A)) = (1:R) - (prob(P, A):R)447proof448  have eventRest : Ω ∖ A ⊆ Ω by simp449  have indicator := expectation.indicator with space, eventRest450  have complement := prob.complement with space, event451  rw [indicator, complement]452  rfl453