Grace/Cumulus/Probability/Bernoulli.g17

Open in Workbench Download source

Imports

Variance · Uniform

Declarations

Source

1-- Bernoulli trials, a fair coin, and a fair die2-- 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.Bernoulli8import Variance9import Uniform1011-- The two-point sample space of a single trial.12def twoPoint : Set := {(0:N), (1:N)}1314theorem twoPoint.membership (x : Set)15  shows x ∈ twoPoint ↔ (x = (0:N) ∨ x = (1:N))16proof17  simp [twoPoint, pair.membership]1819theorem twoPoint.zero20  shows (0:N) ∈ twoPoint21proof22  simp [twoPoint.membership]2324theorem twoPoint.one25  shows (1:N) ∈ twoPoint26proof27  simp [twoPoint.membership]2829theorem twoPoint.as_insert30  shows twoPoint = insert((0:N), {(1:N)})31proof32  ext y33  simp [twoPoint.membership]3435theorem twoPoint.finite36  shows Finite(twoPoint)37proof38  have single := Finite.singleton at (1:N)39  have inserted := Finite.insert at {(1:N)}, (0:N) with single40  rw twoPoint.as_insert41  exact inserted4243theorem twoPoint.nonempty44  shows Nonempty(twoPoint)45proof46  have member := twoPoint.zero47  exact ⟨(0:N), member⟩4849theorem twoPoint.cardinality50  shows cardinality(twoPoint) = 251proof52  unfold twoPoint53  decide5455theorem twoPoint.zero_fresh56  shows ¬((0:N) ∈ {(1:N)})57proof58  decide5960theorem twoPoint.one_fresh61  shows ¬((1:N) ∈ {(0:N)})62proof63  decide6465-- The Bernoulli weight with success probability p: mass p at 1 and 1 - p66-- at 0.67def bernoulliWeight (p : Real) : Set :=68  weightAdd(twoPoint, weightScale(twoPoint, p, realIndicator(twoPoint,69    {(1:N)})),70    weightScale(twoPoint, (1:R) - p, realIndicator(twoPoint, {(0:N)})))7172theorem bernoulliWeight.function (p : Real)73  shows bernoulliWeight(p) : twoPoint → ℝ74proof75  have failure := realSubValue.real at (1:R), p76  have successes := realIndicator.function at twoPoint, {(1:N)}77  have failures := realIndicator.function at twoPoint, {(0:N)}78  have scaledSuccess := weightScale.function at twoPoint, p,79    realIndicator(twoPoint, {(1:N)}) with successes80  have scaledFailure := weightScale.function at twoPoint, (1:R) - p,81    realIndicator(twoPoint, {(0:N)}) with failures82  unfold bernoulliWeight83  exact weightAdd.function with scaledSuccess, scaledFailure8485theorem bernoulliWeight.at_one (p : Real)86  shows bernoulliWeight(p)((1:N)) = p87proof88  have failure := realSubValue.real at (1:R), p89  have successes := realIndicator.function at twoPoint, {(1:N)}90  have failures := realIndicator.function at twoPoint, {(0:N)}91  have scaledSuccess := weightScale.function at twoPoint, p,92    realIndicator(twoPoint, {(1:N)}) with successes93  have scaledFailure := weightScale.function at twoPoint, (1:R) - p,94    realIndicator(twoPoint, {(0:N)}) with failures95  have point := twoPoint.one96  have sum := weightAdd.value at twoPoint, weightScale(twoPoint, p,97      realIndicator(twoPoint, {(1:N)})),98    weightScale(twoPoint, (1:R) - p, realIndicator(twoPoint, {(0:N)})),99      (1:N) with100    scaledSuccess, scaledFailure, point101  have first := weightScale.value at twoPoint, p, realIndicator(twoPoint,102      {(1:N)}), (1:N) with103    successes, point104  have second := weightScale.value at twoPoint, (1:R) - p,105      realIndicator(twoPoint, {(0:N)}),106    (1:N) with failures, point107  have self := singleton.self at (1:N)108  have fresh := twoPoint.one_fresh109  have inside := realIndicator.inside at twoPoint, {(1:N)}, (1:N) with point,110      self111  have outside := realIndicator.outside at twoPoint, {(0:N)}, (1:N) with point,112      fresh113  simp [bernoulliWeight]114  ring115116theorem bernoulliWeight.at_zero (p : Real)117  shows bernoulliWeight(p)((0:N)) = (1:R) - p118proof119  have failure := realSubValue.real at (1:R), p120  have successes := realIndicator.function at twoPoint, {(1:N)}121  have failures := realIndicator.function at twoPoint, {(0:N)}122  have scaledSuccess := weightScale.function at twoPoint, p,123    realIndicator(twoPoint, {(1:N)}) with successes124  have scaledFailure := weightScale.function at twoPoint, (1:R) - p,125    realIndicator(twoPoint, {(0:N)}) with failures126  have point := twoPoint.zero127  have sum := weightAdd.value at twoPoint, weightScale(twoPoint, p,128      realIndicator(twoPoint, {(1:N)})),129    weightScale(twoPoint, (1:R) - p, realIndicator(twoPoint, {(0:N)})),130      (0:N) with131    scaledSuccess, scaledFailure, point132  have first := weightScale.value at twoPoint, p, realIndicator(twoPoint,133      {(1:N)}), (0:N) with134    successes, point135  have second := weightScale.value at twoPoint, (1:R) - p,136      realIndicator(twoPoint, {(0:N)}),137    (0:N) with failures, point138  have self := singleton.self at (0:N)139  have fresh := twoPoint.zero_fresh140  have outside := realIndicator.outside at twoPoint, {(1:N)}, (0:N) with point,141      fresh142  have inside := realIndicator.inside at twoPoint, {(0:N)}, (0:N) with point,143      self144  simp [bernoulliWeight]145  ring146147theorem bernoulliWeight.nonnegative (p : Real)148  requires lower : (0:R) ≤ p149  requires upper : p ≤ (1:R)150  shows ∀ ω ∈ twoPoint, (0:R) ≤ (bernoulliWeight(p)(ω):R)151proof152  intros ω point153  have alternatives := twoPoint.membership.forward with point154  cases alternatives with zero | one155  . have value := bernoulliWeight.at_zero at p156    rw [zero, value]157    linarith158  . have value := bernoulliWeight.at_one at p159    rw [one, value]160    exact lower161162theorem bernoulliWeight.total (p : Real)163  shows realSetSum(twoPoint, bernoulliWeight(p)) = (1:R)164proof165  have function := bernoulliWeight.function at p166  have single := Finite.singleton at (1:N)167  have subset : {(1:N)} ⊆ twoPoint168    intros y member169    have equal := singleton.membership.forward with member170    rw equal171    exact twoPoint.one172  have zeroIn := twoPoint.zero173  have oneIn := twoPoint.one174  have fresh := twoPoint.zero_fresh175  have inserted := realSetSum.insert with single, function, subset, zeroIn,176      fresh177  have singleton := realSetSum.singleton with function, oneIn178  have atZero := bernoulliWeight.at_zero at p179  have atOne := bernoulliWeight.at_one at p180  rw twoPoint.as_insert181  rw [inserted, singleton, atZero, atOne]182  ring183184theorem bernoulliWeight.space (p : Real)185  requires lower : (0:R) ≤ p186  requires upper : p ≤ (1:R)187  shows ProbabilitySpace(twoPoint, bernoulliWeight(p))188proof189  have finite := twoPoint.finite190  have function := bernoulliWeight.function at p191  have nonnegative := bernoulliWeight.nonnegative with lower, upper192  have total := bernoulliWeight.total at p193  exact ProbabilitySpace.intro with finite, function, nonnegative, total194195theorem bernoulliWeight.prob_one (p : Real)196  requires lower : (0:R) ≤ p197  requires upper : p ≤ (1:R)198  shows prob(bernoulliWeight(p), {(1:N)}) = p199proof200  have space := bernoulliWeight.space with lower, upper201  have point := twoPoint.one202  have singleton := prob.singleton with space, point203  rw singleton204  exact bernoulliWeight.at_one at p205206theorem bernoulliWeight.prob_zero (p : Real)207  requires lower : (0:R) ≤ p208  requires upper : p ≤ (1:R)209  shows prob(bernoulliWeight(p), {(0:N)}) = (1:R) - p210proof211  have space := bernoulliWeight.space with lower, upper212  have point := twoPoint.zero213  have singleton := prob.singleton with space, point214  rw singleton215  exact bernoulliWeight.at_zero at p216217-- The outcome of the trial as a random variable: one on success.218def bernoulliVariable : Set := realIndicator(twoPoint, {(1:N)})219220theorem bernoulliVariable.function221  shows bernoulliVariable : twoPoint → ℝ222proof223  unfold bernoulliVariable224  exact realIndicator.function at twoPoint, {(1:N)}225226theorem bernoulliVariable.expectation (p : Real)227  requires lower : (0:R) ≤ p228  requires upper : p ≤ (1:R)229  shows expectation(twoPoint, bernoulliWeight(p), bernoulliVariable) = p230proof231  have space := bernoulliWeight.space with lower, upper232  have event : {(1:N)} ⊆ twoPoint233    intros y member234    have equal := singleton.membership.forward with member235    rw equal236    exact twoPoint.one237  have indicator := expectation.indicator with space, event238  have success := bernoulliWeight.prob_one with lower, upper239  unfold bernoulliVariable240  cc241242-- An indicator is its own square.243theorem bernoulliVariable.square_expectation (p : Real)244  requires lower : (0:R) ≤ p245  requires upper : p ≤ (1:R)246  shows expectation(twoPoint, bernoulliWeight(p), squareVariable(twoPoint,247      bernoulliVariable)) = p248proof249  have space := bernoulliWeight.space with lower, upper250  have random := bernoulliVariable.function251  have square := squareVariable.function with random252  have agree : ∀ ω ∈ twoPoint, squareVariable(twoPoint, bernoulliVariable)(ω) =253      bernoulliVariable(ω)254    intros ω point255    have value := squareVariable.value at twoPoint, bernoulliVariable, ω with256        random, point257    have alternatives : ω ∈ {(1:N)} ∨ ¬(ω ∈ {(1:N)}) by tauto258    cases alternatives with inside | outside259    . have one : bernoulliVariable(ω) = (1:R)260        unfold bernoulliVariable261        exact realIndicator.inside at twoPoint, {(1:N)}, ω with point, inside262      rw [value, one]263      ring264    . have zero : bernoulliVariable(ω) = (0:R)265        unfold bernoulliVariable266        exact realIndicator.outside at twoPoint, {(1:N)}, ω with point, outside267      rw [value, zero]268      ring269  have same := expectation.congr with space, square, random, agree270  rw same271  exact bernoulliVariable.expectation with lower, upper272273theorem bernoulliVariable.variance (p : Real)274  requires lower : (0:R) ≤ p275  requires upper : p ≤ (1:R)276  shows variance(twoPoint, bernoulliWeight(p),277      bernoulliVariable) = p * ((1:R) - p)278proof279  have space := bernoulliWeight.space with lower, upper280  have random := bernoulliVariable.function281  have formula := variance.formula with space, random282  have mean := bernoulliVariable.expectation with lower, upper283  have squareMean := bernoulliVariable.square_expectation with lower, upper284  rw [formula, mean, squareMean]285  ring286287-- A fair coin is the uniform distribution on two points.288def fairCoin : Set := uniformWeight(twoPoint)289290theorem fairCoin.space291  shows ProbabilitySpace(twoPoint, fairCoin)292proof293  have finite := twoPoint.finite294  have inhabited := twoPoint.nonempty295  unfold fairCoin296  exact uniformWeight.space with finite, inhabited297298theorem twoPoint.size299  shows realSize(twoPoint) = (2:R)300proof301  have numeral := realNumeral.nat at 2302  rw [realSize.value, twoPoint.cardinality, numeral]303  rfl304305theorem fairCoin.heads306  shows prob(fairCoin, {(1:N)}) = (1:R) / (2:R)307proof308  have finite := twoPoint.finite309  have point := twoPoint.one310  have classical := prob.uniform_point with finite, point311  have size := twoPoint.size312  unfold fairCoin313  cc314315theorem fairCoin.tails316  shows prob(fairCoin, {(0:N)}) = (1:R) / (2:R)317proof318  have finite := twoPoint.finite319  have point := twoPoint.zero320  have classical := prob.uniform_point with finite, point321  have size := twoPoint.size322  unfold fairCoin323  cc324325theorem fairCoin.expectation326  shows expectation(twoPoint, fairCoin, bernoulliVariable) = (1:R) / (2:R)327proof328  have space := fairCoin.space329  have event : {(1:N)} ⊆ twoPoint330    intros y member331    have equal := singleton.membership.forward with member332    rw equal333    exact twoPoint.one334  have indicator := expectation.indicator with space, event335  have heads := fairCoin.heads336  unfold bernoulliVariable337  cc338339-- A fair die is the uniform distribution on six faces.340def dieFaces : Set := {(1:N), (2:N), (3:N), (4:N), (5:N), (6:N)}341342theorem dieFaces.bounded343  shows dieFaces ⊆ (7:N)344proof345  unfold dieFaces346  decide347348theorem dieFaces.finite349  shows Finite(dieFaces)350proof351  have seven := Finite.natural at (7:N)352  have bounded := dieFaces.bounded353  exact Finite.subset with seven, bounded354355theorem dieFaces.one356  shows (1:N) ∈ dieFaces357proof358  unfold dieFaces359  decide360361theorem dieFaces.nonempty362  shows Nonempty(dieFaces)363proof364  have member := dieFaces.one365  exact ⟨(1:N), member⟩366367theorem dieFaces.cardinality368  shows cardinality(dieFaces) = 6369proof370  unfold dieFaces371  decide372373theorem dieFaces.size374  shows realSize(dieFaces) = (6:R)375proof376  have numeral := realNumeral.nat at 6377  rw [realSize.value, dieFaces.cardinality, numeral]378  rfl379380def fairDie : Set := uniformWeight(dieFaces)381382theorem fairDie.space383  shows ProbabilitySpace(dieFaces, fairDie)384proof385  have finite := dieFaces.finite386  have inhabited := dieFaces.nonempty387  unfold fairDie388  exact uniformWeight.space with finite, inhabited389390theorem fairDie.six391  shows prob(fairDie, {(6:N)}) = (1:R) / (6:R)392proof393  have finite := dieFaces.finite394  have point : (6:N) ∈ dieFaces395    unfold dieFaces396    decide397  have classical := prob.uniform_point with finite, point398  have size := dieFaces.size399  unfold fairDie400  cc401402def evenFaces : Set := {(2:N), (4:N), (6:N)}403404theorem evenFaces.event405  shows evenFaces ⊆ dieFaces406proof407  unfold evenFaces408  unfold dieFaces409  decide410411theorem evenFaces.cardinality412  shows cardinality(evenFaces) = 3413proof414  unfold evenFaces415  decide416417theorem evenFaces.size418  shows realSize(evenFaces) = (3:R)419proof420  have numeral := realNumeral.nat at 3421  rw [realSize.value, evenFaces.cardinality, numeral]422  rfl423424theorem fairDie.even425  shows prob(fairDie, evenFaces) = (3:R) / (6:R)426proof427  have finite := dieFaces.finite428  have event := evenFaces.event429  have classical := prob.uniform with finite, event430  have sizeEven := evenFaces.size431  have sizeAll := dieFaces.size432  unfold fairDie433  cc434435theorem realDiv.three_sixths436  shows (3:R) / (6:R) = (1:R) / (2:R)437proof438  have twoReal := realNumeral.real at 2439  have threeReal := realNumeral.real at 3440  have sixReal := realNumeral.real at 6441  have twoPositive : (0:R) < (2:R) by linarith442  have sixPositive : (0:R) < (6:R) by linarith443  have twoNonzero : (2:R) ≠ (0:R)444    intro zero445    rw zero at twoPositive446    exact realLess.not_self with twoPositive447  have sixNonzero : (6:R) ≠ (0:R)448    intro zero449    rw zero at sixPositive450    exact realLess.not_self with sixPositive451  have inverseSixReal := realInvValue.real at (6:R)452  have inverseTwoReal := realInvValue.real at (2:R)453  have sixLaw := realInvValue.mul_right at (6:R) with sixNonzero454  have divisionThree := realDiv.eq_mul_inv at (3:R), (6:R)455  have divisionOne := realDiv.eq_mul_inv at (1:R), (2:R)456  have product : (2:R) * ((3:R) * (realInvValue((6:R)):R)) = (1:R)457    calc458      (2:R) * ((3:R) * (realInvValue((6:R)):R)) =459        (6:R) * (realInvValue((6:R)):R) := by ring460      _ = (1:R) := sixLaw461  have inverse := realInvValue.eq_of_mul_right at (2:R),462      (3:R) * (realInvValue((6:R)):R) with463    twoNonzero, product464  have oneLeft := realMulValue.one_left at realInvValue((2:R))465  rw [divisionThree, divisionOne, inverse, oneLeft]466  rfl467468theorem fairDie.even_half469  shows prob(fairDie, evenFaces) = (1:R) / (2:R)470proof471  have even := fairDie.even472  have same := realDiv.three_sixths473  rw [even, same]474  rfl475