MeasurableStieltjes

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

Statistics

Metric	Count
Definitions IsMeasurableRatCDF, stieltjesFunction, stieltjesFunctionAux, IsRatStieltjesPoint, defaultRatCDF, stieltjesOfMeasurableRat, toRatCDF	7
Theorems continuousWithinAt_stieltjesFunctionAux_Ici, iInf_rat_gt_eq, instIsProbabilityMeasure_stieltjesFunction, isRatStieltjesPoint, le_one, measurable, measurable_measure_stieltjesFunction, measurable_stieltjesFunction, measure_stieltjesFunction_Iic, measure_stieltjesFunction_univ, monotone_stieltjesFunctionAux, nonneg, stieltjesFunctionAux_def, stieltjesFunctionAux_def', stieltjesFunctionAux_eq, stieltjesFunctionAux_nonneg, stieltjesFunctionAux_unit_prod, stieltjesFunction_eq, stieltjesFunction_le_one, stieltjesFunction_nonneg, stronglyMeasurable_stieltjesFunction, tendsto_atBot_zero, tendsto_atTop_one, tendsto_stieltjesFunction_atBot, tendsto_stieltjesFunction_atTop, IsMeasurableRatCDF_defaultRatCDF, iInf_rat_gt_eq, ite, mono, tendsto_atBot_zero, tendsto_atTop_one, defaultRatCDF_le_one, defaultRatCDF_nonneg, iInf_rat_gt_defaultRatCDF, instIsProbabilityMeasure_stieltjesOfMeasurableRat, isMeasurableRatCDF_toRatCDF, isRatStieltjesPoint_defaultRatCDF, isRatStieltjesPoint_unit_prod_iff, measurableSet_isRatStieltjesPoint, measurable_measure_stieltjesOfMeasurableRat, measurable_stieltjesOfMeasurableRat, measurable_toRatCDF, measure_stieltjesOfMeasurableRat_Iic, measure_stieltjesOfMeasurableRat_univ, monotone_defaultRatCDF, stieltjesOfMeasurableRat_eq, stieltjesOfMeasurableRat_le_one, stieltjesOfMeasurableRat_nonneg, stieltjesOfMeasurableRat_unit_prod, stronglyMeasurable_stieltjesOfMeasurableRat, tendsto_defaultRatCDF_atBot, tendsto_defaultRatCDF_atTop, tendsto_stieltjesOfMeasurableRat_atBot, tendsto_stieltjesOfMeasurableRat_atTop, toRatCDF_of_isRatStieltjesPoint, toRatCDF_unit_prod, measurable_measure	57
Total	64

ProbabilityTheory

Definitions

Name	Category	Theorems
IsMeasurableRatCDF 📖	CompData	2 math math: isMeasurableRatCDF_toRatCDF, IsMeasurableRatCDF_defaultRatCDF
IsRatStieltjesPoint 📖	CompData	6 math math: IsMeasurableRatCDF.isRatStieltjesPoint, isRatStieltjesPoint_defaultRatCDF, isRatStieltjesPoint_unit_prod_iff, IsRatCondKernelCDFAux.isRatStieltjesPoint_ae, IsRatCondKernelCDF.isRatStieltjesPoint_ae, measurableSet_isRatStieltjesPoint
defaultRatCDF 📖	CompOp	8 math math: tendsto_defaultRatCDF_atBot, tendsto_defaultRatCDF_atTop, monotone_defaultRatCDF, defaultRatCDF_le_one, isRatStieltjesPoint_defaultRatCDF, IsMeasurableRatCDF_defaultRatCDF, iInf_rat_gt_defaultRatCDF, defaultRatCDF_nonneg
stieltjesOfMeasurableRat 📖	CompOp	22 math math: stieltjesOfMeasurableRat_ae_eq, setLIntegral_stieltjesOfMeasurableRat_rat, stieltjesOfMeasurableRat_nonneg, integral_stieltjesOfMeasurableRat, tendsto_stieltjesOfMeasurableRat_atTop, stieltjesOfMeasurableRat_le_one, stieltjesOfMeasurableRat_unit_prod, setIntegral_stieltjesOfMeasurableRat, measurable_measure_stieltjesOfMeasurableRat, stronglyMeasurable_stieltjesOfMeasurableRat, condCDF_eq_stieltjesOfMeasurableRat_unit_prod, tendsto_stieltjesOfMeasurableRat_atBot, measurable_stieltjesOfMeasurableRat, stieltjesOfMeasurableRat_eq, isCondKernelCDF_stieltjesOfMeasurableRat, measure_stieltjesOfMeasurableRat_univ, measure_stieltjesOfMeasurableRat_Iic, instIsProbabilityMeasure_stieltjesOfMeasurableRat, lintegral_stieltjesOfMeasurableRat, setIntegral_stieltjesOfMeasurableRat_rat, setLIntegral_stieltjesOfMeasurableRat, integrable_stieltjesOfMeasurableRat
toRatCDF 📖	CompOp	5 math math: toRatCDF_of_isRatStieltjesPoint, isMeasurableRatCDF_toRatCDF, stieltjesOfMeasurableRat_eq, measurable_toRatCDF, toRatCDF_unit_prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
IsMeasurableRatCDF_defaultRatCDF 📖	mathematical	—	IsMeasurableRatCDF defaultRatCDF	—	isRatStieltjesPoint_defaultRatCDF measurable_const
defaultRatCDF_le_one 📖	mathematical	—	Real Real.instLE defaultRatCDF Real.instOne	—	Real.instZeroLEOneClass
defaultRatCDF_nonneg 📖	mathematical	—	Real Real.instLE Real.instZero defaultRatCDF	—	le_rfl zero_le_one Real.instZeroLEOneClass
iInf_rat_gt_defaultRatCDF 📖	mathematical	—	iInf Real Set.Elem Set.Ioi Rat.instPreorder Real.instInfSet defaultRatCDF Set Set.instMembership	—	Set.mem_range le_rfl zero_le_one Real.instZeroLEOneClass le_antisymm lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Rat.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt IsStrictOrderedRing.toIsOrderedRing CancelDenoms.sub_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_inv_pos Rat.instCharZero Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Linarith.mul_nonpos Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Meta.NormNum.isNat_lt_true LE.le.trans ciInf_le le_refl le_ciInf Set.nonempty_Ioi_subtype instNoMaxOrderOfNontrivial Rat.nontrivial lt_add_one Rat.instZeroLEOneClass NeZero.charZero_one IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Rat.instAddLeftMono not_lt LT.lt.le Set.mem_Ioi Subtype.prop
instIsProbabilityMeasure_stieltjesOfMeasurableRat 📖	mathematical	Measurable MeasurableSpace.pi Real Real.measurableSpace	MeasureTheory.IsProbabilityMeasure StieltjesFunction.measure Real.linearOrder UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace stieltjesOfMeasurableRat 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	—	IsMeasurableRatCDF.instIsProbabilityMeasure_stieltjesFunction isMeasurableRatCDF_toRatCDF
isMeasurableRatCDF_toRatCDF 📖	mathematical	Measurable MeasurableSpace.pi Real Real.measurableSpace	IsMeasurableRatCDF toRatCDF	—	IsRatStieltjesPoint.ite isRatStieltjesPoint_defaultRatCDF measurable_toRatCDF
isRatStieltjesPoint_defaultRatCDF 📖	mathematical	—	IsRatStieltjesPoint defaultRatCDF	—	monotone_defaultRatCDF tendsto_defaultRatCDF_atTop tendsto_defaultRatCDF_atBot iInf_rat_gt_defaultRatCDF
isRatStieltjesPoint_unit_prod_iff 📖	mathematical	—	IsRatStieltjesPoint	—	IsRatStieltjesPoint.mono IsRatStieltjesPoint.tendsto_atTop_one IsRatStieltjesPoint.tendsto_atBot_zero IsRatStieltjesPoint.iInf_rat_gt_eq
measurableSet_isRatStieltjesPoint 📖	mathematical	Measurable MeasurableSpace.pi Real Real.measurableSpace	MeasurableSet setOf IsRatStieltjesPoint	—	Set.setOf_forall MeasurableSet.iInter Encodable.countable Prop.countable measurableSet_le BorelSpace.opensMeasurable Real.borelSpace HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid instSecondCountableTopologyReal Measurable.eval measurableSet_tendsto instIsCountablyGenerated_atTop Rat.instOrderTopology TopologicalSpace.SecondCountableTopology.to_separableSpace TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace Countable.LindelofSpace PseudoEMetricSpace.pseudoMetrizableSpace FirstCountableTopology.nhds_generated_countable TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology nhds_isMeasurablyGenerated instIsCountablyGenerated_atBot measurableSet_eq_fun instMeasurableEqOfSecondCountableTopologyOfT2Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Measurable.iInf instOrderTopologyReal SetCoe.countable Set.ext IsRatStieltjesPoint.mono IsRatStieltjesPoint.tendsto_atTop_one IsRatStieltjesPoint.tendsto_atBot_zero IsRatStieltjesPoint.iInf_rat_gt_eq MeasurableSet.inter
measurable_measure_stieltjesOfMeasurableRat 📖	mathematical	Measurable MeasurableSpace.pi Real Real.measurableSpace	MeasureTheory.Measure MeasureTheory.Measure.instMeasurableSpace StieltjesFunction.measure Real.linearOrder UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace stieltjesOfMeasurableRat 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	—	IsMeasurableRatCDF.measurable_measure_stieltjesFunction isMeasurableRatCDF_toRatCDF
measurable_stieltjesOfMeasurableRat 📖	mathematical	Measurable MeasurableSpace.pi Real Real.measurableSpace	StieltjesFunction.toFun Real.linearOrder UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace stieltjesOfMeasurableRat	—	IsMeasurableRatCDF.measurable_stieltjesFunction isMeasurableRatCDF_toRatCDF
measurable_toRatCDF 📖	mathematical	Measurable MeasurableSpace.pi Real Real.measurableSpace	toRatCDF	—	Measurable.ite measurableSet_isRatStieltjesPoint measurable_const
measure_stieltjesOfMeasurableRat_Iic 📖	mathematical	Measurable MeasurableSpace.pi Real Real.measurableSpace	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike StieltjesFunction.measure Real.linearOrder UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace stieltjesOfMeasurableRat 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	—	IsMeasurableRatCDF.measure_stieltjesFunction_Iic isMeasurableRatCDF_toRatCDF
measure_stieltjesOfMeasurableRat_univ 📖	mathematical	Measurable MeasurableSpace.pi Real Real.measurableSpace	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike StieltjesFunction.measure Real.linearOrder UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace stieltjesOfMeasurableRat 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	—	IsMeasurableRatCDF.measure_stieltjesFunction_univ isMeasurableRatCDF_toRatCDF
monotone_defaultRatCDF 📖	mathematical	—	Monotone Real Rat.instPreorder Real.instPreorder defaultRatCDF	—	le_rfl zero_le_one Real.instZeroLEOneClass LE.le.trans_lt
stieltjesOfMeasurableRat_eq 📖	mathematical	Measurable MeasurableSpace.pi Real Real.measurableSpace	StieltjesFunction.toFun Real.linearOrder UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace stieltjesOfMeasurableRat Real.instRatCast toRatCDF	—	IsMeasurableRatCDF.stieltjesFunction_eq isMeasurableRatCDF_toRatCDF
stieltjesOfMeasurableRat_le_one 📖	mathematical	Measurable MeasurableSpace.pi Real Real.measurableSpace	Real.instLE StieltjesFunction.toFun Real.linearOrder UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace stieltjesOfMeasurableRat Real.instOne	—	IsMeasurableRatCDF.stieltjesFunction_le_one isMeasurableRatCDF_toRatCDF
stieltjesOfMeasurableRat_nonneg 📖	mathematical	Measurable MeasurableSpace.pi Real Real.measurableSpace	Real.instLE Real.instZero StieltjesFunction.toFun Real.linearOrder UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace stieltjesOfMeasurableRat	—	IsMeasurableRatCDF.stieltjesFunction_nonneg isMeasurableRatCDF_toRatCDF
stieltjesOfMeasurableRat_unit_prod 📖	mathematical	Measurable MeasurableSpace.pi Real Real.measurableSpace	stieltjesOfMeasurableRat Prod.instMeasurableSpace PUnit.instMeasurableSpace Measurable.comp measurable_snd	—	Measurable.comp measurable_snd isMeasurableRatCDF_toRatCDF IsMeasurableRatCDF.monotone_stieltjesFunctionAux IsMeasurableRatCDF.continuousWithinAt_stieltjesFunctionAux_Ici IsMeasurableRatCDF.stieltjesFunctionAux_unit_prod toRatCDF_unit_prod
stronglyMeasurable_stieltjesOfMeasurableRat 📖	mathematical	Measurable MeasurableSpace.pi Real Real.measurableSpace	MeasureTheory.StronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace StieltjesFunction.toFun Real.linearOrder stieltjesOfMeasurableRat	—	IsMeasurableRatCDF.stronglyMeasurable_stieltjesFunction isMeasurableRatCDF_toRatCDF
tendsto_defaultRatCDF_atBot 📖	mathematical	—	Filter.Tendsto Real defaultRatCDF Filter.atBot Rat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero	—	Filter.tendsto_congr' Filter.EventuallyEq.eq_1 Filter.eventually_atBot instIsCodirectedOrder IsStrictOrderedRing.toIsOrderedRing Rat.instIsStrictOrderedRing instArchimedeanRat LE.le.trans_lt lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.add_lt_of_neg_of_le neg_neg_of_pos Rat.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_nonpos_of_le tendsto_const_nhds
tendsto_defaultRatCDF_atTop 📖	mathematical	—	Filter.Tendsto Real defaultRatCDF Filter.atTop Rat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instOne	—	Filter.tendsto_congr' Filter.EventuallyEq.eq_1 Filter.eventually_atTop instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Rat.instIsStrictOrderedRing instArchimedeanRat not_lt tendsto_const_nhds
tendsto_stieltjesOfMeasurableRat_atBot 📖	mathematical	Measurable MeasurableSpace.pi Real Real.measurableSpace	Filter.Tendsto StieltjesFunction.toFun Real.linearOrder UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace stieltjesOfMeasurableRat Filter.atBot Real.instPreorder nhds Real.instZero	—	IsMeasurableRatCDF.tendsto_stieltjesFunction_atBot isMeasurableRatCDF_toRatCDF
tendsto_stieltjesOfMeasurableRat_atTop 📖	mathematical	Measurable MeasurableSpace.pi Real Real.measurableSpace	Filter.Tendsto StieltjesFunction.toFun Real.linearOrder UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace stieltjesOfMeasurableRat Filter.atTop Real.instPreorder nhds Real.instOne	—	IsMeasurableRatCDF.tendsto_stieltjesFunction_atTop isMeasurableRatCDF_toRatCDF
toRatCDF_of_isRatStieltjesPoint 📖	mathematical	IsRatStieltjesPoint	toRatCDF	—	toRatCDF.eq_1
toRatCDF_unit_prod 📖	mathematical	—	toRatCDF	—	isRatStieltjesPoint_unit_prod_iff

ProbabilityTheory.IsMeasurableRatCDF

Definitions

Name	Category	Theorems
stieltjesFunction 📖	CompOp	11 math math: instIsProbabilityMeasure_stieltjesFunction, stronglyMeasurable_stieltjesFunction, measure_stieltjesFunction_univ, stieltjesFunction_eq, measure_stieltjesFunction_Iic, measurable_stieltjesFunction, measurable_measure_stieltjesFunction, tendsto_stieltjesFunction_atTop, stieltjesFunction_le_one, stieltjesFunction_nonneg, tendsto_stieltjesFunction_atBot
stieltjesFunctionAux 📖	CompOp	7 math math: stieltjesFunctionAux_eq, stieltjesFunctionAux_unit_prod, continuousWithinAt_stieltjesFunctionAux_Ici, stieltjesFunctionAux_def, stieltjesFunctionAux_def', monotone_stieltjesFunctionAux, stieltjesFunctionAux_nonneg

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousWithinAt_stieltjesFunctionAux_Ici 📖	mathematical	ProbabilityTheory.IsMeasurableRatCDF	ContinuousWithinAt Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace stieltjesFunctionAux Set.Ici Real.instPreorder	—	continuousWithinAt_Ioi_iff_Ici sInf_image' Real.iInf_Ioi_eq_iInf_rat_gt stieltjesFunctionAux_nonneg monotone_stieltjesFunctionAux stieltjesFunctionAux_eq ContinuousWithinAt.eq_1 stieltjesFunctionAux_def Monotone.tendsto_nhdsGT instOrderTopologyReal
iInf_rat_gt_eq 📖	mathematical	ProbabilityTheory.IsMeasurableRatCDF	iInf Real Set.Elem Set.Ioi Rat.instPreorder Real.instInfSet Set Set.instMembership	—	ProbabilityTheory.IsRatStieltjesPoint.iInf_rat_gt_eq isRatStieltjesPoint
instIsProbabilityMeasure_stieltjesFunction 📖	mathematical	ProbabilityTheory.IsMeasurableRatCDF	MeasureTheory.IsProbabilityMeasure Real Real.measurableSpace StieltjesFunction.measure Real.linearOrder UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace stieltjesFunction 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_stieltjesFunction_univ
isRatStieltjesPoint 📖	mathematical	ProbabilityTheory.IsMeasurableRatCDF	ProbabilityTheory.IsRatStieltjesPoint	—	—
le_one 📖	mathematical	ProbabilityTheory.IsMeasurableRatCDF	Real Real.instLE Real.instOne	—	Monotone.ge_of_tendsto HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Rat.instIsStrictOrderedRing instArchimedeanRat ProbabilityTheory.IsRatStieltjesPoint.mono isRatStieltjesPoint ProbabilityTheory.IsRatStieltjesPoint.tendsto_atTop_one
measurable 📖	mathematical	ProbabilityTheory.IsMeasurableRatCDF	Measurable MeasurableSpace.pi Real Real.measurableSpace	—	—
measurable_measure_stieltjesFunction 📖	mathematical	ProbabilityTheory.IsMeasurableRatCDF	Measurable MeasureTheory.Measure Real Real.measurableSpace MeasureTheory.Measure.instMeasurableSpace StieltjesFunction.measure Real.linearOrder UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace stieltjesFunction 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	—	StieltjesFunction.measurable_measure measurable_stieltjesFunction tendsto_stieltjesFunction_atBot tendsto_stieltjesFunction_atTop
measurable_stieltjesFunction 📖	mathematical	ProbabilityTheory.IsMeasurableRatCDF	Measurable Real Real.measurableSpace StieltjesFunction.toFun Real.linearOrder UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace stieltjesFunction	—	StieltjesFunction.iInf_rat_gt_eq stieltjesFunction_eq Measurable.iInf Real.borelSpace instOrderTopologyReal instSecondCountableTopologyReal Subtype.countable Encodable.countable Measurable.eval measurable
measure_stieltjesFunction_Iic 📖	mathematical	ProbabilityTheory.IsMeasurableRatCDF	DFunLike.coe MeasureTheory.Measure Real Real.measurableSpace Set ENNReal MeasureTheory.Measure.instFunLike StieltjesFunction.measure Real.linearOrder UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace stieltjesFunction 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_stieltjesFunction_atBot
measure_stieltjesFunction_univ 📖	mathematical	ProbabilityTheory.IsMeasurableRatCDF	DFunLike.coe MeasureTheory.Measure Real Real.measurableSpace Set ENNReal MeasureTheory.Measure.instFunLike StieltjesFunction.measure Real.linearOrder UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace stieltjesFunction 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_stieltjesFunction_atBot tendsto_stieltjesFunction_atTop
monotone_stieltjesFunctionAux 📖	mathematical	ProbabilityTheory.IsMeasurableRatCDF	Monotone Real Real.instPreorder stieltjesFunctionAux	—	exists_rat_gt Real.instIsStrictOrderedRing Real.instArchimedean stieltjesFunctionAux_def le_ciInf LE.le.trans_eq LE.le.trans_lt Subtype.prop ciInf_le nonneg
nonneg 📖	mathematical	ProbabilityTheory.IsMeasurableRatCDF	Real Real.instLE Real.instZero	—	Monotone.le_of_tendsto HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid instIsCodirectedOrder IsStrictOrderedRing.toIsOrderedRing Rat.instIsStrictOrderedRing instArchimedeanRat ProbabilityTheory.IsRatStieltjesPoint.mono isRatStieltjesPoint ProbabilityTheory.IsRatStieltjesPoint.tendsto_atBot_zero
stieltjesFunctionAux_def 📖	mathematical	—	stieltjesFunctionAux iInf Real Real.instLT Real.instRatCast Real.instInfSet	—	—
stieltjesFunctionAux_def' 📖	mathematical	—	stieltjesFunctionAux iInf Real Real.instLT Real.instRatCast Real.instInfSet	—	stieltjesFunctionAux_def
stieltjesFunctionAux_eq 📖	mathematical	ProbabilityTheory.IsMeasurableRatCDF	stieltjesFunctionAux Real Real.instRatCast	—	iInf_rat_gt_eq stieltjesFunctionAux_def Equiv.iInf_congr Real.instIsStrictOrderedRing Subtype.coe_eta
stieltjesFunctionAux_nonneg 📖	mathematical	ProbabilityTheory.IsMeasurableRatCDF	Real Real.instLE Real.instZero stieltjesFunctionAux	—	exists_rat_gt Real.instIsStrictOrderedRing Real.instArchimedean stieltjesFunctionAux_def le_ciInf nonneg
stieltjesFunctionAux_unit_prod 📖	mathematical	—	stieltjesFunctionAux	—	stieltjesFunctionAux_def'
stieltjesFunction_eq 📖	mathematical	ProbabilityTheory.IsMeasurableRatCDF	StieltjesFunction.toFun Real Real.linearOrder UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace stieltjesFunction Real.instRatCast	—	stieltjesFunctionAux_eq
stieltjesFunction_le_one 📖	mathematical	ProbabilityTheory.IsMeasurableRatCDF	Real Real.instLE StieltjesFunction.toFun Real.linearOrder UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace stieltjesFunction Real.instOne	—	exists_rat_gt Real.instIsStrictOrderedRing Real.instArchimedean StieltjesFunction.iInf_rat_gt_eq stieltjesFunction_eq ciInf_le_of_le nonneg le_one
stieltjesFunction_nonneg 📖	mathematical	ProbabilityTheory.IsMeasurableRatCDF	Real Real.instLE Real.instZero StieltjesFunction.toFun Real.linearOrder UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace stieltjesFunction	—	stieltjesFunctionAux_nonneg
stronglyMeasurable_stieltjesFunction 📖	mathematical	ProbabilityTheory.IsMeasurableRatCDF	MeasureTheory.StronglyMeasurable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace StieltjesFunction.toFun Real.linearOrder stieltjesFunction	—	Measurable.stronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace instSecondCountableTopologyReal BorelSpace.opensMeasurable Real.borelSpace measurable_stieltjesFunction
tendsto_atBot_zero 📖	mathematical	ProbabilityTheory.IsMeasurableRatCDF	Filter.Tendsto Real Filter.atBot Rat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero	—	ProbabilityTheory.IsRatStieltjesPoint.tendsto_atBot_zero isRatStieltjesPoint
tendsto_atTop_one 📖	mathematical	ProbabilityTheory.IsMeasurableRatCDF	Filter.Tendsto Real Filter.atTop Rat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instOne	—	ProbabilityTheory.IsRatStieltjesPoint.tendsto_atTop_one isRatStieltjesPoint
tendsto_stieltjesFunction_atBot 📖	mathematical	ProbabilityTheory.IsMeasurableRatCDF	Filter.Tendsto Real StieltjesFunction.toFun Real.linearOrder UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace stieltjesFunction Filter.atBot Real.instPreorder nhds Real.instZero	—	exists_rat_btwn Real.instIsStrictOrderedRing Real.instArchimedean lt_add_one Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Filter.tendsto_atBot_atBot instIsCodirectedOrder Real.instIsOrderedRing LE.le.trans LT.lt.le add_le_add covariant_swap_add_of_covariant_add le_rfl sub_add_cancel tendsto_of_tendsto_of_tendsto_of_le_of_le instOrderTopologyReal tendsto_const_nhds Filter.Tendsto.comp tendsto_atBot_zero stieltjesFunction_nonneg stieltjesFunction_eq StieltjesFunction.mono
tendsto_stieltjesFunction_atTop 📖	mathematical	ProbabilityTheory.IsMeasurableRatCDF	Filter.Tendsto Real StieltjesFunction.toFun Real.linearOrder UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace stieltjesFunction Filter.atTop Real.instPreorder nhds Real.instOne	—	exists_rat_btwn Real.instIsStrictOrderedRing Real.instArchimedean sub_one_lt Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Filter.tendsto_atTop_atTop instIsDirectedOrder Real.instIsOrderedRing LT.lt.le le_of_add_le_add_right IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le LE.le.trans sub_le_iff_le_add covariant_swap_add_of_covariant_add tendsto_of_tendsto_of_tendsto_of_le_of_le instOrderTopologyReal Filter.Tendsto.comp tendsto_atTop_one tendsto_const_nhds stieltjesFunction_eq StieltjesFunction.mono le_of_lt stieltjesFunction_le_one

ProbabilityTheory.IsRatStieltjesPoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iInf_rat_gt_eq 📖	mathematical	ProbabilityTheory.IsRatStieltjesPoint	iInf Real Set.Elem Set.Ioi Rat.instPreorder Real.instInfSet Set Set.instMembership	—	—
ite 📖	—	ProbabilityTheory.IsRatStieltjesPoint	—	—	mono tendsto_atTop_one tendsto_atBot_zero iInf_rat_gt_eq
mono 📖	mathematical	ProbabilityTheory.IsRatStieltjesPoint	Monotone Real Rat.instPreorder Real.instPreorder	—	—
tendsto_atBot_zero 📖	mathematical	ProbabilityTheory.IsRatStieltjesPoint	Filter.Tendsto Real Filter.atBot Rat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero	—	—
tendsto_atTop_one 📖	mathematical	ProbabilityTheory.IsRatStieltjesPoint	Filter.Tendsto Real Filter.atTop Rat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instOne	—	—

StieltjesFunction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurable_measure 📖	mathematical	Measurable Real Real.measurableSpace toFun Real.linearOrder UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Filter.Tendsto Filter.atBot Real.instPreorder nhds Real.instZero Filter.atTop Real.instOne	MeasureTheory.Measure MeasureTheory.Measure.instMeasurableSpace measure 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 isProbabilityMeasure Measurable.measure_of_isPiSystem_of_isProbabilityMeasure borel_eq_generateFrom_Iic isPiSystem_Iic measure_Iic sub_zero Measurable.ennreal_ofReal

---

← Back to Index