MeanValue

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

Statistics

Metric	Count
Definitions	0
Theorems exists_eq_const_mul_setIntegral_of_ae_nonneg, exists_eq_const_mul_setIntegral_of_nonneg	2
Total	2

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_eq_const_mul_setIntegral_of_ae_nonneg 📖	mathematical	IsConnected MeasurableSet ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace MeasureTheory.IntegrableOn SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Real.instMul Filter.Eventually Real.instLE Real.instZero MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.restrict	Set Set.instMembership MeasureTheory.integral Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField	—	MeasureTheory.Measure.instOuterMeasureClass AEMeasurable.ennreal_ofReal MeasureTheory.AEStronglyMeasurable.aemeasurable PseudoEMetricSpace.pseudoMetrizableSpace Real.borelSpace MeasureTheory.Integrable.aestronglyMeasurable Filter.Eventually.mono MeasureTheory.integral_congr_ae mul_comm setIntegral_withDensity_eq_setIntegral_toReal_smul₀ mul_one IsConnected.nonempty MeasureTheory.setIntegral_eq_zero_iff_of_nonneg_ae MulZeroClass.mul_zero MeasureTheory.integral_zero MeasureTheory.integral_const Real.instCompleteSpace MeasureTheory.measureReal_restrict_apply Set.univ_inter MeasureTheory.integrableOn_congr_fun_ae MeasureTheory.integrable_withDensity_iff_integrable_smul₀' MeasureTheory.IntegrableOn.eq_1 MeasureTheory.Measure.ext MeasureTheory.Measure.restrict_apply MeasureTheory.withDensity_apply MeasureTheory.Measure.restrict_restrict MeasureTheory.exists_eq_setAverage MeasureTheory.setAverage_eq MeasureTheory.measureReal_def Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial
exists_eq_const_mul_setIntegral_of_nonneg 📖	mathematical	IsConnected MeasurableSet ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace MeasureTheory.IntegrableOn SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Real.instMul Real.instLE Real.instZero	Set Set.instMembership MeasureTheory.integral Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField MeasureTheory.Measure.restrict	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.ae_restrict_iff' MeasureTheory.ae_of_all exists_eq_const_mul_setIntegral_of_ae_nonneg

---

← Back to Index