Commit 2024-01-16 10:45 bc6f44c3

View on Github →

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.

Estimated changes

Modified Mathlib/Probability/Cdf.lean

modified theorem ProbabilityTheory.cdf_le_one

modified theorem ProbabilityTheory.cdf_nonneg

modified theorem ProbabilityTheory.monotone_cdf

modified theorem ProbabilityTheory.tendsto_cdf_atBot

modified theorem ProbabilityTheory.tendsto_cdf_atTop

Modified Mathlib/Probability/Distributions/Exponential.lean

added def ProbabilityTheory.exponentialCDFReal

added theorem ProbabilityTheory.exponentialCDFReal_eq

added theorem ProbabilityTheory.exponentialCDFReal_eq_integral

added theorem ProbabilityTheory.exponentialCDFReal_eq_lintegral

deleted def ProbabilityTheory.exponentialCdfReal

deleted theorem ProbabilityTheory.exponentialCdfReal_eq

deleted theorem ProbabilityTheory.exponentialCdfReal_eq_integral

deleted theorem ProbabilityTheory.exponentialCdfReal_eq_lintegral

added def ProbabilityTheory.exponentialPDF

added def ProbabilityTheory.exponentialPDFReal

added theorem ProbabilityTheory.exponentialPDFReal_nonneg

added theorem ProbabilityTheory.exponentialPDFReal_pos

added theorem ProbabilityTheory.exponentialPDF_eq

added theorem ProbabilityTheory.exponentialPDF_of_neg

added theorem ProbabilityTheory.exponentialPDF_of_nonneg

deleted def ProbabilityTheory.exponentialPdf

deleted def ProbabilityTheory.exponentialPdfReal

deleted theorem ProbabilityTheory.exponentialPdfReal_nonneg

deleted theorem ProbabilityTheory.exponentialPdfReal_pos

deleted theorem ProbabilityTheory.exponentialPdf_eq

deleted theorem ProbabilityTheory.exponentialPdf_of_neg

deleted theorem ProbabilityTheory.exponentialPdf_of_nonneg

added theorem ProbabilityTheory.lintegral_exponentialPDF_eq_antiDeriv

added theorem ProbabilityTheory.lintegral_exponentialPDF_eq_one

added theorem ProbabilityTheory.lintegral_exponentialPDF_of_nonpos

deleted theorem ProbabilityTheory.lintegral_exponentialPdf_eq_antiDeriv

deleted theorem ProbabilityTheory.lintegral_exponentialPdf_eq_one

deleted theorem ProbabilityTheory.lintegral_exponentialPdf_of_nonpos

added theorem ProbabilityTheory.measurable_exponentialPDFReal

deleted theorem ProbabilityTheory.measurable_exponentialPdfReal

added theorem ProbabilityTheory.stronglyMeasurable_exponentialPDFReal

deleted theorem ProbabilityTheory.stronglyMeasurable_exponentialPdfReal

Modified Mathlib/Probability/Distributions/Gamma.lean

added def ProbabilityTheory.gammaCDFReal

added theorem ProbabilityTheory.gammaCDFReal_eq_integral

added theorem ProbabilityTheory.gammaCDFReal_eq_lintegral

deleted def ProbabilityTheory.gammaCdfReal

deleted theorem ProbabilityTheory.gammaCdfReal_eq_integral

deleted theorem ProbabilityTheory.gammaCdfReal_eq_lintegral

added def ProbabilityTheory.gammaPDF

added def ProbabilityTheory.gammaPDFReal

added theorem ProbabilityTheory.gammaPDFReal_nonneg

added theorem ProbabilityTheory.gammaPDFReal_pos

added theorem ProbabilityTheory.gammaPDF_eq

added theorem ProbabilityTheory.gammaPDF_of_neg

added theorem ProbabilityTheory.gammaPDF_of_nonneg

deleted def ProbabilityTheory.gammaPdf

deleted def ProbabilityTheory.gammaPdfReal

deleted theorem ProbabilityTheory.gammaPdfReal_nonneg

deleted theorem ProbabilityTheory.gammaPdfReal_pos

deleted theorem ProbabilityTheory.gammaPdf_eq

deleted theorem ProbabilityTheory.gammaPdf_of_neg

deleted theorem ProbabilityTheory.gammaPdf_of_nonneg

added theorem ProbabilityTheory.lintegral_gammaPDF_eq_one

added theorem ProbabilityTheory.lintegral_gammaPDF_of_nonpos

deleted theorem ProbabilityTheory.lintegral_gammaPdf_eq_one

deleted theorem ProbabilityTheory.lintegral_gammaPdf_of_nonpos

added theorem ProbabilityTheory.measurable_gammaPDFReal

deleted theorem ProbabilityTheory.measurable_gammaPdfReal

added theorem ProbabilityTheory.stronglyMeasurable_gammaPDFReal

deleted theorem ProbabilityTheory.stronglyMeasurable_gammaPdfReal

Modified Mathlib/Probability/Distributions/Gaussian.lean

added def ProbabilityTheory.gaussianPDF

added def ProbabilityTheory.gaussianPDFReal

added theorem ProbabilityTheory.gaussianPDFReal_add

added theorem ProbabilityTheory.gaussianPDFReal_def

added theorem ProbabilityTheory.gaussianPDFReal_inv_mul

added theorem ProbabilityTheory.gaussianPDFReal_mul

added theorem ProbabilityTheory.gaussianPDFReal_nonneg

added theorem ProbabilityTheory.gaussianPDFReal_pos

added theorem ProbabilityTheory.gaussianPDFReal_sub

added theorem ProbabilityTheory.gaussianPDFReal_zero_var

added theorem ProbabilityTheory.gaussianPDF_def

added theorem ProbabilityTheory.gaussianPDF_pos

added theorem ProbabilityTheory.gaussianPDF_zero_var

deleted def ProbabilityTheory.gaussianPdf

deleted def ProbabilityTheory.gaussianPdfReal

deleted theorem ProbabilityTheory.gaussianPdfReal_add

deleted theorem ProbabilityTheory.gaussianPdfReal_def

deleted theorem ProbabilityTheory.gaussianPdfReal_inv_mul

deleted theorem ProbabilityTheory.gaussianPdfReal_mul

deleted theorem ProbabilityTheory.gaussianPdfReal_nonneg

deleted theorem ProbabilityTheory.gaussianPdfReal_pos

deleted theorem ProbabilityTheory.gaussianPdfReal_sub

deleted theorem ProbabilityTheory.gaussianPdfReal_zero_var

deleted theorem ProbabilityTheory.gaussianPdf_def

deleted theorem ProbabilityTheory.gaussianPdf_pos

deleted theorem ProbabilityTheory.gaussianPdf_zero_var

added theorem ProbabilityTheory.integrable_gaussianPDFReal

deleted theorem ProbabilityTheory.integrable_gaussianPdfReal

added theorem ProbabilityTheory.integral_gaussianPDFReal_eq_one

deleted theorem ProbabilityTheory.integral_gaussianPdfReal_eq_one

added theorem ProbabilityTheory.lintegral_gaussianPDFReal_eq_one

added theorem ProbabilityTheory.lintegral_gaussianPDF_eq_one

deleted theorem ProbabilityTheory.lintegral_gaussianPdfReal_eq_one

deleted theorem ProbabilityTheory.lintegral_gaussianPdf_eq_one

added theorem ProbabilityTheory.measurable_gaussianPDF

added theorem ProbabilityTheory.measurable_gaussianPDFReal

deleted theorem ProbabilityTheory.measurable_gaussianPdf

deleted theorem ProbabilityTheory.measurable_gaussianPdfReal

added theorem ProbabilityTheory.stronglyMeasurable_gaussianPDFReal

deleted theorem ProbabilityTheory.stronglyMeasurable_gaussianPdfReal

Modified Mathlib/Probability/Distributions/Poisson.lean

added theorem ProbabilityTheory.measurable_poissonPMFReal

deleted theorem ProbabilityTheory.measurable_poissonPmfReal

modified def ProbabilityTheory.poissonMeasure

added def ProbabilityTheory.poissonPMF

added def ProbabilityTheory.poissonPMFReal

added theorem ProbabilityTheory.poissonPMFRealSum

added theorem ProbabilityTheory.poissonPMFReal_nonneg

added theorem ProbabilityTheory.poissonPMFReal_pos

deleted def ProbabilityTheory.poissonPmf

deleted def ProbabilityTheory.poissonPmfReal

deleted theorem ProbabilityTheory.poissonPmfRealSum

deleted theorem ProbabilityTheory.poissonPmfReal_nonneg

deleted theorem ProbabilityTheory.poissonPmfReal_pos

added theorem ProbabilityTheory.stronglyMeasurable_poissonPMFReal

deleted theorem ProbabilityTheory.stronglyMeasurable_poissonPmfReal

Modified Mathlib/Probability/Kernel/CondCdf.lean

added structure ProbabilityTheory.HasCondCDF

deleted structure ProbabilityTheory.HasCondCdf

added theorem ProbabilityTheory.bddBelow_range_condCDFRat_gt

deleted theorem ProbabilityTheory.bddBelow_range_condCdfRat_gt

added theorem ProbabilityTheory.condCDF'_def'

added theorem ProbabilityTheory.condCDF'_eq_condCDFRat

added theorem ProbabilityTheory.condCDF'_nonneg

added theorem ProbabilityTheory.condCDFRat_ae_eq

added theorem ProbabilityTheory.condCDFRat_le_one

added theorem ProbabilityTheory.condCDFRat_nonneg

added theorem ProbabilityTheory.condCDFRat_of_mem

added theorem ProbabilityTheory.condCDFRat_of_not_mem

added def ProbabilityTheory.condCDFSet

added theorem ProbabilityTheory.condCDF_ae_eq

added theorem ProbabilityTheory.condCDF_eq_condCDFRat

added theorem ProbabilityTheory.condCDF_le_one

added theorem ProbabilityTheory.condCDF_nonneg

deleted theorem ProbabilityTheory.condCdf'_def'

deleted theorem ProbabilityTheory.condCdf'_eq_condCdfRat

deleted theorem ProbabilityTheory.condCdf'_nonneg

deleted theorem ProbabilityTheory.condCdfRat_ae_eq

deleted theorem ProbabilityTheory.condCdfRat_le_one

deleted theorem ProbabilityTheory.condCdfRat_nonneg

deleted theorem ProbabilityTheory.condCdfRat_of_mem

deleted theorem ProbabilityTheory.condCdfRat_of_not_mem

deleted def ProbabilityTheory.condCdfSet

deleted theorem ProbabilityTheory.condCdf_ae_eq

deleted theorem ProbabilityTheory.condCdf_eq_condCdfRat

deleted theorem ProbabilityTheory.condCdf_le_one

deleted theorem ProbabilityTheory.condCdf_nonneg

added theorem ProbabilityTheory.continuousWithinAt_condCDF'_Ici

deleted theorem ProbabilityTheory.continuousWithinAt_condCdf'_Ici

added theorem ProbabilityTheory.hasCondCDF_ae

added theorem ProbabilityTheory.hasCondCDF_of_mem_condCDFSet

deleted theorem ProbabilityTheory.hasCondCdf_ae

deleted theorem ProbabilityTheory.hasCondCdf_of_mem_condCdfSet

added theorem ProbabilityTheory.inf_gt_condCDFRat

deleted theorem ProbabilityTheory.inf_gt_condCdfRat

added theorem ProbabilityTheory.inf_gt_preCDF

deleted theorem ProbabilityTheory.inf_gt_preCdf

added theorem ProbabilityTheory.integrable_condCDF

deleted theorem ProbabilityTheory.integrable_condCdf

added theorem ProbabilityTheory.integral_condCDF

deleted theorem ProbabilityTheory.integral_condCdf

added theorem ProbabilityTheory.lintegral_condCDF

deleted theorem ProbabilityTheory.lintegral_condCdf

added theorem ProbabilityTheory.measurableSet_condCDFSet

deleted theorem ProbabilityTheory.measurableSet_condCdfSet

added theorem ProbabilityTheory.measurable_condCDF

added theorem ProbabilityTheory.measurable_condCDFRat

deleted theorem ProbabilityTheory.measurable_condCdf

deleted theorem ProbabilityTheory.measurable_condCdfRat

added theorem ProbabilityTheory.measurable_measure_condCDF

deleted theorem ProbabilityTheory.measurable_measure_condCdf

added theorem ProbabilityTheory.measurable_preCDF

deleted theorem ProbabilityTheory.measurable_preCdf

added theorem ProbabilityTheory.measure_condCDF_Iic

added theorem ProbabilityTheory.measure_condCDF_univ

deleted theorem ProbabilityTheory.measure_condCdf_Iic

deleted theorem ProbabilityTheory.measure_condCdf_univ

added theorem ProbabilityTheory.mem_condCDFSet_ae

deleted theorem ProbabilityTheory.mem_condCdfSet_ae

added theorem ProbabilityTheory.monotone_condCDF'

added theorem ProbabilityTheory.monotone_condCDFRat

deleted theorem ProbabilityTheory.monotone_condCdf'

deleted theorem ProbabilityTheory.monotone_condCdfRat

added theorem ProbabilityTheory.monotone_preCDF

deleted theorem ProbabilityTheory.monotone_preCdf

added theorem ProbabilityTheory.ofReal_condCDFRat_ae_eq

added theorem ProbabilityTheory.ofReal_condCDF_ae_eq

deleted theorem ProbabilityTheory.ofReal_condCdfRat_ae_eq

deleted theorem ProbabilityTheory.ofReal_condCdf_ae_eq

added theorem ProbabilityTheory.preCDF_le_one

deleted theorem ProbabilityTheory.preCdf_le_one

added theorem ProbabilityTheory.set_integral_condCDF

deleted theorem ProbabilityTheory.set_integral_condCdf

added theorem ProbabilityTheory.set_lintegral_condCDF

added theorem ProbabilityTheory.set_lintegral_condCDF_rat

deleted theorem ProbabilityTheory.set_lintegral_condCdf

deleted theorem ProbabilityTheory.set_lintegral_condCdf_rat

added theorem ProbabilityTheory.set_lintegral_iInf_gt_preCDF

deleted theorem ProbabilityTheory.set_lintegral_iInf_gt_preCdf

added theorem ProbabilityTheory.set_lintegral_preCDF_fst

deleted theorem ProbabilityTheory.set_lintegral_preCdf_fst

added theorem ProbabilityTheory.stronglyMeasurable_condCDF

deleted theorem ProbabilityTheory.stronglyMeasurable_condCdf

added theorem ProbabilityTheory.tendsto_condCDFRat_atBot

added theorem ProbabilityTheory.tendsto_condCDFRat_atTop

added theorem ProbabilityTheory.tendsto_condCDF_atBot

added theorem ProbabilityTheory.tendsto_condCDF_atTop

deleted theorem ProbabilityTheory.tendsto_condCdfRat_atBot

deleted theorem ProbabilityTheory.tendsto_condCdfRat_atTop

deleted theorem ProbabilityTheory.tendsto_condCdf_atBot

deleted theorem ProbabilityTheory.tendsto_condCdf_atTop

added theorem ProbabilityTheory.tendsto_lintegral_preCDF_atBot

added theorem ProbabilityTheory.tendsto_lintegral_preCDF_atTop

deleted theorem ProbabilityTheory.tendsto_lintegral_preCdf_atBot

deleted theorem ProbabilityTheory.tendsto_lintegral_preCdf_atTop

added theorem ProbabilityTheory.tendsto_preCDF_atBot_zero

added theorem ProbabilityTheory.tendsto_preCDF_atTop_one

deleted theorem ProbabilityTheory.tendsto_preCdf_atBot_zero

deleted theorem ProbabilityTheory.tendsto_preCdf_atTop_one

added theorem ProbabilityTheory.withDensity_preCDF

deleted theorem ProbabilityTheory.withDensity_preCdf

Modified Mathlib/Probability/Kernel/Disintegration.lean