ProductMeasure

📁 Source: Mathlib/Probability/ProductMeasure.lean

Statistics

Metric	Count
Definitions `infinitePi`, `infinitePiNat`, `piContent`	3
Theorems `eq_infinitePi`, `infinitePiNat_map_piCongrLeft`, `infinitePiNat_map_restrict`, `infinitePi_cylinder`, `infinitePi_dirac`, `infinitePi_eq_pi`, `infinitePi_map_curry`, `infinitePi_map_curry_symm`, `infinitePi_map_eval`, `infinitePi_map_pi`, `infinitePi_map_piCongrLeft`, `infinitePi_map_piCurry`, `infinitePi_map_piCurry_symm`, `infinitePi_map_restrict`, `infinitePi_map_restrict'`, `infinitePi_pi`, `infinitePi_pi_of_countable`, `infinitePi_pi_univ`, `infinitePi_singleton`, `infinitePi_singleton_of_fintype`, `instIsProbabilityMeasureForallInfinitePi`, `instIsProbabilityMeasureForallInfinitePiNat`, `isProjectiveLimit_infinitePi`, `isProjectiveLimit_infinitePiNat`, `map_piSingleton`, `piContent_eq_infinitePiNat`, `pi_prod_map_IicProdIoc`, `pi_prod_map_IocProdIoc`, `integral_infinitePi_of_piFinset`, `integral_restrict_infinitePi`, `isProjectiveMeasureFamily_pi`, `isSigmaSubadditive_piContent`, `lintegral_infinitePi_of_piFinset`, `lintegral_restrict_infinitePi`, `partialTraj_const`, `partialTraj_const_restrict₂`, `piContent_cylinder`, `piContent_eq_measure_pi`, `piContent_tendsto_zero`, `measurePreserving_eval_infinitePi`	40
Total	43

MeasureTheory

Definitions

Name	Category	Theorems
`piContent` 📖	CompOp	6 math math: `piContent_tendsto_zero`, `piContent_cylinder`, `piContent_eq_measure_pi`, `Measure.infinitePiNat_map_piCongrLeft`, `isSigmaSubadditive_piContent`, `Measure.piContent_eq_infinitePiNat`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`integral_infinitePi_of_piFinset` 📖	mathematical	`IsProbabilityMeasure` `StronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Filtration.seq` `Finset` `PartialOrder.toPreorder` `Finset.partialOrder` `MeasurableSpace.pi` `Filtration.piFinset`	`integral` `Measure.infinitePi` `SetLike.instMembership` `Finset.instSetLike` `Measure.pi` `Finset.Subtype.fintype` `Function.updateFinset`	—	`StronglyMeasurable.dependsOn_of_piFinset` `PseudoEMetricSpace.pseudoMetrizableSpace` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `integral_congr_ae` `ae_of_all` `Measure.instOuterMeasureClass` `integral_restrict_infinitePi` `StronglyMeasurable.aestronglyMeasurable` `StronglyMeasurable.comp_measurable` `Measurable.mono` `measurable_updateFinset` `le_rfl` `Filtration.le`
`integral_restrict_infinitePi` 📖	mathematical	`IsProbabilityMeasure` `AEStronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `MeasurableSpace.pi` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Measure.pi` `Finset.Subtype.fintype`	`integral` `Measure.infinitePi` `Finset.restrict`	—	`integral_map` `Measurable.aemeasurable` `Finset.measurable_restrict` `Measure.infinitePi_map_restrict`
`isProjectiveMeasureFamily_pi` 📖	mathematical	`IsProbabilityMeasure`	`IsProjectiveMeasureFamily` `Measure.pi` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.Subtype.fintype`	—	`Measure.pi_eq` `IsFiniteMeasure.toSigmaFinite` `IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `Measure.map_apply` `Finset.measurable_restrict₂` `MeasurableSet.univ_pi` `Finite.to_countable` `Finite.of_fintype` `Finset.restrict₂_preimage` `Measure.pi_pi` `Finset.prod_eq_prod_extend` `Finset.prod_subset_one_on_sdiff` `Finset.mem_sdiff` `Function.extend_val_apply` `IsProbabilityMeasure.measure_univ`
`isSigmaSubadditive_piContent` 📖	mathematical	`IsProbabilityMeasure`	`AddContent.IsSigmaSubadditive` `measurableCylinders` `piContent`	—	`isSigmaSubadditive_of_addContent_iUnion_eq_tsum` `isSetRing_measurableCylinders` `addContent_iUnion_eq_sum_of_tendsto_zero` `projectiveFamilyContent_ne_top` `Measure.pi.instIsFiniteMeasure` `IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `isProjectiveMeasureFamily_pi` `piContent_tendsto_zero`
`lintegral_infinitePi_of_piFinset` 📖	mathematical	`IsProbabilityMeasure` `Measurable` `ENNReal` `Filtration.seq` `Finset` `PartialOrder.toPreorder` `Finset.partialOrder` `MeasurableSpace.pi` `Filtration.piFinset` `ENNReal.measurableSpace`	`lintegral` `Measure.infinitePi` `lmarginal`	—	`Measurable.dependsOn_of_piFinset` `instMeasurableSingletonClassOfMeasurableEq` `instMeasurableEqOfSecondCountableTopologyOfT2Space` `BorelSpace.opensMeasurable` `ENNReal.borelSpace` `ENNReal.instSecondCountableTopology` `ENNReal.instT2Space` `lintegral_congr_ae` `ae_of_all` `Measure.instOuterMeasureClass` `lintegral_restrict_infinitePi` `Measurable.comp` `Measurable.mono` `measurable_updateFinset` `le_rfl` `Filtration.le`
`lintegral_restrict_infinitePi` 📖	mathematical	`IsProbabilityMeasure` `Measurable` `ENNReal` `MeasurableSpace.pi` `Finset` `SetLike.instMembership` `Finset.instSetLike` `ENNReal.measurableSpace`	`lintegral` `Measure.infinitePi` `Finset.restrict` `Measure.pi` `Finset.Subtype.fintype`	—	`lintegral_map` `Finset.measurable_restrict` `Measure.isProjectiveLimit_infinitePi`
`partialTraj_const` 📖	mathematical	`IsProbabilityMeasure`	`ProbabilityTheory.Kernel.partialTraj` `ProbabilityTheory.Kernel.const` `MeasurableSpace.pi` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.Iic` `Nat.instPreorder` `LocallyFiniteOrder.toLocallyFiniteOrderBot` `Nat.instOrderBot` `Nat.instLocallyFiniteOrder` `ProbabilityTheory.Kernel.map` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Nat.instLinearOrder` `Prod.instMeasurableSpace` `Finset.Ioc` `ProbabilityTheory.Kernel.prod` `ProbabilityTheory.Kernel.id` `Measure.pi` `Finset.Subtype.fintype` `IicProdIoc`	—	`Finset.Ioc_subset_Iic_self` `ProbabilityTheory.Kernel.partialTraj_eq_prod` `ProbabilityTheory.Kernel.const.instIsSFiniteKernel` `instSFiniteOfSigmaFinite` `IsFiniteMeasure.toSigmaFinite` `IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `partialTraj_const_restrict₂`
`partialTraj_const_restrict₂` 📖	mathematical	`IsProbabilityMeasure`	`ProbabilityTheory.Kernel.map` `MeasurableSpace.pi` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.Iic` `Nat.instPreorder` `LocallyFiniteOrder.toLocallyFiniteOrderBot` `Nat.instOrderBot` `Nat.instLocallyFiniteOrder` `Finset.Ioc` `ProbabilityTheory.Kernel.partialTraj` `ProbabilityTheory.Kernel.const` `Finset.restrict₂` `Finset.Ioc_subset_Iic_self` `Measure.pi` `Finset.Subtype.fintype`	—	`Finset.Ioc_subset_Iic_self` `lt_or_ge` `Nat.le_induction` `ProbabilityTheory.Kernel.ext` `ProbabilityTheory.Kernel.partialTraj_succ_self` `ProbabilityTheory.Kernel.map_comp_right` `measurable_IicProdIoc` `Finset.measurable_restrict₂` `ProbabilityTheory.Kernel.map_apply` `Measurable.fun_comp` `ProbabilityTheory.Kernel.prod_apply` `ProbabilityTheory.Kernel.IsFiniteKernel.isSFiniteKernel` `ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel` `ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel` `ProbabilityTheory.Kernel.instIsMarkovKernelId` `ProbabilityTheory.Kernel.IsSFiniteKernel.map` `ProbabilityTheory.Kernel.const.instIsSFiniteKernel` `instSFiniteOfSigmaFinite` `IsFiniteMeasure.toSigmaFinite` `IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `MeasurableEquiv.measurable` `ProbabilityTheory.Kernel.const_apply` `Measure.map_piSingleton` `restrict₂_comp_IicProdIoc` `IsScalarTower.right` `Measure.map_snd_prod` `Measure.pi.sigmaFinite` `IsProbabilityMeasure.measure_univ` `ProbabilityTheory.IsMarkovKernel.is_probability_measure'` `one_smul` `ProbabilityTheory.Kernel.partialTraj_succ_of_le` `ProbabilityTheory.Kernel.map_const` `ProbabilityTheory.Kernel.prod_const_comp` `ProbabilityTheory.Kernel.instIsSFiniteKernelForallValNatMemFinsetIicPartialTraj` `Measure.instSFiniteMap` `ProbabilityTheory.Kernel.id_comp` `Measurable.prodMap` `measurable_id'` `measurable_IocProdIoc` `ProbabilityTheory.Kernel.map_prod_map` `ProbabilityTheory.Kernel.map_id` `Measure.pi_prod_map_IocProdIoc` `Finset.Ioc_eq_empty_of_le` `Subtype.isEmpty_false` `Measure.ext` `Subsingleton.eq_univ_of_nonempty` `Unique.instSubsingleton` `ProbabilityTheory.IsMarkovKernel.isProbabilityMeasure` `ProbabilityTheory.Kernel.IsMarkovKernel.map` `ProbabilityTheory.Kernel.instIsMarkovKernelForallValNatMemFinsetIicPartialTrajOfHAddOfNat` `ProbabilityTheory.Kernel.const.instIsMarkovKernel` `Measure.pi.instIsProbabilityMeasure` `Set.not_nonempty_iff_eq_empty` `measure_empty` `Measure.instOuterMeasureClass`
`piContent_cylinder` 📖	mathematical	`IsProbabilityMeasure` `MeasurableSet` `MeasurableSpace.pi` `Finset` `SetLike.instMembership` `Finset.instSetLike`	`DFunLike.coe` `AddContent` `ENNReal` `ENNReal.instAddCommMonoid` `measurableCylinders` `Set` `instFunLikeAddContentSet` `piContent` `cylinder` `Measure` `Measure.instFunLike` `Measure.pi` `Finset.Subtype.fintype`	—	`projectiveFamilyContent_cylinder` `isProjectiveMeasureFamily_pi`
`piContent_eq_measure_pi` 📖	mathematical	`IsProbabilityMeasure` `MeasurableSet` `MeasurableSpace.pi`	`DFunLike.coe` `AddContent` `ENNReal` `ENNReal.instAddCommMonoid` `measurableCylinders` `Set` `instFunLikeAddContentSet` `piContent` `Measure` `Measure.instFunLike` `Measure.pi`	—	`Finset.mem_univ` `piContent_cylinder` `MeasurableSet.preimage` `MeasurableEquiv.measurable` `Measure.pi_map_piCongrLeft` `IsFiniteMeasure.toSigmaFinite` `IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `Measure.map_apply`
`piContent_tendsto_zero` 📖	mathematical	`IsProbabilityMeasure` `Set` `Set.instMembership` `measurableCylinders` `Antitone` `Nat.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `Set.iInter` `Set.instEmptyCollection`	`Filter.Tendsto` `ENNReal` `DFunLike.coe` `AddContent` `ENNReal.instAddCommMonoid` `instFunLikeAddContentSet` `piContent` `Filter.atTop` `nhds` `ENNReal.instTopologicalSpace` `instZeroENNReal`	—	`nonempty_of_isProbabilityMeasure` `mem_measurableCylinders` `Function.Injective.injOn` `Subtype.val_injective` `Finset.mem_preimage` `Set.mem_iUnion` `Subtype.coe_eta` `MeasurableSet.preimage` `measurable_piCongrLeft` `MeasurableSet.of_mem_measurableCylinders` `Set.preimage_mono` `piContent_cylinder` `Measure.pi_map_piCongrLeft` `IsFiniteMeasure.toSigmaFinite` `IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `Measure.map_apply` `MeasurableEquiv.measurable` `finite_or_infinite` `piContent_eq_measure_pi` `measure_empty` `Measure.instOuterMeasureClass` `tendsto_measure_iInter_atTop` `instIsCountablyGenerated_atTop` `OrderTopology.of_linearLocallyFinite` `instDiscreteTopologyNat` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace` `Countable.LindelofSpace` `instCountableNat` `PseudoEMetricSpace.pseudoMetrizableSpace` `MeasurableSet.nullMeasurableSet` `measure_ne_top` `Measure.pi.instIsFiniteMeasure` `Set.countable_iUnion` `Finset.countable_toSet` `nonempty_equiv_of_countable` `instInfiniteNat` `Measure.infinitePiNat_map_piCongrLeft` `Measure.isFiniteMeasure_map` `Measure.instIsProbabilityMeasureForallInfinitePiNat`

MeasureTheory.Measure

Definitions

Name	Category	Theorems
`infinitePi` 📖	CompOp	34 math math: `ProbabilityTheory.iIndepFun_iff_map_fun_eq_infinitePi_map₀`, `ProbabilityTheory.iIndepFun_infinitePi`, `MeasureTheory.integral_infinitePi_of_piFinset`, `MeasureTheory.lintegral_restrict_infinitePi`, `isProjectiveLimit_infinitePi`, `infinitePi_map_piCongrLeft`, `infinitePi_map_piCurry`, `MeasureTheory.lintegral_infinitePi_of_piFinset`, `infinitePi_pi`, `ProbabilityTheory.setBernoulli_apply'`, `eq_infinitePi`, `infinitePi_singleton_of_fintype`, `infinitePi_map_eval`, `measurePreserving_eval_infinitePi`, `infinitePi_dirac`, `infinitePi_map_curry_symm`, `instIsProbabilityMeasureForallInfinitePi`, `ProbabilityTheory.iIndepFun_iff_map_fun_eq_infinitePi_map₀'`, `ProbabilityTheory.iIndepFun_uncurry_infinitePi`, `infinitePi_map_pi`, `infinitePi_cylinder`, `ProbabilityTheory.iIndepFun_uncurry_infinitePi'`, `infinitePi_singleton`, `ProbabilityTheory.iIndepFun_iff_map_fun_eq_infinitePi_map`, `infinitePi_map_restrict`, `MeasureTheory.integral_restrict_infinitePi`, `ProbabilityTheory.setBernoulli_apply`, `infinitePi_map_piCurry_symm`, `infinitePi_pi_univ`, `infinitePi_map_restrict'`, `infinitePi_pi_of_countable`, `infinitePi_map_curry`, `infinitePi_eq_pi`, `ProbabilityTheory.setBernoulli_eq_map`
`infinitePiNat` 📖	CompOp	5 math math: `infinitePiNat_map_piCongrLeft`, `isProjectiveLimit_infinitePiNat`, `infinitePiNat_map_restrict`, `instIsProbabilityMeasureForallInfinitePiNat`, `piContent_eq_infinitePiNat`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_infinitePi` 📖	mathematical	`MeasureTheory.IsProbabilityMeasure` `DFunLike.coe` `MeasureTheory.Measure` `MeasurableSpace.pi` `Set` `ENNReal` `instFunLike` `Set.pi` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.prod` `CommSemiring.toCommMonoid` `ENNReal.instCommSemiring`	`infinitePi`	—	`MeasureTheory.IsProjectiveLimit.unique` `pi.instIsFiniteMeasure` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `isProjectiveLimit_infinitePi` `pi_eq` `MeasureTheory.IsFiniteMeasure.toSigmaFinite` `map_apply` `Finset.measurable_restrict` `MeasurableSet.univ_pi` `Finite.to_countable` `Finite.of_fintype` `Finset.restrict_preimage_univ` `MeasurableSet.univ` `Finset.prod_attach` `Finset.univ_eq_attach`
`infinitePiNat_map_piCongrLeft` 📖	mathematical	`MeasureTheory.IsProbabilityMeasure` `Set` `Set.instMembership` `MeasureTheory.measurableCylinders`	`DFunLike.coe` `MeasureTheory.Measure` `MeasurableSpace.pi` `ENNReal` `instFunLike` `map` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `MeasurableEquiv` `MeasurableEquiv.instEquivLike` `MeasurableEquiv.piCongrLeft` `infinitePiNat` `MeasureTheory.AddContent` `ENNReal.instAddCommMonoid` `MeasureTheory.instFunLikeAddContentSet` `MeasureTheory.piContent`	—	`MeasureTheory.mem_measurableCylinders` `map_apply` `MeasurableEquiv.measurable` `MeasurableSet.cylinder` `MeasureTheory.cylinder.eq_1` `Set.preimage_comp` `MeasurableEquiv.coe_piCongrLeft` `Function.Injective.injOn` `Equiv.injective` `Finset.restrict_comp_piCongrLeft` `Finset.measurable_restrict` `MeasurableSet.preimage` `measurable_piCongrLeft` `infinitePiNat_map_restrict` `MeasureTheory.piContent_cylinder` `pi_map_piCongrLeft` `MeasureTheory.IsFiniteMeasure.toSigmaFinite` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure`
`infinitePiNat_map_restrict` 📖	mathematical	`MeasureTheory.IsProbabilityMeasure`	`map` `MeasurableSpace.pi` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.restrict` `infinitePiNat` `pi` `Finset.Subtype.fintype`	—	`isProjectiveLimit_infinitePiNat`
`infinitePi_cylinder` 📖	mathematical	`MeasureTheory.IsProbabilityMeasure` `MeasurableSet` `MeasurableSpace.pi` `Finset` `SetLike.instMembership` `Finset.instSetLike`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike` `infinitePi` `MeasureTheory.cylinder` `pi` `Finset.Subtype.fintype`	—	`MeasureTheory.cylinder.eq_1` `map_apply` `Finset.measurable_restrict` `infinitePi_map_restrict`
`infinitePi_dirac` 📖	mathematical	—	`infinitePi` `dirac` `MeasurableSpace.pi`	—	`eq_infinitePi` `dirac.isProbabilityMeasure` `dirac_apply'` `Set.indicator_pi_one_apply` `Finset.prod_congr`
`infinitePi_eq_pi` 📖	mathematical	`MeasureTheory.IsProbabilityMeasure`	`infinitePi` `pi`	—	`pi_eq` `MeasureTheory.IsFiniteMeasure.toSigmaFinite` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `Finset.coe_univ` `infinitePi_pi`
`infinitePi_map_curry` 📖	mathematical	`MeasureTheory.IsProbabilityMeasure`	`map` `MeasurableSpace.pi` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `MeasurableEquiv.curry` `infinitePi`	—	`MeasurableEquiv.map_apply_eq_iff_map_symm_apply_eq` `infinitePi_map_curry_symm`
`infinitePi_map_curry_symm` 📖	mathematical	`MeasureTheory.IsProbabilityMeasure`	`map` `MeasurableSpace.pi` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `MeasurableEquiv.symm` `MeasurableEquiv.curry` `infinitePi`	—	`MeasurableEquiv.map_measurableEquiv_injective` `map_map` `MeasurableEquiv.measurable` `Equiv.piCongrLeft'_symm` `infinitePi_map_piCurry_symm` `infinitePi_map_piCongrLeft`
`infinitePi_map_eval` 📖	mathematical	`MeasureTheory.IsProbabilityMeasure`	`map` `MeasurableSpace.pi` `infinitePi`	—	`MeasureTheory.MeasurePreserving.map_eq` `measurePreserving_eval_infinitePi`
`infinitePi_map_pi` 📖	mathematical	`MeasureTheory.IsProbabilityMeasure` `Measurable`	`map` `MeasurableSpace.pi` `infinitePi`	—	`isProbabilityMeasure_map` `Measurable.aemeasurable` `eq_infinitePi` `map_apply` `measurable_pi_lambda` `Measurable.fun_comp` `measurable_pi_apply` `MeasurableSet.pi` `Finset.countable_toSet` `Set.ext` `infinitePi_pi` `Finset.prod_congr`
`infinitePi_map_piCongrLeft` 📖	mathematical	`MeasureTheory.IsProbabilityMeasure`	`map` `MeasurableSpace.pi` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `MeasurableEquiv` `MeasurableEquiv.instEquivLike` `MeasurableEquiv.piCongrLeft` `infinitePi`	—	`eq_infinitePi` `Function.Injective.injOn` `Equiv.injective` `Equiv.image_preimage` `Finset.coe_preimage` `map_apply` `MeasurableEquiv.measurable` `MeasurableSet.pi` `Set.Countable.image` `Finset.countable_toSet` `MeasurableEquiv.coe_piCongrLeft` `Equiv.piCongrLeft_preimage_pi` `infinitePi_pi` `Finset.prod_equiv`
`infinitePi_map_piCurry` 📖	mathematical	`MeasureTheory.IsProbabilityMeasure`	`map` `MeasurableSpace.pi` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `MeasurableEquiv.piCurry` `infinitePi`	—	`MeasurableEquiv.map_apply_eq_iff_map_symm_apply_eq` `infinitePi_map_piCurry_symm`
`infinitePi_map_piCurry_symm` 📖	mathematical	`MeasureTheory.IsProbabilityMeasure`	`map` `MeasurableSpace.pi` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `MeasurableEquiv.symm` `MeasurableEquiv.piCurry` `infinitePi`	—	`eq_infinitePi` `map_apply` `MeasurableEquiv.measurable` `MeasurableSet.pi` `Finset.countable_toSet` `Function.Injective.injOn` `sigma_mk_injective` `MeasurableEquiv.coe_piCurry_symm` `Finset.coe_sigma` `Set.uncurry_preimage_sigma_pi` `infinitePi_pi` `instIsProbabilityMeasureForallInfinitePi` `Finset.prod_sigma` `Finset.prod_congr`
`infinitePi_map_restrict` 📖	mathematical	`MeasureTheory.IsProbabilityMeasure`	`map` `MeasurableSpace.pi` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.restrict` `infinitePi` `pi` `Finset.Subtype.fintype`	—	`isProjectiveLimit_infinitePi`
`infinitePi_map_restrict'` 📖	mathematical	`MeasureTheory.IsProbabilityMeasure`	`map` `MeasurableSpace.pi` `Set.Elem` `Set` `Set.instMembership` `Set.restrict` `infinitePi`	—	`eq_infinitePi` `map_apply` `Set.measurable_restrict` `MeasurableSet.pi` `Finset.countable_toSet` `Finset.restrict_preimage` `infinitePi_pi` `Finset.prod_image` `Finset.prod_congr`
`infinitePi_pi` 📖	mathematical	`MeasureTheory.IsProbabilityMeasure` `MeasurableSet`	`DFunLike.coe` `MeasureTheory.Measure` `MeasurableSpace.pi` `Set` `ENNReal` `instFunLike` `infinitePi` `Set.pi` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.prod` `CommSemiring.toCommMonoid` `ENNReal.instCommSemiring`	—	`Set.ext` `MeasureTheory.cylinder.eq_1` `map_apply` `Finset.measurable_restrict` `MeasurableSet.univ_pi` `Finite.to_countable` `Finite.of_fintype` `infinitePi_map_restrict` `pi_pi` `MeasureTheory.IsFiniteMeasure.toSigmaFinite` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `Finset.univ_eq_attach` `Finset.prod_attach`
`infinitePi_pi_of_countable` 📖	mathematical	`MeasureTheory.IsProbabilityMeasure` `MeasurableSet`	`DFunLike.coe` `MeasureTheory.Measure` `MeasurableSpace.pi` `Set` `ENNReal` `instFunLike` `infinitePi` `Set.pi` `tprod` `Set.Elem` `CommSemiring.toCommMonoid` `ENNReal.instCommSemiring` `ENNReal.instTopologicalSpace` `Set.instMembership` `SummationFilter.unconditional`	—	`tendsto_nhds_unique` `ENNReal.instT2Space` `Filter.atTop_neBot` `Finset.isDirected_le` `infinitePi_pi` `infinitePi_map_restrict'` `map_apply` `Set.measurable_restrict` `MeasurableSet.pi` `Finset.countable_toSet` `Finset.restrict_preimage` `Finset.coe_image` `Set.pi_iUnion_eq_iInter_pi` `Set.iUnion_finset_eq_set` `MeasureTheory.tendsto_measure_iInter_atTop` `Filter.atTop.isCountablyGenerated` `Finset.countable` `MeasurableSet.nullMeasurableSet` `Set.Countable.image` `Set.pi_mono'` `Set.instReflSubset` `Set.image_mono` `Finset.coe_singleton` `Set.image_singleton` `Set.singleton_pi` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `instIsProbabilityMeasureForallInfinitePi` `ENNReal.tprod_eq_iInf_prod` `tendsto_atTop_iInf` `LinearOrder.infConvergenceClass` `ENNReal.instOrderTopology` `Finset.prod_anti_set_of_le_one` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid` `Set.not_nonempty_iff_eq_empty'` `Set.empty_pi` `MeasureTheory.IsProbabilityMeasure.measure_univ` `tprod_empty`
`infinitePi_pi_univ` 📖	mathematical	`MeasureTheory.IsProbabilityMeasure` `MeasurableSet`	`DFunLike.coe` `MeasureTheory.Measure` `MeasurableSpace.pi` `Set` `ENNReal` `instFunLike` `infinitePi` `Set.pi` `Set.univ` `tprod` `CommSemiring.toCommMonoid` `ENNReal.instCommSemiring` `ENNReal.instTopologicalSpace` `SummationFilter.unconditional`	—	`infinitePi_pi_of_countable` `tprod_univ`
`infinitePi_singleton` 📖	mathematical	`MeasureTheory.IsProbabilityMeasure` `MeasurableSingletonClass`	`DFunLike.coe` `MeasureTheory.Measure` `MeasurableSpace.pi` `Set` `ENNReal` `instFunLike` `infinitePi` `Set.instSingletonSet` `tprod` `CommSemiring.toCommMonoid` `ENNReal.instCommSemiring` `ENNReal.instTopologicalSpace` `SummationFilter.unconditional`	—	`Set.univ_pi_singleton` `infinitePi_pi_univ`
`infinitePi_singleton_of_fintype` 📖	mathematical	`MeasureTheory.IsProbabilityMeasure` `MeasurableSingletonClass`	`DFunLike.coe` `MeasureTheory.Measure` `MeasurableSpace.pi` `Set` `ENNReal` `instFunLike` `infinitePi` `Set.instSingletonSet` `Finset.prod` `CommSemiring.toCommMonoid` `ENNReal.instCommSemiring` `Finset.univ`	—	`infinitePi_singleton` `Finite.to_countable` `Finite.of_fintype` `tprod_fintype` `SummationFilter.instLeAtTopUnconditional`
`instIsProbabilityMeasureForallInfinitePi` 📖	mathematical	`MeasureTheory.IsProbabilityMeasure`	`MeasurableSpace.pi` `infinitePi`	—	`MeasureTheory.cylinder_univ` `MeasureTheory.cylinder.eq_1` `map_apply` `Finset.measurable_restrict` `MeasurableSet.univ` `infinitePi_map_restrict` `MeasureTheory.IsProbabilityMeasure.measure_univ` `pi.instIsProbabilityMeasure`
`instIsProbabilityMeasureForallInfinitePiNat` 📖	mathematical	`MeasureTheory.IsProbabilityMeasure`	`MeasurableSpace.pi` `infinitePiNat`	—	`infinitePiNat.eq_1` `instIsProbabilityMeasureBindCoeKernelOfIsMarkovKernel` `pi.instIsProbabilityMeasure` `ProbabilityTheory.Kernel.instIsMarkovKernelForallValNatMemFinsetIicForallTraj`
`isProjectiveLimit_infinitePi` 📖	mathematical	`MeasureTheory.IsProbabilityMeasure`	`MeasureTheory.IsProjectiveLimit` `infinitePi` `pi` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.Subtype.fintype`	—	`ext` `map_apply` `Finset.measurable_restrict` `MeasureTheory.isSetSemiring_measurableCylinders` `MeasureTheory.isSigmaSubadditive_piContent` `infinitePi.eq_1` `Eq.le` `MeasureTheory.generateFrom_measurableCylinders` `MeasureTheory.AddContent.measure_eq` `MeasureTheory.cylinder_mem_measurableCylinders` `MeasureTheory.cylinder.eq_1` `MeasureTheory.piContent_cylinder`
`isProjectiveLimit_infinitePiNat` 📖	mathematical	`MeasureTheory.IsProbabilityMeasure`	`MeasureTheory.IsProjectiveLimit` `infinitePiNat` `pi` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.Subtype.fintype`	—	`Finset.subset_Iic_sup_id` `MeasureTheory.isProjectiveMeasureFamily_pi` `Finset.restrict₂_comp_restrict` `map_map` `Finset.measurable_restrict₂` `Finset.measurable_restrict` `Preorder.frestrictLe.eq_1` `infinitePiNat.eq_1` `map_comp` `Preorder.measurable_frestrictLe` `ProbabilityTheory.Kernel.traj_map_frestrictLe` `MeasureTheory.partialTraj_const` `measurable_IicProdIoc` `compProd_eq_comp_prod` `MeasureTheory.instSFiniteOfSigmaFinite` `pi.sigmaFinite` `MeasureTheory.IsFiniteMeasure.toSigmaFinite` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `ProbabilityTheory.Kernel.const.instIsSFiniteKernel` `compProd_const` `pi_prod_map_IicProdIoc`
`map_piSingleton` 📖	mathematical	`MeasureTheory.SigmaFinite`	`map` `MeasurableSpace.pi` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.Ioc` `Nat.instPreorder` `Nat.instLocallyFiniteOrder` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `MeasurableEquiv.piSingleton` `pi` `Finset.Subtype.fintype`	—	`pi_eq` `Nat.Ioc_succ_singleton` `Unique.instSubsingleton` `Finset.mem_Ioc` `Fintype.prod_subsingleton` `map_apply` `MeasurableEquiv.measurable` `MeasurableSet.univ_pi` `Subtype.countable` `instCountableNat` `Set.ext`
`piContent_eq_infinitePiNat` 📖	mathematical	`MeasureTheory.IsProbabilityMeasure` `Set` `Set.instMembership` `MeasureTheory.measurableCylinders`	`DFunLike.coe` `MeasureTheory.AddContent` `ENNReal` `ENNReal.instAddCommMonoid` `MeasureTheory.instFunLikeAddContentSet` `MeasureTheory.piContent` `MeasureTheory.Measure` `MeasurableSpace.pi` `instFunLike` `infinitePiNat`	—	`MeasureTheory.piContent_cylinder` `MeasureTheory.cylinder.eq_1` `map_apply` `Finset.measurable_restrict` `infinitePiNat_map_restrict`
`pi_prod_map_IicProdIoc` 📖	mathematical	`MeasureTheory.IsProbabilityMeasure`	`map` `Prod.instMeasurableSpace` `MeasurableSpace.pi` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.Iic` `Nat.instPreorder` `LocallyFiniteOrder.toLocallyFiniteOrderBot` `Nat.instOrderBot` `Nat.instLocallyFiniteOrder` `Finset.Ioc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Nat.instLinearOrder` `IicProdIoc` `prod` `pi` `Finset.Subtype.fintype`	—	`le_total` `pi_eq` `MeasureTheory.IsFiniteMeasure.toSigmaFinite` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `map_apply` `measurable_IicProdIoc` `MeasurableSet.univ_pi` `Subtype.countable` `instCountableNat` `Finset.Ioc_subset_Iic_self` `IicProdIoc_preimage` `prod_prod` `MeasureTheory.instSFiniteOfSigmaFinite` `pi.sigmaFinite` `pi_pi` `Finset.prod_eq_prod_extend` `Finset.Iic_union_Ioc_eq_Iic` `Finset.prod_union` `Finset.Iic_disjoint_Ioc` `le_rfl` `Finset.prod_congr` `Function.extend_val_apply` `Finset.Iic_subset_Iic` `Preorder.frestrictLe₂.eq_1` `Finset.restrict₂.eq_1` `IicProdIoc_le` `map_map` `Preorder.measurable_frestrictLe₂` `Measurable.fst` `measurable_id'` `fst.eq_1` `fst_prod` `pi.instIsProbabilityMeasure` `MeasureTheory.isProjectiveMeasureFamily_pi`
`pi_prod_map_IocProdIoc` 📖	mathematical	`MeasureTheory.IsProbabilityMeasure`	`map` `Prod.instMeasurableSpace` `MeasurableSpace.pi` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.Ioc` `Nat.instPreorder` `Nat.instLocallyFiniteOrder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Nat.instLinearOrder` `IocProdIoc` `prod` `pi` `Finset.Subtype.fintype`	—	`pi_eq` `MeasureTheory.IsFiniteMeasure.toSigmaFinite` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `map_apply` `measurable_IocProdIoc` `MeasurableSet.univ_pi` `Subtype.countable` `instCountableNat` `Finset.Ioc_subset_Ioc_right` `Finset.Ioc_subset_Ioc_left` `IocProdIoc_preimage` `prod_prod` `MeasureTheory.instSFiniteOfSigmaFinite` `pi.sigmaFinite` `pi_pi` `Finset.prod_eq_prod_extend` `Finset.Ioc_union_Ioc_eq_Ioc` `Finset.prod_union` `Finset.Ioc_disjoint_Ioc_of_le` `le_rfl` `Finset.prod_congr` `Function.extend_val_apply` `Finset.restrict₂.eq_1`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`measurePreserving_eval_infinitePi` 📖	mathematical	`MeasureTheory.IsProbabilityMeasure`	`MeasureTheory.MeasurePreserving` `MeasurableSpace.pi` `Function.eval` `MeasureTheory.Measure.infinitePi`	—	`measurable_pi_apply` `MeasureTheory.Measure.ext` `MeasureTheory.Measure.map_map` `Finset.measurable_restrict` `MeasureTheory.Measure.infinitePi_map_restrict` `MeasureTheory.MeasurePreserving.map_eq` `MeasureTheory.measurePreserving_eval`

---

← Back to Index