Documentation Verification Report

Basic

📁 Source: Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems `exp_mul_le_cosh_add_mul_sinh`, `convexOn_exp`, `convexOn_rpow`, `convexOn_rpow_left`, `one_add_mul_self_le_rpow_one_add`, `one_add_mul_self_lt_rpow_one_add`, `rpow_one_add_le_one_add_mul_self`, `rpow_one_add_lt_one_add_mul_self`, `strictConcaveOn_log_Iio`, `strictConcaveOn_log_Ioi`, `strictConvexOn_exp`, `strictConvexOn_rpow`	12
Total	12

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exp_mul_le_cosh_add_mul_sinh` 📖	mathematical	`Real` `instLE` `abs` `lattice` `instAddGroup` `instOne`	`exp` `instMul` `instAdd` `cosh` `sinh`	—	`Nat.instAtLeastTwoHAddOfNat` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Meta.NormNum.IsNNRat.to_raw_eq` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Meta.NormNum.IsRat.to_raw_eq` `Mathlib.Meta.NormNum.isRat_mul` `Mathlib.Meta.NormNum.IsInt.to_isRat` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Meta.NormNum.IsNNRat.of_raw` `Mathlib.Meta.NormNum.IsNNRat.den_nz` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Meta.NormNum.IsRat.to_isNNRat` `Mathlib.Meta.NormNum.IsRat.of_raw` `Mathlib.Meta.NormNum.IsRat.den_nz` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_add` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.IsRat.to_isInt` `Mathlib.Meta.NormNum.isRat_add` `Mathlib.Tactic.RingNF.nat_rawCast_1` `pow_one` `mul_one` `add_zero` `convexOn_exp` `Set.mem_univ` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Linarith.add_lt_of_le_of_neg` `instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `instIsOrderedRing` `abs_le` `instIsOrderedAddMonoid` `CancelDenoms.sub_subst` `CancelDenoms.div_subst` `CancelDenoms.add_subst` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Tactic.Linarith.mul_neg` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Mathlib.Meta.NormNum.isNat_lt_true` `cosh_eq` `sinh_eq`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`convexOn_exp` 📖	mathematical	—	`ConvexOn` `Real` `Real.semiring` `Real.partialOrder` `Real.instAddCommMonoid` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Set.univ` `Real.exp`	—	`StrictConvexOn.convexOn` `strictConvexOn_exp`
`convexOn_rpow` 📖	mathematical	`Real` `Real.instLE` `Real.instOne`	`ConvexOn` `Real.semiring` `Real.partialOrder` `Real.instAddCommMonoid` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Set.Ici` `Real.instPreorder` `Real.instZero` `Real.instPow`	—	`eq_or_lt_of_le` `Real.rpow_one` `convexOn_id` `convex_Ici` `Real.instIsOrderedAddMonoid` `IsOrderedModule.toPosSMulMono` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `Real.instIsStrictOrderedRing` `StrictConvexOn.convexOn` `strictConvexOn_rpow`
`convexOn_rpow_left` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`ConvexOn` `Real.semiring` `Real.partialOrder` `Real.instAddCommMonoid` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Set.univ` `Real.instPow`	—	`smulCommClass_self` `Algebra.to_smulCommClass` `IsScalarTower.right` `Real.rpow_def_of_pos` `ConvexOn.comp_linearMap` `convexOn_exp`
`one_add_mul_self_le_rpow_one_add` 📖	mathematical	`Real` `Real.instLE` `Real.instNeg` `Real.instOne`	`Real.instAdd` `Real.instMul` `Real.instPow`	—	`eq_or_lt_of_le` `one_mul` `Real.rpow_one` `MulZeroClass.mul_zero` `add_zero` `Real.one_rpow` `LT.lt.le` `one_add_mul_self_lt_rpow_one_add`
`one_add_mul_self_lt_rpow_one_add` 📖	mathematical	`Real` `Real.instLE` `Real.instNeg` `Real.instOne` `Real.instLT`	`Real.instAdd` `Real.instMul` `Real.instPow`	—	`LT.lt.trans` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `eq_or_lt_of_le` `add_neg_cancel` `Real.zero_rpow` `LT.lt.ne'` `mul_neg_one` `add_neg_lt_iff_lt_add` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `zero_add` `neg_lt_iff_pos_add'` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `le_or_gt` `LE.le.trans_lt` `Real.rpow_pos_of_pos` `add_eq_left` `Mathlib.Tactic.Contrapose.contrapose₄` `eq_false_intro` `mul_eq_zero` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `Real.rpow_def_of_pos` `Real.exp_log` `Real.exp_strictMono` `lt_or_gt_of_ne` `div_lt_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `div_lt_div_right_of_neg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `add_sub_cancel_left` `Real.log_one` `sub_zero` `div_div` `StrictConcaveOn.secant_strict_mono` `strictConcaveOn_log_Ioi` `zero_lt_one'` `add_lt_add_right` `mul_lt_of_one_lt_left` `AddGroup.existsAddOfLE` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `div_lt_div_iff_of_pos_right` `lt_mul_of_one_lt_left`
`rpow_one_add_le_one_add_mul_self` 📖	mathematical	`Real` `Real.instLE` `Real.instNeg` `Real.instOne` `Real.instZero`	`Real.instPow` `Real.instAdd` `Real.instMul`	—	`eq_or_lt_of_le` `Real.rpow_zero` `MulZeroClass.zero_mul` `add_zero` `Real.rpow_one` `one_mul` `Real.one_rpow` `MulZeroClass.mul_zero` `LT.lt.le` `rpow_one_add_lt_one_add_mul_self`
`rpow_one_add_lt_one_add_mul_self` 📖	mathematical	`Real` `Real.instLE` `Real.instNeg` `Real.instOne` `Real.instLT` `Real.instZero`	`Real.instPow` `Real.instAdd` `Real.instMul`	—	`eq_or_lt_of_le` `add_neg_cancel` `Real.zero_rpow` `LT.lt.ne'` `mul_neg_one` `lt_add_neg_iff_add_lt` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `zero_add` `neg_lt_iff_pos_add'` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `lt_or_gt_of_ne` `LT.lt.trans` `lt_mul_of_lt_one_left` `AddGroup.existsAddOfLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `neg_one_lt_zero` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `add_eq_left` `Mathlib.Tactic.Contrapose.contrapose₄` `eq_false_intro` `mul_eq_zero` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `Real.rpow_def_of_pos` `Real.exp_log` `Real.exp_strictMono` `lt_div_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `div_lt_div_right_of_neg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `add_sub_cancel_left` `div_div` `Real.log_one` `sub_zero` `StrictConcaveOn.secant_strict_mono` `strictConcaveOn_log_Ioi` `zero_lt_one'` `add_lt_add_right` `div_lt_div_iff_of_pos_right` `mul_lt_of_lt_one_left`
`strictConcaveOn_log_Iio` 📖	mathematical	—	`StrictConcaveOn` `Real` `Real.semiring` `Real.partialOrder` `Real.instAddCommMonoid` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Set.Iio` `Real.instPreorder` `Real.instZero` `Real.log`	—	`convex_Iio` `Real.instIsOrderedCancelAddMonoid` `IsStrictOrderedModule.toPosSMulStrictMono` `IsStrictOrderedRing.toIsStrictOrderedModule` `Real.instIsStrictOrderedRing` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Mathlib.Tactic.Contrapose.contrapose₄` `Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Linarith.lt_of_eq_of_lt` `sub_eq_zero_of_eq` `Mathlib.Tactic.Ring.add_pf_add_gt` `neg_eq_zero` `Real.log_neg_eq_log` `strictConcaveOn_log_Ioi` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.zero_mul`
`strictConcaveOn_log_Ioi` 📖	mathematical	—	`StrictConcaveOn` `Real` `Real.semiring` `Real.partialOrder` `Real.instAddCommMonoid` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Set.Ioi` `Real.instPreorder` `Real.instZero` `Real.log`	—	`strictConcaveOn_of_slope_strict_anti_adjacent` `Real.instIsStrictOrderedRing` `convex_Ioi` `Real.instIsOrderedCancelAddMonoid` `IsStrictOrderedModule.toPosSMulStrictMono` `IsStrictOrderedRing.toIsStrictOrderedModule` `LT.lt.trans` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `div_lt_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Mathlib.Tactic.Contrapose.contrapose₃` `div_eq_one_iff_eq` `LT.lt.ne'` `sub_self` `Real.log_div` `Real.log_lt_sub_one_of_pos` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.subst_sub` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_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` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.one_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `ne_of_gt` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.Ring.cast_pos` `Nat.cast_one` `lt_div_iff₀` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Tactic.Ring.inv_mul` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Linarith.add_lt_of_le_of_neg` `Mathlib.Tactic.Linarith.without_one_mul` `CancelDenoms.sub_subst` `CancelDenoms.neg_subst`
`strictConvexOn_exp` 📖	mathematical	—	`StrictConvexOn` `Real` `Real.semiring` `Real.partialOrder` `Real.instAddCommMonoid` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Set.univ` `Real.exp`	—	`strictConvexOn_of_slope_strict_mono_adjacent` `Real.instIsStrictOrderedRing` `convex_univ` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `div_lt_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.exp_add` `Mathlib.Tactic.Ring.atom_pf'` `Mathlib.Tactic.RingNF.nat_rawCast_1` `pow_one` `mul_one` `add_zero` `Mathlib.Tactic.RingNF.int_rawCast_neg` `Mathlib.Tactic.RingNF.mul_neg` `Mathlib.Tactic.RingNF.add_neg` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.cast_pos` `Nat.cast_one` `mul_lt_mul_of_pos_left` `IsStrictOrderedRing.toPosMulStrictMono` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Linarith.add_lt_of_le_of_neg` `Real.add_one_lt_exp` `LT.lt.ne` `Real.exp_pos` `lt_div_iff₀` `LT.lt.ne'` `le_refl`
`strictConvexOn_rpow` 📖	mathematical	`Real` `Real.instLT` `Real.instOne`	`StrictConvexOn` `Real.semiring` `Real.partialOrder` `Real.instAddCommMonoid` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Set.Ici` `Real.instPreorder` `Real.instZero` `Real.instPow`	—	`strictConvexOn_of_slope_strict_mono_adjacent` `Real.instIsStrictOrderedRing` `convex_Ici` `Real.instIsOrderedAddMonoid` `IsOrderedModule.toPosSMulMono` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `LE.le.trans_lt` `Real.rpow_pos_of_pos` `sub_pos` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `div_lt_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `div_lt_div_iff_of_pos_right` `sub_div` `div_self` `LT.lt.ne'` `Real.div_rpow` `LT.lt.le` `sub_lt_comm` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `add_sub_cancel_right` `add_comm` `add_sub_assoc` `div_mul_eq_mul_div` `mul_div_assoc` `Real.rpow_sub` `sub_sub_cancel_left` `Real.rpow_neg_one` `mul_assoc` `div_eq_inv_mul` `sub_eq_add_neg` `mul_neg` `neg_div` `neg_sub` `one_add_mul_self_lt_rpow_one_add` `le_sub_iff_add_le` `neg_add_cancel` `div_nonneg_iff` `sub_ne_zero` `LT.lt.ne` `div_lt_one` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `lt_div_iff₀` `lt_sub_iff_add_lt'` `one_lt_div`

---

← Back to Index