Pow

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

Statistics

Metric	Count
Definitions	0
Theorems concaveOn_rpow, strictConcaveOn_rpow, strictConcaveOn_sqrt, concaveOn_rpow, strictConcaveOn_rpow, strictConcaveOn_sqrt	6
Total	6

NNReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
concaveOn_rpow 📖	mathematical	Real Real.instLE Real.instZero Real.instOne	ConcaveOn NNReal instSemiringNNReal instPartialOrderNNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toSMul instCommSemiringNNReal CommSemiring.toSemiring Algebra.id Set.univ instPowReal	—	eq_or_lt_of_le rpow_zero concaveOn_const convex_univ rpow_one concaveOn_id StrictConcaveOn.concaveOn strictConcaveOn_rpow
strictConcaveOn_rpow 📖	mathematical	Real Real.instLT Real.instZero Real.instOne	StrictConcaveOn NNReal instSemiringNNReal instPartialOrderNNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toSMul instCommSemiringNNReal CommSemiring.toSemiring Algebra.id Set.univ instPowReal	—	div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike one_lt_div convex_univ strictConvexOn_rpow Nat.cast_one one_div_pos one_div div_inv_eq_mul one_mul orderIsoRpow.congr_simp orderIsoRpow_symm_eq OrderIso.strictConcaveOn_symm
strictConcaveOn_sqrt 📖	mathematical	—	StrictConcaveOn NNReal instSemiringNNReal instPartialOrderNNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toSMul instCommSemiringNNReal CommSemiring.toSemiring Algebra.id Set.univ DFunLike.coe OrderIso Preorder.toLE PartialOrder.toPreorder instFunLikeOrderIso sqrt	—	Nat.instAtLeastTwoHAddOfNat eq Nat.cast_one sqrt_eq_rpow strictConcaveOn_rpow div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.neg_add 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.mul_congr 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.zero_mul Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le neg_neg_of_pos Real.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one CancelDenoms.derive_trans Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.isRat_sub Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Linarith.mul_nonpos Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Meta.NormNum.isNat_lt_true

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
concaveOn_rpow 📖	mathematical	Real instLE instZero instOne	ConcaveOn semiring partialOrder instAddCommMonoid Algebra.toSMul instCommSemiring CommSemiring.toSemiring Algebra.id Set.Ici instPreorder instPow	—	eq_or_lt_of_le rpow_zero concaveOn_const convex_Ici instIsOrderedAddMonoid IsOrderedModule.toPosSMulMono IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule instIsStrictOrderedRing rpow_one concaveOn_id StrictConcaveOn.concaveOn strictConcaveOn_rpow
strictConcaveOn_rpow 📖	mathematical	Real instLT instZero instOne	StrictConcaveOn semiring partialOrder instAddCommMonoid Algebra.toSMul instCommSemiring CommSemiring.toSemiring Algebra.id Set.Ici instPreorder instPow	—	convex_Ici instIsOrderedAddMonoid IsOrderedModule.toPosSMulMono IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule instIsStrictOrderedRing LT.lt.le Subtype.coe_ne_coe NNReal.eq NNReal.strictConcaveOn_rpow Set.mem_univ Nat.cast_zero
strictConcaveOn_sqrt 📖	mathematical	—	StrictConcaveOn Real semiring partialOrder instAddCommMonoid Algebra.toSMul instCommSemiring CommSemiring.toSemiring Algebra.id Set.Ici instPreorder instZero sqrt	—	Nat.instAtLeastTwoHAddOfNat sqrt_eq_rpow strictConcaveOn_rpow div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing Mathlib.Meta.Positivity.pos_of_isNat instIsOrderedRing instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.instAtLeastTwo lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.neg_add 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.mul_congr 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.zero_mul Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le neg_neg_of_pos instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one CancelDenoms.derive_trans Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.isRat_sub Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Linarith.mul_nonpos Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Meta.NormNum.isNat_lt_true

---

← Back to Index