Cylinders

📁 Source: Mathlib/MeasureTheory/Constructions/Cylinders.lean

Statistics

Metric	Count
Definitions `cylinder`, `cylinderEvents`, `measurableCylinders`, `finset`, `squareCylinders`	5
Theorems `cylinder`, `of_mem_measurableCylinders`, `cylinder`, `eval_cylinderEvents`, `comap_eval_le_generateFrom_squareCylinders_singleton`, `compl_cylinder`, `compl_mem_measurableCylinders`, `cylinderEvents_le_pi`, `cylinderEvents_mono`, `cylinderEvents_univ`, `cylinder_empty`, `cylinder_eq_cylinder_union`, `cylinder_eq_empty_iff`, `cylinder_mem_measurableCylinders`, `cylinder_univ`, `dependsOn_cylinder_indicator_const`, `diff_cylinder_same`, `diff_mem_measurableCylinders`, `disjoint_cylinder_iff`, `empty_mem_measurableCylinders`, `eq_of_cylinder_eq_of_subset`, `generateFrom_measurableCylinders`, `generateFrom_squareCylinders`, `inter_cylinder`, `inter_cylinder_same`, `inter_mem_measurableCylinders`, `isPiSystem_measurableCylinders`, `isPiSystem_squareCylinders`, `eq_cylinder`, `measurableSet`, `measurableCylinders_nat`, `measurable_cylinderEvent_apply`, `measurable_cylinderEvents_iff`, `measurable_cylinderEvents_lambda`, `measurable_restrict_cylinderEvents`, `measurable_uniqueElim_cylinderEvents`, `measurable_update_cylinderEvents`, `measurable_update_cylinderEvents'`, `measurable_update_cylinderEvents_left`, `mem_cylinder`, `mem_measurableCylinders`, `squareCylinders_eq_iUnion_image`, `union_cylinder`, `union_cylinder_same`, `union_mem_measurableCylinders`, `univ_mem_measurableCylinders`	46
Total	51

MeasurableSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cylinder` 📖	mathematical	`MeasurableSet` `MeasurableSpace.pi` `Finset` `SetLike.instMembership` `Finset.instSetLike`	`MeasureTheory.cylinder`	—	`measurable_pi_lambda` `measurable_pi_apply`
`of_mem_measurableCylinders` 📖	mathematical	`Set` `Set.instMembership` `MeasureTheory.measurableCylinders`	`MeasurableSet` `MeasurableSpace.pi`	—	`MeasureTheory.mem_measurableCylinders` `cylinder`

MeasureTheory

Definitions

Name	Category	Theorems
`cylinder` 📖	CompOp	28 math math: `ProbabilityTheory.Kernel.trajContent_cylinder`, `inter_cylinder_same`, `cylinder_empty`, `inter_cylinder`, `piContent_cylinder`, `cylinder_eq_cylinder_union`, `compl_cylinder`, `union_cylinder`, `cylinder_univ`, `closedCompactCylinders.eq_cylinder`, `projectiveFamilyContent_cylinder`, `measurableCylinders_nat`, `disjoint_cylinder_iff`, `mem_closedCompactCylinders`, `IsClosed.cylinder`, `cylinder_mem_measurableCylinders`, `MeasurableSet.cylinder`, `IsProjectiveLimit.measure_cylinder`, `cylinder_eq_empty_iff`, `mem_cylinder`, `dependsOn_cylinder_indicator_const`, `Measure.infinitePi_cylinder`, `measurableCylinders.eq_cylinder`, `ProbabilityTheory.Kernel.trajContent_eq_lmarginalPartialTraj`, `cylinder_mem_closedCompactCylinders`, `union_cylinder_same`, `mem_measurableCylinders`, `diff_cylinder_same`
`cylinderEvents` 📖	CompOp	9 math math: `measurable_restrict_cylinderEvents`, `measurable_update_cylinderEvents`, `measurable_update_cylinderEvents_left`, `cylinderEvents_mono`, `measurable_update_cylinderEvents'`, `measurable_cylinderEvents_iff`, `measurable_cylinderEvent_apply`, `cylinderEvents_le_pi`, `cylinderEvents_univ`
`measurableCylinders` 📖	CompOp	20 math math: `ProbabilityTheory.Kernel.trajContent_cylinder`, `empty_mem_measurableCylinders`, `ProbabilityTheory.Kernel.isSigmaSubadditive_trajContent`, `piContent_cylinder`, `projectiveFamilyContent_eq`, `isSetSemiring_measurableCylinders`, `univ_mem_measurableCylinders`, `projectiveFamilyContent_cylinder`, `isSetRing_measurableCylinders`, `projectiveFamilyContent_congr`, `piContent_eq_measure_pi`, `measurableCylinders_nat`, `mem_measurableCylinders_of_mem_closedCompactCylinders`, `isSetAlgebra_measurableCylinders`, `isSigmaSubadditive_piContent`, `cylinder_mem_measurableCylinders`, `isPiSystem_measurableCylinders`, `generateFrom_measurableCylinders`, `ProbabilityTheory.Kernel.trajContent_eq_lmarginalPartialTraj`, `mem_measurableCylinders`
`squareCylinders` 📖	CompOp	3 math math: `isPiSystem_squareCylinders`, `generateFrom_squareCylinders`, `squareCylinders_eq_iUnion_image`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap_eval_le_generateFrom_squareCylinders_singleton` 📖	mathematical	—	`MeasurableSpace` `MeasurableSpace.instLE` `MeasurableSpace.comap` `Function.eval` `MeasurableSpace.generateFrom` `Set.image` `Set` `Set.pi` `Set.instSingletonSet` `Set.univ` `setOf` `MeasurableSet`	—	`Set.image_congr` `Set.singleton_pi` `MeasurableSpace.comap_eq_generateFrom` `MeasurableSpace.generateFrom_mono`
`compl_cylinder` 📖	mathematical	—	`Compl.compl` `Set` `Set.instCompl` `cylinder`	—	`Set.ext`
`compl_mem_measurableCylinders` 📖	mathematical	`Set` `Set.instMembership` `measurableCylinders`	`Compl.compl` `Set.instCompl`	—	`mem_measurableCylinders` `MeasurableSet.compl` `compl_cylinder`
`cylinderEvents_le_pi` 📖	mathematical	—	`MeasurableSpace` `MeasurableSpace.instLE` `cylinderEvents` `MeasurableSpace.pi`	—	`cylinderEvents_univ` `cylinderEvents_mono` `Set.subset_univ`
`cylinderEvents_mono` 📖	mathematical	`Set` `Set.instHasSubset`	`MeasurableSpace` `MeasurableSpace.instLE` `cylinderEvents`	—	`biSup_mono`
`cylinderEvents_univ` 📖	mathematical	—	`cylinderEvents` `Set.univ` `MeasurableSpace.pi`	—	`iSup_congr_Prop` `iSup_pos`
`cylinder_empty` 📖	mathematical	—	`cylinder` `Set` `Set.instEmptyCollection`	—	`cylinder.eq_1` `Set.preimage_empty`
`cylinder_eq_cylinder_union` 📖	mathematical	—	`cylinder` `Finset` `Finset.instUnion` `Set.preimage` `Finset.restrict₂` `Finset.subset_union_left`	—	`Set.ext` `Finset.subset_union_left`
`cylinder_eq_empty_iff` 📖	mathematical	—	`cylinder` `Set` `Set.instEmptyCollection`	—	`Set.nonempty_iff_ne_empty` `mem_cylinder` `Set.notMem_empty` `cylinder_empty`
`cylinder_mem_measurableCylinders` 📖	mathematical	`MeasurableSet` `MeasurableSpace.pi` `Finset` `SetLike.instMembership` `Finset.instSetLike`	`Set` `Set.instMembership` `measurableCylinders` `cylinder`	—	`mem_measurableCylinders`
`cylinder_univ` 📖	mathematical	—	`cylinder` `Set.univ`	—	`cylinder.eq_1` `Set.preimage_univ`
`dependsOn_cylinder_indicator_const` 📖	mathematical	—	`DependsOn` `Set.indicator` `cylinder` `SetLike.coe` `Finset` `Finset.instSetLike`	—	`Set.indicator_const_eq_indicator_const`
`diff_cylinder_same` 📖	mathematical	—	`Set` `Set.instSDiff` `cylinder`	—	`Set.ext`
`diff_mem_measurableCylinders` 📖	mathematical	`Set` `Set.instMembership` `measurableCylinders`	`Set.instSDiff`	—	`Set.diff_eq_compl_inter` `inter_mem_measurableCylinders` `compl_mem_measurableCylinders`
`disjoint_cylinder_iff` 📖	mathematical	—	`Disjoint` `Set` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `cylinder` `Set.preimage` `Finset.restrict₂` `Finset` `Finset.instUnion` `Finset.subset_union_left` `Finset.subset_union_right`	—	`Finset.subset_union_left` `Finset.subset_union_right`
`empty_mem_measurableCylinders` 📖	mathematical	—	`Set` `Set.instMembership` `measurableCylinders` `Set.instEmptyCollection`	—	`MeasurableSet.empty` `cylinder_empty`
`eq_of_cylinder_eq_of_subset` 📖	mathematical	`cylinder` `Finset` `Finset.instHasSubset`	`Set.preimage` `Finset.restrict₂`	—	`Set.ext` `Subtype.prop` `Set.ext_iff`
`generateFrom_measurableCylinders` 📖	mathematical	—	`MeasurableSpace.generateFrom` `measurableCylinders` `MeasurableSpace.pi`	—	`le_antisymm` `MeasurableSpace.generateFrom_le` `mem_measurableCylinders` `MeasurableSet.cylinder` `iSup_le` `LE.le.trans` `comap_eval_le_generateFrom_squareCylinders_singleton` `MeasurableSpace.generateFrom_mono` `Set.image_congr` `Set.singleton_pi` `Finset.mem_singleton_self` `measurable_pi_apply` `Set.ext`
`generateFrom_squareCylinders` 📖	mathematical	—	`MeasurableSpace.generateFrom` `squareCylinders` `setOf` `Set` `MeasurableSet` `MeasurableSpace.pi`	—	`le_antisymm` `MeasurableSpace.generateFrom_le_iff` `MeasurableSet.pi` `Finset.countable_toSet` `iSup_le` `LE.le.trans` `comap_eval_le_generateFrom_squareCylinders_singleton` `MeasurableSpace.generateFrom_mono` `Finset.coe_singleton` `squareCylinders_eq_iUnion_image` `Set.subset_iUnion`
`inter_cylinder` 📖	mathematical	—	`Set` `Set.instInter` `cylinder` `Finset` `Finset.instUnion` `Set.preimage` `Finset.restrict₂` `Finset.subset_union_left` `Finset.subset_union_right`	—	—
`inter_cylinder_same` 📖	mathematical	—	`Set` `Set.instInter` `cylinder`	—	—
`inter_mem_measurableCylinders` 📖	mathematical	`Set` `Set.instMembership` `measurableCylinders`	`Set.instInter`	—	`mem_measurableCylinders` `Finset.subset_union_left` `Finset.subset_union_right` `MeasurableSet.inter` `measurable_pi_lambda` `measurable_pi_apply` `inter_cylinder`
`isPiSystem_measurableCylinders` 📖	mathematical	—	`IsPiSystem` `measurableCylinders`	—	`inter_mem_measurableCylinders`
`isPiSystem_squareCylinders` 📖	mathematical	`IsPiSystem` `Set` `Set.instMembership` `Set.univ`	`squareCylinders`	—	`Finset.piecewise_eq_of_mem` `Finset.piecewise_eq_of_notMem` `Set.pi_congr` `Set.union_pi_inter` `Set.mem_univ_pi` `Set.mem_pi` `Set.mem_inter_iff` `Set.mem_univ` `Finset.coe_union`
`measurableCylinders_nat` 📖	mathematical	—	`measurableCylinders` `Set.iUnion` `Set` `MeasurableSet` `MeasurableSpace.pi` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.Iic` `Nat.instPreorder` `LocallyFiniteOrder.toLocallyFiniteOrderBot` `Nat.instOrderBot` `Nat.instLocallyFiniteOrder` `Set.instSingletonSet` `cylinder`	—	`Set.ext` `Finset.subset_Iic_sup_id` `Finset.measurable_restrict₂` `Set.preimage_comp` `Finset.restrict₂_comp_restrict` `Set.mem_singleton`
`measurable_cylinderEvent_apply` 📖	mathematical	`Set` `Set.instMembership`	`Measurable` `cylinderEvents`	—	`measurable_cylinderEvents_iff` `measurable_id`
`measurable_cylinderEvents_iff` 📖	mathematical	—	`Measurable` `cylinderEvents`	—	`MeasurableSpace.comap_iSup` `iSup_congr_Prop` `MeasurableSpace.comap_comp`
`measurable_cylinderEvents_lambda` 📖	mathematical	`Measurable`	`MeasurableSpace.pi`	—	`measurable_pi_iff`
`measurable_restrict_cylinderEvents` 📖	mathematical	—	`Measurable` `cylinderEvents` `MeasurableSpace.pi` `Set.Elem` `Set` `Set.instMembership` `Set.restrict`	—	`measurable_pi_iff` `measurable_cylinderEvent_apply`
`measurable_uniqueElim_cylinderEvents` 📖	mathematical	—	`Measurable` `Unique.instInhabited` `MeasurableSpace.pi` `uniqueElim`	—	`measurable_id`
`measurable_update_cylinderEvents` 📖	mathematical	—	`Measurable` `cylinderEvents` `Function.update`	—	`Measurable.comp` `measurable_update_cylinderEvents'` `measurable_prodMk_left`
`measurable_update_cylinderEvents'` 📖	mathematical	—	`Measurable` `MeasurableSpace.prod` `cylinderEvents` `Function.update`	—	`measurable_cylinderEvents_iff` `measurable_snd` `measurable_fst`
`measurable_update_cylinderEvents_left` 📖	mathematical	—	`Measurable` `cylinderEvents` `Function.update`	—	`Measurable.comp` `measurable_update_cylinderEvents'` `measurable_prodMk_right`
`mem_cylinder` 📖	mathematical	—	`Set` `Set.instMembership` `cylinder` `Finset.restrict`	—	`Set.mem_preimage`
`mem_measurableCylinders` 📖	mathematical	—	`Set` `Set.instMembership` `measurableCylinders` `MeasurableSet` `MeasurableSpace.pi` `Finset` `SetLike.instMembership` `Finset.instSetLike` `cylinder`	—	—
`squareCylinders_eq_iUnion_image` 📖	mathematical	—	`squareCylinders` `Set.iUnion` `Set` `Finset` `Set.image` `Set.pi` `SetLike.coe` `Finset.instSetLike` `Set.univ`	—	`Set.ext`
`union_cylinder` 📖	mathematical	—	`Set` `Set.instUnion` `cylinder` `Finset` `Finset.instUnion` `Set.preimage` `Finset.restrict₂` `Finset.subset_union_left` `Finset.subset_union_right`	—	—
`union_cylinder_same` 📖	mathematical	—	`Set` `Set.instUnion` `cylinder`	—	—
`union_mem_measurableCylinders` 📖	mathematical	`Set` `Set.instMembership` `measurableCylinders`	`Set.instUnion`	—	`Set.union_eq_compl_compl_inter_compl` `compl_mem_measurableCylinders` `inter_mem_measurableCylinders`
`univ_mem_measurableCylinders` 📖	mathematical	—	`Set` `Set.instMembership` `measurableCylinders` `Set.univ`	—	`Set.compl_empty` `compl_mem_measurableCylinders` `empty_mem_measurableCylinders`

MeasureTheory.IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cylinder` 📖	mathematical	—	`IsClosed` `Pi.topologicalSpace` `MeasureTheory.cylinder`	—	`IsClosed.preimage` `continuous_pi` `continuous_apply`

MeasureTheory.Measurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eval_cylinderEvents` 📖	—	`Set` `Set.instMembership` `Measurable` `MeasureTheory.cylinderEvents`	—	—	`Measurable.comp` `MeasureTheory.measurable_cylinderEvent_apply`

MeasureTheory.measurableCylinders

Definitions

Name	Category	Theorems
`finset` 📖	CompOp	2 math math: `eq_cylinder`, `measurableSet`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_cylinder` 📖	mathematical	`Set` `Set.instMembership` `MeasureTheory.measurableCylinders`	`MeasureTheory.cylinder` `finset` `set`	—	`MeasureTheory.mem_measurableCylinders`
`measurableSet` 📖	mathematical	`Set` `Set.instMembership` `MeasureTheory.measurableCylinders`	`MeasurableSet` `MeasurableSpace.pi` `Finset` `SetLike.instMembership` `Finset.instSetLike` `finset` `set`	—	`MeasureTheory.mem_measurableCylinders`

---

← Back to Index