Grace/Cumulus/Probability/Variance.g17

Open in Workbench Download source

Imports

RandomVariable

Declarations

Source

1-- Variance and Chebyshev's inequality2-- 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.Variance8import RandomVariable910-- The pointwise square of a random random.11defgraph squareVariable (Ω X : Set) (x ∈ Ω) : ℝ := call2(realMul, X(x), X(x))12requires random : X : Ω → ℝ13proof14  have value := FunctionBetween.apply_closed with random, member15  exact realMulValue.real at X(x), X(x)1617-- A random random shifted by the constant m.18defgraph centeredVariable (Ω X : Set) (m : Real) (x ∈ Ω) : ℝ :=19    realSubValue(X(x), m)20requires random : X : Ω → ℝ21proof22  have value := FunctionBetween.apply_closed with random, member23  exact realSubValue.real at X(x), m2425def variance (Ω P X : Set) : Set :=26  expectation(Ω, P, squareVariable(Ω, centeredVariable(Ω, X, expectation(Ω, P,27    X))))2829theorem variance.value (Ω P X : Set)30  shows variance(Ω, P, X) =31    expectation(Ω, P, squareVariable(Ω, centeredVariable(Ω, X, expectation(Ω,32      P, X))))33proof34  simp [variance]3536theorem squareVariable.nonnegative (Ω X ω : Set)37  requires random : X : Ω → ℝ38  requires point : ω ∈ Ω39  shows (0:R) ≤ (squareVariable(Ω, X)(ω):R)40proof41  have xReal := FunctionBetween.apply_closed with random, point42  have value := squareVariable.value at Ω, X, ω with random, point43  rw value44  exact realMulValue.square_nonnegative at X(ω)4546theorem expectation.square_nonnegative (Ω P X : Set)47  requires space : ProbabilitySpace(Ω, P)48  requires random : X : Ω → ℝ49  shows (0:R) ≤ (expectation(Ω, P, squareVariable(Ω, X)):R)50proof51  have square := squareVariable.function with random52  have bounds : ∀ ω ∈ Ω, (0:R) ≤ (squareVariable(Ω, X)(ω):R)53    intros ω point54    exact squareVariable.nonnegative with random, point55  exact expectation.nonnegative with space, square, bounds5657theorem variance.real (Ω P X : Set)58  requires space : ProbabilitySpace(Ω, P)59  requires random : X : Ω → ℝ60  shows Real(variance(Ω, P, X))61proof62  have mean := expectation.real with space, random63  have centered := centeredVariable.function at Ω, X, expectation(Ω, P, X) with64      random65  have square := squareVariable.function with centered66  rw variance.value67  exact expectation.real with space, square6869theorem variance.nonnegative (Ω P X : Set)70  requires space : ProbabilitySpace(Ω, P)71  requires random : X : Ω → ℝ72  shows (0:R) ≤ (variance(Ω, P, X):R)73proof74  have mean := expectation.real with space, random75  have centered := centeredVariable.function at Ω, X, expectation(Ω, P, X) with76      random77  rw variance.value78  exact expectation.square_nonnegative with space, centered7980-- The computational formula: Var X = E[X²] - (E X)².81theorem variance.formula (Ω P X : Set)82  requires space : ProbabilitySpace(Ω, P)83  requires random : X : Ω → ℝ84  shows variance(Ω, P, X) = (expectation(Ω, P, squareVariable(Ω, X)):R) -85    (expectation(Ω, P, X):R) * (expectation(Ω, P, X):R)86proof87  have mean := expectation.real with space, random88  have twoReal := realNumeral.real at 289  have twiceMean := realMulValue.real at (2:R), expectation(Ω, P, X)90  have squaredMean := realMulValue.real at expectation(Ω, P, X), expectation(Ω,91      P, X)92  have centered := centeredVariable.function at Ω, X, expectation(Ω, P, X) with93      random94  have centeredSquare := squareVariable.function with centered95  have square := squareVariable.function with random96  have scaled := weightScale.function at Ω, (2:R) * (expectation(Ω, P, X):R),97      X with random98  have left := weightAdd.function with centeredSquare, scaled99  have constant := constantFunction.function at Ω, ℝ,100    (expectation(Ω, P, X):R) * (expectation(Ω, P, X):R) with squaredMean101  have right := weightAdd.function with square, constant102  have agree : ∀ ω ∈ Ω, weightAdd(Ω, squareVariable(Ω, centeredVariable(Ω, X,103      expectation(Ω, P, X))),104      weightScale(Ω, (2:R) * (expectation(Ω, P, X):R), X))(ω) =105    weightAdd(Ω, squareVariable(Ω, X), constantFunction(Ω, ℝ,106      (expectation(Ω, P, X):R) * (expectation(Ω, P, X):R)))(ω)107    intros ω point108    have xReal := FunctionBetween.apply_closed with random, point109    have leftValue := weightAdd.value at Ω,110      squareVariable(Ω, centeredVariable(Ω, X, expectation(Ω, P, X))),111      weightScale(Ω, (2:R) * (expectation(Ω, P, X):R), X), ω with112        centeredSquare, scaled, point113    have centeredSquareValue := squareVariable.value at Ω,114      centeredVariable(Ω, X, expectation(Ω, P, X)), ω with centered, point115    have centeredValue := centeredVariable.value at Ω, X, expectation(Ω, P, X),116        ω with117      random, point118    have scaledValue := weightScale.value at Ω, (2:R) * (expectation(Ω, P,119        X):R), X, ω with120      random, point121    have rightValue := weightAdd.value at Ω, squareVariable(Ω, X),122        constantFunction(Ω, ℝ,123      (expectation(Ω, P, X):R) * (expectation(Ω, P, X):R)), ω with square,124        constant, point125    have squareValue := squareVariable.value at Ω, X, ω with random, point126    have constantValue := constantFunction.apply at Ω, ℝ, ω,127      (expectation(Ω, P, X):R) * (expectation(Ω, P, X):R) with point,128        squaredMean129    rw [leftValue, centeredSquareValue, centeredValue, scaledValue, rightValue,130      squareValue,131      constantValue]132    ring133  have same := expectation.congr with space, left, right, agree134  have leftSplit := expectation.add with space, centeredSquare, scaled135  have scale := expectation.scale at Ω, P, X, (2:R) * (expectation(Ω, P,136      X):R) with137    space, random138  have rightSplit := expectation.add with space, square, constant139  have constantValue := expectation.constant at Ω, P,140    (expectation(Ω, P, X):R) * (expectation(Ω, P, X):R) with space141  rw [leftSplit, scale, rightSplit, constantValue] at same142  have varianceReal := variance.real with space, random143  have squareReal := expectation.real with space, square144  rw variance.value at varianceReal145  rw variance.value146  calc147    expectation(Ω, P, squareVariable(Ω, centeredVariable(Ω, X, expectation(Ω,148      P, X)))) =149        ((expectation(Ω, P, squareVariable(Ω, centeredVariable(Ω, X,150          expectation(Ω, P, X)))):R) +151          ((2:R) * (expectation(Ω, P, X):R)) * (expectation(Ω, P, X):R)) -152          ((2:R) * (expectation(Ω, P, X):R)) * (expectation(Ω, P,153            X):R) := by ring154    _ = ((expectation(Ω, P, squareVariable(Ω, X)):R) +155          (expectation(Ω, P, X):R) * (expectation(Ω, P, X):R)) -156          ((2:R) * (expectation(Ω, P, X):R)) * (expectation(Ω, P, X):R) := by cc157    _ = (expectation(Ω, P, squareVariable(Ω, X)):R) -158          (expectation(Ω, P, X):R) * (expectation(Ω, P, X):R) := by ring159160theorem variance.le_square_expectation (Ω P X : Set)161  requires space : ProbabilitySpace(Ω, P)162  requires random : X : Ω → ℝ163  shows (variance(Ω, P, X):R) ≤ (expectation(Ω, P, squareVariable(Ω, X)):R)164proof165  have mean := expectation.real with space, random166  have square := squareVariable.function with random167  have squareReal := expectation.real with space, square168  have varianceReal := variance.real with space, random169  have formula := variance.formula with space, random170  have nonnegative := realMulValue.square_nonnegative at expectation(Ω, P, X)171  rw formula172  linarith173174-- Scaling a random by c scales its variance by c².175theorem variance.scale (Ω P X : Set) (c : Real)176  requires space : ProbabilitySpace(Ω, P)177  requires random : X : Ω → ℝ178  shows variance(Ω, P, weightScale(Ω, c, X)) = (c * c) * (variance(Ω, P, X):R)179proof180  have mean := expectation.real with space, random181  have cSquare := realMulValue.real at c, c182  have scaled := weightScale.function at Ω, c, X with random183  have scaledMean := expectation.scale at Ω, P, X, c with space, random184  have centered := centeredVariable.function at Ω, X, expectation(Ω, P, X) with185      random186  have centeredScaled := centeredVariable.function at Ω, weightScale(Ω, c, X),187    expectation(Ω, P, weightScale(Ω, c, X)) with scaled188  have scaledCentered := weightScale.function at Ω, c,189    centeredVariable(Ω, X, expectation(Ω, P, X)) with centered190  have squareCentered := squareVariable.function with centered191  have squareScaledCentered := squareVariable.function with scaledCentered192  have squareCenteredScaled := squareVariable.function with centeredScaled193  have scaledSquare := weightScale.function at Ω, c * c,194    squareVariable(Ω, centeredVariable(Ω, X, expectation(Ω, P, X))) with195      squareCentered196  have agree : ∀ ω ∈ Ω, squareVariable(Ω, centeredVariable(Ω, weightScale(Ω, c,197      X),198      expectation(Ω, P, weightScale(Ω, c, X))))(ω) =199    weightScale(Ω, c * c, squareVariable(Ω, centeredVariable(Ω, X,200      expectation(Ω, P, X))))(ω)201    intros ω point202    have xReal := FunctionBetween.apply_closed with random, point203    have outer := squareVariable.value at Ω, centeredVariable(Ω, weightScale(Ω,204        c, X),205      expectation(Ω, P, weightScale(Ω, c, X))), ω with centeredScaled, point206    have inner := centeredVariable.value at Ω, weightScale(Ω, c, X),207      expectation(Ω, P, weightScale(Ω, c, X)), ω with scaled, point208    have scaledValue := weightScale.value at Ω, c, X, ω with random, point209    have rightOuter := weightScale.value at Ω, c * c,210      squareVariable(Ω, centeredVariable(Ω, X, expectation(Ω, P, X))), ω with211      squareCentered, point212    have rightSquare := squareVariable.value at Ω,213      centeredVariable(Ω, X, expectation(Ω, P, X)), ω with centered, point214    have rightCentered := centeredVariable.value at Ω, X, expectation(Ω, P, X),215        ω with216      random, point217    rw [outer, inner, scaledValue, scaledMean, rightOuter, rightSquare,218      rightCentered]219    ring220  have same := expectation.congr with space, squareCenteredScaled,221      scaledSquare, agree222  have pulled := expectation.scale at Ω, P,223    squareVariable(Ω, centeredVariable(Ω, X, expectation(Ω, P, X))), c * c with224    space, squareCentered225  rw [variance.value, variance.value, same, pulled]226  rfl227228-- Shifting a random by a constant leaves its variance unchanged.229theorem variance.shift (Ω P X : Set) (c : Real)230  requires space : ProbabilitySpace(Ω, P)231  requires random : X : Ω → ℝ232  shows variance(Ω, P, weightAdd(Ω, X, constantFunction(Ω, ℝ,233      c))) = variance(Ω, P, X)234proof235  have mean := expectation.real with space, random236  have scalar : c ∈ ℝ by simp [Real]237  have constant := constantFunction.function at Ω, ℝ, c with scalar238  have shifted := weightAdd.function with random, constant239  have shiftedMean := expectation.add with space, random, constant240  have constantMean := expectation.constant at Ω, P, c with space241  rw constantMean at shiftedMean242  have centered := centeredVariable.function at Ω, X, expectation(Ω, P, X) with243      random244  have centeredShifted := centeredVariable.function at Ω,245    weightAdd(Ω, X, constantFunction(Ω, ℝ, c)),246    expectation(Ω, P, weightAdd(Ω, X, constantFunction(Ω, ℝ, c))) with shifted247  have squareCentered := squareVariable.function with centered248  have squareShifted := squareVariable.function with centeredShifted249  have agree : ∀ ω ∈ Ω, squareVariable(Ω, centeredVariable(Ω,250      weightAdd(Ω, X, constantFunction(Ω, ℝ, c)),251      expectation(Ω, P, weightAdd(Ω, X, constantFunction(Ω, ℝ, c)))))(ω) =252    squareVariable(Ω, centeredVariable(Ω, X, expectation(Ω, P, X)))(ω)253    intros ω point254    have xReal := FunctionBetween.apply_closed with random, point255    have outer := squareVariable.value at Ω, centeredVariable(Ω,256      weightAdd(Ω, X, constantFunction(Ω, ℝ, c)),257      expectation(Ω, P, weightAdd(Ω, X, constantFunction(Ω, ℝ, c)))), ω with258      centeredShifted, point259    have inner := centeredVariable.value at Ω, weightAdd(Ω, X,260        constantFunction(Ω, ℝ, c)),261      expectation(Ω, P, weightAdd(Ω, X, constantFunction(Ω, ℝ, c))), ω with262        shifted, point263    have sum := weightAdd.value at Ω, X, constantFunction(Ω, ℝ, c), ω with264      random, constant, point265    have constantValue := constantFunction.apply at Ω, ℝ, ω, c with point,266        scalar267    have rightSquare := squareVariable.value at Ω,268      centeredVariable(Ω, X, expectation(Ω, P, X)), ω with centered, point269    have rightCentered := centeredVariable.value at Ω, X, expectation(Ω, P, X),270        ω with271      random, point272    rw [outer, inner, sum, constantValue, shiftedMean, rightSquare,273      rightCentered]274    ring275  rw [variance.value, variance.value]276  exact expectation.congr with space, squareShifted, squareCentered, agree277278theorem variance.constant (Ω P : Set) (c : Real)279  requires space : ProbabilitySpace(Ω, P)280  shows variance(Ω, P, constantFunction(Ω, ℝ, c)) = (0:R)281proof282  have scalar : c ∈ ℝ by simp [Real]283  have zeroReal := realZero.real284  have constant := constantFunction.function at Ω, ℝ, c with scalar285  have zeros := constantFunction.function at Ω, ℝ, (0:R) with zeroReal286  have constantMean := expectation.constant at Ω, P, c with space287  have centered := centeredVariable.function at Ω, constantFunction(Ω, ℝ, c),288    expectation(Ω, P, constantFunction(Ω, ℝ, c)) with constant289  have square := squareVariable.function with centered290  have agree : ∀ ω ∈ Ω, squareVariable(Ω, centeredVariable(Ω,291      constantFunction(Ω, ℝ, c),292      expectation(Ω, P, constantFunction(Ω, ℝ, c))))(ω) = constantFunction(Ω,293        ℝ, (0:R))(ω)294    intros ω point295    have outer := squareVariable.value at Ω, centeredVariable(Ω,296        constantFunction(Ω, ℝ, c),297      expectation(Ω, P, constantFunction(Ω, ℝ, c))), ω with centered, point298    have inner := centeredVariable.value at Ω, constantFunction(Ω, ℝ, c),299      expectation(Ω, P, constantFunction(Ω, ℝ, c)), ω with constant, point300    have constantValue := constantFunction.apply at Ω, ℝ, ω, c with point,301        scalar302    have zeroValue := constantFunction.apply at Ω, ℝ, ω, (0:R) with point,303        zeroReal304    rw [outer, inner, constantValue, constantMean, zeroValue]305    ring306  have same := expectation.congr with space, square, zeros, agree307  have zeroMean := expectation.constant at Ω, P, (0:R) with space308  rw [variance.value, same, zeroMean]309  rfl310311-- Chebyshev's inequality in its squared form: the probability that the312-- squared deviation reaches a² is at most Var X / a².313theorem variance.chebyshev_square (Ω P X : Set) (a : Real)314  requires space : ProbabilitySpace(Ω, P)315  requires random : X : Ω → ℝ316  requires positive : (0:R) < a317  shows (prob(P, levelSet(Ω, squareVariable(Ω, centeredVariable(Ω, X,318      expectation(Ω, P, X))),319      a * a)):R) ≤ (variance(Ω, P, X):R) / (a * a)320proof321  have mean := expectation.real with space, random322  have centered := centeredVariable.function at Ω, X, expectation(Ω, P, X) with323      random324  have square := squareVariable.function with centered325  have nonnegative : ∀ ω ∈ Ω,326      (0:R) ≤ (squareVariable(Ω, centeredVariable(Ω, X, expectation(Ω, P,327        X)))(ω):R)328    intros ω point329    exact squareVariable.nonnegative with centered, point330  have squarePositive := realMulValue.positive at a, a with positive, positive331  have markov := expectation.markov at Ω, P,332    squareVariable(Ω, centeredVariable(Ω, X, expectation(Ω, P, X))), a * a with333    space, square, nonnegative, squarePositive334  rw variance.value335  exact markov336337theorem abs.square_le (A B : Real)338  requires nonnegative : (0:R) ≤ A339  requires bound : A ≤ abs(B)340  shows A * A ≤ B * B341proof342  have absReal := abs.real at B343  have absNonnegative := abs.nonnegative at B344  have first := realLe.mul_right_of_nonnegative at A, abs(B), A with bound,345      nonnegative346  have second := realLe.mul_left_of_nonnegative at A, abs(B), abs(B) with347      bound, absNonnegative348  have squareNonnegative := realMulValue.square_nonnegative at B349  have product := abs.mul at B, B350  have same := abs.of_nonnegative at B * B with squareNonnegative351  have chain := realLe.transitive with first, second352  rw ← product at chain353  rwa same at chain354355-- Chebyshev's inequality: the probability that X deviates from its mean by356-- at least a is at most Var X / a².357theorem variance.chebyshev (Ω P X : Set) (a : Real)358  requires space : ProbabilitySpace(Ω, P)359  requires random : X : Ω → ℝ360  requires positive : (0:R) < a361  shows (prob(P, levelSet(Ω, absVariable(Ω, centeredVariable(Ω, X,362      expectation(Ω, P, X))),363      a)):R) ≤ (variance(Ω, P, X):R) / (a * a)364proof365  have mean := expectation.real with space, random366  have centered := centeredVariable.function at Ω, X, expectation(Ω, P, X) with367      random368  have square := squareVariable.function with centered369  have absolute := absVariable.function with centered370  have nonnegative : (0:R) ≤ a by linarith371  have inner : levelSet(Ω, absVariable(Ω, centeredVariable(Ω, X, expectation(Ω,372      P, X))),373      a) ⊆ levelSet(Ω, squareVariable(Ω, centeredVariable(Ω, X, expectation(Ω,374        P, X))),375      a * a)376    intros ω member377    have data := levelSet.membership.forward with member378    have point := data.left379    have deviationReal := FunctionBetween.apply_closed with centered, point380    have absValue := absVariable.value at Ω,381      centeredVariable(Ω, X, expectation(Ω, P, X)), ω with centered, point382    have squareValue := squareVariable.value at Ω,383      centeredVariable(Ω, X, expectation(Ω, P, X)), ω with centered, point384    have bound := data.right385    rw absValue at bound386    have squared := abs.square_le at a, centeredVariable(Ω, X, expectation(Ω,387        P, X))(ω) with388      nonnegative, bound389    apply levelSet.membership.backward390    refine ⟨point, ?_⟩391    rw squareValue392    exact squared393  have eventSquare := levelSet.subset at Ω,394    squareVariable(Ω, centeredVariable(Ω, X, expectation(Ω, P, X))), a * a395  have monotone := prob.monotone with space, eventSquare, inner396  have chebyshev := variance.chebyshev_square with space, random, positive397  have eventAbs := levelSet.subset at Ω,398    absVariable(Ω, centeredVariable(Ω, X, expectation(Ω, P, X))), a399  have realAbs := prob.real with space, eventAbs400  have realSquare := prob.real with space, eventSquare401  have varianceReal := variance.real with space, random402  have squareReal := realMulValue.real at a, a403  have quotientReal := realDiv.real at variance(Ω, P, X), a * a404  exact realLe.transitive with monotone, chebyshev405