MeanValue

📁 Source: Mathlib/MeasureTheory/Integral/IntervalIntegral/MeanValue.lean

Statistics

Metric	Count
Definitions	0
Theorems exists_eq_const_mul_intervalIntegral_of_ae_nonneg, exists_eq_const_mul_intervalIntegral_of_nonneg	2
Total	2

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_eq_const_mul_intervalIntegral_of_ae_nonneg 📖	mathematical	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.uIcc Real.lattice IntervalIntegrable NormedAddGroup.toENormedAddMonoid NormedAddCommGroup.toNormedAddGroup Real.normedAddCommGroup Filter.Eventually Real.instLE Real.instZero MeasureTheory.ae MeasureTheory.Measure Real.measurableSpace MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.restrict Set.uIoc Real.linearOrder	Set Set.instMembership intervalIntegral InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instMul	—	MeasureTheory.Measure.instOuterMeasureClass Set.uIcc_of_le Set.Icc_self intervalIntegral.integral_same MulZeroClass.mul_zero Set.uIoc_of_le LT.lt.le Set.uIoc_subset_uIcc isConnected_Ioc instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing intervalIntegrable_iff PseudoEMetricSpace.pseudoMetrizableSpace IntervalIntegrable.continuousOn_smul NormedSpace.toNormSMulClass exists_eq_const_mul_setIntegral_of_ae_nonneg measurableSet_uIoc BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid ContinuousOn.mono intervalIntegral.integral_of_le Set.mem_of_subset_of_mem Set.uIcc_comm IntervalIntegrable.symm Set.uIoc_comm Set.uIcc_of_ge MeasureTheory.ae.congr_simp Set.uIoc_of_ge MeasureTheory.ae_restrict_eq lt_of_le_of_ne' intervalIntegral.integral_symm mul_neg
exists_eq_const_mul_intervalIntegral_of_nonneg 📖	mathematical	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.uIcc Real.lattice IntervalIntegrable NormedAddGroup.toENormedAddMonoid NormedAddCommGroup.toNormedAddGroup Real.normedAddCommGroup Real.instLE Real.instZero	Set Set.instMembership intervalIntegral InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instMul	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.ae_restrict_iff' measurableSet_uIoc BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid MeasureTheory.ae_of_all exists_eq_const_mul_intervalIntegral_of_ae_nonneg

---

← Back to Index