CondCDF

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

Statistics

Metric	Count
Definitions IicSnd, condCDF, preCDF	3
Theorems IicSnd_ac_fst, IicSnd_apply, IicSnd_le_fst, IicSnd_mono, IicSnd_univ, IicSnd, iInf_IicSnd_gt, tendsto_IicSnd_atBot, tendsto_IicSnd_atTop, condCDF_ae_eq, condCDF_eq_stieltjesOfMeasurableRat_unit_prod, condCDF_le_one, condCDF_nonneg, instIsProbabilityMeasureCondCDF, integrable_condCDF, integrable_preCDF, integral_condCDF, integral_preCDF_fst, isCondKernelCDF_condCDF, isRatCondKernelCDFAux_preCDF, isRatCondKernelCDF_preCDF, lintegral_condCDF, lintegral_preCDF_fst, measurable_condCDF, measurable_measure_condCDF, measurable_preCDF, measurable_preCDF', measure_condCDF_Iic, measure_condCDF_univ, monotone_preCDF, ofReal_condCDF_ae_eq, preCDF_le_one, setIntegral_condCDF, setIntegral_preCDF_fst, setLIntegral_condCDF, setLIntegral_preCDF_fst, stronglyMeasurable_condCDF, tendsto_condCDF_atBot, tendsto_condCDF_atTop, withDensity_preCDF	40
Total	43

MeasureTheory.Measure

Definitions

Name	Category	Theorems
IicSnd 📖	CompOp	14 math math: ProbabilityTheory.setLIntegral_preCDF_fst, iInf_IicSnd_gt, ProbabilityTheory.withDensity_preCDF, IicSnd_apply, ProbabilityTheory.setIntegral_preCDF_fst, IicSnd_le_fst, tendsto_IicSnd_atTop, IsFiniteMeasure.IicSnd, ProbabilityTheory.lintegral_preCDF_fst, IicSnd_mono, IicSnd_univ, tendsto_IicSnd_atBot, IicSnd_ac_fst, ProbabilityTheory.integral_preCDF_fst

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
IicSnd_ac_fst 📖	mathematical	—	AbsolutelyContinuous IicSnd fst Real Real.measurableSpace	—	absolutelyContinuous_of_le IicSnd_le_fst
IicSnd_apply 📖	mathematical	MeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike IicSnd Real Prod.instMeasurableSpace Real.measurableSpace SProd.sprod Set.instSProd Set.Iic Real.instPreorder	—	IicSnd.eq_1 fst_apply restrict_apply' MeasurableSet.prod MeasurableSet.univ measurableSet_Iic BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Set.univ_prod Set.prod_eq
IicSnd_le_fst 📖	mathematical	—	MeasureTheory.Measure Preorder.toLE PartialOrder.toPreorder instPartialOrder IicSnd fst Real Real.measurableSpace	—	fst_mono restrict_le_self
IicSnd_mono 📖	mathematical	Real Real.instLE	MeasureTheory.Measure Preorder.toLE PartialOrder.toPreorder instPartialOrder IicSnd	—	fst_mono restrict_mono Set.prod_mono subset_refl Set.instReflSubset le_refl
IicSnd_univ 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike IicSnd Set.univ Real Prod.instMeasurableSpace Real.measurableSpace SProd.sprod Set.instSProd Set.Iic Real.instPreorder	—	IicSnd_apply MeasurableSet.univ
iInf_IicSnd_gt 📖	mathematical	MeasurableSet	iInf ENNReal ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder DFunLike.coe MeasureTheory.Measure Set instFunLike IicSnd Real Real.instRatCast	—	IicSnd_apply iInf_rat_gt_prod_Iic
tendsto_IicSnd_atBot 📖	mathematical	MeasurableSet	Filter.Tendsto ENNReal DFunLike.coe MeasureTheory.Measure Set instFunLike IicSnd Real Real.instRatCast Filter.atBot Rat.instPreorder nhds ENNReal.instTopologicalSpace instZeroENNReal	—	IicSnd_apply Set.prod_empty MeasureTheory.measure_empty instOuterMeasureClass Real.iInter_Iic_rat Set.prod_iInter MeasureTheory.tendsto_measure_iInter_atTop instIsCountablyGenerated_atTop Rat.instOrderTopology TopologicalSpace.SecondCountableTopology.to_separableSpace TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace Countable.LindelofSpace Encodable.countable PseudoEMetricSpace.pseudoMetrizableSpace MeasurableSet.nullMeasurableSet MeasurableSet.prod measurableSet_Iic BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Set.prod_mono subset_rfl Set.instReflSubset Rat.cast_neg LE.le.trans neg_le_neg Real.instIsStrictOrderedRing MeasureTheory.measure_ne_top Set.ext neg_neg Filter.Tendsto.comp Filter.tendsto_neg_atBot_atTop Rat.instIsOrderedAddMonoid
tendsto_IicSnd_atTop 📖	mathematical	MeasurableSet	Filter.Tendsto ENNReal DFunLike.coe MeasureTheory.Measure Set instFunLike IicSnd Real Real.instRatCast Filter.atTop Rat.instPreorder nhds ENNReal.instTopologicalSpace fst Real.measurableSpace	—	IicSnd_apply fst_apply Real.iUnion_Iic_rat Set.prod_iUnion MeasureTheory.tendsto_measure_iUnion_atTop instIsCountablyGenerated_atTop Rat.instOrderTopology TopologicalSpace.SecondCountableTopology.to_separableSpace TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace Countable.LindelofSpace Encodable.countable PseudoEMetricSpace.pseudoMetrizableSpace Monotone.set_prod monotone_const Monotone.Iic Rat.cast_mono Real.instIsStrictOrderedRing

MeasureTheory.Measure.IsFiniteMeasure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
IicSnd 📖	mathematical	—	MeasureTheory.IsFiniteMeasure MeasureTheory.Measure.IicSnd	—	MeasureTheory.isFiniteMeasure_of_le MeasureTheory.Measure.fst.instIsFiniteMeasure MeasureTheory.Measure.IicSnd_le_fst

ProbabilityTheory

Definitions

Name	Category	Theorems
condCDF 📖	CompOp	19 math math: condCDF_ae_eq, lintegral_condCDF, condCDF_nonneg, tendsto_condCDF_atBot, setIntegral_condCDF, integrable_condCDF, ofReal_condCDF_ae_eq, condCDF_eq_stieltjesOfMeasurableRat_unit_prod, instIsProbabilityMeasureCondCDF, integral_condCDF, condCDF_le_one, isCondKernelCDF_condCDF, stronglyMeasurable_condCDF, measure_condCDF_Iic, measurable_measure_condCDF, setLIntegral_condCDF, measure_condCDF_univ, measurable_condCDF, tendsto_condCDF_atTop
preCDF 📖	CompOp	14 math math: condCDF_ae_eq, setLIntegral_preCDF_fst, integrable_preCDF, isRatCondKernelCDF_preCDF, ofReal_condCDF_ae_eq, measurable_preCDF, monotone_preCDF, withDensity_preCDF, measurable_preCDF', condCDF_eq_stieltjesOfMeasurableRat_unit_prod, setIntegral_preCDF_fst, isRatCondKernelCDFAux_preCDF, lintegral_preCDF_fst, integral_preCDF_fst

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
condCDF_ae_eq 📖	mathematical	—	Filter.EventuallyEq Real MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.fst Real.measurableSpace StieltjesFunction.toFun Real.linearOrder UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace condCDF Real.instRatCast ENNReal.toReal preCDF	—	MeasureTheory.Measure.instOuterMeasureClass Measurable.comp measurable_preCDF' measurable_snd condCDF_eq_stieltjesOfMeasurableRat_unit_prod stieltjesOfMeasurableRat_ae_eq isRatCondKernelCDF_preCDF
condCDF_eq_stieltjesOfMeasurableRat_unit_prod 📖	mathematical	—	condCDF stieltjesOfMeasurableRat Prod.instMeasurableSpace PUnit.instMeasurableSpace ENNReal.toReal preCDF Measurable.comp MeasurableSpace.pi Real Real.measurableSpace measurable_preCDF' measurable_snd	—	StieltjesFunction.ext Measurable.comp measurable_preCDF' measurable_snd condCDF.eq_1 stieltjesOfMeasurableRat_unit_prod
condCDF_le_one 📖	mathematical	—	Real Real.instLE StieltjesFunction.toFun Real.linearOrder UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace condCDF Real.instOne	—	stieltjesOfMeasurableRat_le_one measurable_preCDF'
condCDF_nonneg 📖	mathematical	—	Real Real.instLE Real.instZero StieltjesFunction.toFun Real.linearOrder UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace condCDF	—	stieltjesOfMeasurableRat_nonneg measurable_preCDF'
instIsProbabilityMeasureCondCDF 📖	mathematical	—	MeasureTheory.IsProbabilityMeasure Real Real.measurableSpace StieltjesFunction.measure Real.linearOrder UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace condCDF 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	—	instOrderTopologyReal ConditionallyCompleteLinearOrder.toCompactIccSpace Real.borelSpace instSecondCountableTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing measure_condCDF_univ
integrable_condCDF 📖	mathematical	—	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 condCDF MeasureTheory.Measure.fst Real.measurableSpace	—	IsCondKernelCDF.integrable isCondKernelCDF_condCDF
integrable_preCDF 📖	mathematical	—	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing ENNReal.toReal preCDF MeasureTheory.Measure.fst Real.measurableSpace	—	MeasureTheory.integrable_of_forall_fin_meas_le MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasureTheory.Measure.fst.instIsFiniteMeasure MeasureTheory.measure_lt_top Measurable.aestronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace instSecondCountableTopologyReal BorelSpace.opensMeasurable Real.borelSpace Measurable.ennreal_toReal measurable_preCDF Real.norm_of_nonneg ENNReal.toReal_nonneg MeasureTheory.lintegral_one LE.le.trans MeasureTheory.setLIntegral_le_lintegral MeasureTheory.lintegral_mono_ae Filter.mp_mem MeasureTheory.Measure.instOuterMeasureClass preCDF_le_one Filter.univ_mem' ENNReal.ofReal_toReal_le
integral_condCDF 📖	mathematical	—	MeasureTheory.integral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.Measure.fst Real.measurableSpace StieltjesFunction.toFun Real.linearOrder UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace condCDF MeasureTheory.Measure.real Prod.instMeasurableSpace SProd.sprod Set Set.instSProd Set.univ Set.Iic Real.instPreorder	—	IsCondKernelCDF.integral isCondKernelCDF_condCDF
integral_preCDF_fst 📖	mathematical	—	MeasureTheory.integral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.Measure.fst Real.measurableSpace ENNReal.toReal preCDF MeasureTheory.Measure.real MeasureTheory.Measure.IicSnd Real.instRatCast Set.univ	—	MeasureTheory.setIntegral_univ setIntegral_preCDF_fst MeasurableSet.univ
isCondKernelCDF_condCDF 📖	mathematical	—	IsCondKernelCDF PUnit.instMeasurableSpace condCDF Kernel.const Real Prod.instMeasurableSpace Real.measurableSpace MeasureTheory.Measure.fst	—	Measurable.comp measurable_preCDF' measurable_snd condCDF_eq_stieltjesOfMeasurableRat_unit_prod isCondKernelCDF_stieltjesOfMeasurableRat isRatCondKernelCDF_preCDF Kernel.const.instIsFiniteKernel
isRatCondKernelCDFAux_preCDF 📖	mathematical	—	IsRatCondKernelCDFAux PUnit.instMeasurableSpace ENNReal.toReal preCDF Kernel.const Real Prod.instMeasurableSpace Real.measurableSpace MeasureTheory.Measure.fst	—	Measurable.comp measurable_preCDF' measurable_snd Filter.mp_mem MeasureTheory.Measure.instOuterMeasureClass preCDF_le_one monotone_preCDF Filter.univ_mem' ENNReal.toReal_mono LT.lt.ne LE.le.trans_lt ENNReal.one_lt_top ENNReal.toReal_le_of_le_ofReal zero_le_one Real.instZeroLEOneClass ENNReal.ofReal_one integral_preCDF_fst MeasureTheory.Measure.tendsto_IicSnd_atBot MeasurableSet.univ ENNReal.toReal_zero ENNReal.continuousAt_toReal ENNReal.zero_ne_top Filter.Tendsto.comp MeasureTheory.Measure.tendsto_IicSnd_atTop MeasureTheory.measure_ne_top MeasureTheory.Measure.fst.instIsFiniteMeasure integrable_preCDF Kernel.const_apply setIntegral_preCDF_fst MeasureTheory.measureReal_def MeasureTheory.Measure.IicSnd_apply
isRatCondKernelCDF_preCDF 📖	mathematical	—	IsRatCondKernelCDF PUnit.instMeasurableSpace ENNReal.toReal preCDF Kernel.const Real Prod.instMeasurableSpace Real.measurableSpace MeasureTheory.Measure.fst	—	IsRatCondKernelCDFAux.isRatCondKernelCDF isRatCondKernelCDFAux_preCDF Kernel.const.instIsFiniteKernel MeasureTheory.Measure.fst.instIsFiniteMeasure
lintegral_condCDF 📖	mathematical	—	MeasureTheory.lintegral MeasureTheory.Measure.fst Real Real.measurableSpace ENNReal.ofReal StieltjesFunction.toFun Real.linearOrder UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace condCDF DFunLike.coe MeasureTheory.Measure Prod.instMeasurableSpace Set ENNReal MeasureTheory.Measure.instFunLike SProd.sprod Set.instSProd Set.univ Set.Iic Real.instPreorder	—	IsCondKernelCDF.lintegral Kernel.const.instIsFiniteKernel isCondKernelCDF_condCDF
lintegral_preCDF_fst 📖	mathematical	—	MeasureTheory.lintegral MeasureTheory.Measure.fst Real Real.measurableSpace preCDF DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.Measure.IicSnd Real.instRatCast Set.univ	—	MeasureTheory.setLIntegral_univ setLIntegral_preCDF_fst MeasurableSet.univ
measurable_condCDF 📖	mathematical	—	Measurable Real Real.measurableSpace StieltjesFunction.toFun Real.linearOrder UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace condCDF	—	measurable_stieltjesOfMeasurableRat measurable_preCDF'
measurable_measure_condCDF 📖	mathematical	—	Measurable MeasureTheory.Measure Real Real.measurableSpace MeasureTheory.Measure.instMeasurableSpace StieltjesFunction.measure Real.linearOrder UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace condCDF 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	—	Measurable.measure_of_isPiSystem_of_isProbabilityMeasure instOrderTopologyReal ConditionallyCompleteLinearOrder.toCompactIccSpace Real.borelSpace instSecondCountableTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instIsProbabilityMeasureCondCDF borel_eq_generateFrom_Iic isPiSystem_Iic measure_condCDF_Iic Measurable.ennreal_ofReal measurable_condCDF
measurable_preCDF 📖	mathematical	—	Measurable ENNReal ENNReal.measurableSpace preCDF	—	MeasureTheory.Measure.measurable_rnDeriv
measurable_preCDF' 📖	mathematical	—	Measurable MeasurableSpace.pi Real Real.measurableSpace ENNReal.toReal preCDF	—	measurable_pi_iff Measurable.ennreal_toReal measurable_preCDF
measure_condCDF_Iic 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Real Real.measurableSpace Set ENNReal MeasureTheory.Measure.instFunLike StieltjesFunction.measure Real.linearOrder UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace condCDF 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 Set.Iic Real.instPreorder ENNReal.ofReal StieltjesFunction.toFun	—	instOrderTopologyReal ConditionallyCompleteLinearOrder.toCompactIccSpace Real.borelSpace instSecondCountableTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing sub_zero StieltjesFunction.measure_Iic tendsto_condCDF_atBot
measure_condCDF_univ 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Real Real.measurableSpace Set ENNReal MeasureTheory.Measure.instFunLike StieltjesFunction.measure Real.linearOrder UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace condCDF 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 Set.univ AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	instOrderTopologyReal ConditionallyCompleteLinearOrder.toCompactIccSpace Real.borelSpace instSecondCountableTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing ENNReal.ofReal_one sub_zero StieltjesFunction.measure_univ tendsto_condCDF_atBot tendsto_condCDF_atTop
monotone_preCDF 📖	mathematical	—	Filter.Eventually Monotone ENNReal Rat.instPreorder PartialOrder.toPreorder ENNReal.instPartialOrder preCDF MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.fst Real Real.measurableSpace	—	MeasureTheory.Measure.instOuterMeasureClass Encodable.countable Prop.countable MeasureTheory.ae_le_of_forall_setLIntegral_le_of_sigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasureTheory.Measure.fst.instIsFiniteMeasure measurable_preCDF setLIntegral_preCDF_fst MeasureTheory.Measure.IicSnd_mono Real.instIsStrictOrderedRing
ofReal_condCDF_ae_eq 📖	mathematical	—	Filter.EventuallyEq ENNReal MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.fst Real Real.measurableSpace ENNReal.ofReal StieltjesFunction.toFun Real.linearOrder UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace condCDF Real.instRatCast preCDF	—	Filter.mp_mem MeasureTheory.Measure.instOuterMeasureClass preCDF_le_one condCDF_ae_eq Filter.univ_mem' ENNReal.ofReal_toReal LT.lt.ne LE.le.trans_lt ENNReal.one_lt_top
preCDF_le_one 📖	mathematical	—	Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.fst Real Real.measurableSpace	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.ae_all_iff Encodable.countable MeasureTheory.ae_le_of_forall_setLIntegral_le_of_sigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasureTheory.Measure.fst.instIsFiniteMeasure measurable_preCDF setLIntegral_preCDF_fst MeasureTheory.lintegral_one MeasureTheory.Measure.restrict_apply Set.univ_inter MeasureTheory.Measure.IicSnd_le_fst
setIntegral_condCDF 📖	mathematical	MeasurableSet	MeasureTheory.integral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.Measure.restrict MeasureTheory.Measure.fst Real.measurableSpace StieltjesFunction.toFun Real.linearOrder UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace condCDF MeasureTheory.Measure.real Prod.instMeasurableSpace SProd.sprod Set Set.instSProd Set.Iic Real.instPreorder	—	IsCondKernelCDF.setIntegral isCondKernelCDF_condCDF
setIntegral_preCDF_fst 📖	mathematical	MeasurableSet	MeasureTheory.integral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.Measure.restrict MeasureTheory.Measure.fst Real.measurableSpace ENNReal.toReal preCDF MeasureTheory.Measure.real MeasureTheory.Measure.IicSnd Real.instRatCast	—	MeasureTheory.integral_toReal Measurable.aemeasurable measurable_preCDF MeasureTheory.ae_restrict_of_ae Filter.mp_mem MeasureTheory.Measure.instOuterMeasureClass preCDF_le_one Filter.univ_mem' LE.le.trans_lt ENNReal.one_lt_top setLIntegral_preCDF_fst MeasureTheory.measureReal_def
setLIntegral_condCDF 📖	mathematical	MeasurableSet	MeasureTheory.lintegral MeasureTheory.Measure.restrict MeasureTheory.Measure.fst Real Real.measurableSpace ENNReal.ofReal StieltjesFunction.toFun Real.linearOrder UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace condCDF DFunLike.coe MeasureTheory.Measure Prod.instMeasurableSpace Set ENNReal MeasureTheory.Measure.instFunLike SProd.sprod Set.instSProd Set.Iic Real.instPreorder	—	IsCondKernelCDF.setLIntegral Kernel.const.instIsFiniteKernel isCondKernelCDF_condCDF
setLIntegral_preCDF_fst 📖	mathematical	MeasurableSet	MeasureTheory.lintegral MeasureTheory.Measure.restrict MeasureTheory.Measure.fst Real Real.measurableSpace preCDF DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.Measure.IicSnd Real.instRatCast	—	mul_one MeasureTheory.setLIntegral_withDensity_eq_setLIntegral_mul measurable_preCDF Pi.one_def measurable_const withDensity_preCDF MeasureTheory.lintegral_one MeasureTheory.Measure.restrict_apply Set.univ_inter
stronglyMeasurable_condCDF 📖	mathematical	—	MeasureTheory.StronglyMeasurable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace StieltjesFunction.toFun Real.linearOrder condCDF	—	stronglyMeasurable_stieltjesOfMeasurableRat measurable_preCDF'
tendsto_condCDF_atBot 📖	mathematical	—	Filter.Tendsto Real StieltjesFunction.toFun Real.linearOrder UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace condCDF Filter.atBot Real.instPreorder nhds Real.instZero	—	tendsto_stieltjesOfMeasurableRat_atBot measurable_preCDF'
tendsto_condCDF_atTop 📖	mathematical	—	Filter.Tendsto Real StieltjesFunction.toFun Real.linearOrder UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace condCDF Filter.atTop Real.instPreorder nhds Real.instOne	—	tendsto_stieltjesOfMeasurableRat_atTop measurable_preCDF'
withDensity_preCDF 📖	mathematical	—	MeasureTheory.Measure.withDensity MeasureTheory.Measure.fst Real Real.measurableSpace preCDF MeasureTheory.Measure.IicSnd Real.instRatCast	—	MeasureTheory.Measure.absolutelyContinuous_iff_withDensity_rnDeriv_eq MeasureTheory.Measure.haveLebesgueDecomposition_of_sigmaFinite MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasureTheory.Measure.IsFiniteMeasure.IicSnd MeasureTheory.Measure.fst.instIsFiniteMeasure MeasureTheory.Measure.IicSnd_ac_fst

---

← Back to Index