Grace/Cumulus/Probability/Uniform.g17

Open in Workbench Download source

Imports

Space

Declarations

Source

1-- The uniform distribution on a nonempty finite set2-- 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.Uniform8import Space910-- The number of points of a finite set, as a real.11def realSize (Ω : Set) : Set := realNat(cardinality(Ω))1213theorem realSize.value (Ω : Set)14  shows realSize(Ω) = realNat(cardinality(Ω))15proof16  simp [realSize]1718theorem realSize.real (Ω : Set)19  requires finite : Finite(Ω)20  shows Real(realSize(Ω))21proof22  have natural := cardinality.nat with finite23  rw realSize.value24  exact realNat.real at cardinality(Ω)2526theorem realSize.nonnegative (Ω : Set)27  requires finite : Finite(Ω)28  shows (0:R) ≤ (realSize(Ω):R)29proof30  have natural := cardinality.nat with finite31  rw realSize.value32  exact realNat.zero_le at cardinality(Ω)3334theorem cardinality.ne_zero_of_nonempty (Ω : Set)35  requires finite : Finite(Ω)36  requires inhabited : Nonempty(Ω)37  shows cardinality(Ω) ≠ 038proof39  intro zero40  have correct := cardinality.correct with finite41  rw zero at correct42  have empty := HasCardinality.empty_of_zero with correct43  have different := Nonempty.ne_empty with inhabited44  exact different with empty4546theorem realSize.positive (Ω : Set)47  requires finite : Finite(Ω)48  requires inhabited : Nonempty(Ω)49  shows (0:R) < (realSize(Ω):R)50proof51  have natural := cardinality.nat with finite52  have nonzero := cardinality.ne_zero_of_nonempty with finite, inhabited53  rw realSize.value54  exact realNat.positive at cardinality(Ω) with nonzero5556theorem realSize.nonzero (Ω : Set)57  requires finite : Finite(Ω)58  requires inhabited : Nonempty(Ω)59  shows realSize(Ω) ≠ (0:R)60proof61  have sizeReal := realSize.real with finite62  have positive := realSize.positive with finite, inhabited63  intro zero64  rw zero at positive65  exact realLess.not_self with positive6667theorem realSize.monotone (A B : Set)68  requires finite : Finite(B)69  requires subset : A ⊆ B70  shows (realSize(A):R) ≤ (realSize(B):R)71proof72  have finiteA := Finite.subset with finite, subset73  have naturalA := cardinality.nat with finiteA74  have naturalB := cardinality.nat with finite75  have le := cardinality.monotone with finite, subset76  rw [realSize.value, realSize.value]77  exact realNat.le_of_natural_le at cardinality(A), cardinality(B) with le7879-- The uniform weight gives every point the mass 1 / |Ω|.80def uniformWeight (Ω : Set) : Set :=81  constantFunction(Ω, ℝ, realInvValue(realSize(Ω)))8283theorem uniformWeight.mass_real (Ω : Set)84  requires finite : Finite(Ω)85  shows Real(realInvValue(realSize(Ω)))86proof87  have sizeReal := realSize.real with finite88  exact realInvValue.real at realSize(Ω)8990theorem uniformWeight.function (Ω : Set)91  requires finite : Finite(Ω)92  shows uniformWeight(Ω) : Ω → ℝ93proof94  have massReal := uniformWeight.mass_real with finite95  unfold uniformWeight96  exact constantFunction.function at Ω, ℝ, realInvValue(realSize(Ω)) with97    massReal9899theorem uniformWeight.value (Ω ω : Set)100  requires finite : Finite(Ω)101  requires point : ω ∈ Ω102  shows uniformWeight(Ω)(ω) = realInvValue(realSize(Ω))103proof104  have massReal := uniformWeight.mass_real with finite105  unfold uniformWeight106  exact constantFunction.apply at Ω, ℝ, ω, realInvValue(realSize(Ω)) with107    point, massReal108109theorem uniformWeight.mass_positive (Ω : Set)110  requires finite : Finite(Ω)111  requires inhabited : Nonempty(Ω)112  shows (0:R) < (realInvValue(realSize(Ω)):R)113proof114  have sizeReal := realSize.real with finite115  have positive := realSize.positive with finite, inhabited116  exact realInvValue.positive at realSize(Ω) with positive117118theorem uniformWeight.nonnegative (Ω : Set)119  requires finite : Finite(Ω)120  requires inhabited : Nonempty(Ω)121  shows ∀ ω ∈ Ω, (0:R) ≤ (uniformWeight(Ω)(ω):R)122proof123  intros ω point124  have value := uniformWeight.value with finite, point125  have massReal := uniformWeight.mass_real with finite126  have positive := uniformWeight.mass_positive with finite, inhabited127  rw value128  linarith129130-- Summing the uniform weight over an event gives |A| / |Ω|.131theorem uniformWeight.sum (Ω A : Set)132  requires finite : Finite(Ω)133  requires event : A ⊆ Ω134  shows realSetSum(A,135      uniformWeight(Ω)) = (realSize(A):R) * (realInvValue(realSize(Ω)):R)136proof137  have massReal := uniformWeight.mass_real with finite138  have finiteA := Finite.subset with finite, event139  have constant := realSetSum.constant at A, Ω, realInvValue(realSize(Ω)) with140    finiteA, event141  have size := realSize.value at A142  unfold uniformWeight143  cc144145theorem uniformWeight.total (Ω : Set)146  requires finite : Finite(Ω)147  requires inhabited : Nonempty(Ω)148  shows realSetSum(Ω, uniformWeight(Ω)) = (1:R)149proof150  have whole := Subset.reflexive at Ω151  have sum := uniformWeight.sum with finite, whole152  have sizeReal := realSize.real with finite153  have nonzero := realSize.nonzero with finite, inhabited154  have inverse := realInvValue.mul_right at realSize(Ω) with nonzero155  rw sum156  exact inverse157158theorem uniformWeight.space (Ω : Set)159  requires finite : Finite(Ω)160  requires inhabited : Nonempty(Ω)161  shows ProbabilitySpace(Ω, uniformWeight(Ω))162proof163  have function := uniformWeight.function with finite164  have nonnegative := uniformWeight.nonnegative with finite, inhabited165  have total := uniformWeight.total with finite, inhabited166  exact ProbabilitySpace.intro with finite, function, nonnegative, total167168-- Classical probability: favourable cases over all cases.169theorem prob.uniform (Ω A : Set)170  requires finite : Finite(Ω)171  requires event : A ⊆ Ω172  shows prob(uniformWeight(Ω), A) = (realSize(A):R) / (realSize(Ω):R)173proof174  have finiteA := Finite.subset with finite, event175  have sizeReal := realSize.real with finite176  have sizeAReal := realSize.real with finiteA177  have sum := uniformWeight.sum with finite, event178  have division := realDiv.eq_mul_inv at realSize(A), realSize(Ω)179  rw [prob.value, sum, division]180  rfl181182theorem prob.uniform_point (Ω ω : Set)183  requires finite : Finite(Ω)184  requires point : ω ∈ Ω185  shows prob(uniformWeight(Ω), {ω}) = (1:R) / (realSize(Ω):R)186proof187  have event : {ω} ⊆ Ω by simp188  have classical := prob.uniform with finite, event189  have one : realSize({ω}) = (1:R)190    rw [realSize.value, cardinality.singleton]191    exact realNat.one192  rwa one at classical193194theorem prob.uniform_whole (Ω : Set)195  requires finite : Finite(Ω)196  requires inhabited : Nonempty(Ω)197  shows prob(uniformWeight(Ω), Ω) = (1:R)198proof199  have space := uniformWeight.space with finite, inhabited200  exact prob.whole with space201202theorem prob.uniform_complement (Ω A : Set)203  requires finite : Finite(Ω)204  requires inhabited : Nonempty(Ω)205  requires event : A ⊆ Ω206  shows prob(uniformWeight(Ω),207      Ω ∖ A) = (1:R) - (realSize(A):R) / (realSize(Ω):R)208proof209  have space := uniformWeight.space with finite, inhabited210  have complement := prob.complement with space, event211  have classical := prob.uniform with finite, event212  rwa classical at complement213214-- Events of the same size are equally likely.215theorem prob.uniform_congr (Ω A B : Set)216  requires finite : Finite(Ω)217  requires eventA : A ⊆ Ω218  requires eventB : B ⊆ Ω219  requires same : cardinality(A) = cardinality(B)220  shows prob(uniformWeight(Ω), A) = prob(uniformWeight(Ω), B)221proof222  have classicalA := prob.uniform with finite, eventA223  have classicalB := prob.uniform with finite, eventB224  have sizes : realSize(A) = realSize(B)225    rw [realSize.value, realSize.value, same]226    rfl227  rw [classicalA, classicalB, sizes]228  rfl229230theorem prob.uniform_le_of_size (Ω A B : Set)231  requires finite : Finite(Ω)232  requires eventA : A ⊆ Ω233  requires eventB : B ⊆ Ω234  requires smaller : LessEqual(cardinality(A), cardinality(B))235  shows (prob(uniformWeight(Ω), A):R) ≤ (prob(uniformWeight(Ω), B):R)236proof237  have finiteA := Finite.subset with finite, eventA238  have finiteB := Finite.subset with finite, eventB239  have naturalA := cardinality.nat with finiteA240  have naturalB := cardinality.nat with finiteB241  have sizeReal := realSize.real with finite242  have sizeAReal := realSize.real with finiteA243  have sizeBReal := realSize.real with finiteB244  have massReal := uniformWeight.mass_real with finite245  have classicalA := prob.uniform with finite, eventA246  have classicalB := prob.uniform with finite, eventB247  have divisionA := realDiv.eq_mul_inv at realSize(A), realSize(Ω)248  have divisionB := realDiv.eq_mul_inv at realSize(B), realSize(Ω)249  have inverseNonnegative : (0:R) ≤ (realInvValue(realSize(Ω)):R)250    have alternatives : Nonempty(Ω) ∨ ¬(Nonempty(Ω)) by tauto251    cases alternatives with inhabited | empty252    . have positive := uniformWeight.mass_positive with finite, inhabited253      linarith254    . have isEmpty : Ω = ∅255        have subset : Ω ⊆ ∅256          intros x hx257          exfalso258          apply empty259          exact ⟨x, hx⟩260        exact Subset.antisymmetric with subset, (empty.subset at Ω)261      have emptyCount := cardinality.eq_of_has with HasCardinality.empty_set262      have zero : realSize(Ω) = (0:R)263        rw [realSize.value, isEmpty, emptyCount]264        exact realNat.zero265      rw [zero, realInvValue.zero]266      exact realLe.reflexive with realZero.real267  have sizeLe : (realSize(A):R) ≤ (realSize(B):R)268    rw [realSize.value, realSize.value]269    exact realNat.le_of_natural_le at cardinality(A), cardinality(B) with smaller270  have scaled := realLe.mul_right_of_nonnegative at realSize(A), realSize(B),271    realInvValue(realSize(Ω)) with sizeLe, inverseNonnegative272  rw [classicalA, classicalB, divisionA, divisionB]273  exact scaled274