Documentation Verification Report

ConvergenceInDistribution

📁 Source: Mathlib/MeasureTheory/Function/ConvergenceInDistribution.lean

Statistics

Metric	Count
Definitions `TendstoInDistribution`	1
Theorems `add_of_tendstoInMeasure_const`, `aemeasurable_limit`, `continuous_comp`, `continuous_comp_prodMk_of_tendstoInMeasure_const`, `forall_aemeasurable`, `prodMk_of_tendstoInMeasure_const`, `tendsto`, `tendstoInDistribution`, `tendstoInDistribution_of_aemeasurable`, `tendstoInDistribution_const`, `tendstoInDistribution_of_identDistrib`, `tendstoInDistribution_of_isEmpty`, `tendstoInDistribution_of_tendstoInMeasure_sub`, `tendstoInDistribution_unique`	14
Total	15

MeasureTheory

Definitions

Name	Category	Theorems
`TendstoInDistribution` 📖	CompData	13 math math: `TendstoInDistribution.add_of_tendstoInMeasure_const`, `tendstoInDistribution_const`, `tendstoInDistribution_of_tendstoInMeasure_sub`, `TendstoInDistribution.congr`, `TendstoInDistribution.prodMk_of_tendstoInMeasure_const`, `ProbabilityTheory.tendstoInDistribution_inv_sqrt_mul_sum`, `ProbabilityTheory.tendstoInDistribution_inv_sqrt_mul_sum_sub`, `tendstoInDistribution_of_isEmpty`, `TendstoInMeasure.tendstoInDistribution`, `TendstoInDistribution.continuous_comp`, `TendstoInDistribution.continuous_comp_prodMk_of_tendstoInMeasure_const`, `tendstoInDistribution_of_identDistrib`, `TendstoInMeasure.tendstoInDistribution_of_aemeasurable`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tendstoInDistribution_const` 📖	mathematical	`AEMeasurable`	`TendstoInDistribution`	—	`tendsto_const_nhds` `Measure.isProbabilityMeasure_map`
`tendstoInDistribution_of_identDistrib` 📖	mathematical	`IsProbabilityMeasure` `ProbabilityTheory.IdentDistrib`	`TendstoInDistribution`	—	`ProbabilityTheory.IdentDistrib.aemeasurable_snd` `Measure.isProbabilityMeasure_map` `ProbabilityTheory.IdentDistrib.map_eq` `tendsto_const_nhds`
`tendstoInDistribution_of_isEmpty` 📖	mathematical	`IsProbabilityMeasure`	`TendstoInDistribution` `BorelSpace.opensMeasurable` `DiscreteMeasurableSpace.toBorelSpace` `Subsingleton.discreteTopology` `IsEmpty.instSubsingleton` `MeasurableSingletonClass.toDiscreteMeasurableSpace` `Subsingleton.measurableSingletonClass` `Encodable.countable` `IsEmpty.toEncodable`	—	`BorelSpace.opensMeasurable` `DiscreteMeasurableSpace.toBorelSpace` `Subsingleton.discreteTopology` `IsEmpty.instSubsingleton` `MeasurableSingletonClass.toDiscreteMeasurableSpace` `Subsingleton.measurableSingletonClass` `Encodable.countable` `Measurable.aemeasurable` `measurable_of_subsingleton_codomain` `Measure.isProbabilityMeasure_map` `Measure.instSubsingleton` `tendsto_const_nhds`
`tendstoInDistribution_of_tendstoInMeasure_sub` 📖	mathematical	`TendstoInDistribution` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `BorelSpace.opensMeasurable` `TendstoInMeasure` `PseudoEMetricSpace.toEDist` `PseudoMetricSpace.toPseudoEMetricSpace` `Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `Pi.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `AEMeasurable`	`TendstoInDistribution` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `BorelSpace.opensMeasurable`	—	`BorelSpace.opensMeasurable` `TendstoInDistribution.aemeasurable_limit` `TendstoInDistribution.forall_aemeasurable` `isEmpty_or_nonempty` `DiscreteMeasurableSpace.toBorelSpace` `Subsingleton.discreteTopology` `IsEmpty.instSubsingleton` `MeasurableSingletonClass.toDiscreteMeasurableSpace` `Subsingleton.measurableSingletonClass` `Encodable.countable` `LipschitzWith.continuous` `eq_zero_or_pos` `integral_const` `Real.instCompleteSpace` `Measure.isProbabilityMeasure_map` `probReal_univ` `one_mul` `tendsto_const_nhds` `Nat.instAtLeastTwoHAddOfNat` `LE.le.trans` `abs_sub_le` `Real.instIsOrderedAddMonoid` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Integrable.of_bound` `IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `Continuous.comp_aestronglyMeasurable` `AEMeasurable.aestronglyMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `ae_of_all` `Measure.instOuterMeasureClass` `sub_le_iff_le_add'` `abs_sub_abs_le_abs_sub` `integrable_norm_iff` `Continuous.sub` `IsTopologicalAddGroup.to_continuousSub` `instIsTopologicalAddGroupReal` `Continuous.fst` `continuous_id'` `Continuous.snd` `AEStronglyMeasurable.prodMk` `Integrable.sub` `integral_map` `Continuous.aestronglyMeasurable` `secondCountableTopologyEither_of_right` `instSecondCountableTopologyReal` `integral_sub` `Real.norm_eq_abs` `norm_integral_le_integral_norm` `integral_add_compl₀` `nullMeasurableSet_lt` `Real.borelSpace` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Measurable.comp_aemeasurable'` `Continuous.measurable` `Continuous.norm` `AEMeasurable.sub` `ContinuousSub.measurableSub₂` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `aemeasurable_const` `add_le_add` `setIntegral_mono_on₀` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `Real.instIsStrictOrderedRing` `instClosedIciTopology` `Integrable.integrableOn` `integrableOn_const` `measure_ne_top` `enorm_ne_top` `LipschitzWith.norm_sub_le_of_le` `LT.lt.le` `setIntegral_mono` `dist_eq_norm` `measureReal_restrict_apply` `Set.univ_inter` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Meta.NormNum.IsNNRat.to_raw_eq` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.mul_one` `mul_assoc` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `le_imp_le_of_le_of_le` `measureReal_le_one` `le_of_lt` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `le_refl` `mul_one` `Mathlib.Meta.Positivity.nnreal_coe_pos` `Filter.Tendsto.add` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `mul_div_assoc` `Filter.Tendsto.const_mul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `sub_zero` `TendstoInDistribution.tendsto` `dist_zero_right` `abs_abs` `abs_dist` `MulZeroClass.mul_zero` `add_zero` `half_lt_self` `mul_pos` `Filter.mp_mem` `Filter.Tendsto.eventually_lt_const` `Filter.univ_mem'` `LE.le.trans_lt` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `div_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `ne_of_gt` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `tendsto_iff_forall_lipschitz_integral_tendsto`
`tendstoInDistribution_unique` 📖	mathematical	`IsProbabilityMeasure` `TendstoInDistribution` `BorelSpace.opensMeasurable`	`Measure.map`	—	`BorelSpace.opensMeasurable` `Measure.isProbabilityMeasure_map` `TendstoInDistribution.aemeasurable_limit` `tendsto_nhds_unique` `ProbabilityMeasure.t2Space` `TendstoInDistribution.forall_aemeasurable` `TendstoInDistribution.tendsto`

MeasureTheory.TendstoInDistribution

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_of_tendstoInMeasure_const` 📖	mathematical	`MeasureTheory.TendstoInDistribution` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `BorelSpace.opensMeasurable` `MeasureTheory.TendstoInMeasure` `PseudoEMetricSpace.toEDist` `PseudoMetricSpace.toPseudoEMetricSpace` `AEMeasurable`	`MeasureTheory.TendstoInDistribution` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `BorelSpace.opensMeasurable` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`BorelSpace.opensMeasurable` `continuous_comp_prodMk_of_tendstoInMeasure_const` `continuous_add` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup`
`aemeasurable_limit` 📖	mathematical	`MeasureTheory.IsProbabilityMeasure` `MeasureTheory.TendstoInDistribution`	`AEMeasurable`	—	—
`continuous_comp` 📖	mathematical	`MeasureTheory.IsProbabilityMeasure` `Continuous` `MeasureTheory.TendstoInDistribution`	`MeasureTheory.TendstoInDistribution` `BorelSpace.opensMeasurable`	—	`BorelSpace.opensMeasurable` `Measurable.comp_aemeasurable` `Continuous.measurable` `forall_aemeasurable` `aemeasurable_limit` `MeasureTheory.Measure.isProbabilityMeasure_map` `Measurable.aemeasurable` `AEMeasurable.map_map_of_aemeasurable` `Continuous.aemeasurable` `MeasureTheory.ProbabilityMeasure.tendsto_map_of_tendsto_of_continuous` `tendsto`
`continuous_comp_prodMk_of_tendstoInMeasure_const` 📖	mathematical	`Continuous` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `MeasureTheory.TendstoInDistribution` `BorelSpace.opensMeasurable` `MeasureTheory.TendstoInMeasure` `PseudoEMetricSpace.toEDist` `PseudoMetricSpace.toPseudoEMetricSpace` `AEMeasurable`	`MeasureTheory.TendstoInDistribution` `BorelSpace.opensMeasurable`	—	`BorelSpace.opensMeasurable` `continuous_comp` `Prod.opensMeasurableSpace` `secondCountableTopologyEither_of_right` `prodMk_of_tendstoInMeasure_const`
`forall_aemeasurable` 📖	mathematical	`MeasureTheory.IsProbabilityMeasure` `MeasureTheory.TendstoInDistribution`	`AEMeasurable`	—	—
`prodMk_of_tendstoInMeasure_const` 📖	mathematical	`MeasureTheory.TendstoInDistribution` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `BorelSpace.opensMeasurable` `MeasureTheory.TendstoInMeasure` `PseudoEMetricSpace.toEDist` `PseudoMetricSpace.toPseudoEMetricSpace` `AEMeasurable`	`MeasureTheory.TendstoInDistribution` `Prod.instMeasurableSpace` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Prod.opensMeasurableSpace` `BorelSpace.opensMeasurable` `secondCountableTopologyEither_of_right`	—	`BorelSpace.opensMeasurable` `forall_aemeasurable` `aemeasurable_limit` `MeasureTheory.tendstoInDistribution_of_tendstoInMeasure_sub` `TopologicalSpace.instSecondCountableTopologyProd` `Prod.borelSpace` `secondCountableTopologyEither_of_right` `MeasureTheory.Measure.isProbabilityMeasure_map` `tendsto` `AEMeasurable.prodMk` `aemeasurable_const` `MeasureTheory.ProbabilityMeasure.tendsto_iff_forall_integral_tendsto` `Continuous.comp'` `ContinuousMapClass.map_continuous` `BoundedContinuousMapClass.toContinuousMapClass` `BoundedContinuousFunction.instBoundedContinuousMapClass` `Continuous.prodMk` `continuous_id'` `continuous_const` `BoundedContinuousFunction.map_bounded'` `MeasureTheory.integral_map` `Continuous.aestronglyMeasurable` `Prod.opensMeasurableSpace` `PseudoEMetricSpace.pseudoMetrizableSpace` `instSecondCountableTopologyReal` `Continuous.comp_aestronglyMeasurable` `MeasureTheory.AEStronglyMeasurable.prodMk` `aestronglyMeasurable_id` `MeasureTheory.aestronglyMeasurable_const` `sub_zero` `norm_zero` `sup_of_le_right` `sub_self`
`tendsto` 📖	mathematical	`MeasureTheory.IsProbabilityMeasure` `MeasureTheory.TendstoInDistribution`	`Filter.Tendsto` `MeasureTheory.ProbabilityMeasure` `MeasureTheory.Measure` `MeasureTheory.IsProbabilityMeasure` `MeasureTheory.Measure.map` `MeasureTheory.Measure.isProbabilityMeasure_map` `forall_aemeasurable` `nhds` `MeasureTheory.ProbabilityMeasure.instTopologicalSpace` `aemeasurable_limit`	—	—

MeasureTheory.TendstoInMeasure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tendstoInDistribution` 📖	mathematical	`MeasureTheory.TendstoInMeasure` `PseudoEMetricSpace.toEDist` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `AEMeasurable`	`MeasureTheory.TendstoInDistribution` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `BorelSpace.opensMeasurable`	—	`tendstoInDistribution_of_aemeasurable` `aemeasurable`
`tendstoInDistribution_of_aemeasurable` 📖	mathematical	`MeasureTheory.TendstoInMeasure` `PseudoEMetricSpace.toEDist` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `AEMeasurable`	`MeasureTheory.TendstoInDistribution` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `BorelSpace.opensMeasurable`	—	`MeasureTheory.tendstoInDistribution_of_tendstoInMeasure_sub` `MeasureTheory.tendstoInDistribution_const` `BorelSpace.opensMeasurable` `sub_zero`

---

← Back to Index