Documentation Verification Report

Integral

📁 Source: Mathlib/Analysis/Convex/Integral.lean

Statistics

Metric	Count
Definitions	0
Theorems `average_mem_hypograph`, `le_map_average`, `le_map_integral`, `le_map_set_average`, `set_average_mem_hypograph`, `average_mem`, `average_mem_interior_of_set`, `integral_mem`, `set_average_mem`, `set_average_mem_closure`, `average_mem_epigraph`, `map_average_le`, `map_integral_le`, `map_set_average_le`, `set_average_mem_epigraph`, `ae_eq_const_or_lt_map_average`, `ae_eq_const_or_average_mem_interior`, `ae_eq_const_or_map_average_lt`, `ae_eq_const_or_exists_average_ne_compl`, `ae_eq_const_or_norm_average_lt_of_norm_le_const`, `ae_eq_const_or_norm_integral_lt_of_norm_le_const`, `ae_eq_const_or_norm_setIntegral_lt_of_norm_le_const`	22
Total	22

ConcaveOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`average_mem_hypograph` 📖	mathematical	`ConcaveOn` `Real` `Real.semiring` `Real.partialOrder` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real.instAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `NormedSpace.toModule` `Real.normedField` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `ContinuousOn` `Real.pseudoMetricSpace` `Filter.Eventually` `Set` `Set.instMembership` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Integrable` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing`	`setOf` `Real.instLE` `MeasureTheory.average` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.average_neg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `ConvexOn.average_mem_epigraph` `neg` `ContinuousOn.neg` `IsTopologicalRing.toContinuousNeg` `instIsTopologicalRingReal` `MeasureTheory.Integrable.neg`
`le_map_average` 📖	mathematical	`ConcaveOn` `Real` `Real.semiring` `Real.partialOrder` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real.instAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `NormedSpace.toModule` `Real.normedField` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `ContinuousOn` `Real.pseudoMetricSpace` `Filter.Eventually` `Set` `Set.instMembership` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Integrable` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing`	`Real.instLE` `MeasureTheory.average` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal`	—	`MeasureTheory.Measure.instOuterMeasureClass` `average_mem_hypograph`
`le_map_integral` 📖	mathematical	`ConcaveOn` `Real` `Real.semiring` `Real.partialOrder` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real.instAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `NormedSpace.toModule` `Real.normedField` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `ContinuousOn` `Real.pseudoMetricSpace` `Filter.Eventually` `Set` `Set.instMembership` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Integrable` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing`	`Real.instLE` `MeasureTheory.integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.average_eq_integral` `le_map_average` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `MeasureTheory.IsProbabilityMeasure.neZero`
`le_map_set_average` 📖	mathematical	`ConcaveOn` `Real` `Real.semiring` `Real.partialOrder` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real.instAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `NormedSpace.toModule` `Real.normedField` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `ContinuousOn` `Real.pseudoMetricSpace` `Filter.Eventually` `Set` `Set.instMembership` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.restrict` `MeasureTheory.IntegrableOn` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing`	`Real.instLE` `MeasureTheory.average` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal`	—	`MeasureTheory.Measure.instOuterMeasureClass` `set_average_mem_hypograph`
`set_average_mem_hypograph` 📖	mathematical	`ConcaveOn` `Real` `Real.semiring` `Real.partialOrder` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real.instAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `NormedSpace.toModule` `Real.normedField` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `ContinuousOn` `Real.pseudoMetricSpace` `Filter.Eventually` `Set` `Set.instMembership` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.restrict` `MeasureTheory.IntegrableOn` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing`	`setOf` `Real.instLE` `MeasureTheory.average` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.average_neg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `ConvexOn.set_average_mem_epigraph` `neg` `ContinuousOn.neg` `IsTopologicalRing.toContinuousNeg` `instIsTopologicalRingReal` `MeasureTheory.Integrable.neg`

Convex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`average_mem` 📖	mathematical	`Convex` `Real` `Real.semiring` `Real.partialOrder` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `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` `Filter.Eventually` `Set` `Set.instMembership` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Integrable` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`MeasureTheory.average`	—	`MeasureTheory.Measure.instOuterMeasureClass` `integral_mem` `MeasureTheory.isProbabilityMeasureSMul` `MeasureTheory.Measure.ae_mono'` `IsScalarTower.right` `MeasureTheory.Measure.smul_absolutelyContinuous` `MeasureTheory.Integrable.to_average`
`average_mem_interior_of_set` 📖	—	`Convex` `Real` `Real.semiring` `Real.partialOrder` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `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` `Filter.Eventually` `Set` `Set.instMembership` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Integrable` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `interior` `MeasureTheory.average` `MeasureTheory.Measure.restrict`	—	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.restrict_univ` `MeasureTheory.Measure.restrict_congr_set` `MeasureTheory.ae_eq_univ` `MeasureTheory.Measure.restrict_toMeasurable` `MeasureTheory.measure_ne_top` `openSegment_interior_closure_subset_interior` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `set_average_mem_closure` `MeasureTheory.ae_restrict_of_ae` `MeasureTheory.Integrable.integrableOn` `MeasureTheory.average_mem_openSegment_compl_self` `MeasurableSet.nullMeasurableSet` `MeasureTheory.measurableSet_toMeasurable` `MeasureTheory.measure_toMeasurable`
`integral_mem` 📖	mathematical	`Convex` `Real` `Real.semiring` `Real.partialOrder` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `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` `Filter.Eventually` `Set` `Set.instMembership` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Integrable` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`MeasureTheory.integral`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Integrable.aestronglyMeasurable` `Filter.Eventually.exists` `MeasureTheory.Measure.ae.neBot` `MeasureTheory.IsProbabilityMeasure.neZero` `Filter.Eventually.and` `MeasureTheory.integral_congr_ae` `Filter.mp_mem` `Filter.EventuallyEq.rw` `Filter.univ_mem'` `subset_closure` `Set.mem_range_self` `BorelSpace.opensMeasurable` `MeasureTheory.StronglyMeasurable.measurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `TopologicalSpace.IsSeparable.separableSpace` `TopologicalSpace.IsSeparable.mono` `MeasureTheory.StronglyMeasurable.isSeparable_range` `Set.inter_subset_left` `MeasureTheory.tendsto_integral_approxOn_of_measurable` `MeasureTheory.integrable_congr` `MeasureTheory.integrable_const` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `IsClosed.mem_of_tendsto` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Filter.Eventually.of_forall` `sum_mem` `Real.instIsStrictOrderedRing` `ENNReal.toReal_nonneg` `Finset.sum_congr` `ENNReal.toReal_sum` `MeasureTheory.measure_ne_top` `MeasureTheory.SimpleFunc.sum_range_measure_preimage_singleton` `MeasureTheory.IsProbabilityMeasure.measure_univ` `ENNReal.toReal_one` `Set.inter_subset_right` `MeasureTheory.SimpleFunc.approxOn_mem`
`set_average_mem` 📖	mathematical	`Convex` `Real` `Real.semiring` `Real.partialOrder` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `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` `Filter.Eventually` `Set` `Set.instMembership` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.restrict` `MeasureTheory.IntegrableOn` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`MeasureTheory.average`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Ne.lt_top` `average_mem` `MeasureTheory.Restrict.isFiniteMeasure` `MeasureTheory.Measure.restrict.neZero`
`set_average_mem_closure` 📖	mathematical	`Convex` `Real` `Real.semiring` `Real.partialOrder` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `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` `Filter.Eventually` `Set` `Set.instMembership` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.restrict` `MeasureTheory.IntegrableOn` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`closure` `MeasureTheory.average`	—	`MeasureTheory.Measure.instOuterMeasureClass` `set_average_mem` `closure` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `isClosed_closure` `Filter.Eventually.mono` `subset_closure`

ConvexOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`average_mem_epigraph` 📖	mathematical	`ConvexOn` `Real` `Real.semiring` `Real.partialOrder` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real.instAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `NormedSpace.toModule` `Real.normedField` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `ContinuousOn` `Real.pseudoMetricSpace` `Filter.Eventually` `Set` `Set.instMembership` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Integrable` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing`	`setOf` `Real.instLE` `MeasureTheory.average` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Filter.Eventually.mono` `le_rfl` `Convex.average_mem` `CompleteSpace.prod` `Real.instCompleteSpace` `convex_epigraph` `Real.instIsOrderedAddMonoid` `IsOrderedModule.toPosSMulMono` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `Real.instIsStrictOrderedRing` `IsClosed.epigraph` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `MeasureTheory.Integrable.prodMk` `MeasureTheory.average_pair`
`map_average_le` 📖	mathematical	`ConvexOn` `Real` `Real.semiring` `Real.partialOrder` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real.instAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `NormedSpace.toModule` `Real.normedField` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `ContinuousOn` `Real.pseudoMetricSpace` `Filter.Eventually` `Set` `Set.instMembership` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Integrable` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing`	`Real.instLE` `MeasureTheory.average` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal`	—	`MeasureTheory.Measure.instOuterMeasureClass` `average_mem_epigraph`
`map_integral_le` 📖	mathematical	`ConvexOn` `Real` `Real.semiring` `Real.partialOrder` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real.instAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `NormedSpace.toModule` `Real.normedField` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `ContinuousOn` `Real.pseudoMetricSpace` `Filter.Eventually` `Set` `Set.instMembership` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Integrable` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing`	`Real.instLE` `MeasureTheory.integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.average_eq_integral` `map_average_le` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `MeasureTheory.IsProbabilityMeasure.neZero`
`map_set_average_le` 📖	mathematical	`ConvexOn` `Real` `Real.semiring` `Real.partialOrder` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real.instAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `NormedSpace.toModule` `Real.normedField` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `ContinuousOn` `Real.pseudoMetricSpace` `Filter.Eventually` `Set` `Set.instMembership` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.restrict` `MeasureTheory.IntegrableOn` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing`	`Real.instLE` `MeasureTheory.average` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal`	—	`MeasureTheory.Measure.instOuterMeasureClass` `set_average_mem_epigraph`
`set_average_mem_epigraph` 📖	mathematical	`ConvexOn` `Real` `Real.semiring` `Real.partialOrder` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real.instAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `NormedSpace.toModule` `Real.normedField` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `ContinuousOn` `Real.pseudoMetricSpace` `Filter.Eventually` `Set` `Set.instMembership` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.restrict` `MeasureTheory.IntegrableOn` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing`	`setOf` `Real.instLE` `MeasureTheory.average` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Ne.lt_top` `average_mem_epigraph` `MeasureTheory.Restrict.isFiniteMeasure` `MeasureTheory.Measure.restrict.neZero`

StrictConcaveOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ae_eq_const_or_lt_map_average` 📖	mathematical	`StrictConcaveOn` `Real` `Real.semiring` `Real.partialOrder` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real.instAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `NormedSpace.toModule` `Real.normedField` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `ContinuousOn` `Real.pseudoMetricSpace` `Filter.Eventually` `Set` `Set.instMembership` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Integrable` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing`	`Filter.EventuallyEq` `MeasureTheory.average` `Real.instLT` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.average_neg` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `StrictConvexOn.ae_eq_const_or_map_average_lt` `neg` `ContinuousOn.neg` `IsTopologicalRing.toContinuousNeg` `instIsTopologicalRingReal` `MeasureTheory.Integrable.neg`

StrictConvex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ae_eq_const_or_average_mem_interior` 📖	mathematical	`StrictConvex` `Real` `Real.semiring` `Real.partialOrder` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `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` `Filter.Eventually` `Set` `Set.instMembership` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Integrable` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`Filter.EventuallyEq` `MeasureTheory.average` `interior`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Convex.set_average_mem` `convex` `MeasureTheory.measure_ne_top` `MeasureTheory.ae_restrict_of_ae` `MeasureTheory.Integrable.integrableOn` `openSegment_subset` `MeasureTheory.average_mem_openSegment_compl_self` `MeasurableSet.nullMeasurableSet` `ae_eq_const_or_exists_average_ne_compl`

StrictConvexOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ae_eq_const_or_map_average_lt` 📖	mathematical	`StrictConvexOn` `Real` `Real.semiring` `Real.partialOrder` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real.instAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `NormedSpace.toModule` `Real.normedField` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `ContinuousOn` `Real.pseudoMetricSpace` `Filter.Eventually` `Set` `Set.instMembership` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Integrable` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing`	`Filter.EventuallyEq` `MeasureTheory.average` `Real.instLT` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal`	—	`MeasureTheory.Measure.instOuterMeasureClass` `ConvexOn.set_average_mem_epigraph` `convexOn` `MeasureTheory.measure_ne_top` `MeasureTheory.ae_restrict_of_ae` `MeasureTheory.Integrable.integrableOn` `MeasureTheory.average_mem_openSegment_compl_self` `MeasurableSet.nullMeasurableSet` `MeasureTheory.Integrable.prodMk` `MeasureTheory.average_pair` `Real.instCompleteSpace` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `le_of_lt` `ae_eq_const_or_exists_average_ne_compl`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ae_eq_const_or_exists_average_ne_compl` 📖	mathematical	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.average` `MeasurableSet`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Integrable.ae_eq_of_forall_setIntegral_eq` `MeasureTheory.integrable_const` `MeasureTheory.setIntegral_const` `MeasureTheory.Measure.restrict_eq_zero` `MeasureTheory.integral_zero_measure` `MeasureTheory.measureReal_def` `ENNReal.toReal_zero` `zero_smul` `MeasureTheory.Measure.restrict_congr_set` `MeasureTheory.ae_eq_univ` `MeasureTheory.Measure.restrict_univ` `MeasureTheory.measureReal_congr` `MeasureTheory.measure_smul_average` `MeasureTheory.average_mem_openSegment_compl_self` `MeasurableSet.nullMeasurableSet` `Set.mem_singleton_iff` `openSegment_same` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `Real.instNontrivial` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Push.not_and_eq` `MeasureTheory.measure_smul_setAverage` `MeasureTheory.measure_ne_top`
`ae_eq_const_or_norm_average_lt_of_norm_le_const` 📖	mathematical	`Filter.Eventually` `Real` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	`Filter.EventuallyEq` `MeasureTheory.average` `Real.instLT`	—	`MeasureTheory.Measure.instOuterMeasureClass` `le_or_gt` `Filter.Eventually.mono` `norm_le_zero_iff` `LE.le.trans` `MeasureTheory.average_congr` `MeasureTheory.average_zero` `LE.le.eq_or_lt` `le_top` `MeasureTheory.average_eq` `inv_zero` `zero_smul` `norm_zero` `interior_closedBall` `LT.lt.ne'` `StrictConvex.ae_eq_const_or_average_mem_interior` `strictConvex_closedBall` `Metric.isClosed_closedBall` `MeasureTheory.integral_undef` `smul_zero`
`ae_eq_const_or_norm_integral_lt_of_norm_le_const` 📖	mathematical	`Filter.Eventually` `Real` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	`Filter.EventuallyEq` `MeasureTheory.average` `Real.instLT` `MeasureTheory.integral` `Real.instMul` `MeasureTheory.Measure.real` `Set.univ`	—	`MeasureTheory.Measure.instOuterMeasureClass` `eq_or_ne` `MeasureTheory.average_zero_measure` `MeasureTheory.ae.congr_simp` `MeasureTheory.ae_zero` `MeasureTheory.integral_zero_measure` `norm_zero` `MulZeroClass.zero_mul` `ENNReal.instCanonicallyOrderedAdd` `div_lt_iff₀'` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `div_eq_inv_mul` `abs_of_pos` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.norm_eq_abs` `norm_inv` `norm_smul` `NormedSpace.toNormSMulClass` `MeasureTheory.average_eq` `ae_eq_const_or_norm_average_lt_of_norm_le_const`
`ae_eq_const_or_norm_setIntegral_lt_of_norm_le_const` 📖	mathematical	`Filter.Eventually` `Real` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.restrict`	`Filter.EventuallyEq` `MeasureTheory.average` `Real.instLT` `MeasureTheory.integral` `Real.instMul` `MeasureTheory.Measure.real`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.measureReal_restrict_apply_univ` `ae_eq_const_or_norm_integral_lt_of_norm_le_const` `MeasureTheory.Restrict.isFiniteMeasure` `Ne.lt_top`

---

← Back to Index