IdentDistrib

📁 Source: Mathlib/Probability/IdentDistrib.lean

Statistics

Metric	Count
Definitions `IdentDistrib`	1
Theorems `identDistrib_mk`, `identDistrib_mk`, `identDistrib`, `add_const`, `ae_mem_snd`, `ae_snd`, `aemeasurable_fst`, `aemeasurable_snd`, `aestronglyMeasurable_fst`, `aestronglyMeasurable_iff`, `aestronglyMeasurable_snd`, `coe_nnreal_ennreal`, `comp`, `comp_of_aemeasurable`, `const_add`, `const_div`, `const_mul`, `const_sub`, `div_const`, `eLpNorm_eq`, `essSup_eq`, `evariance_eq`, `hasLaw`, `integrable_iff`, `integrable_snd`, `integral_eq`, `inv`, `lintegral_eq`, `map_eq`, `measure_mem_eq`, `measure_preimage_eq`, `memLp_iff`, `memLp_snd`, `mul_const`, `neg`, `nnnorm`, `norm`, `of_ae_eq`, `pow`, `refl`, `sq`, `sub_const`, `trans`, `variance_eq`, `uniformIntegrable_of_identDistrib`, `uniformIntegrable_of_identDistrib_aux`, `indepFun_of_identDistrib_pair`	47
Total	48

MeasureTheory.AEMeasurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`identDistrib_mk` 📖	mathematical	`AEMeasurable`	`ProbabilityTheory.IdentDistrib`	—	`ProbabilityTheory.IdentDistrib.of_ae_eq`

MeasureTheory.AEStronglyMeasurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`identDistrib_mk` 📖	mathematical	`MeasureTheory.AEStronglyMeasurable`	`ProbabilityTheory.IdentDistrib`	—	`ProbabilityTheory.IdentDistrib.of_ae_eq` `aemeasurable`

ProbabilityTheory

Definitions

Name	Category	Theorems
`IdentDistrib` 📖	CompData	6 math math: `HasLaw.identDistrib`, `MeasureTheory.AEStronglyMeasurable.identDistrib_mk`, `IdentDistrib.of_ae_eq`, `identDistrib_iff_forall_finset_identDistrib`, `IdentDistrib.refl`, `MeasureTheory.AEMeasurable.identDistrib_mk`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`indepFun_of_identDistrib_pair` 📖	—	`IndepFun` `IdentDistrib` `Prod.instMeasurableSpace`	—	—	`indepFun_iff_map_prod_eq_prod_map_map` `AEMeasurable.comp_aemeasurable` `Measurable.aemeasurable` `measurable_fst` `IdentDistrib.aemeasurable_snd` `measurable_snd` `IdentDistrib.map_eq` `IdentDistrib.aemeasurable_fst` `IdentDistrib.comp`

ProbabilityTheory.HasLaw

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`identDistrib` 📖	mathematical	`ProbabilityTheory.HasLaw`	`ProbabilityTheory.IdentDistrib`	—	`aemeasurable` `map_eq`

ProbabilityTheory.IdentDistrib

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_const` 📖	—	`ProbabilityTheory.IdentDistrib`	—	—	`comp` `MeasurableAdd.measurable_add_const`
`ae_mem_snd` 📖	—	`ProbabilityTheory.IdentDistrib` `MeasurableSet` `Filter.Eventually` `Set` `Set.instMembership` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	—	`MeasureTheory.Measure.instOuterMeasureClass` `ae_snd`
`ae_snd` 📖	—	`ProbabilityTheory.IdentDistrib` `MeasurableSet` `setOf` `Filter.Eventually` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	—	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.ae_map_iff` `aemeasurable_snd` `map_eq` `aemeasurable_fst`
`aemeasurable_fst` 📖	mathematical	`ProbabilityTheory.IdentDistrib`	`AEMeasurable`	—	—
`aemeasurable_snd` 📖	mathematical	`ProbabilityTheory.IdentDistrib`	`AEMeasurable`	—	—
`aestronglyMeasurable_fst` 📖	mathematical	`ProbabilityTheory.IdentDistrib`	`MeasureTheory.AEStronglyMeasurable`	—	`AEMeasurable.aestronglyMeasurable` `aemeasurable_fst`
`aestronglyMeasurable_iff` 📖	mathematical	`ProbabilityTheory.IdentDistrib`	`MeasureTheory.AEStronglyMeasurable`	—	`aestronglyMeasurable_snd` `symm`
`aestronglyMeasurable_snd` 📖	—	`ProbabilityTheory.IdentDistrib` `MeasureTheory.AEStronglyMeasurable`	—	—	`MeasureTheory.Measure.instOuterMeasureClass` `aestronglyMeasurable_iff_aemeasurable_separable` `aemeasurable_snd` `TopologicalSpace.IsSeparable.closure` `ae_mem_snd` `IsClosed.measurableSet` `BorelSpace.opensMeasurable` `isClosed_closure` `Filter.mp_mem` `Filter.univ_mem'` `subset_closure`
`coe_nnreal_ennreal` 📖	mathematical	`ProbabilityTheory.IdentDistrib` `NNReal` `NNReal.measurableSpace`	`ENNReal` `ENNReal.measurableSpace` `ENNReal.ofNNReal`	—	`comp` `measurable_coe_nnreal_ennreal`
`comp` 📖	—	`ProbabilityTheory.IdentDistrib` `Measurable`	—	—	`comp_of_aemeasurable` `Measurable.aemeasurable`
`comp_of_aemeasurable` 📖	—	`ProbabilityTheory.IdentDistrib` `AEMeasurable` `MeasureTheory.Measure.map`	—	—	`AEMeasurable.comp_aemeasurable` `aemeasurable_fst` `map_eq` `aemeasurable_snd` `AEMeasurable.map_map_of_aemeasurable`
`const_add` 📖	—	`ProbabilityTheory.IdentDistrib`	—	—	`comp` `MeasurableAdd.measurable_const_add`
`const_div` 📖	—	`ProbabilityTheory.IdentDistrib`	—	—	`comp` `MeasurableDiv.measurable_const_div`
`const_mul` 📖	—	`ProbabilityTheory.IdentDistrib`	—	—	`comp` `MeasurableMul.measurable_const_mul`
`const_sub` 📖	—	`ProbabilityTheory.IdentDistrib`	—	—	`comp` `MeasurableSub.measurable_const_sub`
`div_const` 📖	—	`ProbabilityTheory.IdentDistrib`	—	—	`comp` `MeasurableDiv.measurable_div_const`
`eLpNorm_eq` 📖	mathematical	`ProbabilityTheory.IdentDistrib`	`MeasureTheory.eLpNorm` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm`	—	`MeasureTheory.eLpNorm_exponent_zero` `essSup_eq` `BorelSpace.opensMeasurable` `ENNReal.borelSpace` `OrderTopology.to_orderClosedTopology` `ENNReal.instOrderTopology` `comp` `Measurable.comp` `measurable_coe_nnreal_ennreal` `measurable_nnnorm` `MeasureTheory.eLpNorm_eq_eLpNorm'` `one_div` `lintegral_eq` `Measurable.pow_const` `ENNReal.hasMeasurablePow`
`essSup_eq` 📖	mathematical	`ProbabilityTheory.IdentDistrib`	`essSup` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`measure_mem_eq` `measurableSet_Ioi` `instClosedIicTopology` `essSup_eq_sInf`
`evariance_eq` 📖	mathematical	`ProbabilityTheory.IdentDistrib` `Real` `Real.measurableSpace`	`ProbabilityTheory.evariance`	—	`integral_eq` `Real.borelSpace` `lintegral_eq` `sq` `Monoid.measurablePow` `ENNReal.instMeasurableMul₂` `coe_nnreal_ennreal` `nnnorm` `BorelSpace.opensMeasurable` `sub_const` `ContinuousSub.measurableSub` `IsTopologicalAddGroup.to_continuousSub` `instIsTopologicalAddGroupReal`
`hasLaw` 📖	—	`ProbabilityTheory.IdentDistrib` `ProbabilityTheory.HasLaw`	—	—	`aemeasurable_snd` `ProbabilityTheory.HasLaw.map_eq` `map_eq`
`integrable_iff` 📖	mathematical	`ProbabilityTheory.IdentDistrib`	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`integrable_snd` `symm`
`integrable_snd` 📖	—	`ProbabilityTheory.IdentDistrib` `MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	—	`MeasureTheory.memLp_one_iff_integrable` `memLp_snd`
`integral_eq` 📖	mathematical	`ProbabilityTheory.IdentDistrib`	`MeasureTheory.integral`	—	`MeasureTheory.Measure.instOuterMeasureClass` `aestronglyMeasurable_iff_aemeasurable_separable` `PseudoEMetricSpace.pseudoMetrizableSpace` `aemeasurable_id` `TopologicalSpace.IsSeparable.closure` `MeasureTheory.ae_map_iff` `aemeasurable_fst` `IsClosed.measurableSet` `BorelSpace.opensMeasurable` `isClosed_closure` `Filter.mp_mem` `Filter.univ_mem'` `subset_closure` `MeasureTheory.integral_map` `aemeasurable_snd` `map_eq` `MeasureTheory.integral_non_aestronglyMeasurable` `aestronglyMeasurable_iff`
`inv` 📖	mathematical	`ProbabilityTheory.IdentDistrib`	`Pi.instInv`	—	`comp` `MeasurableInv.measurable_inv`
`lintegral_eq` 📖	mathematical	`ProbabilityTheory.IdentDistrib` `ENNReal` `ENNReal.measurableSpace`	`MeasureTheory.lintegral`	—	`MeasureTheory.lintegral_map'` `aemeasurable_id` `aemeasurable_fst` `aemeasurable_snd` `map_eq`
`map_eq` 📖	mathematical	`ProbabilityTheory.IdentDistrib`	`MeasureTheory.Measure.map`	—	—
`measure_mem_eq` 📖	mathematical	`ProbabilityTheory.IdentDistrib` `MeasurableSet`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `Set.preimage`	—	`MeasureTheory.Measure.map_apply_of_aemeasurable` `aemeasurable_fst` `aemeasurable_snd` `map_eq`
`measure_preimage_eq` 📖	mathematical	`ProbabilityTheory.IdentDistrib` `MeasurableSet`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `Set.preimage`	—	`measure_mem_eq`
`memLp_iff` 📖	mathematical	`ProbabilityTheory.IdentDistrib`	`MeasureTheory.MemLp` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`memLp_snd` `symm`
`memLp_snd` 📖	—	`ProbabilityTheory.IdentDistrib` `MeasureTheory.MemLp` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	—	`aestronglyMeasurable_snd` `PseudoEMetricSpace.pseudoMetrizableSpace` `MeasureTheory.MemLp.aestronglyMeasurable` `eLpNorm_eq` `BorelSpace.opensMeasurable`
`mul_const` 📖	—	`ProbabilityTheory.IdentDistrib`	—	—	`comp` `MeasurableMul.measurable_mul_const`
`neg` 📖	mathematical	`ProbabilityTheory.IdentDistrib`	`Pi.instNeg`	—	`comp` `MeasurableNeg.measurable_neg`
`nnnorm` 📖	mathematical	`ProbabilityTheory.IdentDistrib`	`NNReal` `NNReal.measurableSpace` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`comp` `measurable_nnnorm`
`norm` 📖	mathematical	`ProbabilityTheory.IdentDistrib`	`Real` `Real.measurableSpace` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`comp` `measurable_norm`
`of_ae_eq` 📖	mathematical	`AEMeasurable` `Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	`ProbabilityTheory.IdentDistrib`	—	`MeasureTheory.Measure.instOuterMeasureClass` `AEMeasurable.congr` `MeasureTheory.Measure.map_congr`
`pow` 📖	—	`ProbabilityTheory.IdentDistrib`	—	—	`comp` `Measurable.pow_const` `measurable_id`
`refl` 📖	mathematical	`AEMeasurable`	`ProbabilityTheory.IdentDistrib`	—	—
`sq` 📖	—	`ProbabilityTheory.IdentDistrib`	—	—	`comp` `Measurable.pow_const` `measurable_id`
`sub_const` 📖	—	`ProbabilityTheory.IdentDistrib`	—	—	`comp` `MeasurableSub.measurable_sub_const`
`trans` 📖	—	`ProbabilityTheory.IdentDistrib`	—	—	`aemeasurable_fst` `aemeasurable_snd` `map_eq`
`variance_eq` 📖	mathematical	`ProbabilityTheory.IdentDistrib` `Real` `Real.measurableSpace`	`ProbabilityTheory.variance`	—	`ProbabilityTheory.variance.eq_1` `evariance_eq`

ProbabilityTheory.MemLp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`uniformIntegrable_of_identDistrib` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `MeasureTheory.MemLp` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toPseudoMetricSpace` `ProbabilityTheory.IdentDistrib`	`MeasureTheory.UniformIntegrable`	—	`ProbabilityTheory.IdentDistrib.aestronglyMeasurable_iff` `PseudoEMetricSpace.pseudoMetrizableSpace` `MeasureTheory.Measure.instOuterMeasureClass` `Filter.EventuallyEq.symm` `MeasureTheory.MemLp.ae_eq` `MeasureTheory.UniformIntegrable.ae_eq` `uniformIntegrable_of_identDistrib_aux` `ProbabilityTheory.IdentDistrib.trans` `ProbabilityTheory.IdentDistrib.of_ae_eq` `MeasureTheory.StronglyMeasurable.aemeasurable` `MeasureTheory.AEStronglyMeasurable.aemeasurable`
`uniformIntegrable_of_identDistrib_aux` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `MeasureTheory.MemLp` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toPseudoMetricSpace` `MeasureTheory.StronglyMeasurable` `ProbabilityTheory.IdentDistrib`	`MeasureTheory.UniformIntegrable`	—	`MeasureTheory.uniformIntegrable_of'` `MeasureTheory.MemLp.eLpNorm_indicator_norm_ge_pos_le` `LT.lt.le` `le_trans` `le_of_eq` `Set.ext` `Real.le_toNNReal_iff_coe_le` `norm_nonneg` `MeasureTheory.eLpNorm_norm` `norm_indicator_eq_indicator_norm` `Measurable.indicator` `measurable_norm` `BorelSpace.opensMeasurable` `measurableSet_le` `NNReal.borelSpace` `OrderTopology.to_orderClosedTopology` `NNReal.instOrderTopology` `NNReal.instSecondCountableTopology` `measurable_const` `measurable_nnnorm` `Nat.cast_zero` `MeasureTheory.eLpNorm_map_measure` `Measurable.aestronglyMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `instSecondCountableTopologyReal` `Real.borelSpace` `ProbabilityTheory.IdentDistrib.aemeasurable_fst` `ProbabilityTheory.IdentDistrib.map_eq`

---

← Back to Index