ProbabilityMeasure

📁 Source: Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean

Statistics

Metric	Count
Definitions `normalize`, `ProbabilityMeasure`, `instCoeMeasure`, `instFunLike`, `instInhabited`, `instMeasurableSpace`, `instTopologicalSpace`, `map`, `toFiniteMeasure`, `toMeasure`, `toWeakDualBCNN`	11
Theorems `average_eq_integral_normalize`, `normalize_eq_inv_mass_smul_of_nonzero`, `normalize_eq_of_nonzero`, `normalize_testAgainstNN`, `self_eq_mass_mul_normalize`, `self_eq_mass_smul_normalize`, `tendsto_normalize_iff_tendsto`, `tendsto_normalize_of_tendsto`, `tendsto_normalize_testAgainstNN_of_tendsto`, `tendsto_of_tendsto_normalize_testAgainstNN_of_tendsto_mass`, `tendsto_testAgainstNN_of_tendsto_normalize_testAgainstNN_of_tendsto_mass`, `testAgainstNN_eq_mass_mul`, `toMeasure_normalize_eq_of_nonzero`, `R1Space`, `apply_iUnion_le`, `apply_le_one`, `apply_mono`, `apply_union_le`, `coeFn_comp_toFiniteMeasure_eq_coeFn`, `coeFn_def`, `coeFn_empty`, `coeFn_mk`, `coeFn_toFiniteMeasure`, `coeFn_univ`, `coeFn_univ_ne_zero`, `coe_mk`, `coe_toWeakDualBCNN`, `continuous_iff_forall_continuousMap_continuous_integral`, `continuous_iff_forall_continuousMap_continuous_lintegral`, `continuous_iff_forall_continuous_integral`, `continuous_iff_forall_continuous_lintegral`, `continuous_integral_boundedContinuousFunction`, `continuous_integral_continuousMap`, `continuous_lintegral_boundedContinuousFunction`, `continuous_lintegral_continuousMap`, `continuous_map`, `continuous_testAgainstNN_eval`, `ennreal_coeFn_eq_coeFn_toMeasure`, `eq_of_forall_apply_eq`, `eq_of_forall_toMeasure_apply_eq`, `eq_of_forall_toMeasure_apply_eq_iff`, `instIsProbabilityMeasureToMeasure`, `map_apply`, `map_apply'`, `map_apply_of_aemeasurable`, `mass_toFiniteMeasure`, `measurableSet_isProbabilityMeasure`, `measurable_fun_prod`, `measureReal_eq_coe_coeFn`, `mk_apply`, `nonempty`, `null_iff_toMeasure_null`, `range_toFiniteMeasure`, `t2Space`, `tendsto_iff_forall_integral_rclike_tendsto`, `tendsto_iff_forall_integral_tendsto`, `tendsto_iff_forall_lintegral_tendsto`, `tendsto_map_of_tendsto_of_continuous`, `tendsto_measure_iUnion_accumulate`, `tendsto_nhds_iff_toFiniteMeasure_tendsto_nhds`, `testAgainstNN_lipschitz`, `toFiniteMeasure_apply`, `toFiniteMeasure_apply_eq_apply`, `toFiniteMeasure_continuous`, `toFiniteMeasure_isEmbedding`, `toFiniteMeasure_nonzero`, `toMeasure_comp_toFiniteMeasure_eq_toMeasure`, `toMeasure_injective`, `toMeasure_map`, `toNNReal_measureReal_eq_coeFn`, `toWeakDualBCNN_apply`, `toWeakDualBCNN_continuous`, `val_eq_to_measure`, `isProbabilityMeasure_bind`, `isProbabilityMeasure_join`, `toFiniteMeasure_normalize_eq_self`	76
Total	87

MeasureTheory

Definitions

Name	Category	Theorems
`ProbabilityMeasure` 📖	CompOp	83 math math: `injective_diracProba`, `isCompact_setOf_probabilityMeasure_mass_eq_compl_isCompact_le`, `LevyProkhorov.dist_probabilityMeasure_def`, `ProbabilityMeasure.toMeasure_add_pos_gt_mem_nhds`, `LevyProkhorov.eq_convergenceInDistribution`, `ProbabilityMeasure.prod_prod`, `ProbabilityMeasure.range_toFiniteMeasure`, `ProbabilityMeasure.continuous_pi`, `diracProba_diracProbaInverse`, `ProbabilityMeasure.continuous_lintegral_boundedContinuousFunction`, `ProbabilityMeasure.measurable_fun_prod`, `LevyProkhorov.continuous_equiv_symm_probabilityMeasure`, `continuous_diracProbaEquiv`, `FiniteMeasure.normalize_eq_of_nonzero`, `ProbabilityMeasure.coeFn_comp_toFiniteMeasure_eq_coeFn`, `LevyProkhorov.continuous_equiv_probabilityMeasure`, `ProbabilityMeasure.ennreal_coeFn_eq_coeFn_toMeasure`, `FiniteMeasure.self_eq_mass_mul_normalize`, `ProbabilityMeasure.pi_pi`, `ProbabilityMeasure.apply_mono`, `FiniteMeasure.tendsto_normalize_iff_tendsto`, `ProbabilityMeasure.toNNReal_measureReal_eq_coeFn`, `tendsto_diracProba_iff_tendsto`, `ProbabilityMeasure.coeFn_empty`, `ProbabilityMeasure.continuous_iff_forall_continuousMap_continuous_integral`, `ProbabilityMeasure.coeFn_def`, `ProbabilityMeasure.continuous_map`, `ProbabilityMeasure.tendsto_nhds_iff_toFiniteMeasure_tendsto_nhds`, `ProbabilityMeasure.toFiniteMeasure_apply`, `diracProba_comp_diracProbaEquiv_symm_eq_val`, `ProbabilityMeasure.map_apply_of_aemeasurable`, `ProbabilityMeasure.tendsto_measure_iUnion_accumulate`, `ProbabilityMeasure.apply_le_one`, `instPseudoMetrizableSpaceProbabilityMeasureOfSeparableSpace`, `LevyProkhorov.dist_def`, `ProbabilityMeasure.t2Space`, `ProbabilityMeasure.continuous_lintegral_continuousMap`, `ProbabilityMeasure.continuous_integral_boundedContinuousFunction`, `tendsto_of_forall_isClosed_limsup_real_le'`, `ProbabilityMeasure.tendsto_iff_forall_integral_rclike_tendsto`, `isEmbedding_diracProba`, `ProbabilityMeasure.continuous_iff_forall_continuous_lintegral`, `LevyProkhorov.edist_probabilityMeasure_def`, `tendsto_of_forall_isOpen_le_liminf_nat'`, `ProbabilityMeasure.continuous_prod`, `ProbabilityMeasure.apply_union_le`, `FiniteMeasure.tendsto_normalize_of_tendsto`, `ProbabilityMeasure.map_apply`, `TendstoInDistribution.tendsto`, `ProbabilityMeasure.mk_apply`, `ProbabilityMeasure.continuous_iff_forall_continuous_integral`, `tendsto_diracProbaEquivSymm_iff_tendsto`, `ProbabilityMeasure.toWeakDualBCNN_continuous`, `instMetrizableSpaceProbabilityMeasure`, `instCompactSpaceProbabilityMeasure`, `continuous_diracProba`, `LevyProkhorov.continuous_ofMeasure_probabilityMeasure`, `tendsto_of_forall_isOpen_le_liminf'`, `ProbabilityMeasure.toMeasure_injective`, `ProbabilityMeasure.continuous_testAgainstNN_eval`, `ProbabilityMeasure.coeFn_toFiniteMeasure`, `ProbabilityMeasure.measureReal_eq_coe_coeFn`, `continuous_diracProbaEquivSymm`, `LevyProkhorov.le_convergenceInDistribution`, `ProbabilityMeasure.continuous_integral_continuousMap`, `ProbabilityMeasure.toFiniteMeasure_isEmbedding`, `ProbabilityMeasure.toFiniteMeasure_continuous`, `levyProkhorov_le_convergenceInDistribution`, `LevyProkhorov.continuous_toMeasure_probabilityMeasure`, `ProbabilityMeasure.continuous_iff_forall_continuousMap_continuous_lintegral`, `ProbabilityMeasure.coeFn_univ`, `ProbabilityMeasure.null_iff_toMeasure_null`, `ProbabilityMeasure.prod_apply_symm`, `tendsto_iff_forall_lipschitz_integral_tendsto`, `ProbabilityMeasure.coeFn_mk`, `ProbabilityMeasure.R1Space`, `ProbabilityMeasure.toFiniteMeasure_apply_eq_apply`, `tendsto_of_forall_isClosed_limsup_le'`, `ProbabilityMeasure.prod_apply`, `not_tendsto_diracProba_of_not_tendsto`, `ProbabilityMeasure.tendsto_iff_forall_integral_tendsto`, `ProbabilityMeasure.tendsto_iff_forall_lintegral_tendsto`, `levyProkhorov_eq_convergenceInDistribution`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isProbabilityMeasure_bind` 📖	mathematical	`AEMeasurable` `Measure` `Measure.instMeasurableSpace` `Filter.Eventually` `IsProbabilityMeasure` `ae` `Measure.instFunLike` `Measure.instOuterMeasureClass`	`Measure.bind`	—	`Measure.instOuterMeasureClass` `Measure.bind_apply` `lintegral_eq_const`
`isProbabilityMeasure_join` 📖	mathematical	`Filter.Eventually` `Measure` `IsProbabilityMeasure` `ae` `Measure.instMeasurableSpace` `Measure.instFunLike` `Measure.instOuterMeasureClass`	`Measure.join`	—	`Measure.instOuterMeasureClass` `Measure.join_apply` `lintegral_eq_const`

MeasureTheory.FiniteMeasure

Definitions

Name	Category	Theorems
`normalize` 📖	CompOp	12 math math: `testAgainstNN_eq_mass_mul`, `normalize_eq_of_nonzero`, `self_eq_mass_smul_normalize`, `self_eq_mass_mul_normalize`, `tendsto_normalize_iff_tendsto`, `ProbabilityMeasure.toFiniteMeasure_normalize_eq_self`, `average_eq_integral_normalize`, `toMeasure_normalize_eq_of_nonzero`, `normalize_eq_inv_mass_smul_of_nonzero`, `tendsto_normalize_of_tendsto`, `tendsto_normalize_testAgainstNN_of_tendsto`, `normalize_testAgainstNN`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`average_eq_integral_normalize` 📖	mathematical	—	`MeasureTheory.average` `toMeasure` `MeasureTheory.integral` `MeasureTheory.ProbabilityMeasure.toMeasure` `normalize`	—	`IsScalarTower.right` `toMeasure_normalize_eq_of_nonzero` `MeasureTheory.average.eq_1` `ENNReal.coe_inv` `mass_nonzero_iff` `ennreal_mass`
`normalize_eq_inv_mass_smul_of_nonzero` 📖	mathematical	—	`MeasureTheory.ProbabilityMeasure.toFiniteMeasure` `normalize` `NNReal` `MeasureTheory.FiniteMeasure` `instSMul` `Algebra.toSMul` `instCommSemiringNNReal` `CommSemiring.toSemiring` `Algebra.id` `ENNReal` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiringNNReal` `ENNReal.instMulActionNNReal` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `ENNReal.instAddCommMonoid` `Module.toDistribMulAction` `Semiring.toModule` `IsScalarTower.right` `NNReal.instInv` `mass`	—	`IsScalarTower.left` `IsScalarTower.right` `self_eq_mass_smul_normalize` `smul_assoc` `inv_mul_cancel₀` `mass_nonzero_iff` `one_smul`
`normalize_eq_of_nonzero` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.ProbabilityMeasure` `Set` `NNReal` `MeasureTheory.ProbabilityMeasure.instFunLike` `normalize` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `NNReal.instInv` `mass` `MeasureTheory.FiniteMeasure` `instFunLike`	—	`self_eq_mass_mul_normalize` `inv_mul_cancel_left₀` `mass_nonzero_iff`
`normalize_testAgainstNN` 📖	mathematical	—	`testAgainstNN` `MeasureTheory.ProbabilityMeasure.toFiniteMeasure` `normalize` `NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `NNReal.instInv` `mass`	—	`testAgainstNN_eq_mass_mul` `inv_mul_cancel_left₀` `mass_nonzero_iff`
`self_eq_mass_mul_normalize` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.FiniteMeasure` `Set` `NNReal` `instFunLike` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `mass` `MeasureTheory.ProbabilityMeasure` `MeasureTheory.ProbabilityMeasure.instFunLike` `normalize`	—	`eq_or_ne` `MulZeroClass.zero_mul` `mass_nonzero_iff` `ENNReal.toNNReal_mul` `mul_inv_cancel_left₀`
`self_eq_mass_smul_normalize` 📖	mathematical	—	`NNReal` `MeasureTheory.FiniteMeasure` `instSMul` `Algebra.toSMul` `instCommSemiringNNReal` `CommSemiring.toSemiring` `Algebra.id` `ENNReal` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiringNNReal` `ENNReal.instMulActionNNReal` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `ENNReal.instAddCommMonoid` `Module.toDistribMulAction` `Semiring.toModule` `IsScalarTower.right` `mass` `MeasureTheory.ProbabilityMeasure.toFiniteMeasure` `normalize`	—	`eq_of_forall_apply_eq` `IsScalarTower.left` `IsScalarTower.right` `self_eq_mass_mul_normalize` `smul_apply` `smul_eq_mul` `MeasureTheory.ProbabilityMeasure.coeFn_comp_toFiniteMeasure_eq_coeFn`
`tendsto_normalize_iff_tendsto` 📖	mathematical	—	`Filter.Tendsto` `MeasureTheory.ProbabilityMeasure` `normalize` `nhds` `MeasureTheory.ProbabilityMeasure.instTopologicalSpace` `NNReal` `mass` `NNReal.instTopologicalSpace` `MeasureTheory.FiniteMeasure` `instTopologicalSpace`	—	`tendsto_of_tendsto_normalize_testAgainstNN_of_tendsto_mass` `tendsto_normalize_of_tendsto` `Filter.Tendsto.mass`
`tendsto_normalize_of_tendsto` 📖	mathematical	`Filter.Tendsto` `MeasureTheory.FiniteMeasure` `nhds` `instTopologicalSpace`	`MeasureTheory.ProbabilityMeasure` `normalize` `MeasureTheory.ProbabilityMeasure.instTopologicalSpace`	—	`MeasureTheory.ProbabilityMeasure.tendsto_nhds_iff_toFiniteMeasure_tendsto_nhds` `tendsto_iff_forall_testAgainstNN_tendsto` `tendsto_normalize_testAgainstNN_of_tendsto`
`tendsto_normalize_testAgainstNN_of_tendsto` 📖	mathematical	`Filter.Tendsto` `MeasureTheory.FiniteMeasure` `nhds` `instTopologicalSpace`	`NNReal` `testAgainstNN` `MeasureTheory.ProbabilityMeasure.toFiniteMeasure` `normalize` `NNReal.instTopologicalSpace`	—	`Filter.Tendsto.mass` `IsOpen.mem_nhds` `isOpen_compl_singleton` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `mass_nonzero_iff` `Filter.mp_mem` `Filter.eventually_iff` `Filter.univ_mem'` `normalize_testAgainstNN` `Filter.tendsto_congr'` `Prod.tendsto_iff` `Filter.Tendsto.comp` `ContinuousAt.tendsto` `ContinuousOn.continuousAt` `continuousOn_inv₀` `NNReal.instContinuousInv₀` `tendsto_iff_forall_testAgainstNN_tendsto` `tendsto_mul` `IsTopologicalSemiring.toContinuousMul` `NNReal.instIsTopologicalSemiring`
`tendsto_of_tendsto_normalize_testAgainstNN_of_tendsto_mass` 📖	mathematical	`Filter.Tendsto` `MeasureTheory.ProbabilityMeasure` `normalize` `nhds` `MeasureTheory.ProbabilityMeasure.instTopologicalSpace` `NNReal` `mass` `NNReal.instTopologicalSpace`	`MeasureTheory.FiniteMeasure` `instTopologicalSpace`	—	`tendsto_iff_forall_testAgainstNN_tendsto` `tendsto_testAgainstNN_of_tendsto_normalize_testAgainstNN_of_tendsto_mass`
`tendsto_testAgainstNN_of_tendsto_normalize_testAgainstNN_of_tendsto_mass` 📖	mathematical	`Filter.Tendsto` `MeasureTheory.ProbabilityMeasure` `normalize` `nhds` `MeasureTheory.ProbabilityMeasure.instTopologicalSpace` `NNReal` `mass` `NNReal.instTopologicalSpace`	`testAgainstNN`	—	`mass_zero_iff` `zero_testAgainstNN_apply` `tendsto_zero_testAgainstNN_of_tendsto_zero_mass` `testAgainstNN_eq_mass_mul` `Prod.tendsto_iff` `tendsto_iff_forall_testAgainstNN_tendsto` `MeasureTheory.ProbabilityMeasure.tendsto_nhds_iff_toFiniteMeasure_tendsto_nhds` `Filter.Tendsto.comp` `tendsto_mul` `IsTopologicalSemiring.toContinuousMul` `NNReal.instIsTopologicalSemiring`
`testAgainstNN_eq_mass_mul` 📖	mathematical	—	`testAgainstNN` `NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `mass` `MeasureTheory.ProbabilityMeasure.toFiniteMeasure` `normalize`	—	`IsScalarTower.left` `IsScalarTower.right` `self_eq_mass_smul_normalize` `smul_testAgainstNN_apply` `smul_eq_mul`
`toMeasure_normalize_eq_of_nonzero` 📖	mathematical	—	`MeasureTheory.ProbabilityMeasure.toMeasure` `normalize` `NNReal` `MeasureTheory.Measure` `MeasureTheory.Measure.instSMul` `Algebra.toSMul` `ENNReal` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `IsScalarTower.right` `NNReal.instInv` `mass` `toMeasure`	—	`MeasureTheory.Measure.ext` `IsScalarTower.right` `MeasureTheory.ProbabilityMeasure.ennreal_coeFn_eq_coeFn_toMeasure` `normalize_eq_of_nonzero` `ENNReal.coe_mul` `ennreal_coeFn_eq_coeFn_toMeasure` `MeasureTheory.Measure.coe_nnreal_smul_apply`

MeasureTheory.ProbabilityMeasure

Definitions

Name	Category	Theorems
`instCoeMeasure` 📖	CompOp	—
`instFunLike` 📖	CompOp	27 math math: `prod_prod`, `MeasureTheory.FiniteMeasure.normalize_eq_of_nonzero`, `coeFn_comp_toFiniteMeasure_eq_coeFn`, `ennreal_coeFn_eq_coeFn_toMeasure`, `MeasureTheory.FiniteMeasure.self_eq_mass_mul_normalize`, `pi_pi`, `apply_mono`, `toNNReal_measureReal_eq_coeFn`, `coeFn_empty`, `coeFn_def`, `toFiniteMeasure_apply`, `map_apply_of_aemeasurable`, `tendsto_measure_iUnion_accumulate`, `apply_le_one`, `apply_union_le`, `tendsto_measure_of_isClopen_of_tendsto`, `map_apply`, `mk_apply`, `MeasureTheory.exists_measure_iUnion_gt_of_isCompact_closure`, `coeFn_toFiniteMeasure`, `measureReal_eq_coe_coeFn`, `coeFn_univ`, `null_iff_toMeasure_null`, `prod_apply_symm`, `coeFn_mk`, `toFiniteMeasure_apply_eq_apply`, `prod_apply`
`instInhabited` 📖	CompOp	—
`instMeasurableSpace` 📖	CompOp	1 math math: `measurable_fun_prod`
`instTopologicalSpace` 📖	CompOp	55 math math: `isCompact_setOf_probabilityMeasure_mass_eq_compl_isCompact_le`, `toMeasure_add_pos_gt_mem_nhds`, `MeasureTheory.LevyProkhorov.eq_convergenceInDistribution`, `continuous_pi`, `continuous_lintegral_boundedContinuousFunction`, `MeasureTheory.LevyProkhorov.continuous_equiv_symm_probabilityMeasure`, `MeasureTheory.continuous_diracProbaEquiv`, `MeasureTheory.LevyProkhorov.continuous_equiv_probabilityMeasure`, `MeasureTheory.tendsto_of_forall_isClosed_limsup_le`, `MeasureTheory.FiniteMeasure.tendsto_normalize_iff_tendsto`, `MeasureTheory.tendsto_diracProba_iff_tendsto`, `continuous_iff_forall_continuousMap_continuous_integral`, `continuous_map`, `tendsto_nhds_iff_toFiniteMeasure_tendsto_nhds`, `MeasureTheory.instPseudoMetrizableSpaceProbabilityMeasureOfSeparableSpace`, `t2Space`, `MeasureTheory.tendsto_of_forall_isClosed_limsup_le_nat`, `continuous_lintegral_continuousMap`, `continuous_integral_boundedContinuousFunction`, `MeasureTheory.tendsto_of_forall_isClosed_limsup_real_le'`, `tendsto_iff_forall_integral_rclike_tendsto`, `MeasureTheory.isEmbedding_diracProba`, `continuous_iff_forall_continuous_lintegral`, `MeasureTheory.tendsto_of_forall_isOpen_le_liminf_nat'`, `continuous_prod`, `MeasureTheory.FiniteMeasure.tendsto_normalize_of_tendsto`, `MeasureTheory.TendstoInDistribution.tendsto`, `continuous_iff_forall_continuous_integral`, `MeasureTheory.tendsto_diracProbaEquivSymm_iff_tendsto`, `toWeakDualBCNN_continuous`, `MeasureTheory.instMetrizableSpaceProbabilityMeasure`, `MeasureTheory.tendsto_of_forall_isOpen_le_liminf`, `instCompactSpaceProbabilityMeasure`, `MeasureTheory.continuous_diracProba`, `MeasureTheory.LevyProkhorov.continuous_ofMeasure_probabilityMeasure`, `MeasureTheory.tendsto_of_forall_isOpen_le_liminf'`, `continuous_testAgainstNN_eval`, `IsPiSystem.tendsto_probabilityMeasure_of_tendsto_of_mem`, `MeasureTheory.continuous_diracProbaEquivSymm`, `isCompact_closure_of_isTightMeasureSet`, `MeasureTheory.LevyProkhorov.le_convergenceInDistribution`, `continuous_integral_continuousMap`, `toFiniteMeasure_isEmbedding`, `toFiniteMeasure_continuous`, `MeasureTheory.levyProkhorov_le_convergenceInDistribution`, `MeasureTheory.LevyProkhorov.continuous_toMeasure_probabilityMeasure`, `continuous_iff_forall_continuousMap_continuous_lintegral`, `MeasureTheory.tendsto_iff_forall_lipschitz_integral_tendsto`, `MeasureTheory.tendsto_of_forall_isOpen_le_liminf_nat`, `R1Space`, `MeasureTheory.tendsto_of_forall_isClosed_limsup_le'`, `MeasureTheory.not_tendsto_diracProba_of_not_tendsto`, `tendsto_iff_forall_integral_tendsto`, `tendsto_iff_forall_lintegral_tendsto`, `MeasureTheory.levyProkhorov_eq_convergenceInDistribution`
`map` 📖	CompOp	10 math math: `map_prod_map`, `prod_swap`, `tendsto_map_of_tendsto_of_continuous`, `map_fst_prod`, `continuous_map`, `map_apply_of_aemeasurable`, `map_apply`, `map_apply'`, `map_snd_prod`, `toMeasure_map`
`toFiniteMeasure` 📖	CompOp	19 math math: `mass_toFiniteMeasure`, `toMeasure_comp_toFiniteMeasure_eq_toMeasure`, `range_toFiniteMeasure`, `MeasureTheory.FiniteMeasure.testAgainstNN_eq_mass_mul`, `coeFn_comp_toFiniteMeasure_eq_coeFn`, `MeasureTheory.FiniteMeasure.self_eq_mass_smul_normalize`, `tendsto_nhds_iff_toFiniteMeasure_tendsto_nhds`, `toFiniteMeasure_apply`, `ProbabilityMeasure.toFiniteMeasure_normalize_eq_self`, `MeasureTheory.FiniteMeasure.normalize_eq_inv_mass_smul_of_nonzero`, `coe_toWeakDualBCNN`, `MeasureTheory.FiniteMeasure.tendsto_normalize_testAgainstNN_of_tendsto`, `MeasureTheory.FiniteMeasure.normalize_testAgainstNN`, `testAgainstNN_lipschitz`, `continuous_testAgainstNN_eval`, `coeFn_toFiniteMeasure`, `toFiniteMeasure_isEmbedding`, `toFiniteMeasure_continuous`, `toFiniteMeasure_apply_eq_apply`
`toMeasure` 📖	CompOp	48 math math: `toMeasure_comp_toFiniteMeasure_eq_toMeasure`, `coe_mk`, `map_prod_map`, `MeasureTheory.LevyProkhorov.dist_probabilityMeasure_def`, `toMeasure_add_pos_gt_mem_nhds`, `prod_swap`, `tendsto_map_of_tendsto_of_continuous`, `continuous_lintegral_boundedContinuousFunction`, `measurable_fun_prod`, `toMeasure_prod`, `ennreal_coeFn_eq_coeFn_toMeasure`, `eq_of_forall_toMeasure_apply_eq_iff`, `toNNReal_measureReal_eq_coeFn`, `map_fst_prod`, `continuous_iff_forall_continuousMap_continuous_integral`, `coeFn_def`, `continuous_map`, `le_liminf_measure_open_of_tendsto`, `toMeasure_pi`, `MeasureTheory.FiniteMeasure.average_eq_integral_normalize`, `MeasureTheory.LevyProkhorov.dist_def`, `continuous_lintegral_continuousMap`, `continuous_integral_boundedContinuousFunction`, `MeasureTheory.isTightMeasureSet_of_isCompact_closure`, `tendsto_iff_forall_integral_rclike_tendsto`, `MeasureTheory.FiniteMeasure.toMeasure_normalize_eq_of_nonzero`, `continuous_iff_forall_continuous_lintegral`, `toWeakDualBCNN_apply`, `MeasureTheory.LevyProkhorov.edist_probabilityMeasure_def`, `MeasureTheory.diracProba_toMeasure_apply'`, `instIsProbabilityMeasureToMeasure`, `continuous_iff_forall_continuous_integral`, `MeasureTheory.diracProba_toMeasure_apply`, `toMeasure_injective`, `measureReal_eq_coe_coeFn`, `val_eq_to_measure`, `continuous_integral_continuousMap`, `map_snd_prod`, `continuous_iff_forall_continuousMap_continuous_lintegral`, `null_iff_toMeasure_null`, `prod_apply_symm`, `MeasureTheory.tendsto_iff_forall_lipschitz_integral_tendsto`, `prod_apply`, `MeasureTheory.tendsto_integral_meas_thickening_le`, `limsup_measure_closed_le_of_tendsto`, `tendsto_iff_forall_integral_tendsto`, `MeasureTheory.diracProba_toMeasure_apply_of_mem`, `tendsto_iff_forall_lintegral_tendsto`
`toWeakDualBCNN` 📖	CompOp	3 math math: `toWeakDualBCNN_apply`, `coe_toWeakDualBCNN`, `toWeakDualBCNN_continuous`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`R1Space` 📖	mathematical	—	`R1Space` `MeasureTheory.ProbabilityMeasure` `instTopologicalSpace`	—	`Topology.IsInducing.r1Space` `MeasureTheory.FiniteMeasure.instR1Space` `Topology.IsEmbedding.toIsInducing` `toFiniteMeasure_isEmbedding`
`apply_iUnion_le` 📖	mathematical	`Summable` `NNReal` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `NNReal.instTopologicalSpace` `DFunLike.coe` `MeasureTheory.ProbabilityMeasure` `Set` `instFunLike` `SummationFilter.unconditional`	`Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `Set.iUnion` `tsum`	—	`ennreal_coeFn_eq_coeFn_toMeasure` `ENNReal.coe_tsum` `MeasureTheory.measure_iUnion_le` `MeasureTheory.Measure.instOuterMeasureClass` `instCountableNat`
`apply_le_one` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `DFunLike.coe` `MeasureTheory.ProbabilityMeasure` `Set` `instFunLike` `instOneNNReal`	—	`coeFn_univ` `apply_mono` `Set.subset_univ`
`apply_mono` 📖	mathematical	`Set` `Set.instHasSubset`	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `DFunLike.coe` `MeasureTheory.ProbabilityMeasure` `instFunLike`	—	`coeFn_comp_toFiniteMeasure_eq_coeFn` `MeasureTheory.FiniteMeasure.apply_mono`
`apply_union_le` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `DFunLike.coe` `MeasureTheory.ProbabilityMeasure` `Set` `instFunLike` `Set.instUnion` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`coeFn_comp_toFiniteMeasure_eq_coeFn` `MeasureTheory.FiniteMeasure.apply_union_le`
`coeFn_comp_toFiniteMeasure_eq_coeFn` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.FiniteMeasure` `Set` `NNReal` `MeasureTheory.FiniteMeasure.instFunLike` `toFiniteMeasure` `MeasureTheory.ProbabilityMeasure` `instFunLike`	—	—
`coeFn_def` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.ProbabilityMeasure` `Set` `NNReal` `instFunLike` `ENNReal.toNNReal` `MeasureTheory.Measure` `ENNReal` `MeasureTheory.Measure.instFunLike` `toMeasure`	—	—
`coeFn_empty` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.ProbabilityMeasure` `Set` `NNReal` `instFunLike` `Set.instEmptyCollection` `instZeroNNReal`	—	`MeasureTheory.measure_empty` `MeasureTheory.Measure.instOuterMeasureClass`
`coeFn_mk` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.ProbabilityMeasure` `Set` `NNReal` `instFunLike` `MeasureTheory.Measure` `MeasureTheory.IsProbabilityMeasure` `ENNReal.toNNReal` `ENNReal` `MeasureTheory.Measure.instFunLike`	—	—
`coeFn_toFiniteMeasure` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.FiniteMeasure` `Set` `NNReal` `MeasureTheory.FiniteMeasure.instFunLike` `toFiniteMeasure` `MeasureTheory.ProbabilityMeasure` `instFunLike`	—	—
`coeFn_univ` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.ProbabilityMeasure` `Set` `NNReal` `instFunLike` `Set.univ` `instOneNNReal`	—	`MeasureTheory.IsProbabilityMeasure.measure_univ` `Subtype.prop`
`coeFn_univ_ne_zero` 📖	—	—	—	—	`coeFn_univ` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `NNReal.instIsStrictOrderedRing`
`coe_mk` 📖	mathematical	—	`toMeasure` `MeasureTheory.Measure` `MeasureTheory.IsProbabilityMeasure`	—	—
`coe_toWeakDualBCNN` 📖	mathematical	—	`DFunLike.coe` `WeakDual` `NNReal` `BoundedContinuousFunction` `instPseudoMetricSpaceNNReal` `instCommSemiringNNReal` `NNReal.instTopologicalSpace` `IsTopologicalSemiring.toContinuousAdd` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `NNReal.instIsTopologicalSemiring` `UniformContinuousConstSMul.to_continuousConstSMul` `PseudoMetricSpace.toUniformSpace` `Algebra.toSMul` `Algebra.id` `IsBoundedSMul.toUniformContinuousConstSMul` `instZeroNNReal` `NNReal.isBoundedSMul` `BoundedContinuousFunction.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instSemiringNNReal` `instBoundedAddOfLipschitzAdd` `AddCommMonoid.toAddMonoid` `NNReal.hasLipschitzAdd` `UniformSpace.toTopologicalSpace` `BoundedContinuousFunction.instModule` `Semiring.toModule` `BoundedContinuousFunction.instPseudoMetricSpace` `instFunLikeWeakDual` `toWeakDualBCNN` `MeasureTheory.FiniteMeasure.testAgainstNN` `toFiniteMeasure`	—	`IsTopologicalSemiring.toContinuousAdd` `NNReal.instIsTopologicalSemiring` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NNReal.isBoundedSMul` `instBoundedAddOfLipschitzAdd` `NNReal.hasLipschitzAdd`
`continuous_iff_forall_continuousMap_continuous_integral` 📖	mathematical	—	`Continuous` `MeasureTheory.ProbabilityMeasure` `instTopologicalSpace` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `MeasureTheory.integral` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField` `toMeasure` `DFunLike.coe` `ContinuousMap` `ContinuousMap.instFunLike`	—	`continuous_iff_forall_continuous_integral` `Equiv.forall_congr_left`
`continuous_iff_forall_continuousMap_continuous_lintegral` 📖	mathematical	—	`Continuous` `MeasureTheory.ProbabilityMeasure` `instTopologicalSpace` `ENNReal` `ENNReal.instTopologicalSpace` `MeasureTheory.lintegral` `toMeasure` `ENNReal.ofNNReal` `DFunLike.coe` `ContinuousMap` `NNReal` `NNReal.instTopologicalSpace` `ContinuousMap.instFunLike`	—	`continuous_iff_forall_continuous_lintegral` `Equiv.forall_congr_left`
`continuous_iff_forall_continuous_integral` 📖	mathematical	—	`Continuous` `MeasureTheory.ProbabilityMeasure` `instTopologicalSpace` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `MeasureTheory.integral` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField` `toMeasure` `DFunLike.coe` `BoundedContinuousFunction` `BoundedContinuousFunction.instFunLike`	—	`forall_swap`
`continuous_iff_forall_continuous_lintegral` 📖	mathematical	—	`Continuous` `MeasureTheory.ProbabilityMeasure` `instTopologicalSpace` `ENNReal` `ENNReal.instTopologicalSpace` `MeasureTheory.lintegral` `toMeasure` `ENNReal.ofNNReal` `DFunLike.coe` `BoundedContinuousFunction` `NNReal` `instPseudoMetricSpaceNNReal` `BoundedContinuousFunction.instFunLike`	—	`forall_swap`
`continuous_integral_boundedContinuousFunction` 📖	mathematical	—	`Continuous` `MeasureTheory.ProbabilityMeasure` `Real` `instTopologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `MeasureTheory.integral` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField` `toMeasure` `DFunLike.coe` `BoundedContinuousFunction` `BoundedContinuousFunction.instFunLike`	—	`continuous_iff_forall_continuous_integral` `continuous_id`
`continuous_integral_continuousMap` 📖	mathematical	—	`Continuous` `MeasureTheory.ProbabilityMeasure` `Real` `instTopologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `MeasureTheory.integral` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField` `toMeasure` `DFunLike.coe`	—	`continuous_iff_forall_continuousMap_continuous_integral` `continuous_id` `ContinuousMapClass.map_continuous`
`continuous_lintegral_boundedContinuousFunction` 📖	mathematical	—	`Continuous` `MeasureTheory.ProbabilityMeasure` `ENNReal` `instTopologicalSpace` `ENNReal.instTopologicalSpace` `MeasureTheory.lintegral` `toMeasure` `ENNReal.ofNNReal` `DFunLike.coe` `BoundedContinuousFunction` `NNReal` `instPseudoMetricSpaceNNReal` `BoundedContinuousFunction.instFunLike`	—	`continuous_iff_forall_continuous_lintegral` `continuous_id`
`continuous_lintegral_continuousMap` 📖	mathematical	—	`Continuous` `MeasureTheory.ProbabilityMeasure` `ENNReal` `instTopologicalSpace` `ENNReal.instTopologicalSpace` `MeasureTheory.lintegral` `toMeasure` `ENNReal.ofNNReal` `DFunLike.coe` `NNReal`	—	`continuous_iff_forall_continuousMap_continuous_lintegral` `continuous_id` `ContinuousMapClass.map_continuous`
`continuous_map` 📖	mathematical	`Continuous`	`MeasureTheory.ProbabilityMeasure` `instTopologicalSpace` `BorelSpace.opensMeasurable` `map` `Measurable.aemeasurable` `toMeasure` `Continuous.measurable`	—	`BorelSpace.opensMeasurable` `Measurable.aemeasurable` `Continuous.measurable` `continuous_iff_continuousAt` `tendsto_map_of_tendsto_of_continuous` `Continuous.continuousAt` `continuous_id`
`continuous_testAgainstNN_eval` 📖	mathematical	—	`Continuous` `MeasureTheory.ProbabilityMeasure` `NNReal` `instTopologicalSpace` `NNReal.instTopologicalSpace` `MeasureTheory.FiniteMeasure.testAgainstNN` `toFiniteMeasure`	—	`Continuous.comp` `MeasureTheory.FiniteMeasure.continuous_testAgainstNN_eval` `toFiniteMeasure_continuous`
`ennreal_coeFn_eq_coeFn_toMeasure` 📖	mathematical	—	`ENNReal.ofNNReal` `DFunLike.coe` `MeasureTheory.ProbabilityMeasure` `Set` `NNReal` `instFunLike` `MeasureTheory.Measure` `ENNReal` `MeasureTheory.Measure.instFunLike` `toMeasure`	—	`coeFn_comp_toFiniteMeasure_eq_coeFn` `MeasureTheory.FiniteMeasure.ennreal_coeFn_eq_coeFn_toMeasure` `toMeasure_comp_toFiniteMeasure_eq_toMeasure`
`eq_of_forall_apply_eq` 📖	—	`DFunLike.coe` `MeasureTheory.ProbabilityMeasure` `Set` `NNReal` `instFunLike`	—	—	`eq_of_forall_toMeasure_apply_eq` `ennreal_coeFn_eq_coeFn_toMeasure`
`eq_of_forall_toMeasure_apply_eq` 📖	—	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `toMeasure`	—	—	`toMeasure_injective` `MeasureTheory.Measure.ext`
`eq_of_forall_toMeasure_apply_eq_iff` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `toMeasure`	—	`eq_of_forall_toMeasure_apply_eq`
`instIsProbabilityMeasureToMeasure` 📖	mathematical	—	`MeasureTheory.IsProbabilityMeasure` `toMeasure`	—	`Subtype.prop`
`map_apply` 📖	mathematical	`AEMeasurable` `toMeasure` `MeasurableSet`	`DFunLike.coe` `MeasureTheory.ProbabilityMeasure` `Set` `NNReal` `instFunLike` `map` `Set.preimage`	—	`map_apply_of_aemeasurable`
`map_apply'` 📖	mathematical	`AEMeasurable` `toMeasure` `MeasurableSet`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `map` `Set.preimage`	—	`MeasureTheory.Measure.map_apply_of_aemeasurable`
`map_apply_of_aemeasurable` 📖	mathematical	`AEMeasurable` `toMeasure` `MeasurableSet`	`DFunLike.coe` `MeasureTheory.ProbabilityMeasure` `Set` `NNReal` `instFunLike` `map` `Set.preimage`	—	`ENNReal.toNNReal_eq_toNNReal_iff'` `MeasureTheory.measure_ne_top` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `instIsProbabilityMeasureToMeasure` `map_apply'`
`mass_toFiniteMeasure` 📖	mathematical	—	`MeasureTheory.FiniteMeasure.mass` `toFiniteMeasure` `NNReal` `instOneNNReal`	—	`coeFn_univ`
`measurableSet_isProbabilityMeasure` 📖	mathematical	—	`MeasurableSet` `MeasureTheory.Measure` `MeasureTheory.Measure.instMeasurableSpace` `setOf` `MeasureTheory.IsProbabilityMeasure`	—	`Set.ext` `MeasureTheory.isProbabilityMeasure_iff` `MeasureTheory.Measure.measurable_coe` `MeasurableSet.univ` `MeasurableSingletonClass.measurableSet_singleton` `instMeasurableSingletonClassOfMeasurableEq` `instMeasurableEqOfSecondCountableTopologyOfT2Space` `BorelSpace.opensMeasurable` `ENNReal.borelSpace` `ENNReal.instSecondCountableTopology` `ENNReal.instT2Space`
`measurable_fun_prod` 📖	mathematical	—	`Measurable` `MeasureTheory.ProbabilityMeasure` `MeasureTheory.Measure` `Prod.instMeasurableSpace` `instMeasurableSpace` `MeasureTheory.Measure.instMeasurableSpace` `MeasureTheory.Measure.prod` `toMeasure`	—	`Measurable.measure_of_isPiSystem_of_isProbabilityMeasure` `MeasureTheory.Measure.prod.instIsProbabilityMeasure` `instIsProbabilityMeasureToMeasure` `generateFrom_prod` `isPiSystem_prod` `MeasureTheory.Measure.prod_prod` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.IsFiniteMeasure.toSigmaFinite` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `Measurable.mul` `ENNReal.instMeasurableMul₂` `Measurable.comp` `MeasureTheory.Measure.measurable_coe` `measurable_subtype_coe` `measurable_fst` `measurable_snd`
`measureReal_eq_coe_coeFn` 📖	mathematical	—	`MeasureTheory.Measure.real` `toMeasure` `NNReal.toReal` `DFunLike.coe` `MeasureTheory.ProbabilityMeasure` `Set` `NNReal` `instFunLike`	—	—
`mk_apply` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.ProbabilityMeasure` `Set` `NNReal` `instFunLike` `MeasureTheory.Measure` `MeasureTheory.IsProbabilityMeasure` `ENNReal.toNNReal` `ENNReal` `MeasureTheory.Measure.instFunLike`	—	—
`nonempty` 📖	—	—	—	—	`MeasureTheory.nonempty_of_isProbabilityMeasure` `instIsProbabilityMeasureToMeasure`
`null_iff_toMeasure_null` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.ProbabilityMeasure` `Set` `NNReal` `instFunLike` `instZeroNNReal` `MeasureTheory.Measure` `ENNReal` `MeasureTheory.Measure.instFunLike` `toMeasure` `instZeroENNReal`	—	`ennreal_coeFn_eq_coeFn_toMeasure` `ENNReal.coe_zero`
`range_toFiniteMeasure` 📖	mathematical	—	`Set.range` `MeasureTheory.FiniteMeasure` `MeasureTheory.ProbabilityMeasure` `toFiniteMeasure` `setOf` `NNReal` `MeasureTheory.FiniteMeasure.mass` `instOneNNReal`	—	`Set.ext` `mass_toFiniteMeasure` `MeasureTheory.isProbabilityMeasure_iff_real` `MeasureTheory.FiniteMeasure.eq_of_forall_toMeasure_apply_eq`
`t2Space` 📖	mathematical	—	`T2Space` `MeasureTheory.ProbabilityMeasure` `instTopologicalSpace` `BorelSpace.opensMeasurable`	—	`Topology.IsEmbedding.t2Space` `BorelSpace.opensMeasurable` `MeasureTheory.FiniteMeasure.t2Space` `toFiniteMeasure_isEmbedding`
`tendsto_iff_forall_integral_rclike_tendsto` 📖	mathematical	—	`Filter.Tendsto` `MeasureTheory.ProbabilityMeasure` `nhds` `instTopologicalSpace` `MeasureTheory.integral` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `NormedAlgebra.toNormedSpace` `Real` `Real.normedField` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `RCLike.toNormedAlgebra` `toMeasure` `DFunLike.coe` `BoundedContinuousFunction` `SeminormedRing.toPseudoMetricSpace` `BoundedContinuousFunction.instFunLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace`	—	`MeasureTheory.FiniteMeasure.tendsto_iff_forall_integral_rclike_tendsto`
`tendsto_iff_forall_integral_tendsto` 📖	mathematical	—	`Filter.Tendsto` `MeasureTheory.ProbabilityMeasure` `nhds` `instTopologicalSpace` `Real` `MeasureTheory.integral` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField` `toMeasure` `DFunLike.coe` `BoundedContinuousFunction` `Real.pseudoMetricSpace` `BoundedContinuousFunction.instFunLike` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace`	—	—
`tendsto_iff_forall_lintegral_tendsto` 📖	mathematical	—	`Filter.Tendsto` `MeasureTheory.ProbabilityMeasure` `nhds` `instTopologicalSpace` `ENNReal` `MeasureTheory.lintegral` `toMeasure` `ENNReal.ofNNReal` `DFunLike.coe` `BoundedContinuousFunction` `NNReal` `instPseudoMetricSpaceNNReal` `BoundedContinuousFunction.instFunLike` `ENNReal.instTopologicalSpace`	—	`tendsto_nhds_iff_toFiniteMeasure_tendsto_nhds` `MeasureTheory.FiniteMeasure.tendsto_iff_forall_lintegral_tendsto`
`tendsto_map_of_tendsto_of_continuous` 📖	mathematical	`Filter.Tendsto` `MeasureTheory.ProbabilityMeasure` `nhds` `instTopologicalSpace` `Continuous`	`map` `Measurable.aemeasurable` `toMeasure` `Continuous.measurable` `BorelSpace.opensMeasurable`	—	`Measurable.aemeasurable` `Continuous.measurable` `BorelSpace.opensMeasurable` `tendsto_iff_forall_lintegral_tendsto` `MeasureTheory.lintegral_map` `ENNReal.borelSpace` `Continuous.comp` `ENNReal.continuous_coe` `BoundedContinuousFunction.continuous`
`tendsto_measure_iUnion_accumulate` 📖	mathematical	—	`Filter.Tendsto` `NNReal` `DFunLike.coe` `MeasureTheory.ProbabilityMeasure` `Set` `instFunLike` `Set.accumulate` `Preorder.toLE` `Filter.atTop` `nhds` `NNReal.instTopologicalSpace` `Set.iUnion`	—	`MeasureTheory.tendsto_measure_iUnion_accumulate`
`tendsto_nhds_iff_toFiniteMeasure_tendsto_nhds` 📖	mathematical	—	`Filter.Tendsto` `MeasureTheory.ProbabilityMeasure` `nhds` `instTopologicalSpace` `MeasureTheory.FiniteMeasure` `toFiniteMeasure` `MeasureTheory.FiniteMeasure.instTopologicalSpace`	—	`Topology.IsEmbedding.tendsto_nhds_iff` `toFiniteMeasure_isEmbedding`
`testAgainstNN_lipschitz` 📖	mathematical	—	`LipschitzWith` `BoundedContinuousFunction` `NNReal` `instPseudoMetricSpaceNNReal` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `BoundedContinuousFunction.instMetricSpace` `instMetricSpaceNNReal` `instOneNNReal` `MeasureTheory.FiniteMeasure.testAgainstNN` `toFiniteMeasure`	—	`MeasureTheory.FiniteMeasure.testAgainstNN_lipschitz` `mass_toFiniteMeasure`
`toFiniteMeasure_apply` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.FiniteMeasure` `Set` `NNReal` `MeasureTheory.FiniteMeasure.instFunLike` `toFiniteMeasure` `MeasureTheory.ProbabilityMeasure` `instFunLike`	—	—
`toFiniteMeasure_apply_eq_apply` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.FiniteMeasure` `Set` `NNReal` `MeasureTheory.FiniteMeasure.instFunLike` `toFiniteMeasure` `MeasureTheory.ProbabilityMeasure` `instFunLike`	—	—
`toFiniteMeasure_continuous` 📖	mathematical	—	`Continuous` `MeasureTheory.ProbabilityMeasure` `MeasureTheory.FiniteMeasure` `instTopologicalSpace` `MeasureTheory.FiniteMeasure.instTopologicalSpace` `toFiniteMeasure`	—	`continuous_induced_dom`
`toFiniteMeasure_isEmbedding` 📖	mathematical	—	`Topology.IsEmbedding` `MeasureTheory.ProbabilityMeasure` `MeasureTheory.FiniteMeasure` `instTopologicalSpace` `MeasureTheory.FiniteMeasure.instTopologicalSpace` `toFiniteMeasure`	—	—
`toFiniteMeasure_nonzero` 📖	—	—	—	—	`mass_toFiniteMeasure` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `NNReal.instIsStrictOrderedRing`
`toMeasure_comp_toFiniteMeasure_eq_toMeasure` 📖	mathematical	—	`MeasureTheory.FiniteMeasure.toMeasure` `toFiniteMeasure` `toMeasure`	—	—
`toMeasure_injective` 📖	mathematical	—	`MeasureTheory.ProbabilityMeasure` `MeasureTheory.Measure` `toMeasure`	—	`Subtype.coe_injective`
`toMeasure_map` 📖	mathematical	`AEMeasurable` `toMeasure`	`map` `MeasureTheory.Measure.map`	—	—
`toNNReal_measureReal_eq_coeFn` 📖	mathematical	—	`Real.toNNReal` `MeasureTheory.Measure.real` `toMeasure` `DFunLike.coe` `MeasureTheory.ProbabilityMeasure` `Set` `NNReal` `instFunLike`	—	`measureReal_eq_coe_coeFn` `Real.toNNReal_coe`
`toWeakDualBCNN_apply` 📖	mathematical	—	`DFunLike.coe` `WeakDual` `NNReal` `BoundedContinuousFunction` `instPseudoMetricSpaceNNReal` `instCommSemiringNNReal` `NNReal.instTopologicalSpace` `IsTopologicalSemiring.toContinuousAdd` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `NNReal.instIsTopologicalSemiring` `UniformContinuousConstSMul.to_continuousConstSMul` `PseudoMetricSpace.toUniformSpace` `Algebra.toSMul` `Algebra.id` `IsBoundedSMul.toUniformContinuousConstSMul` `instZeroNNReal` `NNReal.isBoundedSMul` `BoundedContinuousFunction.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instSemiringNNReal` `instBoundedAddOfLipschitzAdd` `AddCommMonoid.toAddMonoid` `NNReal.hasLipschitzAdd` `UniformSpace.toTopologicalSpace` `BoundedContinuousFunction.instModule` `Semiring.toModule` `BoundedContinuousFunction.instPseudoMetricSpace` `instFunLikeWeakDual` `toWeakDualBCNN` `ENNReal.toNNReal` `MeasureTheory.lintegral` `toMeasure` `ENNReal.ofNNReal` `BoundedContinuousFunction.instFunLike`	—	`IsTopologicalSemiring.toContinuousAdd` `NNReal.instIsTopologicalSemiring` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NNReal.isBoundedSMul` `instBoundedAddOfLipschitzAdd` `NNReal.hasLipschitzAdd`
`toWeakDualBCNN_continuous` 📖	mathematical	—	`Continuous` `MeasureTheory.ProbabilityMeasure` `WeakDual` `NNReal` `BoundedContinuousFunction` `instPseudoMetricSpaceNNReal` `instCommSemiringNNReal` `NNReal.instTopologicalSpace` `IsTopologicalSemiring.toContinuousAdd` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `NNReal.instIsTopologicalSemiring` `UniformContinuousConstSMul.to_continuousConstSMul` `PseudoMetricSpace.toUniformSpace` `Algebra.toSMul` `Algebra.id` `IsBoundedSMul.toUniformContinuousConstSMul` `instZeroNNReal` `NNReal.isBoundedSMul` `BoundedContinuousFunction.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instSemiringNNReal` `instBoundedAddOfLipschitzAdd` `AddCommMonoid.toAddMonoid` `NNReal.hasLipschitzAdd` `UniformSpace.toTopologicalSpace` `BoundedContinuousFunction.instModule` `Semiring.toModule` `BoundedContinuousFunction.instPseudoMetricSpace` `instTopologicalSpace` `instTopologicalSpaceWeakDual` `toWeakDualBCNN`	—	`Continuous.comp` `IsTopologicalSemiring.toContinuousAdd` `NNReal.instIsTopologicalSemiring` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NNReal.isBoundedSMul` `instBoundedAddOfLipschitzAdd` `NNReal.hasLipschitzAdd` `MeasureTheory.FiniteMeasure.toWeakDualBCNN_continuous` `toFiniteMeasure_continuous`
`val_eq_to_measure` 📖	mathematical	—	`MeasureTheory.Measure` `MeasureTheory.IsProbabilityMeasure` `toMeasure`	—	—

ProbabilityMeasure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toFiniteMeasure_normalize_eq_self` 📖	mathematical	—	`MeasureTheory.FiniteMeasure.normalize` `MeasureTheory.ProbabilityMeasure.toFiniteMeasure`	—	`MeasureTheory.ProbabilityMeasure.eq_of_forall_apply_eq` `MeasureTheory.FiniteMeasure.normalize_eq_of_nonzero` `MeasureTheory.ProbabilityMeasure.toFiniteMeasure_nonzero` `MeasureTheory.ProbabilityMeasure.mass_toFiniteMeasure` `inv_one` `one_mul`

---

← Back to Index