HepLean Documentation

Mathlib.Probability.UniformOn

Classical probability #

The classical formulation of probability states that the probability of an event occurring in a finite probability space is the ratio of that event to all possible events. This notion can be expressed with measure theory using the counting measure. In particular, given the sets s and t, we define the probability of t occurring in s to be |s|⁻¹ * |s ∩ t|. With this definition, we recover the probability over the entire sample space when s = Set.univ.

Classical probability is often used in combinatorics and we prove some useful lemmas in this file for that purpose.

Main definition #

Notes #

The original aim of this file is to provide a measure theoretic method of describing the probability an element of a set s satisfies some predicate P. Our current formulation still allow us to describe this by abusing the definitional equality of sets and predicates by simply writing uniformOn s P. We should avoid this however as none of the lemmas are written for predicates.

source
def ProbabilityTheory.uniformOn {Ω : Type u_1} [MeasurableSpace Ω] (s : Set Ω) :
MeasureTheory.Measure Ω

Given a set s, uniformOn s is the uniform measure on s, defined as the counting measure conditioned by s. One should think of uniformOn s t as the proportion of s that is contained in t.

This is a probability measure when s is finite and nonempty and is given by ProbabilityTheory.uniformOn_isProbabilityMeasure.

Equations
Instances For
    source
    @[deprecated ProbabilityTheory.uniformOn]
    def ProbabilityTheory.condCount {Ω : Type u_1} [MeasurableSpace Ω] (s : Set Ω) :
    MeasureTheory.Measure Ω

    Alias of ProbabilityTheory.uniformOn.

    Given a set s, uniformOn s is the uniform measure on s, defined as the counting measure conditioned by s. One should think of uniformOn s t as the proportion of s that is contained in t.

    This is a probability measure when s is finite and nonempty and is given by ProbabilityTheory.uniformOn_isProbabilityMeasure.

    Equations
    Instances For
      source
      instance ProbabilityTheory.instIsZeroOrProbabilityMeasureUniformOn {Ω : Type u_1} [MeasurableSpace Ω] {s : Set Ω} :
      MeasureTheory.IsZeroOrProbabilityMeasure (ProbabilityTheory.uniformOn s)
      Equations
      • ⋯ = ⋯
      source
      @[simp]
      theorem ProbabilityTheory.uniformOn_empty_meas {Ω : Type u_1} [MeasurableSpace Ω] :
      ProbabilityTheory.uniformOn ∅ = 0
      source
      @[deprecated ProbabilityTheory.uniformOn_empty_meas]
      theorem ProbabilityTheory.condCount_empty_meas {Ω : Type u_1} [MeasurableSpace Ω] :
      ProbabilityTheory.uniformOn ∅ = 0

      Alias of ProbabilityTheory.uniformOn_empty_meas.

      source
      theorem ProbabilityTheory.uniformOn_empty {Ω : Type u_1} [MeasurableSpace Ω] {s : Set Ω} :
      (ProbabilityTheory.uniformOn s) ∅ = 0
      source
      @[deprecated ProbabilityTheory.uniformOn_empty]
      theorem ProbabilityTheory.condCount_empty {Ω : Type u_1} [MeasurableSpace Ω] {s : Set Ω} :
      (ProbabilityTheory.uniformOn s) ∅ = 0

      Alias of ProbabilityTheory.uniformOn_empty.

      source
      @[simp]
      theorem ProbabilityTheory.uniformOn_eq_zero' {Ω : Type u_1} [MeasurableSpace Ω] {s : Set Ω} (hs : MeasurableSet s) :
      ProbabilityTheory.uniformOn s = 0 ↔ s.Infinite ∨ s = ∅

      See uniformOn_eq_zero for a version assuming MeasurableSingletonClass Ω instead of MeasurableSet s.

      source
      @[simp]
      theorem ProbabilityTheory.uniformOn_eq_zero {Ω : Type u_1} [MeasurableSpace Ω] {s : Set Ω} [MeasurableSingletonClass Ω] :
      ProbabilityTheory.uniformOn s = 0 ↔ s.Infinite ∨ s = ∅

      See uniformOn_eq_zero' for a version assuming MeasurableSet s instead of MeasurableSingletonClass Ω.

      source
      theorem ProbabilityTheory.finite_of_uniformOn_ne_zero {Ω : Type u_1} [MeasurableSpace Ω] {s t : Set Ω} (h : (ProbabilityTheory.uniformOn s) t ≠ 0) :
      s.Finite
      source
      @[deprecated ProbabilityTheory.finite_of_uniformOn_ne_zero]
      theorem ProbabilityTheory.finite_of_condCount_ne_zero {Ω : Type u_1} [MeasurableSpace Ω] {s t : Set Ω} (h : (ProbabilityTheory.uniformOn s) t ≠ 0) :
      s.Finite

      Alias of ProbabilityTheory.finite_of_uniformOn_ne_zero.

      source
      theorem ProbabilityTheory.uniformOn_univ {Ω : Type u_1} [MeasurableSpace Ω] [Fintype Ω] {s : Set Ω} :
      (ProbabilityTheory.uniformOn Set.univ) s = MeasureTheory.Measure.count s / ↑(Fintype.card Ω)
      source
      @[deprecated ProbabilityTheory.uniformOn_univ]
      theorem ProbabilityTheory.condCount_univ {Ω : Type u_1} [MeasurableSpace Ω] [Fintype Ω] {s : Set Ω} :
      (ProbabilityTheory.uniformOn Set.univ) s = MeasureTheory.Measure.count s / ↑(Fintype.card Ω)

      Alias of ProbabilityTheory.uniformOn_univ.

      source
      theorem ProbabilityTheory.uniformOn_isProbabilityMeasure {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s : Set Ω} (hs : s.Finite) (hs' : s.Nonempty) :
      MeasureTheory.IsProbabilityMeasure (ProbabilityTheory.uniformOn s)
      source
      @[deprecated ProbabilityTheory.uniformOn_isProbabilityMeasure]
      theorem ProbabilityTheory.condCount_isProbabilityMeasure {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s : Set Ω} (hs : s.Finite) (hs' : s.Nonempty) :
      MeasureTheory.IsProbabilityMeasure (ProbabilityTheory.uniformOn s)

      Alias of ProbabilityTheory.uniformOn_isProbabilityMeasure.

      source
      theorem ProbabilityTheory.uniformOn_singleton {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] (ω : Ω) (t : Set Ω) [Decidable (ω ∈ t)] :
      (ProbabilityTheory.uniformOn {ω}) t = if ω ∈ t then 1 else 0
      source
      @[deprecated ProbabilityTheory.uniformOn_singleton]
      theorem ProbabilityTheory.condCount_singleton {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] (ω : Ω) (t : Set Ω) [Decidable (ω ∈ t)] :
      (ProbabilityTheory.uniformOn {ω}) t = if ω ∈ t then 1 else 0

      Alias of ProbabilityTheory.uniformOn_singleton.

      source
      theorem ProbabilityTheory.uniformOn_inter_self {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s t : Set Ω} (hs : s.Finite) :
      (ProbabilityTheory.uniformOn s) (s ∩ t) = (ProbabilityTheory.uniformOn s) t
      source
      @[deprecated ProbabilityTheory.uniformOn_inter_self]
      theorem ProbabilityTheory.condCount_inter_self {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s t : Set Ω} (hs : s.Finite) :
      (ProbabilityTheory.uniformOn s) (s ∩ t) = (ProbabilityTheory.uniformOn s) t

      Alias of ProbabilityTheory.uniformOn_inter_self.

      source
      theorem ProbabilityTheory.uniformOn_self {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s : Set Ω} (hs : s.Finite) (hs' : s.Nonempty) :
      (ProbabilityTheory.uniformOn s) s = 1
      source
      @[deprecated ProbabilityTheory.uniformOn_self]
      theorem ProbabilityTheory.condCount_self {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s : Set Ω} (hs : s.Finite) (hs' : s.Nonempty) :
      (ProbabilityTheory.uniformOn s) s = 1

      Alias of ProbabilityTheory.uniformOn_self.

      source
      theorem ProbabilityTheory.uniformOn_eq_one_of {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s t : Set Ω} (hs : s.Finite) (hs' : s.Nonempty) (ht : s ⊆ t) :
      (ProbabilityTheory.uniformOn s) t = 1
      source
      @[deprecated ProbabilityTheory.uniformOn_eq_one_of]
      theorem ProbabilityTheory.condCount_eq_one_of {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s t : Set Ω} (hs : s.Finite) (hs' : s.Nonempty) (ht : s ⊆ t) :
      (ProbabilityTheory.uniformOn s) t = 1

      Alias of ProbabilityTheory.uniformOn_eq_one_of.

      source
      theorem ProbabilityTheory.pred_true_of_uniformOn_eq_one {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s t : Set Ω} (h : (ProbabilityTheory.uniformOn s) t = 1) :
      s ⊆ t
      source
      @[deprecated ProbabilityTheory.pred_true_of_uniformOn_eq_one]
      theorem ProbabilityTheory.pred_true_of_condCount_eq_one {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s t : Set Ω} (h : (ProbabilityTheory.uniformOn s) t = 1) :
      s ⊆ t

      Alias of ProbabilityTheory.pred_true_of_uniformOn_eq_one.

      source
      theorem ProbabilityTheory.uniformOn_eq_zero_iff {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s t : Set Ω} (hs : s.Finite) :
      (ProbabilityTheory.uniformOn s) t = 0 ↔ s ∩ t = ∅
      source
      @[deprecated ProbabilityTheory.uniformOn_eq_zero_iff]
      theorem ProbabilityTheory.condCount_eq_zero_iff {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s t : Set Ω} (hs : s.Finite) :
      (ProbabilityTheory.uniformOn s) t = 0 ↔ s ∩ t = ∅

      Alias of ProbabilityTheory.uniformOn_eq_zero_iff.

      source
      theorem ProbabilityTheory.uniformOn_of_univ {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s : Set Ω} (hs : s.Finite) (hs' : s.Nonempty) :
      (ProbabilityTheory.uniformOn s) Set.univ = 1
      source
      @[deprecated ProbabilityTheory.uniformOn_of_univ]
      theorem ProbabilityTheory.condCount_of_univ {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s : Set Ω} (hs : s.Finite) (hs' : s.Nonempty) :
      (ProbabilityTheory.uniformOn s) Set.univ = 1

      Alias of ProbabilityTheory.uniformOn_of_univ.

      source
      theorem ProbabilityTheory.uniformOn_inter {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s t u : Set Ω} (hs : s.Finite) :
      (ProbabilityTheory.uniformOn s) (t ∩ u) = (ProbabilityTheory.uniformOn (s ∩ t)) u * (ProbabilityTheory.uniformOn s) t
      source
      @[deprecated ProbabilityTheory.uniformOn_inter]
      theorem ProbabilityTheory.condCount_inter {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s t u : Set Ω} (hs : s.Finite) :
      (ProbabilityTheory.uniformOn s) (t ∩ u) = (ProbabilityTheory.uniformOn (s ∩ t)) u * (ProbabilityTheory.uniformOn s) t

      Alias of ProbabilityTheory.uniformOn_inter.

      source
      theorem ProbabilityTheory.uniformOn_inter' {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s t u : Set Ω} (hs : s.Finite) :
      (ProbabilityTheory.uniformOn s) (t ∩ u) = (ProbabilityTheory.uniformOn (s ∩ u)) t * (ProbabilityTheory.uniformOn s) u
      source
      @[deprecated ProbabilityTheory.uniformOn_inter']
      theorem ProbabilityTheory.condCount_inter' {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s t u : Set Ω} (hs : s.Finite) :
      (ProbabilityTheory.uniformOn s) (t ∩ u) = (ProbabilityTheory.uniformOn (s ∩ u)) t * (ProbabilityTheory.uniformOn s) u

      Alias of ProbabilityTheory.uniformOn_inter'.

      source
      theorem ProbabilityTheory.uniformOn_union {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s t u : Set Ω} (hs : s.Finite) (htu : Disjoint t u) :
      (ProbabilityTheory.uniformOn s) (t ∪ u) = (ProbabilityTheory.uniformOn s) t + (ProbabilityTheory.uniformOn s) u
      source
      @[deprecated ProbabilityTheory.uniformOn_union]
      theorem ProbabilityTheory.condCount_union {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s t u : Set Ω} (hs : s.Finite) (htu : Disjoint t u) :
      (ProbabilityTheory.uniformOn s) (t ∪ u) = (ProbabilityTheory.uniformOn s) t + (ProbabilityTheory.uniformOn s) u

      Alias of ProbabilityTheory.uniformOn_union.

      source
      theorem ProbabilityTheory.uniformOn_compl {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s : Set Ω} (t : Set Ω) (hs : s.Finite) (hs' : s.Nonempty) :
      (ProbabilityTheory.uniformOn s) t + (ProbabilityTheory.uniformOn s) tᶜ = 1
      source
      @[deprecated ProbabilityTheory.uniformOn_compl]
      theorem ProbabilityTheory.condCount_compl {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s : Set Ω} (t : Set Ω) (hs : s.Finite) (hs' : s.Nonempty) :
      (ProbabilityTheory.uniformOn s) t + (ProbabilityTheory.uniformOn s) tᶜ = 1

      Alias of ProbabilityTheory.uniformOn_compl.

      source
      theorem ProbabilityTheory.uniformOn_disjoint_union {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s t u : Set Ω} (hs : s.Finite) (ht : t.Finite) (hst : Disjoint s t) :
      (ProbabilityTheory.uniformOn s) u * (ProbabilityTheory.uniformOn (s ∪ t)) s + (ProbabilityTheory.uniformOn t) u * (ProbabilityTheory.uniformOn (s ∪ t)) t = (ProbabilityTheory.uniformOn (s ∪ t)) u
      source
      @[deprecated ProbabilityTheory.uniformOn_disjoint_union]
      theorem ProbabilityTheory.condCount_disjoint_union {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s t u : Set Ω} (hs : s.Finite) (ht : t.Finite) (hst : Disjoint s t) :
      (ProbabilityTheory.uniformOn s) u * (ProbabilityTheory.uniformOn (s ∪ t)) s + (ProbabilityTheory.uniformOn t) u * (ProbabilityTheory.uniformOn (s ∪ t)) t = (ProbabilityTheory.uniformOn (s ∪ t)) u

      Alias of ProbabilityTheory.uniformOn_disjoint_union.

      source
      theorem ProbabilityTheory.uniformOn_add_compl_eq {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s : Set Ω} (u t : Set Ω) (hs : s.Finite) :
      (ProbabilityTheory.uniformOn (s ∩ u)) t * (ProbabilityTheory.uniformOn s) u + (ProbabilityTheory.uniformOn (s ∩ uᶜ)) t * (ProbabilityTheory.uniformOn s) uᶜ = (ProbabilityTheory.uniformOn s) t

      A version of the law of total probability for counting probabilities.

      source
      @[deprecated ProbabilityTheory.uniformOn_add_compl_eq]
      theorem ProbabilityTheory.condCount_add_compl_eq {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s : Set Ω} (u t : Set Ω) (hs : s.Finite) :
      (ProbabilityTheory.uniformOn (s ∩ u)) t * (ProbabilityTheory.uniformOn s) u + (ProbabilityTheory.uniformOn (s ∩ uᶜ)) t * (ProbabilityTheory.uniformOn s) uᶜ = (ProbabilityTheory.uniformOn s) t

      Alias of ProbabilityTheory.uniformOn_add_compl_eq.

      A version of the law of total probability for counting probabilities.