IntegralRNDeriv

📁 Source: Mathlib/MeasureTheory/Measure/Decomposition/IntegralRNDeriv.lean

Statistics

Metric	Count
Definitions	0
Theorems integrable_toReal_rnDeriv, le_integral_rnDeriv_of_ac, mul_le_integral_rnDeriv_of_ac	3
Total	3

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
le_integral_rnDeriv_of_ac 📖	mathematical	ConvexOn Real Real.semiring Real.partialOrder Real.instAddCommMonoid Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Set.Ici Real.instPreorder Real.instZero ContinuousWithinAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Integrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing ENNReal.toReal Measure.rnDeriv Measure.AbsolutelyContinuous	Real.instLE Measure.real Set.univ integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal	—	eq_or_lt_of_le ConvexOn.continuousOn_interior FiniteDimensional.rclike_to_real ContinuousAt.continuousWithinAt continuousWithinAt_iff_continuousAt Ioi_mem_nhds instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid interior_Ici' instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMinOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial Measure.integral_toReal_rnDeriv IsFiniteMeasure.toSigmaFinite IsZeroOrProbabilityMeasure.toIsFiniteMeasure instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure average_eq_integral ConvexOn.map_average_le Real.instCompleteSpace IsProbabilityMeasure.neZero isClosed_Ici instClosedIciTopology Measure.instOuterMeasureClass Measure.integrable_toReal_rnDeriv
mul_le_integral_rnDeriv_of_ac 📖	mathematical	ConvexOn Real Real.semiring Real.partialOrder Real.instAddCommMonoid Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Set.Ici Real.instPreorder Real.instZero ContinuousWithinAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Integrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing ENNReal.toReal Measure.rnDeriv Measure.AbsolutelyContinuous	Real.instLE Real.instMul Measure.real Set.univ DivInvMonoid.toDiv Real.instDivInvMonoid integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal	—	div_zero MulZeroClass.zero_mul integral_zero_measure IsScalarTower.right Measure.smul_finite Measure.AbsolutelyContinuous.smul Measure.instOuterMeasureClass Measure.rnDeriv_smul_left_of_ne_top' IsFiniteMeasure.toSigmaFinite IsFiniteMeasure.average Measure.ae_ennreal_smul_measure_eq Measure.rnDeriv_smul_right_of_ne_top' Filter.mp_mem Filter.univ_mem' Pi.smul_apply smul_eq_mul inv_inv mul_assoc ENNReal.inv_mul_cancel one_mul integral_smul_measure ENNReal.toReal_inv integral_congr_ae le_integral_rnDeriv_of_ac isProbabilityMeasureSMul Integrable.smul_measure integrable_congr div_eq_inv_mul ENNReal.toReal_mul div_le_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono mul_comm

MeasureTheory.Measure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integrable_toReal_rnDeriv 📖	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 rnDeriv	—	MeasureTheory.integrable_toReal_of_lintegral_ne_top Measurable.aemeasurable measurable_rnDeriv LT.lt.ne lintegral_rnDeriv_lt_top

---

← Back to Index