chore(probability/*): change to probability notation in the probabili…

…ty folder (#15933)


This PR makes two notational changes in the probability folder: `α` changed to `Ω` and `x` of type `α` to `ω`.

src/probability/cond_count.lean

@@ -40,31 +40,31 @@ open measure_theory measurable_space
 
 namespace probability_theory
 
-variables {α : Type*} [measurable_space α]
+variables {Ω : Type*} [measurable_space Ω]
 
 /-- Given a set `s`, `cond_count s` is the counting measure conditioned on `s`. In particular,
 `cond_count s t` is the proportion of `s` that is contained in `t`.
 
 This is a probability measure when `s` is finite and nonempty and is given by
 `probability_theory.cond_count_is_probability_measure`. -/
-def cond_count (s : set α) : measure α := measure.count[|s]
+def cond_count (s : set Ω) : measure Ω := measure.count[|s]
 
-@[simp] lemma cond_count_empty_meas : (cond_count ∅ : measure α) = 0 :=
+@[simp] lemma cond_count_empty_meas : (cond_count ∅ : measure Ω) = 0 :=
 by simp [cond_count]
 
-lemma cond_count_empty {s : set α} : cond_count s ∅ = 0 :=
+lemma cond_count_empty {s : set Ω} : cond_count s ∅ = 0 :=
 by simp
 
-lemma finite_of_cond_count_ne_zero {s t : set α} (h : cond_count s t ≠ 0) :
+lemma finite_of_cond_count_ne_zero {s t : set Ω} (h : cond_count s t ≠ 0) :
   s.finite :=
 begin
   by_contra hs',
   simpa [cond_count, cond, measure.count_apply_infinite hs'] using h,
 end
 
-variables [measurable_singleton_class α]
+variables [measurable_singleton_class Ω]
 
-lemma cond_count_is_probability_measure {s : set α} (hs : s.finite) (hs' : s.nonempty) :
+lemma cond_count_is_probability_measure {s : set Ω} (hs : s.finite) (hs' : s.nonempty) :
   is_probability_measure (cond_count s) :=
 { measure_univ :=
   begin
@@ -73,17 +73,17 @@ lemma cond_count_is_probability_measure {s : set α} (hs : s.finite) (hs' : s.no
     { exact (measure.count_apply_lt_top.2 hs).ne }
   end }
 
-lemma cond_count_singleton (a : α) (t : set α) [decidable (a ∈ t)] :
-  cond_count {a} t = if a ∈ t then 1 else 0 :=
+lemma cond_count_singleton (ω : Ω) (t : set Ω) [decidable (ω ∈ t)] :
+  cond_count {ω} t = if ω ∈ t then 1 else 0 :=
 begin
-  rw [cond_count, cond_apply _ (measurable_set_singleton a), measure.count_singleton,
+  rw [cond_count, cond_apply _ (measurable_set_singleton ω), measure.count_singleton,
     ennreal.inv_one, one_mul],
   split_ifs,
-  { rw [(by simpa : ({a} : set α) ∩ t = {a}), measure.count_singleton] },
-  { rw [(by simpa : ({a} : set α) ∩ t = ∅), measure.count_empty] },
+  { rw [(by simpa : ({ω} : set Ω) ∩ t = {ω}), measure.count_singleton] },
+  { rw [(by simpa : ({ω} : set Ω) ∩ t = ∅), measure.count_empty] },
 end
 
-variables {s t u : set α}
+variables {s t u : set Ω}
 
 lemma cond_count_inter_self (hs : s.finite):
   cond_count s (s ∩ t) = cond_count s t :=
@@ -159,7 +159,7 @@ begin
   exacts [htu.mono inf_le_right inf_le_right, (hs.inter_of_left _).measurable_set],
 end
 
-lemma cond_count_compl (t : set α) (hs : s.finite) (hs' : s.nonempty) :
+lemma cond_count_compl (t : set Ω) (hs : s.finite) (hs' : s.nonempty) :
   cond_count s t + cond_count s tᶜ = 1 :=
 begin
   rw [← cond_count_union hs disjoint_compl_right, set.union_compl_self,
@@ -190,7 +190,7 @@ begin
 end
 
 /-- A version of the law of total probability for counting probabilites. -/
-lemma cond_count_add_compl_eq (u t : set α) (hs : s.finite) :
+lemma cond_count_add_compl_eq (u t : set Ω) (hs : s.finite) :
   cond_count (s ∩ u) t * cond_count s u + cond_count (s ∩ uᶜ) t * cond_count s uᶜ =
   cond_count s t :=
 begin

src/probability/conditional_expectation.lean

@@ -27,8 +27,8 @@ namespace measure_theory
 
 open probability_theory
 
-variables {α E : Type*} [normed_add_comm_group E] [normed_space ℝ E] [complete_space E]
-  {m₁ m₂ m : measurable_space α} {μ : measure α} {f : α → E}
+variables {Ω E : Type*} [normed_add_comm_group E] [normed_space ℝ E] [complete_space E]
+  {m₁ m₂ m : measurable_space Ω} {μ : measure Ω} {f : Ω → E}
 
 /-- If `m₁, m₂` are independent σ-algebras and `f` is `m₁`-measurable, then `𝔼[f | m₂] = 𝔼[f]`
 almost everywhere. -/

src/probability/conditional_probability.lean

@@ -10,13 +10,13 @@ import probability.independence
 
 This file defines conditional probability and includes basic results relating to it.
 
-Given some measure `μ` defined on a measure space on some type `α` and some `s : set α`,
+Given some measure `μ` defined on a measure space on some type `Ω` and some `s : set Ω`,
 we define the measure of `μ` conditioned on `s` as the restricted measure scaled by
 the inverse of the measure of `s`: `cond μ s = (μ s)⁻¹ • μ.restrict s`. The scaling
 ensures that this is a probability measure (when `μ` is a finite measure).
 
 From this definition, we derive the "axiomatic" definition of conditional probability
-based on application: for any `s t : set α`, we have `μ[t|s] = (μ s)⁻¹ * μ (s ∩ t)`.
+based on application: for any `s t : set Ω`, we have `μ[t|s] = (μ s)⁻¹ * μ (s ∩ t)`.
 
 ## Main Statements
 
@@ -59,7 +59,7 @@ open_locale ennreal
 
 open measure_theory measurable_space
 
-variables {α : Type*} {m : measurable_space α} (μ : measure α) {s t : set α}
+variables {Ω : Type*} {m : measurable_space Ω} (μ : measure Ω) {s t : set Ω}
 
 namespace probability_theory
 
@@ -68,7 +68,7 @@ section definitions
 /-- The conditional probability measure of measure `μ` on set `s` is `μ` restricted to `s`
 and scaled by the inverse of `μ s` (to make it a probability measure):
 `(μ s)⁻¹ • μ.restrict s`. -/
-def cond (s : set α) : measure α :=
+def cond (s : set Ω) : measure Ω :=
   (μ s)⁻¹ • μ.restrict s
 
 end definitions
@@ -93,11 +93,11 @@ by simp [cond]
 by simp [cond, measure_univ, measure.restrict_univ]
 
 /-- The axiomatic definition of conditional probability derived from a measure-theoretic one. -/
-lemma cond_apply (hms : measurable_set s) (t : set α) :
+lemma cond_apply (hms : measurable_set s) (t : set Ω) :
   μ[t|s] = (μ s)⁻¹ * μ (s ∩ t) :=
 by { rw [cond, measure.smul_apply, measure.restrict_apply' hms, set.inter_comm], refl }
 
-lemma cond_inter_self (hms : measurable_set s) (t : set α) :
+lemma cond_inter_self (hms : measurable_set s) (t : set Ω) :
   μ[s ∩ t|s] = μ[t|s] :=
 by rw [cond_apply _ hms, ← set.inter_assoc, set.inter_self, ← cond_apply _ hms]
 
@@ -138,13 +138,13 @@ lemma cond_cond_eq_cond_inter [is_finite_measure μ]
 cond_cond_eq_cond_inter' μ hms hmt (measure_ne_top μ s) hci
 
 lemma cond_mul_eq_inter'
-  (hms : measurable_set s) (hcs : μ s ≠ 0) (hcs' : μ s ≠ ∞) (t : set α) :
+  (hms : measurable_set s) (hcs : μ s ≠ 0) (hcs' : μ s ≠ ∞) (t : set Ω) :
   μ[t|s] * μ s = μ (s ∩ t) :=
 by rw [cond_apply μ hms t, mul_comm, ←mul_assoc,
   ennreal.mul_inv_cancel hcs hcs', one_mul]
 
 lemma cond_mul_eq_inter [is_finite_measure μ]
-  (hms : measurable_set s) (hcs : μ s ≠ 0) (t : set α) :
+  (hms : measurable_set s) (hcs : μ s ≠ 0) (t : set Ω) :
   μ[t|s] * μ s = μ (s ∩ t) :=
 cond_mul_eq_inter' μ hms hcs (measure_ne_top _ s) t