chore(Probability): rename Pmf to PMF (#7542)

Search and replace `Pmf` with `PMF`.

Mathlib/Probability/ProbabilityMassFunction/Binomial.lean

@@ -14,17 +14,17 @@ This file defines the probability mass function of the binomial distribution.
 
 ## Main results
 
-* `binomial_one_eq_bernoulli`: For `n = 1`, it is equal to `Pmf.bernoulli`.
+* `binomial_one_eq_bernoulli`: For `n = 1`, it is equal to `PMF.bernoulli`.
 -/
 
-namespace Pmf
+namespace PMF
 
 open ENNReal
 
-/-- The binomial `Pmf`: the probability of observing exactly `i` “heads” in a sequence of `n`
+/-- The binomial `PMF`: the probability of observing exactly `i` “heads” in a sequence of `n`
 independent coin tosses, each having probability `p` of coming up “heads”. -/
 noncomputable
-def binomial (p : ℝ≥0∞) (h : p ≤ 1) (n : ℕ) : Pmf (Fin (n + 1)) :=
+def binomial (p : ℝ≥0∞) (h : p ≤ 1) (n : ℕ) : PMF (Fin (n + 1)) :=
   .ofFintype (fun i => p^(i : ℕ) * (1-p)^((Fin.last n - i) : ℕ) * (n.choose i : ℕ)) (by
     convert (add_pow p (1-p) n).symm
     · rw [Finset.sum_fin_eq_sum_range]
@@ -52,4 +52,4 @@ theorem binomial_one_eq_bernoulli (p : ℝ≥0∞) (h : p ≤ 1) :
     binomial p h 1 = (bernoulli p h).map (cond · 1 0) := by
   ext i; fin_cases i <;> simp [tsum_bool, binomial_apply]
 
-end Pmf
+end PMF

Mathlib/Probability/ProbabilityMassFunction/Integrals.lean

@@ -10,13 +10,13 @@ import Mathlib.MeasureTheory.Integral.Bochner
 /-!
 # Integrals with a measure derived from probability mass functions.
 
-This files connects `Pmf` with `integral`. The main result is that the integral (i.e. the expected
-value) with regard to a measure derived from a `Pmf` is a sum weighted by the `Pmf`.
+This files connects `PMF` with `integral`. The main result is that the integral (i.e. the expected
+value) with regard to a measure derived from a `PMF` is a sum weighted by the `PMF`.
 
 It also provides the expected value for specific probability mass functions.
 -/
 
-namespace Pmf
+namespace PMF
 
 open MeasureTheory BigOperators ENNReal TopologicalSpace
 
@@ -25,26 +25,26 @@ section General
 variable {α : Type _} [MeasurableSpace α] [MeasurableSingletonClass α]
 variable {E : Type _} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
 
-theorem integral_eq_tsum (p : Pmf α) (f : α → E) (hf : Integrable f p.toMeasure) :
+theorem integral_eq_tsum (p : PMF α) (f : α → E) (hf : Integrable f p.toMeasure) :
     ∫ a, f a ∂(p.toMeasure) = ∑' a, (p a).toReal • f a := calc
   _ = ∫ a in p.support, f a ∂(p.toMeasure) := by rw [restrict_toMeasure_support p]
   _ = ∑' (a : support p), (p.toMeasure {a.val}).toReal • f a := by
     apply integral_countable f p.support_countable
     rwa [restrict_toMeasure_support p]
   _ = ∑' (a : support p), (p a).toReal • f a := by
     congr with x; congr
-    apply Pmf.toMeasure_apply_singleton p x (MeasurableSet.singleton _)
+    apply PMF.toMeasure_apply_singleton p x (MeasurableSet.singleton _)
   _ = ∑' a, (p a).toReal • f a :=
     tsum_subtype_eq_of_support_subset $ by calc
       (fun a ↦ (p a).toReal • f a).support ⊆ (fun a ↦ (p a).toReal).support :=
         Function.support_smul_subset_left _ _
       _ ⊆ support p := fun x h1 h2 => h1 (by simp [h2])
 
-theorem integral_eq_sum [Fintype α] (p : Pmf α) (f : α → E) :
+theorem integral_eq_sum [Fintype α] (p : PMF α) (f : α → E) :
     ∫ a, f a ∂(p.toMeasure) = ∑ a, (p a).toReal • f a := by
   rw [integral_fintype _ (integrable_of_fintype _ f)]
   congr with x; congr
-  exact Pmf.toMeasure_apply_singleton p x (MeasurableSet.singleton _)
+  exact PMF.toMeasure_apply_singleton p x (MeasurableSet.singleton _)
 
 end General