Average

📁 Source: Mathlib/MeasureTheory/Integral/Average.lean

Statistics

Metric	Count
Definitions average, laverage, «term⨍_,_», «term⨍_,_∂_», «term⨍_In_,_», «term⨍_In_,_∂_», «term⨍⁻_,_», «term⨍⁻_,_∂_», «term⨍⁻_In_,_», «term⨍⁻_In_,_∂_»	10
Theorems average_add_measure, average_congr, average_const, average_eq, average_eq', average_eq_integral, average_mem_openSegment_compl_self, average_neg, average_pair, average_union, average_union_mem_openSegment, average_union_mem_segment, average_zero, average_zero_measure, exists_average_le, exists_eq_setAverage, exists_integral_le, exists_laverage_le, exists_le_average, exists_le_integral, exists_le_laverage, exists_le_lintegral, exists_le_setAverage, exists_le_setLAverage, exists_lintegral_le, exists_notMem_null_average_le, exists_notMem_null_integral_le, exists_notMem_null_laverage_le, exists_notMem_null_le_average, exists_notMem_null_le_integral, exists_notMem_null_le_laverage, exists_notMem_null_le_lintegral, exists_notMem_null_lintegral_le, exists_setAverage_le, exists_setLAverage_le, integral_average, integral_average_sub, integral_sub_average, laverage_add_measure, laverage_congr, laverage_const, laverage_eq, laverage_eq', laverage_eq_lintegral, laverage_lt_top, laverage_mem_openSegment_compl_self, laverage_mul_measure_univ, laverage_one, laverage_union, laverage_union_mem_openSegment, laverage_union_mem_segment, laverage_zero, laverage_zero_measure, lintegral_laverage, measure_average_le_pos, measure_integral_le_pos, measure_laverage_le_pos, measure_le_average_pos, measure_le_integral_pos, measure_le_laverage_pos, measure_le_lintegral_pos, measure_le_setAverage_pos, measure_le_setLAverage_pos, measure_lintegral_le_pos, measure_mul_laverage, measure_mul_setLAverage, measure_setAverage_le_pos, measure_setLAverage_le_pos, measure_smul_average, measure_smul_setAverage, ofReal_average, ofReal_setAverage, setAverage_congr, setAverage_congr_fun, setAverage_const, setAverage_eq, setAverage_eq', setAverage_sub_setAverage, setIntegral_setAverage, setIntegral_setAverage_sub, setLAverage_congr, setLAverage_congr_fun, setLAverage_congr_fun_ae, setLAverage_const, setLAverage_eq, setLAverage_eq', setLAverage_lt_top, setLAverage_one, setLIntegral_setLAverage, tendsto_integral_smul_of_tendsto_average_norm_sub, toReal_laverage, toReal_setLAverage	92
Total	102

MeasureTheory

Definitions

Name	Category	Theorems
average 📖	CompOp	73 math math: ConvexOn.map_set_average_le, ae_eq_const_or_exists_average_ne_compl, average_zero_measure, interval_average_eq_div, exists_eq_interval_average_of_noAtoms, ConvexOn.set_average_mem_epigraph, StrictConcaveOn.ae_eq_const_or_lt_map_average, average_mem_openSegment_compl_self, exists_average_le, ae_eq_const_or_norm_setIntegral_lt_of_norm_le_const, integral_average, measure_smul_average, ofReal_setAverage, exists_notMem_null_le_average, integral_average_sub, average_zero, measure_le_setAverage_pos, VitaliFamily.ae_tendsto_average_norm_sub, interval_average_symm, average_eq_integral, ae_eq_const_or_norm_average_lt_of_norm_le_const, setAverage_eq', FiniteMeasure.average_eq_integral_normalize, setAverage_congr, intervalAverage_congr_codiscreteWithin, setAverage_eq, average_congr, setAverage_sub_setAverage, ConcaveOn.set_average_mem_hypograph, average_union_mem_segment, Convex.set_average_mem_closure, average_pair, ConcaveOn.le_map_average, toReal_laverage, ConvexOn.average_mem_epigraph, average_add_measure, Convex.average_mem, ProbabilityTheory.condVar_bot', setAverage_congr_fun, exists_le_setAverage, average_eq', ProbabilityTheory.condVar_bot_ae_eq, exists_eq_interval_average_of_measure, ConvexOn.map_average_le, Real.circleAverage_eq_intervalAverage, exists_setAverage_le, integral_sub_average, average_const, ConcaveOn.average_mem_hypograph, setIntegral_setAverage_sub, setAverage_const, measure_average_le_pos, measure_setAverage_le_pos, StrictConvex.ae_eq_const_or_average_mem_interior, measure_le_average_pos, average_neg, measure_smul_setAverage, exists_eq_setAverage, ConcaveOn.le_map_set_average, Convex.set_average_mem, ofReal_average, interval_average_eq, exists_le_average, VitaliFamily.ae_tendsto_average, exists_eq_interval_average, average_union_mem_openSegment, StrictConvexOn.ae_eq_const_or_map_average_lt, average_union, ae_eq_const_or_norm_integral_lt_of_norm_le_const, setIntegral_setAverage, exists_notMem_null_average_le, toReal_setLAverage, average_eq
laverage 📖	CompOp	39 math math: laverage_congr, measure_le_setLAverage_pos, exists_setLAverage_le, lintegral_laverage, exists_notMem_null_le_laverage, laverage_eq', setLAverage_congr_fun_ae, laverage_zero_measure, laverage_lt_top, laverage_eq, measure_laverage_le_pos, exists_le_setLAverage, measure_le_laverage_pos, laverage_mul_measure_univ, setLAverage_eq', setLAverage_congr, measure_mul_laverage, laverage_one, setLAverage_one, setLAverage_eq, toReal_laverage, laverage_union_mem_segment, laverage_union, laverage_zero, laverage_mem_openSegment_compl_self, setLAverage_const, exists_notMem_null_laverage_le, exists_le_laverage, laverage_const, setLIntegral_setLAverage, laverage_union_mem_openSegment, laverage_add_measure, measure_setLAverage_le_pos, setLAverage_congr_fun, setLAverage_lt_top, measure_mul_setLAverage, exists_laverage_le, laverage_eq_lintegral, toReal_setLAverage
«term⨍_,_» 📖	CompOp	—
«term⨍_,_∂_» 📖	CompOp	—
«term⨍_In_,_» 📖	CompOp	—
«term⨍_In_,_∂_» 📖	CompOp	—
«term⨍⁻_,_» 📖	CompOp	—
«term⨍⁻_,_∂_» 📖	CompOp	—
«term⨍⁻_In_,_» 📖	CompOp	—
«term⨍⁻_In_,_∂_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
average_add_measure 📖	mathematical	Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	average Measure Measure.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid 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 DivInvMonoid.toDiv Real.instDivInvMonoid Measure.real Set.univ Real.instAdd	—	div_eq_inv_mul SemigroupAction.mul_smul measure_smul_average integral_add_measure average_eq measureReal_add_apply measure_ne_top
average_congr 📖	mathematical	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass	average	—	Measure.instOuterMeasureClass average_eq integral_congr_ae
average_const 📖	mathematical	—	average	—	average.eq_1 integral_const measureReal_def IsProbabilityMeasure.measure_univ isProbabilityMeasureSMul ENNReal.toReal_one one_smul
average_eq 📖	mathematical	—	average 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 Real.instInv Measure.real Set.univ integral	—	IsScalarTower.right average_eq' integral_smul_measure ENNReal.toReal_inv measureReal_def
average_eq' 📖	mathematical	—	average integral ENNReal Measure Measure.instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right ENNReal.instInv DFunLike.coe Set Measure.instFunLike Set.univ	—	—
average_eq_integral 📖	mathematical	—	average integral	—	average.eq_1 IsProbabilityMeasure.measure_univ inv_one IsScalarTower.right one_smul
average_mem_openSegment_compl_self 📖	mathematical	NullMeasurableSet Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	Set Set.instMembership openSegment Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField average Measure.restrict Compl.compl Set.instCompl	—	Set.union_compl_self Measure.restrict_univ average_union_mem_openSegment aedisjoint_compl_right NullMeasurableSet.compl measure_ne_top Integrable.integrableOn
average_neg 📖	mathematical	—	average NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	integral_neg
average_pair 📖	mathematical	Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	average Prod.normedAddCommGroup Prod.normedSpace Real Real.normedField	—	integral_pair Integrable.to_average
average_union 📖	mathematical	AEDisjoint NullMeasurableSet IntegrableOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	average Measure.restrict Set Set.instUnion AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid 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 DivInvMonoid.toDiv Real.instDivInvMonoid Measure.real Real.instAdd	—	Measure.restrict_union₀ average_add_measure Restrict.isFiniteMeasure Ne.lt_top measureReal_restrict_apply_univ
average_union_mem_openSegment 📖	mathematical	AEDisjoint NullMeasurableSet IntegrableOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	Set Set.instMembership openSegment Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField average Measure.restrict Set.instUnion	—	ENNReal.toReal_pos mem_openSegment_iff_div Real.instIsStrictOrderedRing average_union
average_union_mem_segment 📖	mathematical	AEDisjoint NullMeasurableSet IntegrableOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	Set Set.instMembership segment Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField average Measure.restrict Set.instUnion	—	Measure.restrict_congr_set Filter.EventuallyEq.union Measure.instOuterMeasureClass ae_eq_empty Filter.EventuallyEq.rfl Set.empty_union right_mem_segment Real.instZeroLEOneClass mem_segment_iff_div Real.instIsStrictOrderedRing ENNReal.toReal_nonneg ENNReal.toReal_pos le_add_of_nonneg_right IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid average_union
average_zero 📖	mathematical	—	average NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	average.eq_1 integral_zero
average_zero_measure 📖	mathematical	—	average Measure Measure.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	average.eq_1 IsScalarTower.right smul_zero integral_zero_measure
exists_average_le 📖	mathematical	Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing	Real.instLE average Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField	—	nonempty_of_measure_ne_zero LT.lt.ne' measure_average_le_pos
exists_eq_setAverage 📖	mathematical	IsConnected ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace IntegrableOn SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing	Set Set.instMembership average Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField Measure.restrict	—	measure_le_setAverage_pos measure_setAverage_le_pos nonempty_of_measure_ne_zero LT.lt.ne' IsPreconnected.intermediate_value HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid IsConnected.isPreconnected
exists_integral_le 📖	mathematical	Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing	Real.instLE integral Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField	—	average_eq_integral exists_average_le IsZeroOrProbabilityMeasure.toIsFiniteMeasure instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure IsProbabilityMeasure.ne_zero
exists_laverage_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder laverage	—	nonempty_of_measure_ne_zero LT.lt.ne' measure_laverage_le_pos
exists_le_average 📖	mathematical	Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing	Real.instLE average Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField	—	nonempty_of_measure_ne_zero LT.lt.ne' measure_le_average_pos
exists_le_integral 📖	mathematical	Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing	Real.instLE integral Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField	—	average_eq_integral exists_le_average IsZeroOrProbabilityMeasure.toIsFiniteMeasure instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure IsProbabilityMeasure.ne_zero
exists_le_laverage 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace	Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder laverage	—	nonempty_of_measure_ne_zero LT.lt.ne' measure_le_laverage_pos
exists_le_lintegral 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace	Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder lintegral	—	laverage_eq_lintegral exists_le_laverage IsZeroOrProbabilityMeasure.toIsFiniteMeasure instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure IsProbabilityMeasure.ne_zero
exists_le_setAverage 📖	mathematical	IntegrableOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing	Set Set.instMembership Real.instLE average Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField Measure.restrict	—	nonempty_of_measure_ne_zero LT.lt.ne' measure_le_setAverage_pos
exists_le_setLAverage 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace Measure.restrict	Set Set.instMembership Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder laverage	—	nonempty_of_measure_ne_zero LT.lt.ne' measure_le_setLAverage_pos
exists_lintegral_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder lintegral	—	laverage_eq_lintegral exists_laverage_le IsProbabilityMeasure.ne_zero
exists_notMem_null_average_le 📖	mathematical	Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing DFunLike.coe Measure Set ENNReal Measure.instFunLike instZeroENNReal	Set.instMembership Real.instLE average Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField	—	average_neg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add exists_notMem_null_le_average Integrable.neg
exists_notMem_null_integral_le 📖	mathematical	Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing DFunLike.coe Measure Set ENNReal Measure.instFunLike instZeroENNReal	Set.instMembership Real.instLE integral Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField	—	average_eq_integral exists_notMem_null_average_le IsZeroOrProbabilityMeasure.toIsFiniteMeasure instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure IsProbabilityMeasure.ne_zero
exists_notMem_null_laverage_le 📖	mathematical	DFunLike.coe Measure Set ENNReal Measure.instFunLike instZeroENNReal	Set.instMembership Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder laverage	—	measure_laverage_le_pos nonempty_of_measure_ne_zero LT.lt.ne' measure_diff_null Measure.instOuterMeasureClass
exists_notMem_null_le_average 📖	mathematical	Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing DFunLike.coe Measure Set ENNReal Measure.instFunLike instZeroENNReal	Set.instMembership Real.instLE average Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField	—	measure_le_average_pos nonempty_of_measure_ne_zero LT.lt.ne' measure_diff_null Measure.instOuterMeasureClass
exists_notMem_null_le_integral 📖	mathematical	Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing DFunLike.coe Measure Set ENNReal Measure.instFunLike instZeroENNReal	Set.instMembership Real.instLE integral Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField	—	average_eq_integral exists_notMem_null_le_average IsZeroOrProbabilityMeasure.toIsFiniteMeasure instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure IsProbabilityMeasure.ne_zero
exists_notMem_null_le_laverage 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace DFunLike.coe Measure Set Measure.instFunLike instZeroENNReal	Set.instMembership Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder laverage	—	measure_le_laverage_pos nonempty_of_measure_ne_zero LT.lt.ne' measure_diff_null Measure.instOuterMeasureClass
exists_notMem_null_le_lintegral 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace DFunLike.coe Measure Set Measure.instFunLike instZeroENNReal	Set.instMembership Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder lintegral	—	laverage_eq_lintegral exists_notMem_null_le_laverage IsZeroOrProbabilityMeasure.toIsFiniteMeasure instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure IsProbabilityMeasure.ne_zero
exists_notMem_null_lintegral_le 📖	mathematical	DFunLike.coe Measure Set ENNReal Measure.instFunLike instZeroENNReal	Set.instMembership Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder lintegral	—	laverage_eq_lintegral exists_notMem_null_laverage_le IsProbabilityMeasure.ne_zero
exists_setAverage_le 📖	mathematical	IntegrableOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing	Set Set.instMembership Real.instLE average Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField Measure.restrict	—	nonempty_of_measure_ne_zero LT.lt.ne' measure_setAverage_le_pos
exists_setLAverage_le 📖	mathematical	NullMeasurableSet	Set Set.instMembership ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder laverage Measure.restrict	—	nonempty_of_measure_ne_zero LT.lt.ne' measure_setLAverage_le_pos
integral_average 📖	mathematical	—	integral average	—	integral_const measure_smul_average
integral_average_sub 📖	mathematical	Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	integral SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup average NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	integral_sub integrable_const integral_average sub_self
integral_sub_average 📖	mathematical	—	integral SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup average NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	integral_sub integrable_const integral_average sub_self integral_undef sub_add_cancel Integrable.add IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup
laverage_add_measure 📖	mathematical	—	laverage Measure Measure.instAdd ENNReal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Distrib.toMul DivInvMonoid.toDiv ENNReal.instDivInvMonoid DFunLike.coe Set Measure.instFunLike Set.univ	—	measure_mul_laverage laverage_eq lintegral_add_measure not_isFiniteMeasure_iff add_top ENNReal.div_top MulZeroClass.zero_mul MulZeroClass.mul_zero add_zero top_add
laverage_congr 📖	mathematical	Filter.EventuallyEq ENNReal ae Measure Measure.instFunLike Measure.instOuterMeasureClass	laverage	—	Measure.instOuterMeasureClass laverage_eq lintegral_congr_ae
laverage_const 📖	mathematical	—	laverage	—	lintegral_const IsProbabilityMeasure.measure_univ isProbabilityMeasureSMul mul_one
laverage_eq 📖	mathematical	—	laverage ENNReal DivInvMonoid.toDiv ENNReal.instDivInvMonoid lintegral DFunLike.coe Measure Set Measure.instFunLike Set.univ	—	IsScalarTower.right laverage_eq' lintegral_smul_measure ENNReal.div_eq_inv_mul smul_eq_mul
laverage_eq' 📖	mathematical	—	laverage lintegral ENNReal Measure Measure.instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right ENNReal.instInv DFunLike.coe Set Measure.instFunLike Set.univ	—	—
laverage_eq_lintegral 📖	mathematical	—	laverage lintegral	—	laverage.eq_1 IsProbabilityMeasure.measure_univ inv_one IsScalarTower.right one_smul
laverage_lt_top 📖	mathematical	—	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder laverage Top.top instTopENNReal	—	eq_or_ne laverage_zero_measure laverage_eq Measure.measure_univ_ne_zero Ne.lt_top ENNReal.div_ne_top
laverage_mem_openSegment_compl_self 📖	mathematical	NullMeasurableSet	ENNReal Set Set.instMembership openSegment CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instPartialOrder ENNReal.instAddCommMonoid Algebra.toSMul Algebra.id laverage Measure.restrict Compl.compl Set.instCompl	—	Set.union_compl_self Measure.restrict_univ laverage_union_mem_openSegment aedisjoint_compl_right NullMeasurableSet.compl measure_ne_top
laverage_mul_measure_univ 📖	mathematical	—	ENNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring laverage DFunLike.coe Measure Set Measure.instFunLike Set.univ lintegral	—	eq_or_ne laverage_zero_measure MulZeroClass.mul_zero lintegral_zero_measure laverage_eq ENNReal.div_mul_cancel Measure.measure_univ_ne_zero measure_ne_top
laverage_one 📖	mathematical	—	laverage ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	laverage_const
laverage_union 📖	mathematical	AEDisjoint NullMeasurableSet	laverage Measure.restrict Set Set.instUnion ENNReal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Distrib.toMul DivInvMonoid.toDiv ENNReal.instDivInvMonoid DFunLike.coe Measure Measure.instFunLike	—	Measure.restrict_union₀ laverage_add_measure Measure.restrict_apply_univ
laverage_union_mem_openSegment 📖	mathematical	AEDisjoint NullMeasurableSet	ENNReal Set Set.instMembership openSegment CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instPartialOrder ENNReal.instAddCommMonoid Algebra.toSMul Algebra.id laverage Measure.restrict Set.instUnion	—	ENNReal.div_pos ENNReal.add_ne_top ENNReal.add_div ENNReal.div_self Iff.not add_eq_zero Unique.instSubsingleton laverage_union
laverage_union_mem_segment 📖	mathematical	AEDisjoint NullMeasurableSet	ENNReal Set Set.instMembership segment CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instPartialOrder ENNReal.instAddCommMonoid Algebra.toSMul Algebra.id laverage Measure.restrict Set.instUnion	—	Measure.restrict_congr_set Filter.EventuallyEq.union Measure.instOuterMeasureClass ae_eq_empty Filter.EventuallyEq.rfl Set.empty_union right_mem_segment IsOrderedRing.toZeroLEOneClass ENNReal.instIsOrderedRing zero_le ENNReal.instCanonicallyOrderedAdd ENNReal.add_div ENNReal.div_self Iff.not add_eq_zero Unique.instSubsingleton ENNReal.add_ne_top laverage_union
laverage_zero 📖	mathematical	—	laverage ENNReal instZeroENNReal	—	laverage.eq_1 lintegral_zero
laverage_zero_measure 📖	mathematical	—	laverage Measure Measure.instZero ENNReal instZeroENNReal	—	ENNReal.inv_zero smul_zero IsScalarTower.right lintegral_zero_measure
lintegral_laverage 📖	mathematical	—	lintegral laverage	—	lintegral_const laverage_mul_measure_univ
measure_average_le_pos 📖	mathematical	Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal DFunLike.coe Measure Set Measure.instFunLike setOf Real.instLE average Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField	—	Measure.restrict_univ measure_setAverage_le_pos Measure.measure_univ_ne_zero measure_ne_top Integrable.integrableOn
measure_integral_le_pos 📖	mathematical	Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal DFunLike.coe Measure Set Measure.instFunLike setOf Real.instLE integral Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField	—	average_eq_integral measure_average_le_pos IsZeroOrProbabilityMeasure.toIsFiniteMeasure instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure IsProbabilityMeasure.ne_zero
measure_laverage_le_pos 📖	mathematical	—	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal DFunLike.coe Measure Set Measure.instFunLike setOf Preorder.toLE laverage	—	Measure.restrict_univ measure_setLAverage_le_pos Measure.measure_univ_ne_zero nullMeasurableSet_univ
measure_le_average_pos 📖	mathematical	Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal DFunLike.coe Measure Set Measure.instFunLike setOf Real.instLE average Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField	—	Measure.restrict_univ measure_le_setAverage_pos Measure.measure_univ_ne_zero measure_ne_top Integrable.integrableOn
measure_le_integral_pos 📖	mathematical	Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal DFunLike.coe Measure Set Measure.instFunLike setOf Real.instLE integral Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField	—	average_eq_integral measure_le_average_pos IsZeroOrProbabilityMeasure.toIsFiniteMeasure instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure IsProbabilityMeasure.ne_zero
measure_le_laverage_pos 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace	Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal DFunLike.coe Measure Set Measure.instFunLike setOf Preorder.toLE laverage	—	Measure.restrict_univ measure_le_setLAverage_pos Measure.measure_univ_ne_zero measure_ne_top AEMeasurable.restrict
measure_le_lintegral_pos 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace	Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal DFunLike.coe Measure Set Measure.instFunLike setOf Preorder.toLE lintegral	—	laverage_eq_lintegral measure_le_laverage_pos IsZeroOrProbabilityMeasure.toIsFiniteMeasure instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure IsProbabilityMeasure.ne_zero
measure_le_setAverage_pos 📖	mathematical	IntegrableOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal DFunLike.coe Measure Set Measure.instFunLike setOf Set.instMembership Real.instLE average Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField Measure.restrict	—	pos_iff_ne_zero ENNReal.instCanonicallyOrderedAdd Measure.restrict_apply₀ AEStronglyMeasurable.nullMeasurableSet_le HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid PseudoEMetricSpace.pseudoMetrizableSpace aestronglyMeasurable_const Set.inter_comm Eq.not_gt integral_sub_average Real.instCompleteSpace Restrict.isFiniteMeasure Ne.lt_top setIntegral_pos_iff_support_of_nonneg_ae measure_mono_null Measure.instOuterMeasureClass LT.lt.le covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Integrable.sub integrableOn_const enorm_ne_top Set.diff_compl Set.diff_inter_self_eq_diff measure_diff_null Set.inter_subset_inter_left Eq.le sub_eq_zero of_not_not Measure.measure_inter_eq_zero_of_restrict
measure_le_setLAverage_pos 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace Measure.restrict	Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal DFunLike.coe Measure Set Measure.instFunLike setOf Set.instMembership Preorder.toLE laverage	—	eq_or_ne Measure.restrict_apply Set.univ_inter lintegral_smul_measure ENNReal.mul_top ENNReal.instCanonicallyOrderedAdd measure_le_setAverage_pos integrable_toReal_of_lintegral_ne_top Set.setOf_inter_eq_sep Measure.restrict_apply₀ AEStronglyMeasurable.nullMeasurableSet_le OrderTopology.to_orderClosedTopology ENNReal.instOrderTopology TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace ENNReal.instMetrizableSpace AEMeasurable.aestronglyMeasurable BorelSpace.opensMeasurable ENNReal.borelSpace ENNReal.instSecondCountableTopology aestronglyMeasurable_const LT.lt.trans_le measure_diff_null Measure.instOuterMeasureClass measure_eq_top_of_lintegral_ne_top HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid PseudoEMetricSpace.pseudoMetrizableSpace Real.borelSpace instSecondCountableTopologyReal AEMeasurable.ennreal_toReal measure_mono ENNReal.toReal_le_toReal LT.lt.ne setLAverage_lt_top toReal_laverage
measure_lintegral_le_pos 📖	mathematical	—	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal DFunLike.coe Measure Set Measure.instFunLike setOf Preorder.toLE lintegral	—	laverage_eq_lintegral measure_laverage_le_pos IsProbabilityMeasure.ne_zero
measure_mul_laverage 📖	mathematical	—	ENNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring DFunLike.coe Measure Set Measure.instFunLike Set.univ laverage lintegral	—	eq_or_ne lintegral_zero_measure laverage_zero_measure MulZeroClass.mul_zero laverage_eq ENNReal.mul_div_cancel Measure.measure_univ_ne_zero measure_ne_top
measure_mul_setLAverage 📖	mathematical	—	ENNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring DFunLike.coe Measure Set Measure.instFunLike laverage Measure.restrict lintegral	—	Ne.lt_top measure_mul_laverage Restrict.isFiniteMeasure Measure.restrict_apply_univ
measure_setAverage_le_pos 📖	mathematical	IntegrableOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal DFunLike.coe Measure Set Measure.instFunLike setOf Set.instMembership Real.instLE average Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField Measure.restrict	—	average_neg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add measure_le_setAverage_pos Integrable.neg
measure_setLAverage_le_pos 📖	mathematical	NullMeasurableSet	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal DFunLike.coe Measure Set Measure.instFunLike setOf Set.instMembership Preorder.toLE laverage Measure.restrict	—	eq_or_ne setLAverage_eq ENNReal.div_top ENNReal.instCanonicallyOrderedAdd exists_measurable_le_lintegral_eq laverage_eq measure_setAverage_le_pos integrable_toReal_of_lintegral_ne_top Measurable.aemeasurable Measure.restrict_apply₀' LT.lt.trans_le measure_diff_null Measure.instOuterMeasureClass measure_eq_top_of_lintegral_ne_top Set.setOf_inter_eq_sep measure_mono LE.le.trans ENNReal.toReal_le_toReal LT.lt.ne setLAverage_lt_top toReal_laverage
measure_smul_average 📖	mathematical	—	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 Measure.real Set.univ average integral	—	eq_or_ne integral_zero_measure average_zero_measure smul_zero average_eq smul_inv_smul₀ LT.lt.ne' ENNReal.toReal_pos Measure.measure_univ_eq_zero measure_ne_top
measure_smul_setAverage 📖	mathematical	—	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 Measure.real average Measure.restrict integral	—	measure_smul_average Restrict.isFiniteMeasure Ne.lt_top measureReal_restrict_apply_univ
ofReal_average 📖	mathematical	Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Filter.EventuallyLE Real.instLE ae Measure Measure.instFunLike Measure.instOuterMeasureClass Pi.instZero Real.instZero	ENNReal.ofReal average Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField ENNReal DivInvMonoid.toDiv ENNReal.instDivInvMonoid lintegral DFunLike.coe Set Set.univ	—	Measure.instOuterMeasureClass eq_or_ne average_zero_measure ENNReal.ofReal_zero lintegral_zero_measure ENNReal.zero_div average_eq smul_eq_mul measureReal_def ENNReal.toReal_inv ENNReal.ofReal_mul ENNReal.toReal_nonneg ENNReal.ofReal_toReal ENNReal.inv_ne_top Measure.measure_univ_ne_zero ofReal_integral_eq_lintegral_ofReal ENNReal.div_eq_inv_mul
ofReal_setAverage 📖	mathematical	IntegrableOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Filter.EventuallyLE Real.instLE ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.restrict Pi.instZero Real.instZero	ENNReal.ofReal average Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField ENNReal DivInvMonoid.toDiv ENNReal.instDivInvMonoid lintegral DFunLike.coe Set	—	Measure.instOuterMeasureClass Measure.restrict_apply Set.univ_inter ofReal_average
setAverage_congr 📖	mathematical	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass	average Measure.restrict	—	Measure.instOuterMeasureClass setAverage_eq measureReal_congr setIntegral_congr_set
setAverage_congr_fun 📖	mathematical	MeasurableSet Filter.Eventually ae Measure Measure.instFunLike Measure.instOuterMeasureClass	average Measure.restrict	—	Measure.instOuterMeasureClass average_eq setIntegral_congr_ae
setAverage_const 📖	mathematical	—	average Measure.restrict	—	Ne.lt_top average_const Restrict.isFiniteMeasure Measure.restrict.neZero
setAverage_eq 📖	mathematical	—	average Measure.restrict 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 Real.instInv Measure.real integral	—	average_eq measureReal_restrict_apply_univ
setAverage_eq' 📖	mathematical	—	average Measure.restrict integral ENNReal Measure Measure.instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right ENNReal.instInv DFunLike.coe Set Measure.instFunLike	—	IsScalarTower.right Measure.restrict_apply_univ
setAverage_sub_setAverage 📖	mathematical	—	integral Measure.restrict SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup average NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	integral_sub_average Restrict.isFiniteMeasure lt_top_iff_ne_top
setIntegral_setAverage 📖	mathematical	—	integral Measure.restrict average	—	integral_average isFiniteMeasureRestrict
setIntegral_setAverage_sub 📖	mathematical	IntegrableOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup	integral Measure.restrict SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup average NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	integral_average_sub Restrict.isFiniteMeasure lt_top_iff_ne_top
setLAverage_congr 📖	mathematical	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass	laverage Measure.restrict	—	Measure.instOuterMeasureClass setLAverage_eq setLIntegral_congr measure_congr
setLAverage_congr_fun 📖	mathematical	MeasurableSet Set.EqOn ENNReal	laverage Measure.restrict	—	laverage_eq setLIntegral_congr_fun
setLAverage_congr_fun_ae 📖	mathematical	MeasurableSet Filter.Eventually ae Measure Measure.instFunLike Measure.instOuterMeasureClass	laverage Measure.restrict	—	Measure.instOuterMeasureClass laverage_eq setLIntegral_congr_fun_ae
setLAverage_const 📖	mathematical	—	laverage Measure.restrict	—	setLAverage_eq lintegral_const Measure.restrict_apply Set.univ_inter div_eq_mul_inv mul_assoc ENNReal.mul_inv_cancel mul_one
setLAverage_eq 📖	mathematical	—	laverage Measure.restrict ENNReal DivInvMonoid.toDiv ENNReal.instDivInvMonoid lintegral DFunLike.coe Measure Set Measure.instFunLike	—	laverage_eq Measure.restrict_apply_univ
setLAverage_eq' 📖	mathematical	—	laverage Measure.restrict lintegral ENNReal Measure Measure.instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right ENNReal.instInv DFunLike.coe Set Measure.instFunLike	—	IsScalarTower.right Measure.restrict_apply_univ
setLAverage_lt_top 📖	mathematical	—	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder laverage Measure.restrict Top.top instTopENNReal	—	laverage_lt_top
setLAverage_one 📖	mathematical	—	laverage Measure.restrict ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	setLAverage_const
setLIntegral_setLAverage 📖	mathematical	—	lintegral Measure.restrict laverage	—	lintegral_laverage isFiniteMeasureRestrict
tendsto_integral_smul_of_tendsto_average_norm_sub 📖	mathematical	Filter.Tendsto Real average Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField Measure.restrict Norm.norm NormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero Filter.Eventually IntegrableOn SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup integral Real.instOne Set Set.instHasSubset Function.support	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule	—	Filter.mp_mem tendsto_order instOrderTopologyReal zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Filter.univ_mem' Mathlib.Tactic.Contrapose.contrapose₁ integral_undef integral_smul_const integral_add smul_sub Integrable.sub Set.Subset.trans Function.support_smul_subset_left integrableOn_iff_integrable_of_support_subset PseudoEMetricSpace.pseudoMetrizableSpace Integrable.smul_of_top_right NormedSpace.toIsBoundedSMul memLp_top_of_bound AEStronglyMeasurable.restrict Integrable.aestronglyMeasurable Filter.Eventually.of_forall Measure.instOuterMeasureClass Integrable.smul_const sub_add_cancel Filter.Tendsto.const_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal squeeze_zero_norm' lt_top_iff_ne_top div_zero IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add integral_zero LE.le.trans norm_integral_le_integral_norm average_eq norm_smul NormedSpace.toNormSMulClass Function.notMem_support norm_zero MulZeroClass.zero_mul setIntegral_eq_integral_of_forall_compl_eq_zero integral_mono_of_nonneg IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing norm_nonneg Integrable.const_mul Integrable.norm mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono measureReal_restrict_apply Set.univ_inter MulZeroClass.mul_zero Filter.Tendsto.add IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup Filter.Tendsto.smul_const IsBoundedSMul.continuousSMul Filter.Tendsto.congr' one_smul zero_add
toReal_laverage 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace Filter.Eventually Top.top instTopENNReal ae Measure Measure.instFunLike Measure.instOuterMeasureClass	ENNReal.toReal laverage average Real Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField	—	Measure.instOuterMeasureClass average_eq laverage_eq smul_eq_mul ENNReal.toReal_div div_eq_inv_mul integral_toReal Filter.Eventually.mono lt_top_iff_ne_top measureReal_def
toReal_setLAverage 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace Measure.restrict Filter.Eventually Top.top instTopENNReal ae Measure Measure.instFunLike Measure.instOuterMeasureClass	ENNReal.toReal laverage average Real Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField	—	Measure.instOuterMeasureClass laverage_eq Measure.restrict_apply Set.univ_inter ENNReal.toReal_div toReal_laverage

---

← Back to Index