Traj

📁 Source: Mathlib/Probability/Kernel/IonescuTulcea/Traj.lean

Statistics

Metric	Count
Definitions inducedFamily, traj, trajContent, trajFun, trajMeasure, iterateInduction	6
Theorems inducedFamily_Iic, instIsFiniteMeasureForallValNatMemFinsetInducedFamilyOfForallIic, instIsProbabilityMeasureForallValNatMemFinsetInducedFamilyOfForallIic, instIsZeroOrProbabilityMeasureForallValNatMemFinsetInducedFamilyOfForallIic, instSFiniteForallValNatMemFinsetInducedFamilyOfForallIic, isProjectiveLimit_nat_iff, isProjectiveLimit_nat_iff', isProjectiveMeasureFamily_inducedFamily, aestronglyMeasurable_traj, condDistrib_trajMeasure, condExp_traj, condExp_traj', eq_traj, eq_traj', instIsMarkovKernelForallValNatMemFinsetIicForallTraj, instIsProbabilityMeasureForallTrajMeasure, integrable_traj, integral_traj, integral_traj_partialTraj, integral_traj_partialTraj', isProbabilityMeasure_trajFun, isProjectiveLimit_trajFun, isProjectiveMeasureFamily_partialTraj, isSigmaSubadditive_trajContent, le_lmarginalPartialTraj_succ, lintegral_traj, lintegral_traj₀, map_frestrictLe_trajMeasure_compProd_eq_map_trajMeasure, map_traj_succ_self, measurable_trajFun, partialTraj_compProd_eq_map_traj, partialTraj_compProd_traj, setIntegral_traj_partialTraj, setIntegral_traj_partialTraj', trajContent_cylinder, trajContent_eq_lmarginalPartialTraj, trajContent_ne_top, trajContent_tendsto_zero, traj_apply, traj_comp_partialTraj, traj_eq_prod, traj_map_frestrictLe, traj_map_frestrictLe_apply, traj_map_frestrictLe_of_le, traj_map_updateFinset, frestrictLe_iterateInduction	46
Total	52

MeasureTheory

Definitions

Name	Category	Theorems
inducedFamily 📖	CompOp	8 math math: instSFiniteForallValNatMemFinsetInducedFamilyOfForallIic, isProjectiveMeasureFamily_inducedFamily, inducedFamily_Iic, instIsProbabilityMeasureForallValNatMemFinsetInducedFamilyOfForallIic, instIsFiniteMeasureForallValNatMemFinsetInducedFamilyOfForallIic, ProbabilityTheory.Kernel.isProjectiveLimit_trajFun, ProbabilityTheory.Kernel.isProjectiveMeasureFamily_partialTraj, instIsZeroOrProbabilityMeasureForallValNatMemFinsetInducedFamilyOfForallIic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inducedFamily_Iic 📖	mathematical	—	inducedFamily Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	—	inducedFamily.eq_1 Finset.sup_Iic Finset.restrict₂.eq_1
instIsFiniteMeasureForallValNatMemFinsetInducedFamilyOfForallIic 📖	mathematical	IsFiniteMeasure MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	IsFiniteMeasure MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike inducedFamily	—	inducedFamily.eq_1 Measure.isFiniteMeasure_map
instIsProbabilityMeasureForallValNatMemFinsetInducedFamilyOfForallIic 📖	mathematical	IsProbabilityMeasure MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	IsProbabilityMeasure MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike inducedFamily	—	inducedFamily.eq_1 Measure.isProbabilityMeasure_map Measurable.aemeasurable Finset.measurable_restrict₂
instIsZeroOrProbabilityMeasureForallValNatMemFinsetInducedFamilyOfForallIic 📖	mathematical	IsZeroOrProbabilityMeasure MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	IsZeroOrProbabilityMeasure MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike inducedFamily	—	inducedFamily.eq_1 instIsZeroOrProbabilityMeasureMap
instSFiniteForallValNatMemFinsetInducedFamilyOfForallIic 📖	mathematical	SFinite MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	SFinite MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike inducedFamily	—	inducedFamily.eq_1 Measure.instSFiniteMap
isProjectiveLimit_nat_iff 📖	mathematical	IsProjectiveMeasureFamily	IsProjectiveLimit Measure.map MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder Preorder.frestrictLe	—	isProjectiveLimit_nat_iff' Nat.instCanonicallyOrderedAdd
isProjectiveLimit_nat_iff' 📖	mathematical	IsProjectiveMeasureFamily	IsProjectiveLimit Measure.map MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder Preorder.frestrictLe	—	HasSubset.Subset.trans Finset.instIsTransSubset Finset.subset_Iic_sup_id Finset.Iic_subset_Iic le_max_left Finset.restrict₂_comp_restrict Measure.map_map Finset.measurable_restrict₂ Finset.measurable_restrict Preorder.frestrictLe.eq_1 le_max_right
isProjectiveMeasureFamily_inducedFamily 📖	mathematical	Measure.map MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder Preorder.frestrictLe₂	IsProjectiveMeasureFamily inducedFamily	—	Finset.sup_mono Measure.map_map Finset.measurable_restrict₂ HasSubset.Subset.trans Finset.instIsTransSubset Finset.restrict₂_comp_restrict₂ Finset.subset_Iic_sup_id Finset.Iic_subset_Iic Preorder.frestrictLe₂.eq_def

ProbabilityTheory.Kernel

Definitions

Name	Category	Theorems
traj 📖	CompOp	24 math math: condExp_traj', eq_traj, eq_traj', traj_map_updateFinset, integral_traj_partialTraj', aestronglyMeasurable_traj, partialTraj_compProd_traj, traj_comp_partialTraj, lintegral_traj, condExp_traj, traj_map_frestrictLe_of_le, instIsMarkovKernelForallValNatMemFinsetIicForallTraj, integral_traj_partialTraj, traj_apply, integrable_traj, traj_map_frestrictLe, integral_traj, traj_map_frestrictLe_apply, map_traj_succ_self, setIntegral_traj_partialTraj, lintegral_traj₀, partialTraj_compProd_eq_map_traj, setIntegral_traj_partialTraj', traj_eq_prod
trajContent 📖	CompOp	4 math math: trajContent_cylinder, isSigmaSubadditive_trajContent, trajContent_tendsto_zero, trajContent_eq_lmarginalPartialTraj
trajFun 📖	CompOp	4 math math: isProbabilityMeasure_trajFun, measurable_trajFun, isProjectiveLimit_trajFun, traj_apply
trajMeasure 📖	CompOp	3 math math: map_frestrictLe_trajMeasure_compProd_eq_map_trajMeasure, instIsProbabilityMeasureForallTrajMeasure, condDistrib_trajMeasure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aestronglyMeasurable_traj 📖	mathematical	ProbabilityTheory.IsMarkovKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder MeasureTheory.AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike traj	Filter.Eventually MeasureTheory.AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasurableSpace.pi DFunLike.coe ProbabilityTheory.Kernel Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder MeasureTheory.Measure instFunLike traj MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass partialTraj	—	MeasureTheory.AEStronglyMeasurable.comp traj_comp_partialTraj
condDistrib_trajMeasure 📖	mathematical	ProbabilityTheory.IsMarkovKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	Filter.EventuallyEq MeasureTheory.Measure MeasureTheory.ae MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.map Preorder.frestrictLe trajMeasure DFunLike.coe ProbabilityTheory.Kernel instFunLike ProbabilityTheory.condDistrib MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure instIsProbabilityMeasureForallTrajMeasure	—	ProbabilityTheory.condDistrib_ae_eq_of_measure_eq_compProd_of_measurable MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure instIsProbabilityMeasureForallTrajMeasure Preorder.measurable_frestrictLe measurable_pi_apply ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel map_frestrictLe_trajMeasure_compProd_eq_map_trajMeasure
condExp_traj 📖	mathematical	ProbabilityTheory.IsMarkovKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike traj	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasurableSpace.pi MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe ProbabilityTheory.Kernel Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder instFunLike traj MeasureTheory.condExp MeasureTheory.Filtration.seq MeasureTheory.Filtration.piLE MeasureTheory.integral Preorder.frestrictLe	—	map_apply Preorder.measurable_frestrictLe traj_map_frestrictLe MeasureTheory.Integrable.integral_comp traj_comp_partialTraj Filter.EventuallyEq.symm MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.ae_eq_condExp_of_forall_setIntegral_eq MeasureTheory.Filtration.le MeasureTheory.sigmaFinite_of_sigmaFiniteFiltration MeasureTheory.IsFiniteMeasure.sigmaFiniteFiltration ProbabilityTheory.IsFiniteKernel.isFiniteMeasure ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelForallValNatMemFinsetIicForallTraj MeasureTheory.Integrable.integrableOn MeasureTheory.Integrable.comp_aemeasurable Measurable.aemeasurable MeasureTheory.Filtration.piLE_eq_comap_frestrictLe MeasureTheory.setIntegral_map setIntegral_traj_partialTraj MeasureTheory.AEStronglyMeasurable.comp_ae_measurable'
condExp_traj' 📖	mathematical	ProbabilityTheory.IsMarkovKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasurableSpace.pi MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe ProbabilityTheory.Kernel Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder instFunLike traj MeasureTheory.condExp MeasureTheory.Filtration.seq MeasureTheory.Filtration.piLE MeasureTheory.integral partialTraj Preorder.frestrictLe Function.updateFinset	—	MeasureTheory.integrable_condExp MeasureTheory.StronglyMeasurable.mono MeasureTheory.stronglyMeasurable_condExp MeasureTheory.Filtration.le Filter.mp_mem MeasureTheory.Measure.instOuterMeasureClass condExp_traj MeasureTheory.Filtration.condExp_condExp MeasureTheory.sigmaFinite_of_sigmaFiniteFiltration MeasureTheory.IsFiniteMeasure.sigmaFiniteFiltration ProbabilityTheory.IsFiniteKernel.isFiniteMeasure ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelForallValNatMemFinsetIicForallTraj Filter.univ_mem' traj_map_frestrictLe map_apply Preorder.measurable_frestrictLe MeasureTheory.integral_map Measurable.aemeasurable MeasureTheory.StronglyMeasurable.aestronglyMeasurable MeasureTheory.StronglyMeasurable.comp_measurable measurable_updateFinset MeasureTheory.StronglyMeasurable.dependsOn_of_piLE PseudoEMetricSpace.pseudoMetrizableSpace T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace
eq_traj 📖	mathematical	ProbabilityTheory.IsMarkovKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder map Preorder.frestrictLe partialTraj	traj	—	eq_traj'
eq_traj' 📖	mathematical	ProbabilityTheory.IsMarkovKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder map Preorder.frestrictLe partialTraj	traj	—	ext MeasureTheory.IsProjectiveLimit.unique MeasureTheory.instIsFiniteMeasureForallValNatMemFinsetInducedFamilyOfForallIic ProbabilityTheory.IsFiniteKernel.isFiniteMeasure instIsFiniteKernelForallValNatMemFinsetIicPartialTrajOfHAddOfNat ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel isProjectiveLimit_trajFun MeasureTheory.isProjectiveLimit_nat_iff' isProjectiveMeasureFamily_partialTraj MeasureTheory.inducedFamily_Iic map_apply Preorder.measurable_frestrictLe
instIsMarkovKernelForallValNatMemFinsetIicForallTraj 📖	mathematical	ProbabilityTheory.IsMarkovKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	ProbabilityTheory.IsMarkovKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder traj	—	isProbabilityMeasure_trajFun
instIsProbabilityMeasureForallTrajMeasure 📖	mathematical	ProbabilityTheory.IsMarkovKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	MeasureTheory.IsProbabilityMeasure MeasurableSpace.pi trajMeasure	—	trajMeasure.eq_1 MeasureTheory.Measure.isProbabilityMeasure_map Measurable.aemeasurable MeasurableEquiv.measurable MeasureTheory.Measure.instIsProbabilityMeasureBindCoeKernelOfIsMarkovKernel instIsMarkovKernelForallValNatMemFinsetIicForallTraj
integrable_traj 📖	mathematical	ProbabilityTheory.IsMarkovKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike traj	Filter.Eventually MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup MeasurableSpace.pi DFunLike.coe ProbabilityTheory.Kernel Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder MeasureTheory.Measure instFunLike traj Preorder.frestrictLe MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	MeasureTheory.ae_of_ae_map Measurable.aemeasurable Preorder.measurable_frestrictLe MeasureTheory.Measure.instOuterMeasureClass traj_map_frestrictLe map_apply ProbabilityTheory.integrable_comp_iff MeasureTheory.Integrable.aestronglyMeasurable traj_comp_partialTraj
integral_traj 📖	mathematical	ProbabilityTheory.IsMarkovKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder MeasureTheory.AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike traj	MeasureTheory.integral MeasurableSpace.pi DFunLike.coe ProbabilityTheory.Kernel Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder MeasureTheory.Measure instFunLike traj Function.updateFinset	—	traj_map_updateFinset MeasureTheory.integral_map Measurable.aemeasurable measurable_updateFinset_left
integral_traj_partialTraj 📖	mathematical	ProbabilityTheory.IsMarkovKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike traj	MeasureTheory.integral MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike partialTraj traj	—	integral_traj_partialTraj' MeasureTheory.Integrable.comp_measurable MeasureTheory.Measure.snd_compProd ProbabilityTheory.IsSFiniteKernel.sFinite instIsSFiniteKernelForallValNatMemFinsetIicPartialTraj IsFiniteKernel.isSFiniteKernel ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelForallValNatMemFinsetIicForallTraj comp_apply traj_comp_partialTraj measurable_snd
integral_traj_partialTraj' 📖	mathematical	ProbabilityTheory.IsMarkovKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Prod.instMeasurableSpace MeasureTheory.Measure.compProd DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike partialTraj traj	MeasureTheory.integral MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike partialTraj traj Preorder.frestrictLe	—	MeasureTheory.Measure.integral_compProd ProbabilityTheory.IsSFiniteKernel.sFinite instIsSFiniteKernelForallValNatMemFinsetIicPartialTraj IsFiniteKernel.isSFiniteKernel ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelForallValNatMemFinsetIicForallTraj partialTraj_compProd_traj MeasureTheory.integral_map AEMeasurable.prodMk Measurable.aemeasurable Preorder.measurable_frestrictLe aemeasurable_id
isProbabilityMeasure_trajFun 📖	mathematical	ProbabilityTheory.IsMarkovKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	MeasureTheory.IsProbabilityMeasure MeasurableSpace.pi trajFun	—	MeasureTheory.cylinder_univ MeasureTheory.isSetSemiring_measurableCylinders isSigmaSubadditive_trajContent trajFun.eq_1 Eq.le MeasureTheory.generateFrom_measurableCylinders MeasureTheory.AddContent.measure_eq MeasureTheory.cylinder_mem_measurableCylinders MeasurableSet.univ trajContent_cylinder MeasureTheory.IsProbabilityMeasure.measure_univ ProbabilityTheory.IsMarkovKernel.is_probability_measure' instIsMarkovKernelForallValNatMemFinsetIicPartialTrajOfHAddOfNat
isProjectiveLimit_trajFun 📖	mathematical	ProbabilityTheory.IsMarkovKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	MeasureTheory.IsProjectiveLimit trajFun MeasureTheory.inducedFamily DFunLike.coe ProbabilityTheory.Kernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder MeasureTheory.Measure instFunLike partialTraj	—	MeasureTheory.isProjectiveLimit_nat_iff isProjectiveMeasureFamily_partialTraj MeasureTheory.Measure.ext MeasureTheory.Measure.map_apply Preorder.measurable_frestrictLe MeasureTheory.isSetSemiring_measurableCylinders isSigmaSubadditive_trajContent trajFun.eq_1 Eq.le MeasureTheory.generateFrom_measurableCylinders MeasureTheory.AddContent.measure_eq MeasureTheory.cylinder_mem_measurableCylinders trajContent.eq_1 MeasureTheory.projectiveFamilyContent_congr
isProjectiveMeasureFamily_partialTraj 📖	mathematical	ProbabilityTheory.IsMarkovKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	MeasureTheory.IsProjectiveMeasureFamily MeasureTheory.inducedFamily DFunLike.coe ProbabilityTheory.Kernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder MeasureTheory.Measure instFunLike partialTraj	—	MeasureTheory.isProjectiveMeasureFamily_inducedFamily partialTraj_map_frestrictLe₂_apply
isSigmaSubadditive_trajContent 📖	mathematical	ProbabilityTheory.IsMarkovKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	MeasureTheory.AddContent.IsSigmaSubadditive MeasureTheory.measurableCylinders trajContent	—	MeasureTheory.isSigmaSubadditive_of_addContent_iUnion_eq_tsum MeasureTheory.isSetRing_measurableCylinders MeasureTheory.addContent_iUnion_eq_sum_of_tendsto_zero trajContent_ne_top trajContent_tendsto_zero
le_lmarginalPartialTraj_succ 📖	mathematical	ProbabilityTheory.IsMarkovKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder DependsOn ENNReal SetLike.coe Measurable ENNReal.measurableSpace Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder Antitone lmarginalPartialTraj Filter.Tendsto Filter.atTop nhds ENNReal.instTopologicalSpace Function.updateFinset	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder lmarginalPartialTraj Function.update Function.updateFinset Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	—	Nat.case_strong_induction_on Finset.mem_Iic zero_le Nat.instCanonicallyOrderedAdd MeasureTheory.nonempty_of_isProbabilityMeasure ProbabilityTheory.IsMarkovKernel.is_probability_measure' lt_trichotomy lmarginalPartialTraj_self LT.lt.le lmarginalPartialTraj_le le_rfl DependsOn.lmarginalPartialTraj_of_le MeasureTheory.lintegral_le_const instIsMarkovKernelForallValNatMemFinsetIicPartialTrajOfHAddOfNat MeasureTheory.ae_of_all MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.tendsto_lintegral_of_dominated_convergence Measurable.comp measurable_lmarginalPartialTraj measurable_updateFinset Filter.Eventually.of_forall MeasureTheory.lintegral_const MeasureTheory.IsProbabilityMeasure.measure_univ mul_one ge_of_tendsto instClosedIciTopology OrderTopology.to_orderClosedTopology ENNReal.instOrderTopology Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat ne_top_of_le_ne_top le_of_tendsto' instClosedIicTopology MeasureTheory.exists_lintegral_le LE.le.trans lmarginalPartialTraj_succ IsFiniteKernel.isSFiniteKernel ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel ENNReal.measurable_of_tendsto tendsto_pi_nhds Preorder.frestrictLe_updateFinset le_trans Antitone.le_of_tendsto DependsOn.dependsOn_lmarginalPartialTraj Finset.mem_coe
lintegral_traj 📖	mathematical	ProbabilityTheory.IsMarkovKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder Measurable ENNReal ENNReal.measurableSpace	MeasureTheory.lintegral MeasurableSpace.pi DFunLike.coe ProbabilityTheory.Kernel Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder MeasureTheory.Measure instFunLike traj Function.updateFinset	—	lintegral_traj₀ Measurable.aemeasurable
lintegral_traj₀ 📖	mathematical	ProbabilityTheory.IsMarkovKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder AEMeasurable ENNReal ENNReal.measurableSpace DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike traj	MeasureTheory.lintegral MeasurableSpace.pi DFunLike.coe ProbabilityTheory.Kernel Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder MeasureTheory.Measure instFunLike traj Function.updateFinset	—	traj_map_updateFinset MeasureTheory.lintegral_map' Measurable.aemeasurable measurable_updateFinset_left
map_frestrictLe_trajMeasure_compProd_eq_map_trajMeasure 📖	mathematical	ProbabilityTheory.IsMarkovKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	MeasureTheory.Measure.compProd MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder MeasureTheory.Measure.map Preorder.frestrictLe trajMeasure Prod.instMeasurableSpace	—	MeasureTheory.Measure.compProd_eq_comp_prod MeasureTheory.Measure.instSFiniteMap MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure instIsProbabilityMeasureForallTrajMeasure IsFiniteKernel.isSFiniteKernel ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel trajMeasure.eq_1 MeasureTheory.Measure.map_comp Preorder.measurable_frestrictLe traj_map_frestrictLe MeasureTheory.Measure.comp_assoc Measurable.prodMk measurable_pi_apply ext comp_apply ProbabilityTheory.IsSFiniteKernel.sFinite instIsSFiniteKernelForallValNatMemFinsetIicPartialTraj map_apply partialTraj_compProd_eq_map_traj zero_le'
map_traj_succ_self 📖	mathematical	ProbabilityTheory.IsMarkovKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	map MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder traj	—	Finset.mem_Iic le_rfl map_comp_right Preorder.measurable_frestrictLe measurable_pi_apply traj_map_frestrictLe map_partialTraj_succ_self
measurable_trajFun 📖	mathematical	ProbabilityTheory.IsMarkovKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	Measurable MeasureTheory.Measure MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder MeasureTheory.Measure.instMeasurableSpace trajFun	—	MeasureTheory.Measure.measurable_of_measurable_coe MeasurableSpace.induction_on_inter MeasureTheory.generateFrom_measurableCylinders MeasureTheory.isPiSystem_measurableCylinders MeasureTheory.measure_empty MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.measurableCylinders_nat MeasureTheory.isSetSemiring_measurableCylinders isSigmaSubadditive_trajContent Eq.le MeasureTheory.AddContent.measure_eq isProjectiveMeasureFamily_partialTraj MeasureTheory.projectiveFamilyContent_congr MeasureTheory.Measure.measurable_measure Measurable.comp MeasureTheory.Measure.measurable_map Finset.measurable_restrict₂ measurable isProbabilityMeasure_trajFun MeasurableSet.compl MeasureTheory.measure_compl MeasureTheory.measure_ne_top MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure MeasureTheory.IsProbabilityMeasure.measure_univ Measurable.const_sub MeasurableSub₂.toMeasurableSub ENNReal.instMeasurableSub₂ MeasurableSet.iUnion instCountableNat MeasureTheory.measure_iUnion Measurable.ennreal_tsum
partialTraj_compProd_eq_map_traj 📖	mathematical	ProbabilityTheory.IsMarkovKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	MeasureTheory.Measure.compProd MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike partialTraj MeasureTheory.Measure.map Prod.instMeasurableSpace Preorder.frestrictLe traj	—	MeasureTheory.Measure.map_map Measurable.prodMap measurable_id' measurable_pi_apply Measurable.prodMk Preorder.measurable_frestrictLe partialTraj_compProd_traj MeasureTheory.Measure.compProd_map ProbabilityTheory.IsSFiniteKernel.sFinite instIsSFiniteKernelForallValNatMemFinsetIicPartialTraj IsFiniteKernel.isSFiniteKernel ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelForallValNatMemFinsetIicForallTraj map_traj_succ_self
partialTraj_compProd_traj 📖	mathematical	ProbabilityTheory.IsMarkovKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	MeasureTheory.Measure.compProd MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike partialTraj traj MeasureTheory.Measure.map Prod.instMeasurableSpace Preorder.frestrictLe	—	MeasureTheory.Measure.ext MeasureTheory.Measure.map_apply Measurable.prodMk Preorder.measurable_frestrictLe measurable_id' MeasurableSet.preimage MeasureTheory.Measure.compProd_apply ProbabilityTheory.IsSFiniteKernel.sFinite instIsSFiniteKernelForallValNatMemFinsetIicPartialTraj IsFiniteKernel.isSFiniteKernel ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelForallValNatMemFinsetIicForallTraj traj_comp_partialTraj comp_apply' traj_map_updateFinset measurable_updateFinset_left measurable_const Set.ext
setIntegral_traj_partialTraj 📖	mathematical	ProbabilityTheory.IsMarkovKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike traj MeasurableSet	MeasureTheory.integral MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder MeasureTheory.Measure.restrict DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike partialTraj traj Set.preimage Preorder.frestrictLe	—	setIntegral_traj_partialTraj' MeasureTheory.Integrable.comp_measurable MeasureTheory.Measure.snd_compProd ProbabilityTheory.IsSFiniteKernel.sFinite instIsSFiniteKernelForallValNatMemFinsetIicPartialTraj IsFiniteKernel.isSFiniteKernel ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelForallValNatMemFinsetIicForallTraj comp_apply traj_comp_partialTraj measurable_snd
setIntegral_traj_partialTraj' 📖	mathematical	ProbabilityTheory.IsMarkovKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Prod.instMeasurableSpace MeasureTheory.Measure.compProd DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike partialTraj traj MeasurableSet	MeasureTheory.integral MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder MeasureTheory.Measure.restrict DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike partialTraj traj Set.preimage Preorder.frestrictLe	—	integral_integral_indicator integral_traj_partialTraj' Set.indicator_of_mem Set.indicator_of_notMem MeasureTheory.Integrable.indicator MeasurableSet.prod MeasurableSet.univ MeasureTheory.integral_indicator Preorder.measurable_frestrictLe
trajContent_cylinder 📖	mathematical	ProbabilityTheory.IsMarkovKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder MeasurableSet	DFunLike.coe MeasureTheory.AddContent ENNReal ENNReal.instAddCommMonoid MeasureTheory.measurableCylinders Set MeasureTheory.instFunLikeAddContentSet trajContent MeasureTheory.cylinder Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder MeasureTheory.Measure MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike partialTraj	—	isProjectiveMeasureFamily_partialTraj trajContent.eq_1 MeasureTheory.projectiveFamilyContent_cylinder MeasureTheory.inducedFamily_Iic
trajContent_eq_lmarginalPartialTraj 📖	mathematical	ProbabilityTheory.IsMarkovKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder MeasurableSet	DFunLike.coe MeasureTheory.AddContent ENNReal ENNReal.instAddCommMonoid MeasureTheory.measurableCylinders Set MeasureTheory.instFunLikeAddContentSet trajContent Preorder.frestrictLe Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder MeasureTheory.cylinder Finset.Iic lmarginalPartialTraj Set.indicator instZeroENNReal Pi.instOne AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	trajContent_cylinder MeasureTheory.lintegral_indicator_one lmarginalPartialTraj.eq_1 Set.indicator_const_eq_indicator_const MeasureTheory.mem_cylinder
trajContent_ne_top 📖	—	ProbabilityTheory.IsMarkovKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	—	—	MeasureTheory.projectiveFamilyContent_ne_top MeasureTheory.instIsFiniteMeasureForallValNatMemFinsetInducedFamilyOfForallIic ProbabilityTheory.IsFiniteKernel.isFiniteMeasure instIsFiniteKernelForallValNatMemFinsetIicPartialTrajOfHAddOfNat ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel isProjectiveMeasureFamily_partialTraj
trajContent_tendsto_zero 📖	mathematical	ProbabilityTheory.IsMarkovKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder Set Set.instMembership MeasureTheory.measurableCylinders Antitone PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.iInter Set.instEmptyCollection	Filter.Tendsto ENNReal DFunLike.coe MeasureTheory.AddContent ENNReal.instAddCommMonoid MeasureTheory.measurableCylinders Set MeasureTheory.instFunLikeAddContentSet trajContent Filter.atTop Nat.instPreorder nhds ENNReal.instTopologicalSpace instZeroENNReal	—	Nat.case_strong_induction_on Finset.mem_Iic zero_le Nat.instCanonicallyOrderedAdd MeasureTheory.nonempty_of_isProbabilityMeasure ProbabilityTheory.IsMarkovKernel.is_probability_measure' MeasureTheory.measurableCylinders_nat measurable_indicator_const_iff instMeasurableSingletonClassOfMeasurableEq instMeasurableEqOfSecondCountableTopologyOfT2Space BorelSpace.opensMeasurable ENNReal.borelSpace ENNReal.instSecondCountableTopology ENNReal.instT2Space NeZero.charZero_one ENNReal.instCharZero MeasurableSet.cylinder MeasureTheory.dependsOn_cylinder_indicator_const DependsOn.dependsOn_lmarginalPartialTraj IsFiniteKernel.isSFiniteKernel ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel Finset.mem_coe Set.indicator_le ENNReal.instCanonicallyOrderedAdd Set.indicator_of_mem instReflLe DependsOn.lmarginalPartialTraj_const_right le_rfl le_max_left le_max_right lmarginalPartialTraj_mono tendsto_atTop_of_antitone ENNReal.instOrderTopology Filter.Tendsto.mono_right Filter.OrderBot.atBot_eq pure_le_nhds tendsto_nhds_unique Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Antitone.le_of_tendsto OrderTopology.to_orderClosedTopology Nat.le_induction frestrictLe_iterateInduction iterateInduction.eq_2 Preorder.frestrictLe_updateFinset trajContent_eq_lmarginalPartialTraj lmarginalPartialTraj_le Preorder.updateFinset_frestrictLe bot_eq_zero' lt_of_lt_of_le Ne.bot_lt Set.mem_of_indicator_ne_zero ne_of_lt Set.mem_iInter le_lmarginalPartialTraj_succ Function.sometimes_spec
traj_apply 📖	mathematical	ProbabilityTheory.IsMarkovKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	DFunLike.coe ProbabilityTheory.Kernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder MeasureTheory.Measure instFunLike traj trajFun	—	—
traj_comp_partialTraj 📖	mathematical	ProbabilityTheory.IsMarkovKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	comp MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder traj partialTraj	—	eq_traj map_comp traj_map_frestrictLe partialTraj_comp_partialTraj'
traj_eq_prod 📖	mathematical	ProbabilityTheory.IsMarkovKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	traj map MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder Prod.instMeasurableSpace Set.Elem Set.Ioi Set Set.instMembership prod id Set.restrict DFunLike.coe MeasurableEquiv PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Nat.instLinearOrder EquivLike.toFunLike MeasurableEquiv.instEquivLike MeasurableEquiv.IicProdIoi	—	eq_traj' map_comp_right MeasurableEquiv.measurable Preorder.measurable_frestrictLe Set.mem_Ioi Finset.mem_Ioc Measurable.prodMap measurable_id' measurable_pi_lambda measurable_pi_apply measurable_IicProdIoc map_prod_map IsFiniteKernel.isSFiniteKernel ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelId IsSFiniteKernel.map instIsMarkovKernelForallValNatMemFinsetIicForallTraj Set.measurable_restrict Finset.Ioc_subset_Iic_self Finset.restrict₂_comp_restrict Preorder.frestrictLe.eq_1 Finset.measurable_restrict₂ traj_map_frestrictLe map_id partialTraj_eq_prod
traj_map_frestrictLe 📖	mathematical	ProbabilityTheory.IsMarkovKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	map MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder traj Preorder.frestrictLe partialTraj	—	ext MeasureTheory.Measure.ext map_apply Preorder.measurable_frestrictLe traj_apply Preorder.frestrictLe.eq_1 isProjectiveLimit_trajFun MeasureTheory.inducedFamily_Iic
traj_map_frestrictLe_apply 📖	mathematical	ProbabilityTheory.IsMarkovKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	MeasureTheory.Measure.map MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder Preorder.frestrictLe DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike traj partialTraj	—	map_apply Preorder.measurable_frestrictLe traj_map_frestrictLe
traj_map_frestrictLe_of_le 📖	mathematical	ProbabilityTheory.IsMarkovKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	map MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder traj Preorder.frestrictLe deterministic Preorder.frestrictLe₂ Preorder.measurable_frestrictLe₂	—	Preorder.measurable_frestrictLe₂ traj_map_frestrictLe partialTraj_le
traj_map_updateFinset 📖	mathematical	ProbabilityTheory.IsMarkovKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	MeasureTheory.Measure.map MeasurableSpace.pi Function.updateFinset Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder DFunLike.coe ProbabilityTheory.Kernel Finset SetLike.instMembership Finset.instSetLike MeasureTheory.Measure instFunLike traj	—	traj_eq_prod Function.comp_assoc MeasureTheory.Measure.map_map Measurable.fun_comp MeasurableEquiv.measurable Measurable.prodMk measurable_const measurable_id' Set.measurable_restrict map_apply prod_apply IsFiniteKernel.isSFiniteKernel ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelId IsSFiniteKernel.map instIsMarkovKernelForallValNatMemFinsetIicForallTraj id_apply MeasureTheory.Measure.dirac_prod MeasureTheory.Measure.instSFiniteMap ProbabilityTheory.IsSFiniteKernel.sFinite

(root)

Definitions

Name	Category	Theorems
iterateInduction 📖	CompOp	1 math math: frestrictLe_iterateInduction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
frestrictLe_iterateInduction 📖	mathematical	—	Preorder.frestrictLe Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder iterateInduction	—	iterateInduction.eq_1 iterateInduction.eq_2 Finset.mem_Iic

---

← Back to Index