Commit 2023-06-07 06:36 556d5fc3

View on Github →

feat: port MeasureTheory.Measure.ProbabilityMeasure (#4765)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean

added theorem MeasureTheory.FiniteMeasure.average_eq_integral_normalize

added def MeasureTheory.FiniteMeasure.normalize

added theorem MeasureTheory.FiniteMeasure.normalize_eq_inv_mass_smul_of_nonzero

added theorem MeasureTheory.FiniteMeasure.normalize_eq_of_nonzero

added theorem MeasureTheory.FiniteMeasure.normalize_testAgainstNN

added theorem MeasureTheory.FiniteMeasure.self_eq_mass_mul_normalize

added theorem MeasureTheory.FiniteMeasure.self_eq_mass_smul_normalize

added theorem MeasureTheory.FiniteMeasure.tendsto_normalize_iff_tendsto

added theorem MeasureTheory.FiniteMeasure.tendsto_normalize_of_tendsto

added theorem MeasureTheory.FiniteMeasure.tendsto_normalize_testAgainstNN_of_tendsto

added theorem MeasureTheory.FiniteMeasure.tendsto_of_tendsto_normalize_testAgainstNN_of_tendsto_mass

added theorem MeasureTheory.FiniteMeasure.tendsto_testAgainstNN_of_tendsto_normalize_testAgainstNN_of_tendsto_mass

added theorem MeasureTheory.FiniteMeasure.testAgainstNN_eq_mass_mul

added theorem MeasureTheory.FiniteMeasure.toMeasure_normalize_eq_of_nonzero

added theorem MeasureTheory.ProbabilityMeasure.apply_mono

added theorem MeasureTheory.ProbabilityMeasure.coeFn_comp_toFiniteMeasure_eq_coeFn

added theorem MeasureTheory.ProbabilityMeasure.coeFn_univ

added theorem MeasureTheory.ProbabilityMeasure.coeFn_univ_ne_zero

added theorem MeasureTheory.ProbabilityMeasure.coe_toWeakDualBCNN

added theorem MeasureTheory.ProbabilityMeasure.continuous_testAgainstNN_eval

added theorem MeasureTheory.ProbabilityMeasure.ennreal_coeFn_eq_coeFn_toMeasure

added theorem MeasureTheory.ProbabilityMeasure.eq_of_forall_apply_eq

added theorem MeasureTheory.ProbabilityMeasure.eq_of_forall_toMeasure_apply_eq

added theorem MeasureTheory.ProbabilityMeasure.mass_toFiniteMeasure

added theorem MeasureTheory.ProbabilityMeasure.nonempty

added theorem MeasureTheory.ProbabilityMeasure.tendsto_iff_forall_integral_tendsto

added theorem MeasureTheory.ProbabilityMeasure.tendsto_iff_forall_lintegral_tendsto

added theorem MeasureTheory.ProbabilityMeasure.tendsto_nhds_iff_toFiniteMeasure_tendsto_nhds

added theorem MeasureTheory.ProbabilityMeasure.testAgainstNN_lipschitz

added def MeasureTheory.ProbabilityMeasure.toFiniteMeasure

added theorem MeasureTheory.ProbabilityMeasure.toFiniteMeasure_continuous

added theorem MeasureTheory.ProbabilityMeasure.toFiniteMeasure_embedding

added theorem MeasureTheory.ProbabilityMeasure.toFiniteMeasure_nonzero

added def MeasureTheory.ProbabilityMeasure.toMeasure

added theorem MeasureTheory.ProbabilityMeasure.toMeasure_comp_toFiniteMeasure_eq_toMeasure

added theorem MeasureTheory.ProbabilityMeasure.toMeasure_injective

added def MeasureTheory.ProbabilityMeasure.toWeakDualBCNN

added theorem MeasureTheory.ProbabilityMeasure.toWeakDualBCNN_apply

added theorem MeasureTheory.ProbabilityMeasure.toWeakDualBCNN_continuous

added theorem MeasureTheory.ProbabilityMeasure.val_eq_to_measure

added def MeasureTheory.ProbabilityMeasure

added theorem ProbabilityMeasure.toFiniteMeasure_normalize_eq_self