IntegralRNDeriv

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

Statistics

Metric	Count
Definitions	0
Theorems apply_rnDeriv_ae_le_integral, integrable_apply_rnDeriv_of_integrable_compProd, integrable_toReal_rnDeriv, le_integral_rnDeriv_of_ac, lintegral_rnDeriv_compProd, mul_le_integral_rnDeriv_of_ac	6
Total	6

ConvexOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_rnDeriv_ae_le_integral 📖	mathematical	MeasureTheory.StronglyMeasurable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.measurableSpace ConvexOn Real.semiring Real.partialOrder Real.instAddCommMonoid Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Set.Ici Real.instPreorder Real.instZero ContinuousWithinAt MeasureTheory.Integrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Prod.instMeasurableSpace ENNReal.toReal MeasureTheory.Measure.rnDeriv MeasureTheory.Measure.compProd MeasureTheory.Measure.AbsolutelyContinuous	Filter.EventuallyLE Real Real.instLE MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass ENNReal.toReal MeasureTheory.Measure.rnDeriv MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal DFunLike.coe ProbabilityTheory.Kernel ProbabilityTheory.Kernel.instFunLike Prod.instMeasurableSpace MeasureTheory.Measure.compProd	—	eq_or_lt_of_le continuousOn_interior FiniteDimensional.rclike_to_real interior_Ici' instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMinOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial ContinuousAt.continuousWithinAt continuousWithinAt_iff_continuousAt Ioi_mem_nhds instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.ae_ae_of_ae_compProd MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite ProbabilityTheory.Kernel.IsFiniteKernel.isSFiniteKernel ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel MeasureTheory.Measure.rnDeriv_lt_top MeasureTheory.Measure.instIsFiniteMeasureProdCompProdOfIsFiniteKernel MeasureTheory.Measure.integrable_toReal_rnDeriv Filter.mp_mem MeasureTheory.Measure.ae_rnDeriv_ne_zero_imp_of_ae MeasureTheory.lintegral_rnDeriv_compProd Filter.univ_mem' MulZeroClass.zero_mul MeasureTheory.IsProbabilityMeasure.measure_univ ProbabilityTheory.IsMarkovKernel.is_probability_measure' mul_one Filter.EventuallyEq.symm ProbabilityTheory.rnDeriv_compProd MeasureTheory.Measure.ae_compProd_iff Measurable.eq instMeasurableEqOfSecondCountableTopologyOfT2Space BorelSpace.opensMeasurable ENNReal.borelSpace ENNReal.instSecondCountableTopology ENNReal.instT2Space Measurable.mul ENNReal.instMeasurableMul₂ Measurable.fun_comp MeasureTheory.Measure.measurable_rnDeriv Measurable.fst measurable_id' Filter.EventuallyEq.eq_1 MeasureTheory.Measure.integrable_compProd_iff MeasureTheory.StronglyMeasurable.aestronglyMeasurable MeasureTheory.StronglyMeasurable.comp_measurable Measurable.ennreal_toReal Measurable.stronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace instSecondCountableTopologyReal Real.borelSpace MeasureTheory.lintegral_const_mul Measurable.prodMk measurable_const MeasureTheory.lintegral_congr_ae MeasureTheory.integral_toReal Measurable.comp_aemeasurable' AEMeasurable.prodMk aemeasurable_const aemeasurable_id MeasureTheory.average_eq_integral map_average_le Real.instCompleteSpace ProbabilityTheory.IsFiniteKernel.isFiniteMeasure MeasureTheory.IsProbabilityMeasure.neZero isClosed_Ici instClosedIciTopology
integrable_apply_rnDeriv_of_integrable_compProd 📖	mathematical	MeasureTheory.StronglyMeasurable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.measurableSpace ConvexOn Real.semiring Real.partialOrder Real.instAddCommMonoid Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Set.Ici Real.instPreorder Real.instZero ContinuousWithinAt MeasureTheory.Integrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Prod.instMeasurableSpace ENNReal.toReal MeasureTheory.Measure.rnDeriv MeasureTheory.Measure.compProd MeasureTheory.Measure.AbsolutelyContinuous	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 MeasureTheory.Measure.rnDeriv	—	eq_or_lt_of_le continuousOn_interior FiniteDimensional.rclike_to_real interior_Ici' instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMinOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial ContinuousAt.continuousWithinAt continuousWithinAt_iff_continuousAt Ioi_mem_nhds instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid exists_affine_le_real isClosed_Ici instClosedIciTopology ContinuousOn.lowerSemicontinuousOn MeasureTheory.integrable_of_le_of_le MeasureTheory.StronglyMeasurable.aestronglyMeasurable MeasureTheory.StronglyMeasurable.comp_measurable Measurable.ennreal_toReal MeasureTheory.Measure.measurable_rnDeriv MeasureTheory.ae_of_all MeasureTheory.Measure.instOuterMeasureClass ENNReal.toReal_nonneg apply_rnDeriv_ae_le_integral MeasureTheory.Integrable.fun_add IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal MeasureTheory.Integrable.const_mul MeasureTheory.Measure.integrable_toReal_rnDeriv MeasureTheory.integrable_const MeasureTheory.Integrable.integral_compProd ProbabilityTheory.Kernel.const.instIsSFiniteKernel MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite ProbabilityTheory.Kernel.IsSFiniteKernel.prodMkLeft ProbabilityTheory.Kernel.IsFiniteKernel.isSFiniteKernel ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel

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 Real.instLE Measure.real Set.univ integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal ENNReal.toReal Measure.rnDeriv	—	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
lintegral_rnDeriv_compProd 📖	mathematical	Measure.AbsolutelyContinuous Prod.instMeasurableSpace Measure.compProd	Filter.Eventually ENNReal lintegral DFunLike.coe ProbabilityTheory.Kernel Measure ProbabilityTheory.Kernel.instFunLike Measure.rnDeriv Prod.instMeasurableSpace Measure.compProd Set Measure.instFunLike Set.univ ae Measure.instOuterMeasureClass	—	ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite IsFiniteMeasure.toSigmaFinite Measurable.lintegral_kernel_prod_left ProbabilityTheory.Kernel.IsFiniteKernel.isSFiniteKernel Measurable.fun_comp Measure.measurable_rnDeriv Measurable.prodMk Measurable.snd measurable_id' Measurable.fst ProbabilityTheory.Kernel.measurable_coe MeasurableSet.univ Measure.restrict_univ Measure.setLIntegral_compProd instSFiniteOfSigmaFinite Measure.setLIntegral_rnDeriv Measure.haveLebesgueDecomposition_of_sigmaFinite Measure.instSFiniteProdCompProd Measure.instIsFiniteMeasureProdCompProdOfIsFiniteKernel Measure.compProd_apply_prod
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 Real.instLE Real.instMul Measure.real Set.univ DivInvMonoid.toDiv Real.instDivInvMonoid integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal ENNReal.toReal Measure.rnDeriv	—	div_zero MulZeroClass.zero_mul integral_zero_measure instReflLe 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