chore : fix camelcase naming of PDF, CDF and PMF (#9681)

Replaces occurences of Pdf, Cdf and Pmf within camelCase situations by PDF, CDF and PMF respectively.

Mathlib/Probability/Cdf.lean

@@ -15,11 +15,11 @@ Two probability measures are equal if and only if they have the same cdf.
 ## Main definitions
 
 * `ProbabilityTheory.cdf μ`: cumulative distribution function of `μ : Measure ℝ`, defined as the
-  conditional cdf (`ProbabilityTheory.condCdf`) of the product measure
+  conditional cdf (`ProbabilityTheory.condCDF`) of the product measure
   `(Measure.dirac Unit.unit).prod μ` evaluated at `Unit.unit`.
 
 The definition could be replaced by the more elementary `cdf μ x = (μ (Iic x)).toReal`, but using
-`condCdf` gives us access to its API, from which most properties of the cdf follow directly.
+`condCDF` gives us access to its API, from which most properties of the cdf follow directly.
 
 ## Main statements
 
@@ -30,11 +30,11 @@ The definition could be replaced by the more elementary `cdf μ x = (μ (Iic x))
 
 ## TODO
 
-The definition could be extended to a finite measure by rescaling `condCdf`, but it would be nice
+The definition could be extended to a finite measure by rescaling `condCDF`, but it would be nice
 to have more structure on Stieltjes functions first. Right now, if `f` is a Stieltjes function,
 `2 • f` makes no sense. We could define Stieltjes functions as a submodule.
 
-The definition could be extended to `ℝⁿ`, either by extending the definition of `condCdf`, or by
+The definition could be extended to `ℝⁿ`, either by extending the definition of `condCDF`, or by
 using another construction here.
 -/
 
@@ -49,29 +49,29 @@ for probability measures. In that case, it satisfies `cdf μ x = (μ (Iic x)).to
 `ProbabilityTheory.cdf_eq_toReal`). -/
 noncomputable
 def cdf (μ : Measure ℝ) : StieltjesFunction :=
-  condCdf ((Measure.dirac Unit.unit).prod μ) Unit.unit
+  condCDF ((Measure.dirac Unit.unit).prod μ) Unit.unit
 
 section ExplicitMeasureArg
 variable (μ : Measure ℝ)
 
 /-- The cdf is non-negative. -/
-lemma cdf_nonneg (x : ℝ) : 0 ≤ cdf μ x := condCdf_nonneg _ _ _
+lemma cdf_nonneg (x : ℝ) : 0 ≤ cdf μ x := condCDF_nonneg _ _ _
 
 /-- The cdf is lower or equal to 1. -/
-lemma cdf_le_one (x : ℝ) : cdf μ x ≤ 1 := condCdf_le_one _ _ _
+lemma cdf_le_one (x : ℝ) : cdf μ x ≤ 1 := condCDF_le_one _ _ _
 
 /-- The cdf is monotone. -/
-lemma monotone_cdf : Monotone (cdf μ) := (condCdf _ _).mono
+lemma monotone_cdf : Monotone (cdf μ) := (condCDF _ _).mono
 
 /-- The cdf tends to 0 at -∞. -/
-lemma tendsto_cdf_atBot : Tendsto (cdf μ) atBot (𝓝 0) := tendsto_condCdf_atBot _ _
+lemma tendsto_cdf_atBot : Tendsto (cdf μ) atBot (𝓝 0) := tendsto_condCDF_atBot _ _
 
 /-- The cdf tends to 1 at +∞. -/
-lemma tendsto_cdf_atTop : Tendsto (cdf μ) atTop (𝓝 1) := tendsto_condCdf_atTop _ _
+lemma tendsto_cdf_atTop : Tendsto (cdf μ) atTop (𝓝 1) := tendsto_condCDF_atTop _ _
 
 lemma ofReal_cdf [IsProbabilityMeasure μ] (x : ℝ) : ENNReal.ofReal (cdf μ x) = μ (Iic x) := by
   have := IsProbabilityMeasure.toIsFiniteMeasure (Measure.prod (Measure.dirac ()) μ)
-  have h := lintegral_condCdf ((Measure.dirac Unit.unit).prod μ) x
+  have h := lintegral_condCDF ((Measure.dirac Unit.unit).prod μ) x
   simpa only [MeasureTheory.Measure.fst_prod, Measure.prod_prod, measure_univ, one_mul,
     lintegral_dirac] using h
 

Mathlib/Probability/Distributions/Exponential.lean

@@ -14,17 +14,17 @@ import Mathlib.Probability.Distributions.Gamma
 Define the Exponential measure over the reals.
 
 ## Main definitions
-* `exponentialPdfReal`: the function `r x ↦ r * exp (-(r * x)` for `0 ≤ x`
+* `exponentialPDFReal`: the function `r x ↦ r * exp (-(r * x)` for `0 ≤ x`
   or `0` else, which is the probability density function of a exponential distribution with
   rate `r` (when `hr : 0 < r`).
-* `exponentialPdf`: `ℝ≥0∞`-valued pdf,
-  `exponentialPdf r = ENNReal.ofReal (exponentialPdfReal r)`.
+* `exponentialPDF`: `ℝ≥0∞`-valued pdf,
+  `exponentialPDF r = ENNReal.ofReal (exponentialPDFReal r)`.
 * `expMeasure`: an exponential measure on `ℝ`, parametrized by its rate `r`.
-* `exponentialCdfReal`: the Cdf given by the definition of CDF in `ProbabilityTheory.Cdf` applied to
+* `exponentialCDFReal`: the CDF given by the definition of CDF in `ProbabilityTheory.CDF` applied to
   the exponential measure.
 
 ## Main results
-* `exponentialCdfReal_eq`: Proof that the `exponentialCdfReal` given by the definition equals the
+* `exponentialCDFReal_eq`: Proof that the `exponentialCDFReal` given by the definition equals the
   known function given as `r x ↦ 1 - exp (- (r * x))` for `0 ≤ x` or `0` else.
 -/
 
@@ -34,59 +34,59 @@ open MeasureTheory Real Set Filter Topology
 
 namespace ProbabilityTheory
 
-section ExponentialPdf
+section ExponentialPDF
 
 /-- The pdf of the exponential distribution depending on its rate -/
 noncomputable
-def exponentialPdfReal (r x : ℝ) : ℝ :=
-  gammaPdfReal 1 r x
+def exponentialPDFReal (r x : ℝ) : ℝ :=
+  gammaPDFReal 1 r x
 
 /-- The pdf of the exponential distribution, as a function valued in `ℝ≥0∞` -/
 noncomputable
-def exponentialPdf (r x : ℝ) : ℝ≥0∞ :=
-  ENNReal.ofReal (exponentialPdfReal r x)
+def exponentialPDF (r x : ℝ) : ℝ≥0∞ :=
+  ENNReal.ofReal (exponentialPDFReal r x)
 
-lemma exponentialPdf_eq (r x : ℝ) :
-    exponentialPdf r x = ENNReal.ofReal (if 0 ≤ x then r * exp (-(r * x)) else 0) := by
-  rw [exponentialPdf, exponentialPdfReal, gammaPdfReal]
+lemma exponentialPDF_eq (r x : ℝ) :
+    exponentialPDF r x = ENNReal.ofReal (if 0 ≤ x then r * exp (-(r * x)) else 0) := by
+  rw [exponentialPDF, exponentialPDFReal, gammaPDFReal]
   simp only [rpow_one, Gamma_one, div_one, sub_self, rpow_zero, mul_one]
 
-lemma exponentialPdf_of_neg {r x : ℝ} (hx : x < 0) : exponentialPdf r x = 0 := gammaPdf_of_neg hx
+lemma exponentialPDF_of_neg {r x : ℝ} (hx : x < 0) : exponentialPDF r x = 0 := gammaPDF_of_neg hx
 
-lemma exponentialPdf_of_nonneg {r x : ℝ} (hx : 0 ≤ x) :
-    exponentialPdf r x = ENNReal.ofReal (r * rexp (-(r * x))) := by
-  simp only [exponentialPdf_eq, if_pos hx]
+lemma exponentialPDF_of_nonneg {r x : ℝ} (hx : 0 ≤ x) :
+    exponentialPDF r x = ENNReal.ofReal (r * rexp (-(r * x))) := by
+  simp only [exponentialPDF_eq, if_pos hx]
 
 /-- The Lebesgue integral of the exponential pdf over nonpositive reals equals 0-/
-lemma lintegral_exponentialPdf_of_nonpos {x r : ℝ} (hx : x ≤ 0) :
-    ∫⁻ y in Iio x, exponentialPdf r y = 0 := lintegral_gammaPdf_of_nonpos hx
+lemma lintegral_exponentialPDF_of_nonpos {x r : ℝ} (hx : x ≤ 0) :
+    ∫⁻ y in Iio x, exponentialPDF r y = 0 := lintegral_gammaPDF_of_nonpos hx
 
 /-- The exponential pdf is measurable. -/
 @[measurability]
-lemma measurable_exponentialPdfReal (r : ℝ) : Measurable (exponentialPdfReal r) :=
-  measurable_gammaPdfReal 1 r
+lemma measurable_exponentialPDFReal (r : ℝ) : Measurable (exponentialPDFReal r) :=
+  measurable_gammaPDFReal 1 r
 
 -- The exponential pdf is strongly measurable -/
 @[measurability]
- lemma stronglyMeasurable_exponentialPdfReal (r : ℝ) :
-     StronglyMeasurable (exponentialPdfReal r) := stronglyMeasurable_gammaPdfReal 1 r
+ lemma stronglyMeasurable_exponentialPDFReal (r : ℝ) :
+     StronglyMeasurable (exponentialPDFReal r) := stronglyMeasurable_gammaPDFReal 1 r
 
 /-- The exponential pdf is positive for all positive reals -/
-lemma exponentialPdfReal_pos {x r : ℝ} (hr : 0 < r) (hx : 0 < x) :
-    0 < exponentialPdfReal r x := gammaPdfReal_pos zero_lt_one hr hx
+lemma exponentialPDFReal_pos {x r : ℝ} (hr : 0 < r) (hx : 0 < x) :
+    0 < exponentialPDFReal r x := gammaPDFReal_pos zero_lt_one hr hx
 
 /-- The exponential pdf is nonnegative-/
-lemma exponentialPdfReal_nonneg {r : ℝ} (hr : 0 < r) (x : ℝ) :
-    0 ≤ exponentialPdfReal r x := gammaPdfReal_nonneg zero_lt_one hr x
+lemma exponentialPDFReal_nonneg {r : ℝ} (hr : 0 < r) (x : ℝ) :
+    0 ≤ exponentialPDFReal r x := gammaPDFReal_nonneg zero_lt_one hr x
 
 open Measure
 
 /-- The pdf of the exponential distribution integrates to 1 -/
 @[simp]
-lemma lintegral_exponentialPdf_eq_one {r : ℝ} (hr : 0 < r) : ∫⁻ x, exponentialPdf r x = 1 :=
-  lintegral_gammaPdf_eq_one zero_lt_one hr
+lemma lintegral_exponentialPDF_eq_one {r : ℝ} (hr : 0 < r) : ∫⁻ x, exponentialPDF r x = 1 :=
+  lintegral_gammaPDF_eq_one zero_lt_one hr
 
-end ExponentialPdf
+end ExponentialPDF
 
 open MeasureTheory
 
@@ -97,20 +97,20 @@ def expMeasure (r : ℝ) : Measure ℝ := gammaMeasure 1 r
 lemma isProbabilityMeasureExponential {r : ℝ} (hr : 0 < r) :
     IsProbabilityMeasure (expMeasure r) := isProbabilityMeasureGamma zero_lt_one hr
 
-section ExponentialCdf
+section ExponentialCDF
 
 /-- CDF of the exponential distribution -/
 noncomputable
-def exponentialCdfReal (r : ℝ) : StieltjesFunction :=
+def exponentialCDFReal (r : ℝ) : StieltjesFunction :=
   cdf (expMeasure r)
 
-lemma exponentialCdfReal_eq_integral {r : ℝ} (hr : 0 < r) (x : ℝ) :
-    exponentialCdfReal r x = ∫ x in Iic x, exponentialPdfReal r x :=
-  gammaCdfReal_eq_integral zero_lt_one hr x
+lemma exponentialCDFReal_eq_integral {r : ℝ} (hr : 0 < r) (x : ℝ) :
+    exponentialCDFReal r x = ∫ x in Iic x, exponentialPDFReal r x :=
+  gammaCDFReal_eq_integral zero_lt_one hr x
 
-lemma exponentialCdfReal_eq_lintegral {r : ℝ} (hr : 0 < r) (x : ℝ) :
-    exponentialCdfReal r x = ENNReal.toReal (∫⁻ x in Iic x, exponentialPdf r x) :=
-  gammaCdfReal_eq_lintegral zero_lt_one hr x
+lemma exponentialCDFReal_eq_lintegral {r : ℝ} (hr : 0 < r) (x : ℝ) :
+    exponentialCDFReal r x = ENNReal.toReal (∫⁻ x in Iic x, exponentialPDF r x) :=
+  gammaCDFReal_eq_lintegral zero_lt_one hr x
 
 open Topology
 
@@ -126,18 +126,18 @@ lemma exp_neg_integrableOn_Ioc {b x : ℝ} (hb : 0 < b) :
   simp only [neg_mul_eq_neg_mul]
   exact (exp_neg_integrableOn_Ioi _ hb).mono_set Ioc_subset_Ioi_self
 
-lemma lintegral_exponentialPdf_eq_antiDeriv {r : ℝ} (hr : 0 < r) (x : ℝ) :
-    ∫⁻ y in Iic x, exponentialPdf r y
+lemma lintegral_exponentialPDF_eq_antiDeriv {r : ℝ} (hr : 0 < r) (x : ℝ) :
+    ∫⁻ y in Iic x, exponentialPDF r y
     = ENNReal.ofReal (if 0 ≤ x then 1 - exp (-(r * x)) else 0) := by
   split_ifs with h
   case neg =>
-    simp only [exponentialPdf_eq]
+    simp only [exponentialPDF_eq]
     rw [set_lintegral_congr_fun measurableSet_Iic, lintegral_zero, ENNReal.ofReal_zero]
     exact ae_of_all _ fun a (_ : a ≤ _) ↦ by rw [if_neg (by linarith), ENNReal.ofReal_eq_zero]
   case pos =>
-    rw [lintegral_Iic_eq_lintegral_Iio_add_Icc _ h, lintegral_exponentialPdf_of_nonpos (le_refl 0),
+    rw [lintegral_Iic_eq_lintegral_Iio_add_Icc _ h, lintegral_exponentialPDF_of_nonpos (le_refl 0),
       zero_add]
-    simp only [exponentialPdf_eq]
+    simp only [exponentialPDF_eq]
     rw [set_lintegral_congr_fun measurableSet_Icc (ae_of_all _
         (by intro a ⟨(hle : _ ≤ a), _⟩; rw [if_pos hle]))]
     rw [← ENNReal.toReal_eq_toReal _ ENNReal.ofReal_ne_top, ← integral_eq_lintegral_of_nonneg_ae
@@ -164,13 +164,13 @@ lemma lintegral_exponentialPdf_eq_antiDeriv {r : ℝ} (hr : 0 < r) (x : ℝ) :
       exact Integrable.const_mul (exp_neg_integrableOn_Ioc hr) _
 
 /-- The CDF of the exponential distribution equals ``1 - exp (-(r * x))``-/
-lemma exponentialCdfReal_eq {r : ℝ} (hr : 0 < r) (x : ℝ) :
-    exponentialCdfReal r x = if 0 ≤ x then 1 - exp (-(r * x)) else 0 := by
-  rw [exponentialCdfReal_eq_lintegral hr, lintegral_exponentialPdf_eq_antiDeriv hr x,
+lemma exponentialCDFReal_eq {r : ℝ} (hr : 0 < r) (x : ℝ) :
+    exponentialCDFReal r x = if 0 ≤ x then 1 - exp (-(r * x)) else 0 := by
+  rw [exponentialCDFReal_eq_lintegral hr, lintegral_exponentialPDF_eq_antiDeriv hr x,
     ENNReal.toReal_ofReal_eq_iff]
   split_ifs with h
   · simp only [sub_nonneg, exp_le_one_iff, Left.neg_nonpos_iff, gt_iff_lt, ge_iff_le]
     exact mul_nonneg hr.le h
   · exact le_rfl
 
-end ExponentialCdf
+end ExponentialCDF