IntervalAverage

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

Statistics

Metric	Count
Definitions _,_»	1
Theorems exists_eq_interval_average, exists_eq_interval_average_of_measure, exists_eq_interval_average_of_noAtoms, intervalAverage_congr_codiscreteWithin, interval_average_eq, interval_average_eq_div, interval_average_symm	7
Total	8

(root)

Definitions

Name	Category	Theorems
«term⨍_In_.._,_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_eq_interval_average 📖	mathematical	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.uIcc Real.lattice	Set Set.instMembership Set.uIoo Real.linearOrder MeasureTheory.average MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume Set.uIoc	—	exists_eq_interval_average_of_noAtoms Real.noAtoms_volume Real.volume_uIoc IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add sub_ne_zero
exists_eq_interval_average_of_measure 📖	mathematical	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.uIcc Real.lattice	Set Set.instMembership Set.uIoc Real.linearOrder MeasureTheory.average Real.measurableSpace Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.Measure.restrict	—	MeasureTheory.exists_eq_setAverage MeasureTheory.nonempty_of_measure_ne_zero isPreconnected_Ioc instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing ContinuousOn.mono Set.uIoc_subset_uIcc ContinuousOn.integrableOn_of_subset_isCompact BorelSpace.opensMeasurable Real.borelSpace isCompact_uIcc ConditionallyCompleteLinearOrder.toCompactIccSpace measurableSet_uIoc instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid
exists_eq_interval_average_of_noAtoms 📖	mathematical	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.uIcc Real.lattice	Set Set.instMembership Set.uIoo Real.linearOrder MeasureTheory.average Real.measurableSpace Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.Measure.restrict Set.uIoc	—	ContinuousOn.integrableOn_of_subset_isCompact BorelSpace.opensMeasurable Real.borelSpace isCompact_uIcc ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopologyReal measurableSet_uIoc instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Set.uIoc_subset_uIcc Set.uIoc_of_le Set.Ioc_eq_empty MeasureTheory.measure_empty MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Ioo_ae_eq_Ioc MeasureTheory.measure_congr MeasureTheory.exists_eq_setAverage isConnected_uIoo LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing ContinuousOn.mono Set.uIoo_subset_uIcc_self MeasureTheory.IntegrableOn.mono_set MeasureTheory.measure_ne_top_of_subset MeasureTheory.setAverage_congr
intervalAverage_congr_codiscreteWithin 📖	mathematical	Filter.EventuallyEq Real Filter.codiscreteWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.uIoc Real.linearOrder	MeasureTheory.average MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume	—	interval_average_eq intervalIntegral.integral_congr_codiscreteWithin
interval_average_eq 📖	mathematical	—	MeasureTheory.average Real MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume Set.uIoc Real.linearOrder 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 Real.instSub intervalIntegral	—	le_or_gt MeasureTheory.setAverage_eq Set.uIoc_of_le Real.volume_real_Ioc_of_le intervalIntegral.integral_of_le Set.uIoc_of_ge LT.lt.le intervalIntegral.integral_of_ge smul_neg neg_smul inv_neg neg_sub
interval_average_eq_div 📖	mathematical	—	MeasureTheory.average Real MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume Set.uIoc Real.linearOrder DivInvMonoid.toDiv Real.instDivInvMonoid intervalIntegral Real.instSub	—	interval_average_eq smul_eq_mul div_eq_inv_mul
interval_average_symm 📖	mathematical	—	MeasureTheory.average Real MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume Set.uIoc Real.linearOrder	—	MeasureTheory.setAverage_eq Set.uIoc_comm

---

← Back to Index