Grace/Cumulus/Probability/Dirac.g17

Open in Workbench Download source

Imports

Variance

Declarations

Source

1-- Point masses: the probability space concentrated at one outcome2-- 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.Dirac8import Variance910-- The weight that puts all mass on the single outcome ω₀.11def diracWeight (Ω ω₀ : Set) : Set := realIndicator(Ω, {ω₀})1213theorem diracWeight.function (Ω ω₀ : Set)14  shows diracWeight(Ω, ω₀) : Ω → ℝ15proof16  unfold diracWeight17  exact realIndicator.function at Ω, {ω₀}1819theorem diracWeight.at_point (Ω ω₀ : Set)20  requires point : ω₀ ∈ Ω21  shows diracWeight(Ω, ω₀)(ω₀) = (1:R)22proof23  have self := singleton.self at ω₀24  unfold diracWeight25  exact realIndicator.inside at Ω, {ω₀}, ω₀ with point, self2627theorem diracWeight.elsewhere (Ω ω₀ ω : Set)28  requires point : ω ∈ Ω29  requires different : ω ≠ ω₀30  shows diracWeight(Ω, ω₀)(ω) = (0:R)31proof32  have outside : ¬(ω ∈ {ω₀}) by simp [singleton.membership]33  unfold diracWeight34  exact realIndicator.outside at Ω, {ω₀}, ω with point, outside3536theorem diracWeight.nonnegative (Ω ω₀ : Set)37  shows ∀ ω ∈ Ω, (0:R) ≤ (diracWeight(Ω, ω₀)(ω):R)38proof39  intros ω point40  unfold diracWeight41  exact realIndicator.nonnegative at Ω, {ω₀}, ω with point4243-- Summing the point mass over an event counts whether ω₀ lies in it.44theorem diracWeight.sum_of_member (Ω ω₀ A : Set)45  requires finite : Finite(A)46  requires event : A ⊆ Ω47  requires member : ω₀ ∈ A48  shows realSetSum(A, diracWeight(Ω, ω₀)) = (1:R)49proof50  have counted := realSetSum.indicator at A, {ω₀}, Ω with finite, event51  have meet : A ∩ {ω₀} = {ω₀}52    ext y53    simp54  have one := cardinality.singleton at ω₀55  simp [diracWeight]56  exact realNat.one5758theorem diracWeight.sum_of_absent (Ω ω₀ A : Set)59  requires finite : Finite(A)60  requires event : A ⊆ Ω61  requires absent : ¬(ω₀ ∈ A)62  shows realSetSum(A, diracWeight(Ω, ω₀)) = (0:R)63proof64  have counted := realSetSum.indicator at A, {ω₀}, Ω with finite, event65  have meet : A ∩ {ω₀} = ∅66    ext y67    simp68  have zero := cardinality.eq_of_has with HasCardinality.empty_set69  simp [diracWeight]7071theorem diracWeight.total (Ω ω₀ : Set)72  requires finite : Finite(Ω)73  requires point : ω₀ ∈ Ω74  shows realSetSum(Ω, diracWeight(Ω, ω₀)) = (1:R)75proof76  have whole := Subset.reflexive at Ω77  exact diracWeight.sum_of_member with finite, whole, point7879theorem diracWeight.space (Ω ω₀ : Set)80  requires finite : Finite(Ω)81  requires point : ω₀ ∈ Ω82  shows ProbabilitySpace(Ω, diracWeight(Ω, ω₀))83proof84  have function := diracWeight.function at Ω, ω₀85  have nonnegative := diracWeight.nonnegative at Ω, ω₀86  have total := diracWeight.total with finite, point87  exact ProbabilitySpace.intro with finite, function, nonnegative, total8889theorem prob.dirac_of_member (Ω ω₀ A : Set)90  requires finite : Finite(Ω)91  requires event : A ⊆ Ω92  requires member : ω₀ ∈ A93  shows prob(diracWeight(Ω, ω₀), A) = (1:R)94proof95  have finiteA := Finite.subset with finite, event96  rw prob.value97  exact diracWeight.sum_of_member with finiteA, event, member9899theorem prob.dirac_of_absent (Ω ω₀ A : Set)100  requires finite : Finite(Ω)101  requires event : A ⊆ Ω102  requires absent : ¬(ω₀ ∈ A)103  shows prob(diracWeight(Ω, ω₀), A) = (0:R)104proof105  have finiteA := Finite.subset with finite, event106  rw prob.value107  exact diracWeight.sum_of_absent with finiteA, event, absent108109-- Under a point mass, every random variable is constant in expectation.110theorem expectation.dirac (Ω ω₀ X : Set)111  requires finite : Finite(Ω)112  requires point : ω₀ ∈ Ω113  requires random : X : Ω → ℝ114  shows expectation(Ω, diracWeight(Ω, ω₀), X) = X(ω₀)115proof116  have whole := Subset.reflexive at Ω117  have function := diracWeight.function at Ω, ω₀118  have product := weightMul.function with function, random119  have masked := maskedWeight.function at Ω, {ω₀}, X with random120  have agree : ∀ ω ∈ Ω, weightMul(Ω, diracWeight(Ω, ω₀), X)(ω) =121      maskedWeight(Ω, {ω₀}, X)(ω)122    intros ω inside123    have xReal := FunctionBetween.apply_closed with random, inside124    have natural := indicator.natural at {ω₀}, ω125    have maskReal := realNat.real at indicator({ω₀}, ω)126    have left := weightMul.value at Ω, diracWeight(Ω, ω₀), X, ω with function,127        random, inside128    have inner : diracWeight(Ω, ω₀)(ω) = realNat(indicator({ω₀}, ω))129      unfold diracWeight130      exact realIndicator.value at Ω, {ω₀}, ω with inside131    have right := maskedWeight.value at Ω, {ω₀}, X, ω with random, inside132    rw [left, inner, right]133    ring134  have same := realSetSum.congr with product, masked, whole, agree135  have counted := realSetSum.masked_intersection at Ω, {ω₀}, Ω, X with finite,136      random, whole137  have meet : Ω ∩ {ω₀} = {ω₀}138    ext y139    simp140  have single := realSetSum.singleton with random, point141  rw [expectation.value, same, counted, meet, single]142  rfl143144theorem variance.dirac (Ω ω₀ X : Set)145  requires finite : Finite(Ω)146  requires point : ω₀ ∈ Ω147  requires random : X : Ω → ℝ148  shows variance(Ω, diracWeight(Ω, ω₀), X) = (0:R)149proof150  have mean := expectation.dirac with finite, point, random151  have xReal := FunctionBetween.apply_closed with random, point152  have centered := centeredVariable.function at Ω, X, expectation(Ω,153      diracWeight(Ω, ω₀), X)154    with random155  have square := squareVariable.function with centered156  have squareMean := expectation.dirac at Ω, ω₀,157    squareVariable(Ω, centeredVariable(Ω, X, expectation(Ω, diracWeight(Ω, ω₀),158      X))) with159    finite, point, square160  have squareValue := squareVariable.value at Ω,161    centeredVariable(Ω, X, expectation(Ω, diracWeight(Ω, ω₀), X)), ω₀ with162      centered, point163  have centeredValue := centeredVariable.value at Ω, X, expectation(Ω,164      diracWeight(Ω, ω₀), X),165    ω₀ with random, point166  rw [variance.value, squareMean, squareValue, centeredValue, mean]167  ring168169theorem diracWeight.prob_point (Ω ω₀ : Set)170  requires finite : Finite(Ω)171  requires point : ω₀ ∈ Ω172  shows prob(diracWeight(Ω, ω₀), {ω₀}) = (1:R)173proof174  have event : {ω₀} ⊆ Ω by simp175  have self := singleton.self at ω₀176  exact prob.dirac_of_member with finite, event, self177