Documentation Verification Report

StandardBorel

📁 Source: Mathlib/Probability/Kernel/Disintegration/StandardBorel.lean

Statistics

Metric	Count
Definitions `condKernel`, `borelMarkovFromReal`, `condKernel`, `condKernelBorel`, `condKernelCDF`, `condKernelReal`, `condKernelUnitBorel`, `condKernelUnitReal`	8
Theorems `instIsCondKernel`, `condKernel_apply`, `condKernel_apply_of_ne_zero`, `condKernel_def`, `instIsMarkovKernelCondKernel`, `borelMarkovFromReal_apply`, `borelMarkovFromReal_apply'`, `compProd_fst_borelMarkovFromReal`, `compProd_fst_borelMarkovFromReal_eq_comapRight_compProd`, `compProd_fst_condKernelReal`, `instIsCondKernel`, `instIsCondKernel`, `instIsCondKernel`, `instIsCondKernel`, `condKernel_def`, `instIsFiniteKernelBorelMarkovFromReal`, `instIsMarkovKernelBorelMarkovFromReal`, `instIsMarkovKernelCondKernel`, `instIsMarkovKernelCondKernelBorel`, `instIsMarkovKernelCondKernelReal`, `instIsMarkovKernelCondKernelUnitBorel`, `instIsMarkovKernelCondKernelUnitReal`, `instIsSFiniteKernelBorelMarkovFromReal`, `isCondKernelCDF_condKernelCDF`, `isRatCondKernelCDFAux_density_Iic`, `isRatCondKernelCDF_density_Iic`	26
Total	34

MeasureTheory.Measure

Definitions

Name	Category	Theorems
`condKernel` 📖	CompOp	30 math math: `ProbabilityTheory.Kernel.apply_eq_measure_condKernel_of_compProd_eq`, `condKernel_def`, `MeasureTheory.AEStronglyMeasurable.ae_integrable_condKernel_iff`, `setIntegral_condKernel`, `setIntegral_condKernel_univ_left`, `integral_condKernel`, `MeasureTheory.Integrable.condKernel_ae`, `setIntegral_condKernel_univ_right`, `condKernel_apply_of_ne_zero`, `ProbabilityTheory.Kernel.condKernel_apply_eq_condKernel`, `MeasureTheory.Integrable.norm_integral_condKernel`, `condKernel.instIsCondKernel`, `lintegral_condKernel`, `ProbabilityTheory.condKernel_compProd`, `setLIntegral_condKernel`, `lintegral_condKernel_mem`, `ProbabilityTheory.condDistrib_def`, `MeasureTheory.AEStronglyMeasurable.integral_condKernel`, `ProbabilityTheory.eq_condKernel_of_measure_eq_compProd_real`, `setLIntegral_condKernel_univ_left`, `ProbabilityTheory.eq_condKernel_of_measure_eq_compProd'`, `ProbabilityTheory.Kernel.condKernel_def`, `setLIntegral_condKernel_univ_right`, `ProbabilityTheory.condKernel_const`, `MeasureTheory.Integrable.integral_norm_condKernel`, `instIsMarkovKernelCondKernel`, `ProbabilityTheory.eq_condKernel_of_measure_eq_compProd`, `condKernel_apply`, `MeasureTheory.Integrable.integral_condKernel`, `setLIntegral_condKernel_eq_measure_prod`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`condKernel_apply` 📖	mathematical	—	`DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike` `condKernel` `Prod.instMeasurableSpace` `PUnit.instMeasurableSpace` `ProbabilityTheory.Kernel.condKernelUnitBorel` `ProbabilityTheory.Kernel.const` `ProbabilityTheory.Kernel.const.instIsFiniteKernel`	—	`ProbabilityTheory.Kernel.const.instIsFiniteKernel` `measurable_prodMk_left` `condKernel_def`
`condKernel_apply_of_ne_zero` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike` `condKernel` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instInv` `fst` `Set.instSingletonSet` `Prod.instMeasurableSpace` `SProd.sprod` `Set.instSProd`	—	`IsCondKernel.apply_of_ne_zero` `condKernel.instIsCondKernel`
`condKernel_def` 📖	mathematical	—	`condKernel` `ProbabilityTheory.Kernel.comap` `Prod.instMeasurableSpace` `PUnit.instMeasurableSpace` `ProbabilityTheory.Kernel.condKernelUnitBorel` `ProbabilityTheory.Kernel.const` `measurable_prodMk_left`	—	`measurable_prodMk_left`
`instIsMarkovKernelCondKernel` 📖	mathematical	—	`ProbabilityTheory.IsMarkovKernel` `condKernel`	—	`measurable_prodMk_left` `condKernel_def` `ProbabilityTheory.Kernel.IsMarkovKernel.comap` `ProbabilityTheory.Kernel.instIsMarkovKernelCondKernelUnitBorel`

MeasureTheory.Measure.condKernel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsCondKernel` 📖	mathematical	—	`MeasureTheory.Measure.IsCondKernel` `MeasureTheory.Measure.condKernel`	—	`ProbabilityTheory.Kernel.ext` `MeasureTheory.Measure.ext` `ProbabilityTheory.Kernel.const.instIsFiniteKernel` `MeasureTheory.Measure.condKernel_apply` `MeasureTheory.Measure.compProd.eq_1` `ProbabilityTheory.Kernel.disintegrate` `ProbabilityTheory.Kernel.condKernelUnitBorel.instIsCondKernel`

ProbabilityTheory.Kernel

Definitions

Name	Category	Theorems
`borelMarkovFromReal` 📖	CompOp	7 math math: `borelMarkovFromReal_apply'`, `instIsMarkovKernelBorelMarkovFromReal`, `compProd_fst_borelMarkovFromReal_eq_comapRight_compProd`, `instIsSFiniteKernelBorelMarkovFromReal`, `compProd_fst_borelMarkovFromReal`, `borelMarkovFromReal_apply`, `instIsFiniteKernelBorelMarkovFromReal`
`condKernel` 📖	CompOp	17 math math: `ProbabilityTheory.setIntegral_condKernel_univ_left`, `ProbabilityTheory.setLIntegral_condKernel_univ_right`, `ProbabilityTheory.setIntegral_condKernel_univ_right`, `condKernel.instIsCondKernel`, `ProbabilityTheory.setLIntegral_condKernel`, `ProbabilityTheory.lintegral_condKernel`, `condKernel_apply_eq_condKernel`, `ProbabilityTheory.setLIntegral_condKernel_univ_left`, `MeasureTheory.AEStronglyMeasurable.integral_kernel_condKernel`, `ProbabilityTheory.setIntegral_condKernel`, `instIsMarkovKernelCondKernel`, `ProbabilityTheory.setLIntegral_condKernel_eq_measure_prod`, `condKernel_def`, `ProbabilityTheory.eq_condKernel_of_kernel_eq_compProd`, `ProbabilityTheory.integral_condKernel`, `ProbabilityTheory.lintegral_condKernel_mem`, `ProbabilityTheory.condKernel_const`
`condKernelBorel` 📖	CompOp	3 math math: `instIsMarkovKernelCondKernelBorel`, `condKernelBorel.instIsCondKernel`, `condKernel_def`
`condKernelCDF` 📖	CompOp	1 math math: `isCondKernelCDF_condKernelCDF`
`condKernelReal` 📖	CompOp	2 math math: `compProd_fst_condKernelReal`, `instIsMarkovKernelCondKernelReal`
`condKernelUnitBorel` 📖	CompOp	4 math math: `condKernelUnitBorel.instIsCondKernel`, `MeasureTheory.Measure.condKernel_def`, `instIsMarkovKernelCondKernelUnitBorel`, `MeasureTheory.Measure.condKernel_apply`
`condKernelUnitReal` 📖	CompOp	2 math math: `instIsMarkovKernelCondKernelUnitReal`, `condKernelUnitReal.instIsCondKernel`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`borelMarkovFromReal_apply` 📖	mathematical	—	`DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `instFunLike` `borelMarkovFromReal` `ENNReal` `Real` `Real.measurableSpace` `Set` `MeasureTheory.Measure.instFunLike` `Compl.compl` `Set.instCompl` `Set.range` `MeasureTheory.embeddingReal` `instZeroENNReal` `LinearOrder.toDecidableEq` `ENNReal.instLinearOrder` `MeasureTheory.Measure.comap` `MeasureTheory.Measure.dirac` `Set.instMembership` `Set.range_nonempty`	—	`Set.range_nonempty` `MeasureTheory.measurableEmbedding_embeddingReal` `measurable_const` `borelMarkovFromReal.eq_1` `comapRight_apply` `piecewise_apply` `deterministic_apply`
`borelMarkovFromReal_apply'` 📖	mathematical	`MeasurableSet`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `ProbabilityTheory.Kernel` `instFunLike` `borelMarkovFromReal` `Real` `Real.measurableSpace` `Compl.compl` `Set.instCompl` `Set.range` `MeasureTheory.embeddingReal` `instZeroENNReal` `LinearOrder.toDecidableEq` `ENNReal.instLinearOrder` `Set.image` `Set.indicator` `Pi.instOne` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Set.instMembership` `Set.range_nonempty`	—	`MeasureTheory.measurableEmbedding_embeddingReal` `Set.range_nonempty` `borelMarkovFromReal_apply` `MeasureTheory.Measure.comap_apply` `MeasurableEmbedding.injective` `MeasurableEmbedding.measurableSet_image'` `MeasureTheory.Measure.dirac_apply` `instMeasurableSingletonClassOfMeasurableEq` `instMeasurableEqOfSecondCountableTopologyOfT2Space` `BorelSpace.opensMeasurable` `Real.borelSpace` `instSecondCountableTopologyReal` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace`
`compProd_fst_borelMarkovFromReal` 📖	mathematical	`compProd` `Real` `Real.measurableSpace` `fst` `map` `Prod.instMeasurableSpace` `MeasureTheory.embeddingReal`	`borelMarkovFromReal`	—	`MeasureTheory.measurableEmbedding_embeddingReal` `MeasurableEmbedding.prodMap` `MeasurableEmbedding.id` `ext` `MeasureTheory.Measure.ext` `comapRight_apply` `map_apply` `Measurable.prodMap` `measurable_id'` `MeasureTheory.measurable_embeddingReal` `MeasurableEmbedding.comap_map` `compProd_fst_borelMarkovFromReal_eq_comapRight_compProd`
`compProd_fst_borelMarkovFromReal_eq_comapRight_compProd` 📖	mathematical	`compProd` `Real` `Real.measurableSpace` `fst` `map` `Prod.instMeasurableSpace` `MeasureTheory.embeddingReal`	`borelMarkovFromReal` `comapRight` `MeasurableEmbedding.prodMap` `MeasurableEmbedding.id` `MeasureTheory.measurableEmbedding_embeddingReal`	—	`MeasureTheory.measurableEmbedding_embeddingReal` `MeasurableEmbedding.prodMap` `MeasurableEmbedding.id` `comapRight_compProd_id_prod` `IsSFiniteKernel.fst` `IsSFiniteKernel.map` `ext` `MeasureTheory.Measure.ext` `fst_apply` `map_apply` `Measurable.prodMap` `measurable_id'` `MeasureTheory.measurable_embeddingReal` `MeasureTheory.Measure.map_map` `measurable_fst` `MeasurableEmbedding.measurable` `compProd_apply` `instIsSFiniteKernelBorelMarkovFromReal` `IsSFiniteKernel.comapRight` `MeasureTheory.lintegral_congr_ae` `MeasureTheory.Measure.instOuterMeasureClass` `map_apply'` `MeasurableSet.compl` `MeasurableSet.prod` `MeasurableSet.univ` `MeasurableEmbedding.measurableSet_range` `Set.ext` `MeasureTheory.measure_empty` `Set.mk_preimage_prod_right` `compProd_null` `Filter.mp_mem` `Filter.univ_mem'` `measurable_const` `borelMarkovFromReal.eq_1` `comapRight_apply'` `measurable_prodMk_left` `piecewise_apply`
`compProd_fst_condKernelReal` 📖	mathematical	—	`compProd` `Real` `Real.measurableSpace` `fst` `condKernelReal`	—	`isCondKernelCDF_condKernelCDF` `condKernelReal.eq_1` `ProbabilityTheory.compProd_toKernel` `IsSFiniteKernel.fst` `IsFiniteKernel.isSFiniteKernel`
`condKernel_def` 📖	mathematical	—	`condKernel` `ProbabilityTheory.Kernel` `Prod.instMeasurableSpace` `Countable` `condKernelCountable` `MeasureTheory.Measure.condKernel` `DFunLike.coe` `MeasureTheory.Measure` `instFunLike` `condKernelBorel`	—	—
`instIsFiniteKernelBorelMarkovFromReal` 📖	mathematical	—	`ProbabilityTheory.IsFiniteKernel` `borelMarkovFromReal`	—	`IsFiniteKernel.comapRight` `MeasureTheory.measurableEmbedding_embeddingReal` `measurable_const` `IsFiniteKernel.piecewise` `ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel` `ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel` `isMarkovKernel_deterministic`
`instIsMarkovKernelBorelMarkovFromReal` 📖	mathematical	—	`ProbabilityTheory.IsMarkovKernel` `borelMarkovFromReal`	—	`IsMarkovKernel.comapRight` `MeasureTheory.measurableEmbedding_embeddingReal` `measurable_const` `piecewise_apply` `MeasureTheory.prob_compl_eq_zero_iff` `ProbabilityTheory.IsMarkovKernel.is_probability_measure'` `MeasurableEmbedding.measurableSet_range` `deterministic_apply` `MeasureTheory.Measure.dirac_apply_of_mem` `Set.range_nonempty`
`instIsMarkovKernelCondKernel` 📖	mathematical	—	`ProbabilityTheory.IsMarkovKernel` `Prod.instMeasurableSpace` `condKernel`	—	`condKernel_def` `condKernelCountable.instIsMarkovKernel` `MeasureTheory.Measure.instIsMarkovKernelCondKernel` `ProbabilityTheory.IsFiniteKernel.isFiniteMeasure` `instIsMarkovKernelCondKernelBorel`
`instIsMarkovKernelCondKernelBorel` 📖	mathematical	—	`ProbabilityTheory.IsMarkovKernel` `Prod.instMeasurableSpace` `condKernelBorel`	—	`condKernelBorel.eq_1` `instIsMarkovKernelBorelMarkovFromReal` `instIsMarkovKernelCondKernelReal`
`instIsMarkovKernelCondKernelReal` 📖	mathematical	—	`ProbabilityTheory.IsMarkovKernel` `Real` `Prod.instMeasurableSpace` `Real.measurableSpace` `condKernelReal`	—	`isCondKernelCDF_condKernelCDF` `condKernelReal.eq_1` `ProbabilityTheory.instIsMarkovKernel_toKernel`
`instIsMarkovKernelCondKernelUnitBorel` 📖	mathematical	—	`ProbabilityTheory.IsMarkovKernel` `Prod.instMeasurableSpace` `PUnit.instMeasurableSpace` `condKernelUnitBorel`	—	`condKernelUnitBorel.eq_1` `instIsMarkovKernelBorelMarkovFromReal` `instIsMarkovKernelCondKernelUnitReal`
`instIsMarkovKernelCondKernelUnitReal` 📖	mathematical	—	`ProbabilityTheory.IsMarkovKernel` `Real` `Prod.instMeasurableSpace` `PUnit.instMeasurableSpace` `Real.measurableSpace` `condKernelUnitReal`	—	`condKernelUnitReal.eq_1` `ProbabilityTheory.instIsMarkovKernel_toKernel`
`instIsSFiniteKernelBorelMarkovFromReal` 📖	mathematical	—	`ProbabilityTheory.IsSFiniteKernel` `borelMarkovFromReal`	—	`IsSFiniteKernel.comapRight` `MeasureTheory.measurableEmbedding_embeddingReal` `measurable_const` `IsSFiniteKernel.piecewise` `IsFiniteKernel.isSFiniteKernel` `ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel` `ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel` `isMarkovKernel_deterministic`
`isCondKernelCDF_condKernelCDF` 📖	mathematical	—	`ProbabilityTheory.IsCondKernelCDF` `condKernelCDF` `fst` `Real` `Real.measurableSpace`	—	`ProbabilityTheory.isCondKernelCDF_stieltjesOfMeasurableRat` `isRatCondKernelCDF_density_Iic`
`isRatCondKernelCDFAux_density_Iic` 📖	mathematical	—	`ProbabilityTheory.IsRatCondKernelCDFAux` `density` `Real` `Real.measurableSpace` `fst` `Set.Iic` `Real.instPreorder` `Real.instRatCast`	—	`measurable_pi_iff` `measurable_density` `measurableSet_Iic` `BorelSpace.opensMeasurable` `Real.borelSpace` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `MeasureTheory.ae_of_all` `MeasureTheory.Measure.instOuterMeasureClass` `density_mono_set` `le_rfl` `Set.Iic_subset_Iic` `Real.instIsStrictOrderedRing` `density_nonneg` `density_le_one` `tendsto_integral_density_of_antitone` `IsFiniteKernel.fst` `Set.ext` `exists_rat_lt` `Real.instArchimedean` `Filter.tendsto_atTop_atBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `lt_of_le_of_lt` `fst_real_apply` `MeasurableSet.univ` `tendsto_integral_density_of_monotone` `exists_rat_gt` `Filter.tendsto_atTop_atTop` `LE.le.trans` `LT.lt.le` `integrable_density` `setIntegral_density`
`isRatCondKernelCDF_density_Iic` 📖	mathematical	—	`ProbabilityTheory.IsRatCondKernelCDF` `density` `Real` `Real.measurableSpace` `fst` `Set.Iic` `Real.instPreorder` `Real.instRatCast`	—	`ProbabilityTheory.IsRatCondKernelCDFAux.isRatCondKernelCDF` `isRatCondKernelCDFAux_density_Iic` `IsFiniteKernel.fst`

ProbabilityTheory.Kernel.condKernel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsCondKernel` 📖	mathematical	—	`ProbabilityTheory.Kernel.IsCondKernel` `ProbabilityTheory.Kernel.condKernel`	—	`ProbabilityTheory.Kernel.condKernel_def` `ProbabilityTheory.Kernel.disintegrate` `ProbabilityTheory.Kernel.condKernelCountable.instIsCondKernel` `MeasureTheory.Measure.instIsMarkovKernelCondKernel` `ProbabilityTheory.IsFiniteKernel.isFiniteMeasure` `ProbabilityTheory.Kernel.IsFiniteKernel.isSFiniteKernel` `MeasureTheory.Measure.condKernel.instIsCondKernel` `ProbabilityTheory.Kernel.condKernelBorel.instIsCondKernel`

ProbabilityTheory.Kernel.condKernelBorel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsCondKernel` 📖	mathematical	—	`ProbabilityTheory.Kernel.IsCondKernel` `ProbabilityTheory.Kernel.condKernelBorel`	—	`eq_1` `ProbabilityTheory.Kernel.compProd_fst_borelMarkovFromReal` `ProbabilityTheory.Kernel.IsFiniteKernel.isSFiniteKernel` `ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel` `ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel` `ProbabilityTheory.Kernel.instIsMarkovKernelCondKernelReal` `ProbabilityTheory.Kernel.compProd_fst_condKernelReal`

ProbabilityTheory.Kernel.condKernelUnitBorel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsCondKernel` 📖	mathematical	—	`ProbabilityTheory.Kernel.IsCondKernel` `PUnit.instMeasurableSpace` `ProbabilityTheory.Kernel.condKernelUnitBorel`	—	`eq_1` `ProbabilityTheory.Kernel.compProd_fst_borelMarkovFromReal` `ProbabilityTheory.Kernel.IsFiniteKernel.isSFiniteKernel` `ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel` `ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel` `ProbabilityTheory.Kernel.instIsMarkovKernelCondKernelUnitReal` `ProbabilityTheory.Kernel.disintegrate` `ProbabilityTheory.Kernel.condKernelUnitReal.instIsCondKernel`

ProbabilityTheory.Kernel.condKernelUnitReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsCondKernel` 📖	mathematical	—	`ProbabilityTheory.Kernel.IsCondKernel` `Real` `PUnit.instMeasurableSpace` `Real.measurableSpace` `ProbabilityTheory.Kernel.condKernelUnitReal`	—	`eq_1` `ProbabilityTheory.compProd_toKernel` `ProbabilityTheory.Kernel.const.instIsFiniteKernel` `ProbabilityTheory.IsFiniteKernel.isFiniteMeasure` `ProbabilityTheory.Kernel.IsSFiniteKernel.fst` `ProbabilityTheory.Kernel.IsFiniteKernel.isSFiniteKernel` `ProbabilityTheory.Kernel.ext` `MeasureTheory.Measure.ext`

---

← Back to Index