FiniteProbability.lean`

27 declarations, 0 contain sorry, 0 declared as axioms

Finite weighted probability and independent Bernoulli coordinates

Events are finite sets and their weights are finite sums. Normalization and nonnegativity are explicit hypotheses for the generic probability inequalities. The product identities are algebraic, so their statements also hold at the boundary parameters zero and one without dividing by any point weight.

def OAI.QuantitativeVanDerWaerden.FiniteProbability.prob line 31
Source documentation
The weight of a finite event.
```
def prob (w : Ω → ℝ) (A : Finset Ω) : ℝ := ∑ ω ∈ A, w ω
```
theorem OAI.QuantitativeVanDerWaerden.FiniteProbability.prob_empty line 33
theorem OAI.QuantitativeVanDerWaerden.FiniteProbability.prob_univ line 36
theorem OAI.QuantitativeVanDerWaerden.FiniteProbability.prob_nonneg line 39
theorem OAI.QuantitativeVanDerWaerden.FiniteProbability.prob_mono line 43
theorem OAI.QuantitativeVanDerWaerden.FiniteProbability.prob_union_le line 50
theorem OAI.QuantitativeVanDerWaerden.FiniteProbability.prob_biUnion_le line 58
Source documentation
Finite union bound; events need not be independent.
```
theorem prob_biUnion_le {w : Ω → ℝ} (hw : ∀ ω, 0 ≤ w ω)
    (J : Finset I) (A : I → Finset Ω) :
    prob w (J.biUnion A) ≤ ∑ i ∈ J, prob w (A i) := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.FiniteProbability.prob
theorem OAI.QuantitativeVanDerWaerden.FiniteProbability.exists_not_mem_of_prob_lt_one line 69
Source documentation
A normalized event of weight strictly below one misses a point.
```
theorem exists_not_mem_of_prob_lt_one [Fintype Ω] {w : Ω → ℝ}
    (hw : ∑ ω, w ω = 1) (A : Finset Ω) (hA : prob w A < 1) :
    ∃ ω, ω ∉ A := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.FiniteProbability.prob

theorem OAI.QuantitativeVanDerWaerden.FiniteProbability.exists_avoiding_of_sum_probs_lt_one line 84

Source documentation

If the sum of bad-event probabilities is below one, avoid all of them.

theorem exists_avoiding_of_sum_probs_lt_one [Fintype Ω] {w : Ω → ℝ}
    (hw : ∀ ω, 0 ≤ w ω) (htotal : ∑ ω, w ω = 1)
    (J : Finset I) (A : I → Finset Ω)
    (hbudget : (∑ i ∈ J, prob w (A i)) < 1) :
    ∃ ω, ∀ i ∈ J, ω ∉ A i := by
…

Mentions: OAI.QuantitativeVanDerWaerden.FiniteProbability.prob

def OAI.QuantitativeVanDerWaerden.FiniteProbability.bitWeight line 98
Source documentation
A single Bernoulli coordinate gives weight p to true.
```
def bitWeight (p : ℝ) (b : Bool) : ℝ := if b then p else 1 - p
…
```
def OAI.QuantitativeVanDerWaerden.FiniteProbability.bernoulliWeight line 103
Source documentation
Product weight on the actual finite space of all bit assignments.
```
def bernoulliWeight (p : ℝ) (ω : Key → Bool) : ℝ :=
…
```
theorem OAI.QuantitativeVanDerWaerden.FiniteProbability.bernoulliWeight_nonneg line 106
theorem OAI.QuantitativeVanDerWaerden.FiniteProbability.sum_bernoulliWeight line 117
Source documentation
The product Bernoulli weights sum to one, including p = 0 and p = 1.
```
theorem sum_bernoulliWeight (p : ℝ) :
    ∑ ω : Key → Bool, bernoulliWeight p ω = 1 := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.FiniteProbability.bernoulliWeight
theorem OAI.QuantitativeVanDerWaerden.FiniteProbability.expectation_prod line 127
Source documentation
Product expectation for independent bits, expressed entirely by finite sums.
```
theorem expectation_prod (p : ℝ) (f : Key → Bool → ℝ) :
    (∑ ω : Key → Bool, bernoulliWeight p ω * ∏ i, f i (ω i)) =
      ∏ i, ((1 - p) * f i false + p * f i true) := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.FiniteProbability.bernoulliWeight
def OAI.QuantitativeVanDerWaerden.FiniteProbability.coordinateEvent line 143
Source documentation
Each coordinate may restrict its bit independently.
```
def coordinateEvent (P : Key → Bool → Prop) : Finset (Key → Bool) := by
…
```
theorem OAI.QuantitativeVanDerWaerden.FiniteProbability.prob_coordinateEvent line 148
Source documentation
Exact weight of arbitrary coordinatewise restrictions.
```
theorem prob_coordinateEvent (p : ℝ) (P : Key → Bool → Prop)
    [∀ i, DecidablePred (P i)] :
    prob (bernoulliWeight p) (coordinateEvent P) =
      ∏ i, ∑ b : Bool, if P i b then bitWeight p b else 0 := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.FiniteProbability.prob, OAI.QuantitativeVanDerWaerden.FiniteProbability.bernoulliWeight, OAI.QuantitativeVanDerWaerden.FiniteProbability.coordinateEvent, OAI.QuantitativeVanDerWaerden.FiniteProbability.bitWeight
def OAI.QuantitativeVanDerWaerden.FiniteProbability.cylinder line 167
Source documentation
Assign prescribed bits on a named finite set of distinct keys.
```
def cylinder (S : Finset Key) (a : Key → Bool) : Finset (Key → Bool) := by
…
```
theorem OAI.QuantitativeVanDerWaerden.FiniteProbability.mem_cylinder line 171
theorem OAI.QuantitativeVanDerWaerden.FiniteProbability.prob_bernoulli_cylinder line 177
Source documentation
Exact cylinder probability; coordinates outside S are summed out.
```
theorem prob_bernoulli_cylinder (p : ℝ) (S : Finset Key) (a : Key → Bool) :
    prob (bernoulliWeight p) (cylinder S a) =
      ∏ i ∈ S, if a i then p else 1 - p := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.FiniteProbability.prob, OAI.QuantitativeVanDerWaerden.FiniteProbability.bernoulliWeight, OAI.QuantitativeVanDerWaerden.FiniteProbability.cylinder
def OAI.QuantitativeVanDerWaerden.FiniteProbability.DependsOn line 197
Source documentation
A finite event is determined by the coordinates in its declared support.
```
def DependsOn (S : Finset Key) (E : Finset (Key → Bool)) : Prop :=
…
```
def OAI.QuantitativeVanDerWaerden.FiniteProbability.splice line 200
def OAI.QuantitativeVanDerWaerden.FiniteProbability.coordinateSwap line 204
Source documentation
Exchange the complementary coordinates between two complete assignments.
```
private def coordinateSwap (S : Finset Key) :
    ((Key → Bool) × (Key → Bool)) ≃ ((Key → Bool) × (Key → Bool)) where
…
```
theorem OAI.QuantitativeVanDerWaerden.FiniteProbability.bernoulliWeight_splice line 213
theorem OAI.QuantitativeVanDerWaerden.FiniteProbability.sum_pair_product line 223

theorem OAI.QuantitativeVanDerWaerden.FiniteProbability.expectation_mul_of_disjoint_supports line 231

Source documentation

Arbitrary functions of disjoint sets of coordinates factor under the actual finite Bernoulli weights. The proof swaps two complete assignments.

theorem expectation_mul_of_disjoint_supports (p : ℝ) (S T : Finset Key)
    (hST : Disjoint S T) (f g : (Key → Bool) → ℝ)
    (hf : ∀ ω η, (∀ i ∈ S, ω i = η i) → f ω = f η)
    (hg : ∀ ω η, (∀ i ∈ T, ω i = η i) → g ω = g η) :
    (∑ ω : Key → Bool, bernoulliWeight p ω * f ω * g ω) =
      (∑ ω : Key → Bool, bernoulliWeight p ω * f ω) *
      (∑ ω : Key → Bool, bernoulliWeight p ω * g ω) := by
…

Mentions: OAI.QuantitativeVanDerWaerden.FiniteProbability.bernoulliWeight

theorem OAI.QuantitativeVanDerWaerden.FiniteProbability.prob_eq_sum_indicator line 277
Source documentation
Finite-event mass as the expectation of its zero-one indicator.
```
theorem prob_eq_sum_indicator [Fintype Ω] [DecidableEq Ω]
    (w : Ω → ℝ) (E : Finset Ω) :
    prob w E = ∑ ω, w ω * (if ω ∈ E then (1 : ℝ) else 0) := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.FiniteProbability.prob
theorem OAI.QuantitativeVanDerWaerden.FiniteProbability.prob_inter_of_disjoint_supports line 296
Source documentation
Actual events depending on disjoint key sets are independent. No cylinder restriction or probability-factorization hypothesis is imposed on the events.
```
theorem prob_inter_of_disjoint_supports (p : ℝ)
    (E F : Finset (Key → Bool)) (S T : Finset Key)
    (hE : DependsOn S E) (hF : DependsOn T F) (hST : Disjoint S T) :
    prob (bernoulliWeight p) (E ∩ F) =
      prob (bernoulliWeight p) E * prob (bernoulliWeight p) F := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.F, OAI.QuantitativeVanDerWaerden.FiniteProbability.DependsOn, OAI.QuantitativeVanDerWaerden.FiniteProbability.prob, OAI.QuantitativeVanDerWaerden.FiniteProbability.bernoulliWeight