PartitionFiltration

📁 Source: Mathlib/Probability/Process/PartitionFiltration.lean

Statistics

Metric	Count
Definitions countableFiltration, partitionFiltration	2
Theorems iSup_countableFiltration, iSup_partitionFiltration, iSup_partitionFiltration_eq_generateFrom_range, measurableSet_countableFiltration_countablePartitionSet, measurableSet_countableFiltration_of_mem, measurableSet_partitionFiltration_memPartitionSet, measurableSet_partitionFiltration_of_mem, measurable_countableFiltration_countablePartitionSet, measurable_countablePartitionSet, measurable_countablePartitionSet_subtype, measurable_memPartitionSet, measurable_memPartitionSet_subtype, measurable_partitionFiltration_memPartitionSet	13
Total	15

ProbabilityTheory

Definitions

Name	Category	Theorems
countableFiltration 📖	CompOp	16 math math: Kernel.measurable_densityProcess_countableFiltration_aux, Kernel.martingale_densityProcess, Kernel.memL1_limitProcess_densityProcess, measurable_countablePartitionSet_subtype, Kernel.measurable_countableFiltration_densityProcess, Kernel.density_ae_eq_limitProcess, measurableSet_countableFiltration_countablePartitionSet, Kernel.tendsto_eLpNorm_one_densityProcess_limitProcess, iSup_countableFiltration, Kernel.stronglyMeasurable_countableFiltration_densityProcess, Kernel.condExp_densityProcess, Kernel.tendsto_densityProcess_limitProcess, measurableSet_countableFiltration_of_mem, Kernel.tendsto_eLpNorm_one_restrict_densityProcess_limitProcess, measurable_countableFiltration_countablePartitionSet, Kernel.stronglyAdapted_densityProcess
partitionFiltration 📖	CompOp	6 math math: measurableSet_partitionFiltration_of_mem, measurableSet_partitionFiltration_memPartitionSet, iSup_partitionFiltration_eq_generateFrom_range, measurable_memPartitionSet_subtype, iSup_partitionFiltration, measurable_partitionFiltration_memPartitionSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iSup_countableFiltration 📖	mathematical	—	iSup MeasurableSpace ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice MeasurableSpace.instCompleteLattice MeasureTheory.Filtration.seq Nat.instPreorder countableFiltration	—	MeasurableSpace.generateFrom_iUnion_countablePartition MeasurableSpace.iSup_generateFrom
iSup_partitionFiltration 📖	mathematical	MeasurableSet MeasurableSpace.generateFrom Set.range Set	iSup MeasurableSpace ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice MeasurableSpace.instCompleteLattice MeasureTheory.Filtration.seq Nat.instPreorder partitionFiltration	—	iSup_partitionFiltration_eq_generateFrom_range
iSup_partitionFiltration_eq_generateFrom_range 📖	mathematical	MeasurableSet	iSup MeasurableSpace ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice MeasurableSpace.instCompleteLattice MeasureTheory.Filtration.seq Nat.instPreorder partitionFiltration MeasurableSpace.generateFrom Set.range Set	—	MeasurableSpace.generateFrom_iUnion_memPartition MeasurableSpace.iSup_generateFrom
measurableSet_countableFiltration_countablePartitionSet 📖	mathematical	—	MeasurableSet MeasureTheory.Filtration.seq Nat.instPreorder countableFiltration MeasurableSpace.countablePartitionSet	—	measurableSet_countableFiltration_of_mem MeasurableSpace.countablePartitionSet_mem
measurableSet_countableFiltration_of_mem 📖	mathematical	Set Set.instMembership MeasurableSpace.countablePartition	MeasurableSet MeasureTheory.Filtration.seq Nat.instPreorder countableFiltration	—	MeasurableSpace.measurableSet_generateFrom
measurableSet_partitionFiltration_memPartitionSet 📖	mathematical	MeasurableSet	MeasureTheory.Filtration.seq Nat.instPreorder partitionFiltration memPartitionSet	—	measurableSet_partitionFiltration_of_mem memPartitionSet_mem
measurableSet_partitionFiltration_of_mem 📖	mathematical	MeasurableSet Set Set.instMembership memPartition	MeasureTheory.Filtration.seq Nat.instPreorder partitionFiltration	—	MeasurableSpace.measurableSet_generateFrom
measurable_countableFiltration_countablePartitionSet 📖	mathematical	—	Measurable Set MeasureTheory.Filtration.seq Nat.instPreorder countableFiltration Set.instMeasurableSpace MeasurableSpace.countablePartitionSet	—	Measurable.comp MeasurableSpace.countablePartitionSet_mem measurable_subtype_coe measurable_countablePartitionSet_subtype
measurable_countablePartitionSet 📖	mathematical	—	Measurable Set Set.instMeasurableSpace MeasurableSpace.countablePartitionSet	—	Measurable.mono measurable_countableFiltration_countablePartitionSet MeasureTheory.Filtration.le le_rfl
measurable_countablePartitionSet_subtype 📖	mathematical	—	Measurable Set.Elem Set MeasurableSpace.countablePartition MeasureTheory.Filtration.seq Nat.instPreorder countableFiltration Set.instMembership MeasurableSpace.countablePartitionSet MeasurableSpace.countablePartitionSet_mem	—	measurable_memPartitionSet_subtype MeasurableSpace.countable_countableGeneratingSet MeasurableSpace.measurableSet_enumerateCountable_countableGeneratingSet
measurable_memPartitionSet 📖	mathematical	MeasurableSet	Measurable Set Set.instMeasurableSpace memPartitionSet	—	Measurable.mono measurable_partitionFiltration_memPartitionSet MeasureTheory.Filtration.le le_rfl
measurable_memPartitionSet_subtype 📖	mathematical	MeasurableSet	Measurable Set.Elem Set memPartition MeasureTheory.Filtration.seq Nat.instPreorder partitionFiltration Set.instMembership memPartitionSet memPartitionSet_mem	—	measurable_to_countable' Finite.to_countable instFinite_memPartition memPartitionSet_mem memPartitionSet_eq_iff measurableSet_partitionFiltration_of_mem Set.ext
measurable_partitionFiltration_memPartitionSet 📖	mathematical	MeasurableSet	Measurable Set MeasureTheory.Filtration.seq Nat.instPreorder partitionFiltration Set.instMeasurableSpace memPartitionSet	—	Measurable.comp memPartitionSet_mem measurable_subtype_coe measurable_memPartitionSet_subtype

---

← Back to Index