Strong

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

Statistics

Metric	Count
Definitions StrongConcaveOn, StrongConvexOn, UniformConcaveOn, UniformConvexOn	4
Theorems uniformConcaveOn_zero, uniformConvexOn_zero, mono, strictConcaveOn, mono, strictConvexOn, add, concaveOn, mono, neg, strictConcaveOn, sub, add, convexOn, mono, neg, strictConvexOn, sub, strongConcaveOn_iff_convex, strongConcaveOn_zero, strongConvexOn_iff_convex, strongConvexOn_zero, uniformConcaveOn_zero, uniformConvexOn_zero	24
Total	28

ConcaveOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
uniformConcaveOn_zero 📖	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	UniformConcaveOn Pi.instZero Real.instZero	—	uniformConcaveOn_zero

ConvexOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
uniformConvexOn_zero 📖	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	UniformConvexOn Pi.instZero Real.instZero	—	uniformConvexOn_zero

StrongConcaveOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mono 📖	—	Real Real.instLE StrongConcaveOn	—	—	UniformConcaveOn.mono mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono Real.instIsOrderedRing div_le_div_of_nonneg_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing le_of_lt Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Even.pow_nonneg IsStrictOrderedRing.toIsOrderedRing AddGroup.existsAddOfLE Nat.instAtLeastTwoHAddOfNat even_two_mul
strictConcaveOn 📖	mathematical	StrongConcaveOn Real Real.instLT Real.instZero	StrictConcaveOn 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	—	UniformConcaveOn.strictConcaveOn mul_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo lt_of_le_of_ne' Even.pow_nonneg IsStrictOrderedRing.toIsOrderedRing AddGroup.existsAddOfLE Nat.instAtLeastTwoHAddOfNat even_two_mul pow_ne_zero isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass

StrongConvexOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mono 📖	—	Real Real.instLE StrongConvexOn	—	—	UniformConvexOn.mono mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono Real.instIsOrderedRing div_le_div_of_nonneg_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing le_of_lt Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Even.pow_nonneg IsStrictOrderedRing.toIsOrderedRing AddGroup.existsAddOfLE Nat.instAtLeastTwoHAddOfNat even_two_mul
strictConvexOn 📖	mathematical	StrongConvexOn Real Real.instLT Real.instZero	StrictConvexOn 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	—	UniformConvexOn.strictConvexOn mul_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo lt_of_le_of_ne' Even.pow_nonneg IsStrictOrderedRing.toIsOrderedRing AddGroup.existsAddOfLE Nat.instAtLeastTwoHAddOfNat even_two_mul pow_ne_zero isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass

UniformConcaveOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	UniformConcaveOn	Pi.instAdd Real Real.instAdd	—	mul_add Distrib.leftDistribClass add_add_add_comm add_le_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add
concaveOn 📖	mathematical	UniformConcaveOn Pi.hasLe Real Real.instLE Pi.instZero Real.instZero	ConcaveOn 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	—	mono
mono 📖	—	Pi.hasLe Real Real.instLE UniformConcaveOn	—	—	LE.le.trans' add_le_add_right IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Real.instIsOrderedRing mul_nonneg
neg 📖	mathematical	UniformConcaveOn	UniformConvexOn Pi.instNeg Real Real.instNeg	—	le_of_neg_le_neg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add mul_neg sub_eq_add_neg neg_add_rev neg_neg add_comm
strictConcaveOn 📖	mathematical	UniformConcaveOn Real Real.instLT Real.instZero	StrictConcaveOn 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	—	LE.le.trans_lt' LT.lt.le lt_add_of_pos_right IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid LT.lt.ne' norm_pos_iff sub_ne_zero mul_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing
sub 📖	mathematical	UniformConcaveOn UniformConvexOn	Pi.instAdd Real Real.instAdd Pi.instSub Real.instSub	—	add UniformConvexOn.neg

UniformConvexOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	UniformConvexOn	Pi.instAdd Real Real.instAdd	—	mul_add Distrib.leftDistribClass sub_add_sub_comm add_add_add_comm add_le_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add
convexOn 📖	mathematical	UniformConvexOn Pi.hasLe Real Real.instLE Pi.instZero Real.instZero	ConvexOn 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	—	mono
mono 📖	—	Pi.hasLe Real Real.instLE UniformConvexOn	—	—	LE.le.trans sub_le_sub_left IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Real.instIsOrderedRing mul_nonneg
neg 📖	mathematical	UniformConvexOn	UniformConcaveOn Pi.instNeg Real Real.instNeg	—	le_of_neg_le_neg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add neg_neg mul_neg neg_add_rev add_comm
strictConvexOn 📖	mathematical	UniformConvexOn Real Real.instLT Real.instZero	StrictConvexOn 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	—	LE.le.trans_lt LT.lt.le sub_lt_self IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid LT.lt.ne' norm_pos_iff sub_ne_zero mul_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing
sub 📖	mathematical	UniformConvexOn UniformConcaveOn	Pi.instAdd Real Real.instAdd Pi.instSub Real.instSub	—	add UniformConcaveOn.neg

(root)

Definitions

Name	Category	Theorems
StrongConcaveOn 📖	MathDef	2 math math: strongConcaveOn_zero, strongConcaveOn_iff_convex
StrongConvexOn 📖	MathDef	2 math math: strongConvexOn_iff_convex, strongConvexOn_zero
UniformConcaveOn 📖	MathDef	3 math math: ConcaveOn.uniformConcaveOn_zero, uniformConcaveOn_zero, UniformConvexOn.neg
UniformConvexOn 📖	MathDef	3 math math: ConvexOn.uniformConvexOn_zero, UniformConcaveOn.neg, uniformConvexOn_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
strongConcaveOn_iff_convex 📖	mathematical	—	StrongConcaveOn InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup ConcaveOn Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace 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 Real.instAdd Real.instMul DivInvMonoid.toDiv Real.instDivInvMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Monoid.toNatPow Norm.norm NormedAddCommGroup.toNorm	—	Nat.instAtLeastTwoHAddOfNat covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid mul_assoc mul_left_comm
strongConcaveOn_zero 📖	mathematical	—	StrongConcaveOn Real Real.instZero ConcaveOn 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	—	zero_div MulZeroClass.zero_mul
strongConvexOn_iff_convex 📖	mathematical	—	StrongConvexOn InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup ConvexOn Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace 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 Real.instSub Real.instMul DivInvMonoid.toDiv Real.instDivInvMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Monoid.toNatPow Norm.norm NormedAddCommGroup.toNorm	—	Nat.instAtLeastTwoHAddOfNat covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid mul_assoc mul_left_comm
strongConvexOn_zero 📖	mathematical	—	StrongConvexOn Real Real.instZero ConvexOn 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	—	zero_div MulZeroClass.zero_mul
uniformConcaveOn_zero 📖	mathematical	—	UniformConcaveOn Pi.instZero Real Real.instZero ConcaveOn 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	—	MulZeroClass.mul_zero add_zero
uniformConvexOn_zero 📖	mathematical	—	UniformConvexOn Pi.instZero Real Real.instZero ConvexOn 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	—	MulZeroClass.mul_zero sub_zero

---

← Back to Index