L1

📁 Source: Mathlib/MeasureTheory/Integral/Bochner/L1.lean

Statistics

Metric	Count
Definitions integral, integralCLM, integralCLM', negPart, posPart, integral, integralCLM, integralCLM', integral, negPart, posPart, weightedSMul	12
Theorems coe_negPart, coe_posPart, integralCLM'_L1_eq_integral, integral_L1_eq_integral, integral_add, integral_congr, integral_eq_integral, integral_eq_lintegral, integral_eq_norm_posPart_sub, integral_eq_setToL1S, integral_smul, negPart_toSimpleFunc, norm_Integral_le_one, norm_eq_integral, norm_integral_le_norm, posPart_toSimpleFunc, continuous_integral, integral_add, integral_def, integral_eq, integral_eq', integral_eq_norm_posPart_sub, integral_eq_setToL1, integral_neg, integral_smul, integral_sub, integral_zero, nnnorm_Integral_le_one, nnnorm_integral_le, norm_Integral_le_one, norm_integral_le, integral_add, integral_add_measure, integral_congr, integral_const, integral_def, integral_eq, integral_eq_lintegral, integral_eq_lintegral', integral_eq_sum_filter, integral_eq_sum_of_subset, integral_mono, integral_mono_measure, integral_neg, integral_nonneg, integral_piecewise_zero, integral_smul, integral_sub, map_integral, negPart_map_norm, norm_integral_le_integral_norm, norm_setToSimpleFunc_le_integral_norm, posPart_map_norm, posPart_sub_negPart, dominatedFinMeasAdditive_weightedSMul, norm_weightedSMul_le, weightedSMul_add_measure, weightedSMul_apply, weightedSMul_congr, weightedSMul_empty, weightedSMul_nonneg, weightedSMul_null, weightedSMul_smul, weightedSMul_smul_measure, weightedSMul_union, weightedSMul_union', weightedSMul_zero_measure	67
Total	79

MeasureTheory

Definitions

Name	Category	Theorems
weightedSMul 📖	CompOp	17 math math: weightedSMul_apply, weightedSMul_nonneg, L1.SimpleFunc.integral_eq_setToL1S, L1.integral_eq_setToL1, weightedSMul_empty, weightedSMul_null, norm_weightedSMul_le, weightedSMul_add_measure, weightedSMul_smul, weightedSMul_union, SimpleFunc.integral_def, integral_eq_setToFun, weightedSMul_union', weightedSMul_congr, weightedSMul_smul_measure, dominatedFinMeasAdditive_weightedSMul, weightedSMul_zero_measure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dominatedFinMeasAdditive_weightedSMul 📖	mathematical	—	DominatedFinMeasAdditive ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.toSeminormedAddCommGroup DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.normedCommRing weightedSMul Real.instOne	—	RingHomIsometric.ids weightedSMul_union LE.le.trans norm_weightedSMul_le Eq.le one_mul
norm_weightedSMul_le 📖	mathematical	—	Real Real.instLE Norm.norm ContinuousLinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.hasOpNorm DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField weightedSMul Measure.real	—	norm_smul smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul NormedSpace.toNormSMulClass RingHomIsometric.ids LE.le.trans mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Real.instIsOrderedRing ContinuousLinearMap.norm_id_le norm_nonneg Eq.le mul_one Real.norm_eq_abs abs_eq_self Real.instIsOrderedAddMonoid ENNReal.toReal_nonneg
weightedSMul_add_measure 📖	mathematical	—	weightedSMul Measure Measure.instAdd ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.add IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup	—	ContinuousLinearMap.ext IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup weightedSMul_apply measureReal_add_apply add_smul
weightedSMul_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.funLike weightedSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Measure.real	—	—
weightedSMul_congr 📖	mathematical	DFunLike.coe Measure Set ENNReal Measure.instFunLike	weightedSMul	—	ContinuousLinearMap.ext weightedSMul_apply
weightedSMul_empty 📖	mathematical	—	weightedSMul Set Set.instEmptyCollection ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.zero	—	ContinuousLinearMap.ext weightedSMul_apply measureReal_empty zero_smul
weightedSMul_nonneg 📖	mathematical	Preorder.toLE PartialOrder.toPreorder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.funLike weightedSMul	—	smul_nonneg IsOrderedModule.toPosSMulMono ENNReal.toReal_nonneg
weightedSMul_null 📖	mathematical	DFunLike.coe Measure Set ENNReal Measure.instFunLike instZeroENNReal	weightedSMul ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.zero	—	ContinuousLinearMap.ext weightedSMul_apply measureReal_def zero_smul
weightedSMul_smul 📖	mathematical	—	DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.funLike weightedSMul	—	weightedSMul_apply SMulCommClass.smul_comm
weightedSMul_smul_measure 📖	mathematical	—	weightedSMul ENNReal Measure Measure.instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right Real ContinuousLinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.instSMul DistribMulAction.toDistribSMul Real.instMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing Real.commRing UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass IsBoundedSMul.toUniformContinuousConstSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toIsBoundedSMul ENNReal.toReal	—	ContinuousLinearMap.ext IsScalarTower.right smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul weightedSMul_apply measureReal_ennreal_smul_apply smul_smul
weightedSMul_union 📖	mathematical	MeasurableSet Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	weightedSMul Set.instUnion ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.add IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup	—	weightedSMul_union'
weightedSMul_union' 📖	mathematical	MeasurableSet Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	weightedSMul Set.instUnion ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.add IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup	—	ContinuousLinearMap.ext IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup weightedSMul_apply measureReal_union add_smul
weightedSMul_zero_measure 📖	mathematical	—	weightedSMul Measure Measure.instZero Pi.instZero Set ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.zero	—	zero_smul IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul

MeasureTheory.L1

Definitions

Name	Category	Theorems
integral 📖	CompOp	17 math math: integral_smul, continuous_integral, integral_def, integral_eq_setToL1, nnnorm_integral_le, integral_eq_norm_posPart_sub, norm_integral_le, integral_zero, integral_add, integral_eq_integral, MeasureTheory.integral_def, integral_eq', MeasureTheory.integral_eq, integral_sub, SimpleFunc.integral_L1_eq_integral, integral_eq, integral_neg
integralCLM 📖	CompOp	4 math math: integral_def, nnnorm_Integral_le_one, norm_Integral_le_one, integral_eq
integralCLM' 📖	CompOp	2 math math: SimpleFunc.integralCLM'_L1_eq_integral, integral_eq'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_integral 📖	mathematical	—	Continuous MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal MeasureTheory.Lp.instNormedAddCommGroup fact_one_le_one_ennreal integral	—	SeminormedAddCommGroup.toIsTopologicalAddGroup fact_one_le_one_ennreal integral_def ContinuousLinearMap.continuous NormedSpace.toIsBoundedSMul
integral_add 📖	mathematical	—	integral MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal AddSubgroup.add AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	SeminormedAddCommGroup.toIsTopologicalAddGroup fact_one_le_one_ennreal integral_def map_add NormedSpace.toIsBoundedSMul SemilinearMapClass.toAddHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass
integral_def 📖	mathematical	—	integral DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal MeasureTheory.Lp.instNormedAddCommGroup fact_one_le_one_ennreal ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid MeasureTheory.Lp.instModule NormedCommRing.toNormedRing Real.normedCommRing NormedSpace.toModule Real.normedField ContinuousLinearMap.funLike integralCLM	—	SeminormedAddCommGroup.toIsTopologicalAddGroup fact_one_le_one_ennreal
integral_eq 📖	mathematical	—	integral DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal MeasureTheory.Lp.instNormedAddCommGroup fact_one_le_one_ennreal ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid MeasureTheory.Lp.instModule NormedCommRing.toNormedRing Real.normedCommRing NormedSpace.toModule Real.normedField NormedSpace.toIsBoundedSMul ContinuousLinearMap.funLike integralCLM	—	SeminormedAddCommGroup.toIsTopologicalAddGroup fact_one_le_one_ennreal NormedSpace.toIsBoundedSMul integral_def
integral_eq' 📖	mathematical	—	integral DFunLike.coe ContinuousLinearMap Ring.toSemiring NormedRing.toRing RingHom.id Semiring.toNonAssocSemiring MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal MeasureTheory.Lp.instNormedAddCommGroup fact_one_le_one_ennreal ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid MeasureTheory.Lp.instModule ContinuousLinearMap.funLike integralCLM'	—	SeminormedAddCommGroup.toIsTopologicalAddGroup isClosed_property fact_one_le_one_ennreal MeasureTheory.Lp.simpleFunc.denseRange ENNReal.one_ne_top isClosed_eq TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace integral_def ContinuousLinearMap.continuous NormedSpace.toIsBoundedSMul SimpleFunc.integral_L1_eq_integral SimpleFunc.integralCLM'_L1_eq_integral
integral_eq_norm_posPart_sub 📖	mathematical	—	integral Real Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField Real.instCompleteSpace Real.instSub Norm.norm MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal MeasureTheory.Lp.instNorm MeasureTheory.Lp.posPart MeasureTheory.Lp.negPart	—	SeminormedAddCommGroup.toIsTopologicalAddGroup isClosed_property fact_one_le_one_ennreal Real.instCompleteSpace MeasureTheory.Lp.simpleFunc.denseRange ENNReal.one_ne_top isClosed_eq TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace integral_def ContinuousLinearMap.cont Continuous.sub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal Continuous.comp continuous_norm MeasureTheory.Lp.continuous_posPart MeasureTheory.Lp.continuous_negPart SimpleFunc.integral_L1_eq_integral SimpleFunc.integral_eq_norm_posPart_sub
integral_eq_setToL1 📖	mathematical	—	integral DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal MeasureTheory.Lp.instNormedAddCommGroup fact_one_le_one_ennreal ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid MeasureTheory.Lp.instModule NormedCommRing.toNormedRing Real.normedCommRing NormedSpace.toModule Real.normedField NormedSpace.toIsBoundedSMul ContinuousLinearMap.funLike setToL1 MeasureTheory.weightedSMul Real.instOne MeasureTheory.dominatedFinMeasAdditive_weightedSMul	—	SeminormedAddCommGroup.toIsTopologicalAddGroup fact_one_le_one_ennreal NormedSpace.toIsBoundedSMul MeasureTheory.dominatedFinMeasAdditive_weightedSMul integral_def
integral_neg 📖	mathematical	—	integral MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal AddSubgroup.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	SeminormedAddCommGroup.toIsTopologicalAddGroup fact_one_le_one_ennreal integral_def map_neg NormedSpace.toIsBoundedSMul DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass
integral_smul 📖	mathematical	—	integral MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid MeasureTheory.Lp.instNormedAddCommGroup fact_one_le_one_ennreal ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid MeasureTheory.Lp.instModule	—	SeminormedAddCommGroup.toIsTopologicalAddGroup fact_one_le_one_ennreal integral_eq' map_smul SemilinearMapClass.toMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass
integral_sub 📖	mathematical	—	integral MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal AddSubgroup.sub SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	SeminormedAddCommGroup.toIsTopologicalAddGroup fact_one_le_one_ennreal integral_def map_sub NormedSpace.toIsBoundedSMul DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass
integral_zero 📖	mathematical	—	integral MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal AddSubgroup.zero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	SeminormedAddCommGroup.toIsTopologicalAddGroup fact_one_le_one_ennreal integral_def map_zero NormedSpace.toIsBoundedSMul AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass
nnnorm_Integral_le_one 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal MeasureTheory.Lp.instNormedAddCommGroup fact_one_le_one_ennreal ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid MeasureTheory.Lp.instModule NormedCommRing.toNormedRing Real.normedCommRing NormedSpace.toModule Real.normedField NormedSpace.toIsBoundedSMul SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup ContinuousLinearMap.toSeminormedAddCommGroup DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField MeasureTheory.Lp.instNormedSpace NontriviallyNormedField.toNormedField RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing integralCLM instOneNNReal	—	norm_Integral_le_one
nnnorm_integral_le 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup integral MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal MeasureTheory.Lp.instNNNorm	—	SeminormedAddCommGroup.toIsTopologicalAddGroup norm_integral_le
norm_Integral_le_one 📖	mathematical	—	Real Real.instLE Norm.norm ContinuousLinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal MeasureTheory.Lp.instNormedAddCommGroup fact_one_le_one_ennreal ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid MeasureTheory.Lp.instModule NormedCommRing.toNormedRing Real.normedCommRing NormedSpace.toModule Real.normedField NormedSpace.toIsBoundedSMul ContinuousLinearMap.hasOpNorm DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField MeasureTheory.Lp.instNormedSpace NontriviallyNormedField.toNormedField integralCLM Real.instOne	—	norm_setToL1_le MeasureTheory.dominatedFinMeasAdditive_weightedSMul zero_le_one Real.instZeroLEOneClass
norm_integral_le 📖	mathematical	—	Real Real.instLE Norm.norm NormedAddCommGroup.toNorm integral MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal MeasureTheory.Lp.instNorm	—	SeminormedAddCommGroup.toIsTopologicalAddGroup fact_one_le_one_ennreal NormedSpace.toIsBoundedSMul integral_def ContinuousLinearMap.le_opNorm RingHomIsometric.ids mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono Real.instIsOrderedRing norm_Integral_le_one norm_nonneg one_mul

MeasureTheory.L1.SimpleFunc

Definitions

Name	Category	Theorems
integral 📖	CompOp	10 math math: integral_eq_setToL1S, integral_add, integral_eq_norm_posPart_sub, integralCLM'_L1_eq_integral, integral_smul, integral_eq_lintegral, norm_integral_le_norm, integral_L1_eq_integral, integral_eq_integral, integral_congr
integralCLM 📖	CompOp	1 math math: norm_Integral_le_one
integralCLM' 📖	CompOp	—
negPart 📖	CompOp	3 math math: integral_eq_norm_posPart_sub, coe_negPart, negPart_toSimpleFunc
posPart 📖	CompOp	3 math math: integral_eq_norm_posPart_sub, posPart_toSimpleFunc, coe_posPart

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_negPart 📖	mathematical	—	MeasureTheory.AEEqFun Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.normedAddCommGroup AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal AddSubgroup.toAddGroup MeasureTheory.Lp.simpleFunc negPart MeasureTheory.Lp.negPart	—	SeminormedAddCommGroup.toIsTopologicalAddGroup
coe_posPart 📖	mathematical	—	MeasureTheory.AEEqFun Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.normedAddCommGroup AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal AddSubgroup.toAddGroup MeasureTheory.Lp.simpleFunc posPart MeasureTheory.Lp.posPart	—	SeminormedAddCommGroup.toIsTopologicalAddGroup
integralCLM'_L1_eq_integral 📖	mathematical	—	DFunLike.coe ContinuousLinearMap Ring.toSemiring NormedRing.toRing RingHom.id Semiring.toNonAssocSemiring MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal MeasureTheory.Lp.instNormedAddCommGroup fact_one_le_one_ennreal ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid MeasureTheory.Lp.instModule ContinuousLinearMap.funLike MeasureTheory.L1.integralCLM' AddSubgroup.toAddGroup MeasureTheory.Lp.simpleFunc integral	—	SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.extend_eq fact_one_le_one_ennreal MeasureTheory.Lp.simpleFunc.denseRange ENNReal.one_ne_top MeasureTheory.Lp.simpleFunc.isUniformInducing
integral_L1_eq_integral 📖	mathematical	—	MeasureTheory.L1.integral MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal AddSubgroup.toAddGroup MeasureTheory.Lp.simpleFunc integral	—	SeminormedAddCommGroup.toIsTopologicalAddGroup fact_one_le_one_ennreal MeasureTheory.L1.integral_def MeasureTheory.L1.setToL1_eq_setToL1SCLM MeasureTheory.dominatedFinMeasAdditive_weightedSMul
integral_add 📖	mathematical	—	integral MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal AddSubgroup.toAddGroup MeasureTheory.Lp.simpleFunc AddSubgroup.add AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	SeminormedAddCommGroup.toIsTopologicalAddGroup setToL1S_add MeasureTheory.weightedSMul_null MeasureTheory.weightedSMul_union
integral_congr 📖	mathematical	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe MeasureTheory.SimpleFunc MeasureTheory.SimpleFunc.instFunLike MeasureTheory.Lp.simpleFunc.toSimpleFunc ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	integral	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.SimpleFunc.integral_congr integrable
integral_eq_integral 📖	mathematical	—	integral MeasureTheory.SimpleFunc.integral MeasureTheory.Lp.simpleFunc.toSimpleFunc ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	SeminormedAddCommGroup.toIsTopologicalAddGroup
integral_eq_lintegral 📖	mathematical	Filter.EventuallyLE Real Real.instLE MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Pi.instZero Real.instZero DFunLike.coe MeasureTheory.SimpleFunc MeasureTheory.SimpleFunc.instFunLike MeasureTheory.Lp.simpleFunc.toSimpleFunc Real.normedAddCommGroup ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	integral NormedField.toNormedSpace Real.normedField ENNReal.toReal MeasureTheory.lintegral ENNReal.ofReal	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.Measure.instOuterMeasureClass integral.eq_1 MeasureTheory.SimpleFunc.integral_eq_lintegral integrable
integral_eq_norm_posPart_sub 📖	mathematical	—	integral Real Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField Real.instSub Norm.norm MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal AddSubgroup.toAddGroup MeasureTheory.Lp.simpleFunc NormedAddCommGroup.toNorm AddSubgroup.normedAddCommGroup MeasureTheory.Lp.instNormedAddCommGroup fact_one_le_one_ennreal posPart negPart	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.Measure.instOuterMeasureClass Filter.mp_mem posPart_toSimpleFunc Filter.univ_mem' MeasureTheory.SimpleFunc.map_apply MeasureTheory.SimpleFunc.posPart_map_norm negPart_toSimpleFunc MeasureTheory.SimpleFunc.negPart_map_norm fact_one_le_one_ennreal integral.eq_1 norm_eq_integral MeasureTheory.SimpleFunc.integral_sub MeasureTheory.Integrable.congr MeasureTheory.Integrable.pos_part integrable MeasureTheory.Integrable.neg_part MeasureTheory.SimpleFunc.integral_congr MeasureTheory.SimpleFunc.sub_apply DFunLike.congr_fun MeasureTheory.SimpleFunc.posPart_sub_negPart
integral_eq_setToL1S 📖	mathematical	—	integral setToL1S MeasureTheory.weightedSMul	—	SeminormedAddCommGroup.toIsTopologicalAddGroup
integral_smul 📖	mathematical	—	integral MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal AddSubgroup.toAddGroup MeasureTheory.Lp.simpleFunc SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid AddSubgroup.normedAddCommGroup MeasureTheory.Lp.instNormedAddCommGroup fact_one_le_one_ennreal ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid instTopologicalSpaceSubtype MeasureTheory.Lp.simpleFunc.module	—	SeminormedAddCommGroup.toIsTopologicalAddGroup setToL1S_smul MeasureTheory.weightedSMul_null MeasureTheory.weightedSMul_union MeasureTheory.weightedSMul_smul
negPart_toSimpleFunc 📖	mathematical	—	Filter.EventuallyEq Real MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe MeasureTheory.SimpleFunc MeasureTheory.SimpleFunc.instFunLike MeasureTheory.Lp.simpleFunc.toSimpleFunc Real.normedAddCommGroup ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal negPart MeasureTheory.SimpleFunc.negPart Real.linearOrder Real.instZero Real.instNeg	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.Measure.instOuterMeasureClass negPart.eq_1 MeasureTheory.SimpleFunc.negPart.eq_1 Filter.mp_mem MeasureTheory.Lp.simpleFunc.neg_toSimpleFunc posPart_toSimpleFunc Filter.univ_mem'
norm_Integral_le_one 📖	mathematical	—	Real Real.instLE Norm.norm ContinuousLinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal AddSubgroup.toAddGroup MeasureTheory.Lp.simpleFunc instTopologicalSpaceSubtype MeasureTheory.Lp.instNormedAddCommGroup fact_one_le_one_ennreal ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddSubgroup.normedAddCommGroup MeasureTheory.Lp.simpleFunc.module NormedCommRing.toNormedRing Real.normedCommRing NormedSpace.toModule Real.normedField NormedSpace.toIsBoundedSMul ContinuousLinearMap.hasOpNorm AddSubgroup.seminormedAddCommGroup DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField MeasureTheory.Lp.simpleFunc.normedSpace NontriviallyNormedField.toNormedField integralCLM Real.instOne	—	LinearMap.mkContinuous_norm_le fact_one_le_one_ennreal integral_add integral_smul zero_le_one Real.instZeroLEOneClass one_mul norm_integral_le_norm
norm_eq_integral 📖	mathematical	—	Norm.norm MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal AddSubgroup.toAddGroup MeasureTheory.Lp.simpleFunc NormedAddCommGroup.toNorm AddSubgroup.normedAddCommGroup MeasureTheory.Lp.instNormedAddCommGroup fact_one_le_one_ennreal MeasureTheory.SimpleFunc.integral Real Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField MeasureTheory.SimpleFunc.map MeasureTheory.Lp.simpleFunc.toSimpleFunc	—	SeminormedAddCommGroup.toIsTopologicalAddGroup fact_one_le_one_ennreal norm_eq_sum_mul MeasureTheory.SimpleFunc.map_integral integrable norm_zero Finset.sum_congr
norm_integral_le_norm 📖	mathematical	—	Real Real.instLE Norm.norm NormedAddCommGroup.toNorm integral MeasureTheory.AEEqFun UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddSubgroup MeasureTheory.AEEqFun.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup SetLike.instMembership AddSubgroup.instSetLike MeasureTheory.Lp ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal AddSubgroup.toAddGroup MeasureTheory.Lp.simpleFunc AddSubgroup.normedAddCommGroup MeasureTheory.Lp.instNormedAddCommGroup fact_one_le_one_ennreal	—	SeminormedAddCommGroup.toIsTopologicalAddGroup fact_one_le_one_ennreal integral.eq_1 norm_eq_integral MeasureTheory.SimpleFunc.norm_integral_le_integral_norm integrable
posPart_toSimpleFunc 📖	mathematical	—	Filter.EventuallyEq Real MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe MeasureTheory.SimpleFunc MeasureTheory.SimpleFunc.instFunLike MeasureTheory.Lp.simpleFunc.toSimpleFunc Real.normedAddCommGroup ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal posPart MeasureTheory.SimpleFunc.posPart Real.linearOrder Real.instZero	—	SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.Measure.instOuterMeasureClass Filter.mp_mem MeasureTheory.Lp.simpleFunc.toSimpleFunc_eq_toFun MeasureTheory.Lp.coeFn_posPart Filter.univ_mem' Filter.Eventually.mono

MeasureTheory.SimpleFunc

Definitions

Name	Category	Theorems
integral 📖	CompOp	25 math, 2 bridge math: integral_eq_integral, integral_piecewise_zero, integral_neg, integral_eq_sum_filter, MeasureTheory.tendsto_integral_approxOn_of_measurable, MeasureTheory.tendsto_integral_approxOn_of_measurable_of_range_subset, integral_add_measure, integral_mono, norm_integral_le_integral_norm, integral_mono_measure, integral_def, integral_eq_lintegral, integral_sub, integral_eq_sum_of_subset, integral_congr, MeasureTheory.L1.SimpleFunc.norm_eq_integral, integral_const, integral_eq, integral_smul, map_integral, integral_nonneg, norm_setToSimpleFunc_le_integral_norm, integral_add, integral_eq_lintegral', MeasureTheory.L1.SimpleFunc.integral_eq_integral bridge: hasBoxIntegral, box_integral_eq_integral
negPart 📖	CompOp	3 math math: posPart_sub_negPart, negPart_map_norm, MeasureTheory.L1.SimpleFunc.negPart_toSimpleFunc
posPart 📖	CompOp	3 math math: posPart_sub_negPart, posPart_map_norm, MeasureTheory.L1.SimpleFunc.posPart_toSimpleFunc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integral_add 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe MeasureTheory.SimpleFunc instFunLike	integral instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	setToSimpleFunc_add MeasureTheory.weightedSMul_union
integral_add_measure 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe MeasureTheory.SimpleFunc instFunLike MeasureTheory.Measure MeasureTheory.Measure.instAdd	integral AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	setToSimpleFunc_add_left' IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.weightedSMul_add_measure ENNReal.add_ne_top Pi.add_apply MeasureTheory.Measure.coe_add lt_top_iff_ne_top
integral_congr 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe MeasureTheory.SimpleFunc instFunLike Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	integral	—	MeasureTheory.Measure.instOuterMeasureClass setToSimpleFunc_congr MeasureTheory.weightedSMul_null MeasureTheory.weightedSMul_union
integral_const 📖	mathematical	—	integral const Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField MeasureTheory.Measure.real Set.univ	—	integral_eq_sum_of_subset HasSubset.Subset.trans Finset.instIsTransSubset Finset.filter_subset range_const_subset Finset.sum_congr Finset.sum_singleton
integral_def 📖	mathematical	—	integral setToSimpleFunc MeasureTheory.weightedSMul	—	—
integral_eq 📖	mathematical	—	integral Finset.sum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid range Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toModule Real.normedField MeasureTheory.Measure.real Set.preimage DFunLike.coe MeasureTheory.SimpleFunc instFunLike Set Set.instSingletonSet	—	Finset.sum_congr MeasureTheory.weightedSMul_apply
integral_eq_lintegral 📖	mathematical	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 MeasureTheory.SimpleFunc instFunLike Filter.EventuallyLE Real.instLE MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Pi.instZero Real.instZero	integral Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField ENNReal.toReal MeasureTheory.lintegral ENNReal.ofReal	—	MeasureTheory.Measure.instOuterMeasureClass Filter.Eventually.mono ENNReal.toReal_ofReal integral_eq_lintegral' ENNReal.ofReal_zero ENNReal.ofReal_ne_top integral_congr
integral_eq_lintegral' 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe MeasureTheory.SimpleFunc instFunLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup ENNReal instZeroENNReal	integral Real Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField map ENNReal.toReal MeasureTheory.lintegral	—	integrable_iff_finMeasSupp lintegral_eq_lintegral map_integral map_lintegral ENNReal.toReal_sum MulZeroClass.zero_mul WithTop.zero_ne_top ENNReal.mul_ne_top LT.lt.ne FinMeasSupp.meas_preimage_singleton_ne_zero Finset.sum_congr smul_eq_mul ENNReal.toReal_mul mul_comm MeasureTheory.measureReal_def
integral_eq_sum_filter 📖	mathematical	—	integral Finset.sum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Finset.filter NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup range Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toModule Real.normedField MeasureTheory.Measure.real Set.preimage DFunLike.coe MeasureTheory.SimpleFunc instFunLike Set Set.instSingletonSet	—	setToSimpleFunc_eq_sum_filter Finset.sum_congr MeasureTheory.weightedSMul_apply
integral_eq_sum_of_subset 📖	mathematical	Finset Finset.instHasSubset Finset.filter NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup range	integral Finset.sum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toModule Real.normedField MeasureTheory.Measure.real Set.preimage DFunLike.coe MeasureTheory.SimpleFunc instFunLike Set Set.instSingletonSet	—	integral_eq_sum_filter Finset.sum_subset not_and_or Finset.mem_filter smul_zero Set.preimage_eq_empty mem_range MeasureTheory.measureReal_empty zero_smul
integral_mono 📖	mathematical	Filter.EventuallyLE Preorder.toLE PartialOrder.toPreorder MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe MeasureTheory.SimpleFunc instFunLike MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	integral	—	MeasureTheory.Measure.instOuterMeasureClass sub_nonneg covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono integral_sub integral_nonneg MeasureTheory.sub_nonneg_ae
integral_mono_measure 📖	mathematical	Filter.EventuallyLE Preorder.toLE PartialOrder.toPreorder MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup DFunLike.coe MeasureTheory.SimpleFunc instFunLike MeasureTheory.Measure.instPartialOrder MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	integral	—	MeasureTheory.Measure.instOuterMeasureClass integral_eq Finset.sum_le_sum IsOrderedAddMonoid.toAddLeftMono LE.le.eq_or_lt smul_zero smul_le_smul_of_nonneg_right PosSMulMono.toSMulPosMono Real.instIsOrderedRing IsOrderedModule.toPosSMulMono ENNReal.toReal_mono LT.lt.ne integrable_iff LT.lt.ne' MeasureTheory.Measure.measure_mono_left le_of_lt nonpos_iff_eq_zero ENNReal.instCanonicallyOrderedAdd MeasureTheory.ae_iff MeasureTheory.measure_mono LE.le.trans_eq zero_smul
integral_neg 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe MeasureTheory.SimpleFunc instFunLike	integral instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	setToSimpleFunc_neg MeasureTheory.weightedSMul_union
integral_nonneg 📖	mathematical	Filter.EventuallyLE Preorder.toLE PartialOrder.toPreorder MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup DFunLike.coe MeasureTheory.SimpleFunc instFunLike	integral	—	MeasureTheory.Measure.instOuterMeasureClass integral_eq Finset.sum_nonneg IsOrderedAddMonoid.toAddLeftMono forall_mem_range smul_nonneg IsOrderedModule.toPosSMulMono MeasureTheory.measureReal_nonneg nonpos_iff_eq_zero ENNReal.instCanonicallyOrderedAdd MeasureTheory.measure_mono MeasureTheory.ae_iff zero_smul
integral_piecewise_zero 📖	mathematical	MeasurableSet	integral piecewise MeasureTheory.SimpleFunc instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup MeasureTheory.Measure.restrict	—	integral_eq_sum_of_subset Set.piecewise_eq_indicator Set.mem_range_self Finset.sum_congr Set.indicator_preimage_of_notMem Finset.mem_filter MeasureTheory.measureReal_restrict_apply measurableSet_preimage integral_eq_sum_filter
integral_smul 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe MeasureTheory.SimpleFunc instFunLike	integral instSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass	—	setToSimpleFunc_smul MeasureTheory.weightedSMul_union MeasureTheory.weightedSMul_smul
integral_sub 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe MeasureTheory.SimpleFunc instFunLike	integral instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	setToSimpleFunc_sub MeasureTheory.weightedSMul_union
map_integral 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe MeasureTheory.SimpleFunc instFunLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	integral map Finset.sum ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid range Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring NormedSpace.toModule Real.normedField MeasureTheory.Measure.real Set.preimage Set Set.instSingletonSet	—	map_setToSimpleFunc MeasureTheory.weightedSMul_union
negPart_map_norm 📖	mathematical	—	map Real Norm.norm Real.norm negPart Real.linearOrder Real.instZero Real.instNeg	—	negPart.eq_1 posPart_map_norm
norm_integral_le_integral_norm 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe MeasureTheory.SimpleFunc instFunLike	Real Real.instLE Norm.norm NormedAddCommGroup.toNorm integral Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField map	—	LE.le.trans norm_setToSimpleFunc_le_integral_norm MeasureTheory.norm_weightedSMul_le Eq.le one_mul
norm_setToSimpleFunc_le_integral_norm 📖	mathematical	Real Real.instLE Norm.norm ContinuousLinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.hasOpNorm DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instMul MeasureTheory.Measure.real MeasureTheory.Integrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe MeasureTheory.SimpleFunc instFunLike	NormedAddCommGroup.toNorm setToSimpleFunc integral Real.normedAddCommGroup NormedField.toNormedSpace map	—	norm_setToSimpleFunc_le_sum_mul_norm_of_integrable map_integral norm_zero Finset.sum_congr
posPart_map_norm 📖	mathematical	—	map Real Norm.norm Real.norm posPart Real.linearOrder Real.instZero	—	ext map_apply Real.norm_eq_abs abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid le_max_right
posPart_sub_negPart 📖	mathematical	—	MeasureTheory.SimpleFunc Real instSub Real.instSub posPart Real.linearOrder Real.instZero negPart Real.instNeg	—	ext coe_sub max_zero_sub_eq_self IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid

---

← Back to Index