CDFToKernel

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

Statistics

Metric	Count
Definitions `IsCondKernelCDF`, `toKernel`, `IsRatCondKernelCDF`, `IsRatCondKernelCDFAux`	4
Theorems `iInf_rat_gt_prod_Iic`, `integrable`, `integral`, `le_one`, `lintegral`, `measurable`, `nonneg`, `setIntegral`, `setLIntegral`, `tendsto_atBot_zero`, `tendsto_atTop_one`, `toKernel_Iic`, `toKernel_apply`, `iInf_rat_gt_eq`, `integrable`, `isRatStieltjesPoint_ae`, `measurable`, `mono`, `setIntegral`, `tendsto_atBot_zero`, `tendsto_atTop_one`, `bddBelow_range`, `iInf_rat_gt_eq`, `integrable`, `integrable_iInf_rat_gt`, `isRatCondKernelCDF`, `isRatStieltjesPoint_ae`, `le_one`, `le_one'`, `measurable`, `measurable_right`, `mono`, `mono'`, `nonneg`, `nonneg'`, `setIntegral`, `setIntegral_iInf_rat_gt`, `tendsto_atBot_zero`, `tendsto_atTop_one`, `tendsto_integral_of_antitone`, `tendsto_integral_of_monotone`, `tendsto_one_of_monotone`, `tendsto_zero_of_antitone`, `compProd_toKernel`, `instIsMarkovKernel_toKernel`, `integrable_stieltjesOfMeasurableRat`, `integral_stieltjesOfMeasurableRat`, `isCondKernelCDF_stieltjesOfMeasurableRat`, `lintegral_stieltjesOfMeasurableRat`, `lintegral_toKernel_mem`, `lintegral_toKernel_univ`, `setIntegral_stieltjesOfMeasurableRat`, `setIntegral_stieltjesOfMeasurableRat_rat`, `setLIntegral_stieltjesOfMeasurableRat`, `setLIntegral_stieltjesOfMeasurableRat_rat`, `setLIntegral_toKernel_Iic`, `setLIntegral_toKernel_prod`, `setLIntegral_toKernel_univ`, `stieltjesOfMeasurableRat_ae_eq`	59
Total	63

MeasureTheory.Measure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iInf_rat_gt_prod_Iic` 📖	mathematical	`MeasurableSet`	`iInf` `ENNReal` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `DFunLike.coe` `MeasureTheory.Measure` `Real` `Prod.instMeasurableSpace` `Real.measurableSpace` `Set` `instFunLike` `SProd.sprod` `Set.instSProd` `Set.Iic` `Real.instPreorder` `Real.instRatCast`	—	`Monotone.measure_iInter` `SemilatticeInf.instIsCodirectedOrder` `Filter.atBot.isCountablyGenerated` `Subtype.countable` `Encodable.countable` `Set.prod_mono_right` `Rat.cast_mono` `Real.instIsStrictOrderedRing` `MeasurableSet.nullMeasurableSet` `MeasurableSet.prod` `measurableSet_Iic` `BorelSpace.opensMeasurable` `Real.borelSpace` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `lt_add_one` `Rat.instZeroLEOneClass` `NeZero.charZero_one` `Rat.instCharZero` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Rat.instAddLeftMono` `MeasureTheory.measure_ne_top` `Set.prod_iInter` `nonempty_gt` `instNoMaxOrderOfNontrivial` `IsStrictOrderedRing.toIsOrderedRing` `Rat.instIsStrictOrderedRing` `Rat.nontrivial` `Set.ext` `le_of_forall_lt_rat_imp_le` `Real.instArchimedean` `LE.le.trans` `LT.lt.le`

ProbabilityTheory

Definitions

Name	Category	Theorems
`IsCondKernelCDF` 📖	CompData	3 math math: `Kernel.isCondKernelCDF_condKernelCDF`, `isCondKernelCDF_stieltjesOfMeasurableRat`, `isCondKernelCDF_condCDF`
`IsRatCondKernelCDF` 📖	CompData	3 math math: `isRatCondKernelCDF_preCDF`, `IsRatCondKernelCDFAux.isRatCondKernelCDF`, `Kernel.isRatCondKernelCDF_density_Iic`
`IsRatCondKernelCDFAux` 📖	CompData	2 math math: `isRatCondKernelCDFAux_preCDF`, `Kernel.isRatCondKernelCDFAux_density_Iic`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compProd_toKernel` 📖	mathematical	`IsCondKernelCDF`	`Kernel.compProd` `Real` `Real.measurableSpace` `IsCondKernelCDF.toKernel`	—	`Kernel.ext` `MeasureTheory.Measure.ext` `Kernel.compProd_apply` `Kernel.IsFiniteKernel.isSFiniteKernel` `IsZeroOrMarkovKernel.isFiniteKernel` `IsMarkovKernel.IsZeroOrMarkovKernel` `instIsMarkovKernel_toKernel` `lintegral_toKernel_mem`
`instIsMarkovKernel_toKernel` 📖	mathematical	`IsCondKernelCDF`	`IsMarkovKernel` `Real` `Prod.instMeasurableSpace` `Real.measurableSpace` `IsCondKernelCDF.toKernel`	—	`StieltjesFunction.isProbabilityMeasure` `instOrderTopologyReal` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `Real.borelSpace` `instSecondCountableTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `IsCondKernelCDF.tendsto_atBot_zero` `IsCondKernelCDF.tendsto_atTop_one`
`integrable_stieltjesOfMeasurableRat` 📖	mathematical	`IsRatCondKernelCDF`	`MeasureTheory.Integrable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `StieltjesFunction.toFun` `Real.linearOrder` `stieltjesOfMeasurableRat` `Prod.instMeasurableSpace` `IsRatCondKernelCDF.measurable` `DFunLike.coe` `Kernel` `MeasureTheory.Measure` `Kernel.instFunLike`	—	`IsRatCondKernelCDF.measurable` `ENNReal.toReal_ofReal` `stieltjesOfMeasurableRat_nonneg` `MeasureTheory.integrable_toReal_of_lintegral_ne_top` `Measurable.aemeasurable` `Measurable.ennreal_ofReal` `Measurable.comp` `measurable_stieltjesOfMeasurableRat` `measurable_prodMk_left` `lintegral_stieltjesOfMeasurableRat` `MeasureTheory.measure_ne_top` `IsFiniteKernel.isFiniteMeasure`
`integral_stieltjesOfMeasurableRat` 📖	mathematical	`IsRatCondKernelCDF`	`MeasureTheory.integral` `Real` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `DFunLike.coe` `Kernel` `MeasureTheory.Measure` `Kernel.instFunLike` `StieltjesFunction.toFun` `Real.linearOrder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `stieltjesOfMeasurableRat` `Prod.instMeasurableSpace` `IsRatCondKernelCDF.measurable` `MeasureTheory.Measure.real` `Real.measurableSpace` `SProd.sprod` `Set` `Set.instSProd` `Set.univ` `Set.Iic` `Real.instPreorder`	—	`IsRatCondKernelCDF.measurable` `MeasureTheory.setIntegral_univ` `setIntegral_stieltjesOfMeasurableRat` `MeasurableSet.univ`
`isCondKernelCDF_stieltjesOfMeasurableRat` 📖	mathematical	`IsRatCondKernelCDF`	`IsCondKernelCDF` `stieltjesOfMeasurableRat` `Prod.instMeasurableSpace` `IsRatCondKernelCDF.measurable`	—	`IsRatCondKernelCDF.measurable` `measurable_stieltjesOfMeasurableRat` `integrable_stieltjesOfMeasurableRat` `tendsto_stieltjesOfMeasurableRat_atTop` `tendsto_stieltjesOfMeasurableRat_atBot` `setIntegral_stieltjesOfMeasurableRat`
`lintegral_stieltjesOfMeasurableRat` 📖	mathematical	`IsRatCondKernelCDF`	`MeasureTheory.lintegral` `DFunLike.coe` `Kernel` `MeasureTheory.Measure` `Kernel.instFunLike` `ENNReal.ofReal` `StieltjesFunction.toFun` `Real` `Real.linearOrder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `stieltjesOfMeasurableRat` `Prod.instMeasurableSpace` `IsRatCondKernelCDF.measurable` `Real.measurableSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `SProd.sprod` `Set.instSProd` `Set.univ` `Set.Iic` `Real.instPreorder`	—	`IsRatCondKernelCDF.measurable` `MeasureTheory.setLIntegral_univ` `setLIntegral_stieltjesOfMeasurableRat` `MeasurableSet.univ`
`lintegral_toKernel_mem` 📖	mathematical	`IsCondKernelCDF` `MeasurableSet` `Real` `Prod.instMeasurableSpace` `Real.measurableSpace`	`MeasureTheory.lintegral` `DFunLike.coe` `Kernel` `MeasureTheory.Measure` `Kernel.instFunLike` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `IsCondKernelCDF.toKernel` `Set.preimage`	—	`MeasurableSpace.induction_on_inter` `generateFrom_prod` `isPiSystem_prod` `MeasureTheory.measure_empty` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.lintegral_const` `MulZeroClass.zero_mul` `MeasureTheory.lintegral_add_compl` `MeasureTheory.setLIntegral_congr_fun` `Set.mk_preimage_prod_right` `Set.mk_preimage_prod_right_eq_empty` `Set.mem_compl_iff` `MeasurableSet.compl` `add_zero` `setLIntegral_toKernel_prod` `MeasureTheory.measure_compl` `measurable_prodMk_left` `MeasureTheory.measure_ne_top` `IsFiniteKernel.isFiniteMeasure` `IsZeroOrMarkovKernel.isFiniteKernel` `IsMarkovKernel.IsZeroOrMarkovKernel` `instIsMarkovKernel_toKernel` `Filter.Eventually.of_forall` `MeasureTheory.measure_mono` `Set.subset_univ` `MeasureTheory.lintegral_sub` `Kernel.measurable_kernel_prodMk_left'` `Kernel.IsFiniteKernel.isSFiniteKernel` `LT.lt.ne` `LE.le.trans_lt` `MeasureTheory.lintegral_mono_ae` `lintegral_toKernel_univ` `MeasureTheory.measure_lt_top` `Set.preimage_iUnion` `Function.onFun.eq_1` `Set.disjoint_iff_inter_eq_empty` `Set.ext` `Set.mem_inter_iff` `Set.mem_empty_iff_false` `MeasureTheory.measure_iUnion` `instCountableNat` `MeasureTheory.lintegral_tsum` `Measurable.aemeasurable`
`lintegral_toKernel_univ` 📖	mathematical	`IsCondKernelCDF`	`MeasureTheory.lintegral` `DFunLike.coe` `Kernel` `MeasureTheory.Measure` `Kernel.instFunLike` `Real` `Real.measurableSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `Prod.instMeasurableSpace` `IsCondKernelCDF.toKernel` `Set.univ`	—	`MeasureTheory.setLIntegral_univ` `setLIntegral_toKernel_univ` `MeasurableSet.univ` `Set.univ_prod_univ`
`setIntegral_stieltjesOfMeasurableRat` 📖	mathematical	`IsRatCondKernelCDF` `MeasurableSet`	`MeasureTheory.integral` `Real` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `MeasureTheory.Measure.restrict` `DFunLike.coe` `Kernel` `MeasureTheory.Measure` `Kernel.instFunLike` `StieltjesFunction.toFun` `Real.linearOrder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `stieltjesOfMeasurableRat` `Prod.instMeasurableSpace` `IsRatCondKernelCDF.measurable` `MeasureTheory.Measure.real` `Real.measurableSpace` `SProd.sprod` `Set` `Set.instSProd` `Set.Iic` `Real.instPreorder`	—	`IsRatCondKernelCDF.measurable` `ENNReal.ofReal_eq_ofReal_iff` `MeasureTheory.setIntegral_nonneg` `stieltjesOfMeasurableRat_nonneg` `ENNReal.toReal_nonneg` `MeasureTheory.ofReal_measureReal` `MeasureTheory.measure_ne_top` `IsFiniteKernel.isFiniteMeasure` `MeasureTheory.ofReal_integral_eq_lintegral_ofReal` `MeasureTheory.Integrable.restrict` `integrable_stieltjesOfMeasurableRat` `MeasureTheory.ae_of_all` `MeasureTheory.Measure.instOuterMeasureClass` `setLIntegral_stieltjesOfMeasurableRat`
`setIntegral_stieltjesOfMeasurableRat_rat` 📖	mathematical	`IsRatCondKernelCDF` `MeasurableSet`	`MeasureTheory.integral` `Real` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `MeasureTheory.Measure.restrict` `DFunLike.coe` `Kernel` `MeasureTheory.Measure` `Kernel.instFunLike` `StieltjesFunction.toFun` `Real.linearOrder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `stieltjesOfMeasurableRat` `Prod.instMeasurableSpace` `IsRatCondKernelCDF.measurable` `Real.instRatCast` `MeasureTheory.Measure.real` `Real.measurableSpace` `SProd.sprod` `Set` `Set.instSProd` `Set.Iic` `Real.instPreorder`	—	`IsRatCondKernelCDF.measurable` `MeasureTheory.setIntegral_congr_ae` `Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `stieltjesOfMeasurableRat_ae_eq` `Filter.univ_mem'` `IsRatCondKernelCDF.setIntegral`
`setLIntegral_stieltjesOfMeasurableRat` 📖	mathematical	`IsRatCondKernelCDF` `MeasurableSet`	`MeasureTheory.lintegral` `MeasureTheory.Measure.restrict` `DFunLike.coe` `Kernel` `MeasureTheory.Measure` `Kernel.instFunLike` `ENNReal.ofReal` `StieltjesFunction.toFun` `Real` `Real.linearOrder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `stieltjesOfMeasurableRat` `Prod.instMeasurableSpace` `IsRatCondKernelCDF.measurable` `Real.measurableSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `SProd.sprod` `Set.instSProd` `Set.Iic` `Real.instPreorder`	—	`IsRatCondKernelCDF.measurable` `MeasureTheory.lintegral_zero_measure` `exists_rat_gt` `Real.instIsStrictOrderedRing` `Real.instArchimedean` `IsRatCondKernelCDF.setIntegral` `MeasureTheory.integral_zero_measure` `MeasureTheory.measureReal_eq_zero_iff` `MeasureTheory.measure_ne_top` `IsFiniteKernel.isFiniteMeasure` `MeasureTheory.measure_mono_null` `MeasureTheory.Measure.instOuterMeasureClass` `LE.le.trans` `LT.lt.le` `instOrderTopologyReal` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `Real.borelSpace` `instSecondCountableTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Monotone.measure_iInter` `SemilatticeInf.instIsCodirectedOrder` `Filter.atBot.isCountablyGenerated` `Subtype.countable` `Encodable.countable` `Set.Iic_subset_Iic` `nullMeasurableSet_Iic` `BorelSpace.opensMeasurable` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `instIsProbabilityMeasure_stieltjesOfMeasurableRat` `Set.ext` `le_of_forall_lt_rat_imp_le` `MeasureTheory.lintegral_iInf_directed_of_measurable` `Measurable.ennreal_ofReal` `Measurable.comp` `measurable_stieltjesOfMeasurableRat` `measurable_prodMk_left` `setLIntegral_stieltjesOfMeasurableRat_rat` `Monotone.directed_ge` `MeasureTheory.measure_mono` `Set.prod_mono_right` `Rat.cast_mono` `MeasurableSet.nullMeasurableSet` `MeasurableSet.prod` `measurableSet_Iic` `Set.prod_iInter`
`setLIntegral_stieltjesOfMeasurableRat_rat` 📖	mathematical	`IsRatCondKernelCDF` `MeasurableSet`	`MeasureTheory.lintegral` `MeasureTheory.Measure.restrict` `DFunLike.coe` `Kernel` `MeasureTheory.Measure` `Kernel.instFunLike` `ENNReal.ofReal` `StieltjesFunction.toFun` `Real` `Real.linearOrder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `stieltjesOfMeasurableRat` `Prod.instMeasurableSpace` `IsRatCondKernelCDF.measurable` `Real.instRatCast` `Real.measurableSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `SProd.sprod` `Set.instSProd` `Set.Iic` `Real.instPreorder`	—	`IsRatCondKernelCDF.measurable` `MeasureTheory.ofReal_integral_eq_lintegral_ofReal` `MeasureTheory.Integrable.restrict` `MeasureTheory.integrable_congr` `stieltjesOfMeasurableRat_ae_eq` `IsRatCondKernelCDF.integrable` `MeasureTheory.ae_of_all` `MeasureTheory.Measure.instOuterMeasureClass` `stieltjesOfMeasurableRat_nonneg` `setIntegral_stieltjesOfMeasurableRat_rat` `MeasureTheory.ofReal_measureReal` `MeasureTheory.measure_ne_top` `IsFiniteKernel.isFiniteMeasure`
`setLIntegral_toKernel_Iic` 📖	mathematical	`IsCondKernelCDF` `MeasurableSet`	`MeasureTheory.lintegral` `MeasureTheory.Measure.restrict` `DFunLike.coe` `Kernel` `MeasureTheory.Measure` `Kernel.instFunLike` `Real` `Real.measurableSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `Prod.instMeasurableSpace` `IsCondKernelCDF.toKernel` `Set.Iic` `Real.instPreorder` `SProd.sprod` `Set.instSProd`	—	`IsCondKernelCDF.toKernel_Iic` `IsCondKernelCDF.setLIntegral`
`setLIntegral_toKernel_prod` 📖	mathematical	`IsCondKernelCDF` `MeasurableSet` `Real` `Real.measurableSpace`	`MeasureTheory.lintegral` `MeasureTheory.Measure.restrict` `DFunLike.coe` `Kernel` `MeasureTheory.Measure` `Kernel.instFunLike` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `Prod.instMeasurableSpace` `IsCondKernelCDF.toKernel` `SProd.sprod` `Set.instSProd`	—	`MeasurableSpace.induction_on_inter` `borel_eq_generateFrom_Iic` `instSecondCountableTopologyReal` `instOrderTopologyReal` `isPiSystem_Iic` `MeasureTheory.measure_empty` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.lintegral_const` `MulZeroClass.zero_mul` `Set.prod_empty` `setLIntegral_toKernel_Iic` `MeasureTheory.measure_compl` `MeasureTheory.measure_ne_top` `IsFiniteKernel.isFiniteMeasure` `IsZeroOrMarkovKernel.isFiniteKernel` `IsMarkovKernel.IsZeroOrMarkovKernel` `instIsMarkovKernel_toKernel` `MeasureTheory.lintegral_sub` `Measurable.comp` `Kernel.measurable_coe` `measurable_prodMk_left` `Filter.Eventually.of_forall` `MeasureTheory.measure_mono` `Set.subset_univ` `setLIntegral_toKernel_univ` `MeasureTheory.measure_diff` `Set.prod_subset_prod_iff` `subset_rfl` `Set.instReflSubset` `MeasurableSet.nullMeasurableSet` `MeasurableSet.prod` `Set.prod_diff_prod` `Set.compl_eq_univ_diff` `Set.diff_self` `Set.empty_prod` `Set.union_empty` `MeasureTheory.measure_iUnion` `instCountableNat` `MeasureTheory.lintegral_tsum` `AEMeasurable.restrict` `Measurable.aemeasurable` `Set.prod_iUnion` `Pairwise.mono` `Set.Disjoint.set_prod_right`
`setLIntegral_toKernel_univ` 📖	mathematical	`IsCondKernelCDF` `MeasurableSet`	`MeasureTheory.lintegral` `MeasureTheory.Measure.restrict` `DFunLike.coe` `Kernel` `MeasureTheory.Measure` `Kernel.instFunLike` `Real` `Real.measurableSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `Prod.instMeasurableSpace` `IsCondKernelCDF.toKernel` `Set.univ` `SProd.sprod` `Set.instSProd`	—	`Real.iUnion_Iic_rat` `Set.prod_iUnion` `Monotone.directed_le` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Rat.instIsStrictOrderedRing` `instArchimedeanRat` `Set.Iic_subset_Iic` `Real.instIsStrictOrderedRing` `Set.prod_subset_prod_iff` `subset_rfl` `Set.instReflSubset` `Directed.measure_iUnion` `Encodable.countable` `MeasureTheory.lintegral_iSup_directed` `Measurable.aemeasurable` `Measurable.comp` `Kernel.measurable_coe` `measurableSet_Iic` `BorelSpace.opensMeasurable` `Real.borelSpace` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `measurable_prodMk_left` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `setLIntegral_toKernel_Iic`
`stieltjesOfMeasurableRat_ae_eq` 📖	mathematical	`IsRatCondKernelCDF`	`Filter.EventuallyEq` `Real` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `DFunLike.coe` `Kernel` `Kernel.instFunLike` `StieltjesFunction.toFun` `Real.linearOrder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `stieltjesOfMeasurableRat` `Prod.instMeasurableSpace` `IsRatCondKernelCDF.measurable` `Real.instRatCast`	—	`Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `IsRatCondKernelCDF.measurable` `IsRatCondKernelCDF.isRatStieltjesPoint_ae` `Filter.univ_mem'` `stieltjesOfMeasurableRat_eq` `toRatCDF_of_isRatStieltjesPoint`

ProbabilityTheory.IsCondKernelCDF

Definitions

Name	Category	Theorems
`toKernel` 📖	CompOp	9 math math: `toKernel_Iic`, `ProbabilityTheory.lintegral_toKernel_univ`, `ProbabilityTheory.setLIntegral_toKernel_univ`, `ProbabilityTheory.lintegral_toKernel_mem`, `ProbabilityTheory.compProd_toKernel`, `ProbabilityTheory.setLIntegral_toKernel_prod`, `ProbabilityTheory.instIsMarkovKernel_toKernel`, `ProbabilityTheory.setLIntegral_toKernel_Iic`, `toKernel_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`integrable` 📖	mathematical	`ProbabilityTheory.IsCondKernelCDF`	`MeasureTheory.Integrable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `StieltjesFunction.toFun` `Real.linearOrder` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike`	—	—
`integral` 📖	mathematical	`ProbabilityTheory.IsCondKernelCDF`	`MeasureTheory.integral` `Real` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike` `StieltjesFunction.toFun` `Real.linearOrder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `MeasureTheory.Measure.real` `Prod.instMeasurableSpace` `Real.measurableSpace` `SProd.sprod` `Set` `Set.instSProd` `Set.univ` `Set.Iic` `Real.instPreorder`	—	`setIntegral` `MeasurableSet.univ` `MeasureTheory.Measure.restrict_univ`
`le_one` 📖	mathematical	`ProbabilityTheory.IsCondKernelCDF`	`Real` `Real.instLE` `StieltjesFunction.toFun` `Real.linearOrder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instOne`	—	`Monotone.ge_of_tendsto` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `instIsDirectedOrder` `Real.instIsOrderedRing` `Real.instArchimedean` `StieltjesFunction.mono` `tendsto_atTop_one`
`lintegral` 📖	mathematical	`ProbabilityTheory.IsCondKernelCDF`	`MeasureTheory.lintegral` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike` `ENNReal.ofReal` `StieltjesFunction.toFun` `Real` `Real.linearOrder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Prod.instMeasurableSpace` `Real.measurableSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `SProd.sprod` `Set.instSProd` `Set.univ` `Set.Iic` `Real.instPreorder`	—	`setLIntegral` `MeasurableSet.univ` `MeasureTheory.Measure.restrict_univ`
`measurable` 📖	mathematical	`ProbabilityTheory.IsCondKernelCDF`	`Measurable` `Real` `Prod.instMeasurableSpace` `Real.measurableSpace` `StieltjesFunction.toFun` `Real.linearOrder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	—	—
`nonneg` 📖	mathematical	`ProbabilityTheory.IsCondKernelCDF`	`Real` `Real.instLE` `Real.instZero` `StieltjesFunction.toFun` `Real.linearOrder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	—	`Monotone.le_of_tendsto` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `instIsCodirectedOrder` `Real.instIsOrderedRing` `Real.instArchimedean` `StieltjesFunction.mono` `tendsto_atBot_zero`
`setIntegral` 📖	mathematical	`ProbabilityTheory.IsCondKernelCDF` `MeasurableSet`	`MeasureTheory.integral` `Real` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `MeasureTheory.Measure.restrict` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike` `StieltjesFunction.toFun` `Real.linearOrder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `MeasureTheory.Measure.real` `Prod.instMeasurableSpace` `Real.measurableSpace` `SProd.sprod` `Set` `Set.instSProd` `Set.Iic` `Real.instPreorder`	—	—
`setLIntegral` 📖	mathematical	`ProbabilityTheory.IsCondKernelCDF` `MeasurableSet`	`MeasureTheory.lintegral` `MeasureTheory.Measure.restrict` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike` `ENNReal.ofReal` `StieltjesFunction.toFun` `Real` `Real.linearOrder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Prod.instMeasurableSpace` `Real.measurableSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `SProd.sprod` `Set.instSProd` `Set.Iic` `Real.instPreorder`	—	`MeasureTheory.ofReal_integral_eq_lintegral_ofReal` `MeasureTheory.Integrable.restrict` `integrable` `MeasureTheory.ae_of_all` `MeasureTheory.Measure.instOuterMeasureClass` `nonneg` `setIntegral` `MeasureTheory.ofReal_measureReal` `MeasureTheory.measure_ne_top` `ProbabilityTheory.IsFiniteKernel.isFiniteMeasure`
`tendsto_atBot_zero` 📖	mathematical	`ProbabilityTheory.IsCondKernelCDF`	`Filter.Tendsto` `Real` `StieltjesFunction.toFun` `Real.linearOrder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Filter.atBot` `Real.instPreorder` `nhds` `Real.instZero`	—	—
`tendsto_atTop_one` 📖	mathematical	`ProbabilityTheory.IsCondKernelCDF`	`Filter.Tendsto` `Real` `StieltjesFunction.toFun` `Real.linearOrder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Filter.atTop` `Real.instPreorder` `nhds` `Real.instOne`	—	—
`toKernel_Iic` 📖	mathematical	`ProbabilityTheory.IsCondKernelCDF`	`DFunLike.coe` `MeasureTheory.Measure` `Real` `Real.measurableSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `ProbabilityTheory.Kernel` `Prod.instMeasurableSpace` `ProbabilityTheory.Kernel.instFunLike` `toKernel` `Set.Iic` `Real.instPreorder` `ENNReal.ofReal` `StieltjesFunction.toFun` `Real.linearOrder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	—	`instOrderTopologyReal` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `Real.borelSpace` `instSecondCountableTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `toKernel_apply` `StieltjesFunction.measure_Iic` `tendsto_atBot_zero` `sub_zero`
`toKernel_apply` 📖	mathematical	`ProbabilityTheory.IsCondKernelCDF`	`DFunLike.coe` `ProbabilityTheory.Kernel` `Real` `Prod.instMeasurableSpace` `Real.measurableSpace` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike` `toKernel` `StieltjesFunction.measure` `Real.linearOrder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instOrderTopologyReal` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `Real.instConditionallyCompleteLinearOrder` `Real.borelSpace` `instSecondCountableTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `Field.toSemifield` `Real.instField` `Real.partialOrder` `PosMulReflectLE.toPosMulReflectLT` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Real.normedCommRing` `PosMulStrictMono.toPosMulReflectLE` `MulZeroClass.toMul` `MulZeroClass.toZero` `IsStrictOrderedRing.toPosMulStrictMono` `Real.semiring` `Real.instIsStrictOrderedRing`	—	—

ProbabilityTheory.IsRatCondKernelCDF

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iInf_rat_gt_eq` 📖	mathematical	`ProbabilityTheory.IsRatCondKernelCDF`	`Filter.Eventually` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `DFunLike.coe` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike`	—	`Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `isRatStieltjesPoint_ae` `Filter.univ_mem'` `ProbabilityTheory.IsRatStieltjesPoint.iInf_rat_gt_eq`
`integrable` 📖	mathematical	`ProbabilityTheory.IsRatCondKernelCDF`	`MeasureTheory.Integrable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike`	—	—
`isRatStieltjesPoint_ae` 📖	mathematical	`ProbabilityTheory.IsRatCondKernelCDF`	`Filter.Eventually` `ProbabilityTheory.IsRatStieltjesPoint` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `DFunLike.coe` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike`	—	—
`measurable` 📖	mathematical	`ProbabilityTheory.IsRatCondKernelCDF`	`Measurable` `Prod.instMeasurableSpace` `MeasurableSpace.pi` `Real` `Real.measurableSpace`	—	—
`mono` 📖	mathematical	`ProbabilityTheory.IsRatCondKernelCDF`	`Filter.Eventually` `Monotone` `Real` `Rat.instPreorder` `Real.instPreorder` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `DFunLike.coe` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike`	—	`Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `isRatStieltjesPoint_ae` `Filter.univ_mem'` `ProbabilityTheory.IsRatStieltjesPoint.mono`
`setIntegral` 📖	mathematical	`ProbabilityTheory.IsRatCondKernelCDF` `MeasurableSet`	`MeasureTheory.integral` `Real` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `MeasureTheory.Measure.restrict` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike` `MeasureTheory.Measure.real` `Prod.instMeasurableSpace` `Real.measurableSpace` `SProd.sprod` `Set` `Set.instSProd` `Set.Iic` `Real.instPreorder` `Real.instRatCast`	—	—
`tendsto_atBot_zero` 📖	mathematical	`ProbabilityTheory.IsRatCondKernelCDF`	`Filter.Eventually` `Filter.Tendsto` `Real` `Filter.atBot` `Rat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `DFunLike.coe` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike`	—	`Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `isRatStieltjesPoint_ae` `Filter.univ_mem'` `ProbabilityTheory.IsRatStieltjesPoint.tendsto_atBot_zero`
`tendsto_atTop_one` 📖	mathematical	`ProbabilityTheory.IsRatCondKernelCDF`	`Filter.Eventually` `Filter.Tendsto` `Real` `Filter.atTop` `Rat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instOne` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `DFunLike.coe` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike`	—	`Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `isRatStieltjesPoint_ae` `Filter.univ_mem'` `ProbabilityTheory.IsRatStieltjesPoint.tendsto_atTop_one`

ProbabilityTheory.IsRatCondKernelCDFAux

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bddBelow_range` 📖	mathematical	`ProbabilityTheory.IsRatCondKernelCDFAux`	`Filter.Eventually` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `DFunLike.coe` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike`	—	`Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `nonneg` `Filter.univ_mem'`
`iInf_rat_gt_eq` 📖	mathematical	`ProbabilityTheory.IsRatCondKernelCDFAux`	`Filter.Eventually` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `DFunLike.coe` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.ae_all_iff` `Encodable.countable` `MeasureTheory.ae_eq_of_forall_setIntegral_eq_of_sigmaFinite` `Real.instCompleteSpace` `MeasureTheory.IsFiniteMeasure.toSigmaFinite` `ProbabilityTheory.IsFiniteKernel.isFiniteMeasure` `MeasureTheory.Integrable.integrableOn` `integrable_iInf_rat_gt` `integrable` `setIntegral` `setIntegral_iInf_rat_gt`
`integrable` 📖	mathematical	`ProbabilityTheory.IsRatCondKernelCDFAux`	`MeasureTheory.Integrable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike`	—	—
`integrable_iInf_rat_gt` 📖	mathematical	`ProbabilityTheory.IsRatCondKernelCDFAux`	`MeasureTheory.Integrable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `iInf` `Set.Elem` `Set.Ioi` `Rat.instPreorder` `Real.instInfSet` `Set` `Set.instMembership` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike`	—	`MeasureTheory.memLp_one_iff_integrable` `Measurable.aestronglyMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `instSecondCountableTopologyReal` `BorelSpace.opensMeasurable` `Real.borelSpace` `Measurable.iInf` `instOrderTopologyReal` `SetCoe.countable` `Encodable.countable` `measurable_right` `LE.le.trans_lt` `LE.le.trans` `MeasureTheory.eLpNorm_le_of_ae_bound` `Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `le_one` `nonneg` `bddBelow_range` `Filter.univ_mem'` `Real.norm_eq_abs` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `le_ciInf` `Set.nonempty_Ioi_subtype` `instNoMaxOrderOfNontrivial` `IsStrictOrderedRing.toIsOrderedRing` `Rat.instIsStrictOrderedRing` `Rat.nontrivial` `ciInf_le_of_le` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Rat.instAddLeftMono` `contravariant_lt_of_covariant_le` `Rat.instZeroLEOneClass` `NeZero.charZero_one` `Rat.instCharZero` `inv_one` `ENNReal.rpow_one` `ENNReal.ofReal_one` `mul_one` `MeasureTheory.measure_lt_top` `ProbabilityTheory.IsFiniteKernel.isFiniteMeasure`
`isRatCondKernelCDF` 📖	mathematical	`ProbabilityTheory.IsRatCondKernelCDFAux`	`ProbabilityTheory.IsRatCondKernelCDF`	—	`measurable` `isRatStieltjesPoint_ae` `integrable` `setIntegral`
`isRatStieltjesPoint_ae` 📖	mathematical	`ProbabilityTheory.IsRatCondKernelCDFAux`	`Filter.Eventually` `ProbabilityTheory.IsRatStieltjesPoint` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `DFunLike.coe` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike`	—	`Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `mono` `iInf_rat_gt_eq` `tendsto_atBot_zero` `tendsto_atTop_one` `Filter.univ_mem'`
`le_one` 📖	mathematical	`ProbabilityTheory.IsRatCondKernelCDFAux`	`Filter.Eventually` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `DFunLike.coe` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.ae_all_iff` `Encodable.countable` `le_one'`
`le_one'` 📖	mathematical	`ProbabilityTheory.IsRatCondKernelCDFAux`	`Filter.Eventually` `Real` `Real.instLE` `Real.instOne` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `DFunLike.coe` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike`	—	—
`measurable` 📖	mathematical	`ProbabilityTheory.IsRatCondKernelCDFAux`	`Measurable` `Prod.instMeasurableSpace` `MeasurableSpace.pi` `Real` `Real.measurableSpace`	—	—
`measurable_right` 📖	mathematical	`ProbabilityTheory.IsRatCondKernelCDFAux`	`Measurable` `Real` `Real.measurableSpace`	—	`measurable` `Measurable.comp` `measurable_pi_iff` `measurable_prodMk_left`
`mono` 📖	mathematical	`ProbabilityTheory.IsRatCondKernelCDFAux`	`Filter.Eventually` `Monotone` `Real` `Rat.instPreorder` `Real.instPreorder` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `DFunLike.coe` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Encodable.countable` `Prop.countable` `mono'`
`mono'` 📖	mathematical	`ProbabilityTheory.IsRatCondKernelCDFAux`	`Filter.Eventually` `Real` `Real.instLE` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `DFunLike.coe` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike`	—	—
`nonneg` 📖	mathematical	`ProbabilityTheory.IsRatCondKernelCDFAux`	`Filter.Eventually` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `DFunLike.coe` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.ae_all_iff` `Encodable.countable` `nonneg'`
`nonneg'` 📖	mathematical	`ProbabilityTheory.IsRatCondKernelCDFAux`	`Filter.Eventually` `Real` `Real.instLE` `Real.instZero` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `DFunLike.coe` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike`	—	—
`setIntegral` 📖	mathematical	`ProbabilityTheory.IsRatCondKernelCDFAux` `MeasurableSet`	`MeasureTheory.integral` `Real` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `MeasureTheory.Measure.restrict` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike` `MeasureTheory.Measure.real` `Prod.instMeasurableSpace` `Real.measurableSpace` `SProd.sprod` `Set` `Set.instSProd` `Set.Iic` `Real.instPreorder` `Real.instRatCast`	—	—
`setIntegral_iInf_rat_gt` 📖	mathematical	`ProbabilityTheory.IsRatCondKernelCDFAux` `MeasurableSet`	`MeasureTheory.integral` `Real` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `MeasureTheory.Measure.restrict` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike` `iInf` `Set.Elem` `Set.Ioi` `Rat.instPreorder` `Real.instInfSet` `Set` `Set.instMembership` `MeasureTheory.Measure.real` `Prod.instMeasurableSpace` `Real.measurableSpace` `SProd.sprod` `Set.instSProd` `Set.Iic` `Real.instPreorder` `Real.instRatCast`	—	`le_antisymm` `setIntegral` `MeasureTheory.setIntegral_mono_ae` `Real.instIsOrderedAddMonoid` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `Real.instIsStrictOrderedRing` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `MeasureTheory.Integrable.integrableOn` `integrable_iInf_rat_gt` `integrable` `Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `bddBelow_range` `Filter.univ_mem'` `ciInf_le` `le_ciInf` `Set.nonempty_Ioi_subtype` `instNoMaxOrderOfNontrivial` `IsStrictOrderedRing.toIsOrderedRing` `Rat.instIsStrictOrderedRing` `Rat.nontrivial` `MeasureTheory.measureReal_def` `MeasureTheory.Measure.iInf_rat_gt_prod_Iic` `ProbabilityTheory.IsFiniteKernel.isFiniteMeasure` `ENNReal.toReal_iInf` `MeasureTheory.measure_ne_top` `mono` `le_of_lt` `Subtype.prop`
`tendsto_atBot_zero` 📖	mathematical	`ProbabilityTheory.IsRatCondKernelCDFAux`	`Filter.Eventually` `Filter.Tendsto` `Real` `Filter.atBot` `Rat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `DFunLike.coe` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike`	—	`MeasureTheory.Measure.instOuterMeasureClass` `tendsto_zero_of_antitone` `Monotone.neg` `Rat.instAddLeftMono` `covariant_swap_add_of_covariant_add` `Nat.mono_cast` `Rat.instZeroLEOneClass` `Filter.tendsto_neg_atBot_iff` `Rat.instIsOrderedAddMonoid` `tendsto_natCast_atTop_atTop` `IsStrictOrderedRing.toIsOrderedRing` `Rat.instIsStrictOrderedRing` `instArchimedeanRat` `Filter.mp_mem` `mono` `Filter.univ_mem'` `Monotone.comp_antitone` `monotone_id` `tendsto_iff_tendsto_subseq_of_antitone` `instOrderTopologyReal` `instNoMinOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial` `neg_neg` `Filter.Tendsto.comp` `Filter.tendsto_neg_atBot_atTop`
`tendsto_atTop_one` 📖	mathematical	`ProbabilityTheory.IsRatCondKernelCDFAux`	`Filter.Eventually` `Filter.Tendsto` `Real` `Filter.atTop` `Rat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instOne` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `DFunLike.coe` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Filter.mp_mem` `tendsto_one_of_monotone` `Nat.mono_cast` `Rat.instAddLeftMono` `Rat.instZeroLEOneClass` `tendsto_natCast_atTop_atTop` `IsStrictOrderedRing.toIsOrderedRing` `Rat.instIsStrictOrderedRing` `instArchimedeanRat` `Filter.univ_mem'` `mono` `tendsto_iff_tendsto_subseq_of_monotone` `instOrderTopologyReal` `instNoMaxOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial`
`tendsto_integral_of_antitone` 📖	mathematical	`ProbabilityTheory.IsRatCondKernelCDFAux` `Antitone` `Nat.instPreorder` `Rat.instPreorder` `Filter.Tendsto` `Filter.atTop` `Filter.atBot`	`Real` `MeasureTheory.integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero`	—	—
`tendsto_integral_of_monotone` 📖	mathematical	`ProbabilityTheory.IsRatCondKernelCDFAux` `Monotone` `Nat.instPreorder` `Rat.instPreorder` `Filter.Tendsto` `Filter.atTop`	`Real` `MeasureTheory.integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `MeasureTheory.Measure.real` `Set.univ`	—	—
`tendsto_one_of_monotone` 📖	mathematical	`ProbabilityTheory.IsRatCondKernelCDFAux` `Monotone` `Nat.instPreorder` `Rat.instPreorder` `Filter.Tendsto` `Filter.atTop`	`Filter.Eventually` `Real` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instOne` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `DFunLike.coe` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike`	—	`MeasureTheory.tendsto_of_integral_tendsto_of_monotone` `integrable` `MeasureTheory.integrable_const` `ProbabilityTheory.IsFiniteKernel.isFiniteMeasure` `MeasureTheory.integral_const` `Real.instCompleteSpace` `smul_eq_mul` `mul_one` `tendsto_integral_of_monotone` `Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `mono` `Filter.univ_mem'` `le_one`
`tendsto_zero_of_antitone` 📖	mathematical	`ProbabilityTheory.IsRatCondKernelCDFAux` `Antitone` `Nat.instPreorder` `Rat.instPreorder` `Filter.Tendsto` `Filter.atTop` `Filter.atBot`	`Filter.Eventually` `Real` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `DFunLike.coe` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike`	—	`MeasureTheory.tendsto_of_integral_tendsto_of_antitone` `integrable` `MeasureTheory.integrable_const` `ProbabilityTheory.IsFiniteKernel.isFiniteMeasure` `MeasureTheory.integral_zero` `tendsto_integral_of_antitone` `Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `mono` `Filter.univ_mem'` `nonneg`

---

← Back to Index