MeanInequalitiesPow

📁 Source: Mathlib/Analysis/MeanInequalitiesPow.lean

Statistics

Metric	Count
Definitions	0
Theorems add_rpow_le_rpow_add, rpow_add_le_add_rpow, rpow_add_le_mul_rpow_add_rpow, rpow_add_rpow_le, rpow_add_rpow_le_add, rpow_arith_mean_le_arith_mean2_rpow, rpow_arith_mean_le_arith_mean_rpow, add_rpow_le_rpow_add, arith_mean_le_rpow_mean, pow_arith_mean_le_arith_mean_pow, rpow_add_le_add_rpow, rpow_add_le_mul_rpow_add_rpow, rpow_add_rpow_le, rpow_add_rpow_le_add, rpow_arith_mean_le_arith_mean2_rpow, rpow_arith_mean_le_arith_mean_rpow, add_rpow_le_rpow_add, arith_mean_le_rpow_mean, pow_arith_mean_le_arith_mean_pow, pow_arith_mean_le_arith_mean_pow_of_even, rpow_add_le_add_rpow, rpow_add_rpow_le, rpow_add_rpow_le_add, rpow_arith_mean_le_arith_mean_rpow, zpow_arith_mean_le_arith_mean_zpow	25
Total	25

ENNReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_rpow_le_rpow_add 📖	mathematical	Real Real.instLE Real.instOne	ENNReal Preorder.toLE PartialOrder.toPreorder instPartialOrder Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring instPowReal	—	lt_of_lt_of_le Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one rpow_eq_top_iff_of_pos le_top add_ne_top CanLift.prf canLift coe_rpow_of_nonneg LT.lt.le coe_le_coe NNReal.add_rpow_le_rpow_add
rpow_add_le_add_rpow 📖	mathematical	Real Real.instLE Real.instZero Real.instOne	ENNReal Preorder.toLE PartialOrder.toPreorder instPartialOrder instPowReal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring	—	LE.le.eq_or_lt rpow_zero instCanonicallyOrderedAdd rpow_add_rpow_le le_rpow_inv_iff rpow_one one_div one_div_one
rpow_add_le_mul_rpow_add_rpow 📖	mathematical	Real Real.instLE Real.instOne	ENNReal Preorder.toLE PartialOrder.toPreorder instPartialOrder instPowReal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring Distrib.toMul instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat Real.instSub	—	Nat.instAtLeastTwoHAddOfNat one_div inv_mul_cancel two_ne_zero CharZero.NeZero.two instCharZero ofNat_ne_top one_mul rpow_sub rpow_one div_eq_inv_mul mul_one mul_rpow_of_nonneg LE.le.trans zero_le_one Real.instZeroLEOneClass Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf 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.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add rpow_arith_mean_le_arith_mean2_rpow add_halves
rpow_add_rpow_le 📖	mathematical	Real Real.instLT Real.instZero Real.instLE	ENNReal Preorder.toLE PartialOrder.toPreorder instPartialOrder instPowReal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne	—	rpow_mul mul_div_cancel₀ LT.lt.ne' rpow_add_rpow_le_add one_le_div PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing one_div le_rpow_inv_iff mul_comm mul_one_div one_div_div
rpow_add_rpow_le_add 📖	mathematical	Real Real.instLE Real.instOne	ENNReal Preorder.toLE PartialOrder.toPreorder instPartialOrder instPowReal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring DivInvMonoid.toDiv Real.instDivInvMonoid	—	one_div le_rpow_inv_iff PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing lt_of_lt_of_le zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike inv_inv add_rpow_le_rpow_add
rpow_arith_mean_le_arith_mean2_rpow 📖	mathematical	ENNReal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Real Real.instLE Real.instOne	Preorder.toLE PartialOrder.toPreorder instPartialOrder instPowReal Distrib.toMul	—	rpow_arith_mean_le_arith_mean_rpow Finset.sum_congr Fin.sum_univ_succ Finset.univ_unique Matrix.cons_val_succ Matrix.cons_val_fin_one Finset.sum_const Finset.card_singleton one_smul
rpow_arith_mean_le_arith_mean_rpow 📖	mathematical	Finset.sum ENNReal instAddCommMonoid AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Real Real.instLE Real.instOne	Preorder.toLE PartialOrder.toPreorder instPartialOrder instPowReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring	—	lt_of_lt_of_le Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one le_of_lt le_of_top_imp_top_of_toNNReal_le rpow_eq_top_iff sum_eq_top LT.lt.ne lt_top_of_sum_ne_top top_rpow_of_pos toNNReal_sum toNNReal_rpow Finset.sum_congr toNNReal_mul NNReal.rpow_arith_mean_le_arith_mean_rpow coe_finset_sum coe_toNNReal one_ne_top

NNReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_rpow_le_rpow_add 📖	mathematical	Real Real.instLE Real.instOne	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal instPowReal	—	lt_of_lt_of_le Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one add_eq_zero Unique.instSubsingleton instCanonicallyOrderedAdd zero_rpow LT.lt.ne' add_zero add_div div_self Eq.le mul_one mul_le_mul_right mulLeftMono div_rpow one_mul mul_inv_cancel₀ mul_assoc mul_comm mul_add Distrib.leftDistribClass div_eq_mul_inv
arith_mean_le_rpow_mean 📖	mathematical	Finset.sum NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal instOneNNReal Real Real.instLE Real.instOne	Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib instPowReal DivInvMonoid.toDiv Real.instDivInvMonoid	—	Nat.cast_one Finset.sum_congr Real.arith_mean_le_rpow_mean coe_nonneg
pow_arith_mean_le_arith_mean_pow 📖	mathematical	Finset.sum NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal instOneNNReal	Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	Finset.sum_congr Real.pow_arith_mean_le_arith_mean_pow coe_nonneg Nat.cast_one
rpow_add_le_add_rpow 📖	mathematical	Real Real.instLE Real.instZero Real.instOne	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal instPowReal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal	—	LE.le.eq_or_lt rpow_zero addLeftMono IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd addLeftReflectLT instCanonicallyOrderedAdd rpow_add_rpow_le le_rpow_inv_iff rpow_one one_div one_div_one
rpow_add_le_mul_rpow_add_rpow 📖	mathematical	Real Real.instLE Real.instOne	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal instPowReal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal Distrib.toMul instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Nat.instAtLeastTwoHAddOfNat Real.instSub	—	Nat.instAtLeastTwoHAddOfNat eq_or_lt_of_le rpow_one sub_self rpow_zero one_mul le_refl one_div inv_mul_cancel_left₀ CharZero.NeZero.two IsStrictOrderedRing.toCharZero instIsStrictOrderedRing ne_of_gt sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid rpow_sub' div_eq_inv_mul mul_one mul_rpow Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.inv_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul rpow_arith_mean_le_arith_mean2_rpow add_halves
rpow_add_rpow_le 📖	mathematical	Real Real.instLT Real.instZero Real.instLE	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal instPowReal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne	—	rpow_mul div_eq_inv_mul mul_assoc mul_inv_cancel₀ LT.lt.ne one_mul rpow_add_rpow_le_add one_le_div PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing one_div le_rpow_inv_iff mul_comm mul_one_div one_div_div
rpow_add_rpow_le_add 📖	mathematical	Real Real.instLE Real.instOne	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal instPowReal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal DivInvMonoid.toDiv Real.instDivInvMonoid	—	one_div le_rpow_inv_iff PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing lt_of_lt_of_le zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike inv_inv add_rpow_le_rpow_add
rpow_arith_mean_le_arith_mean2_rpow 📖	mathematical	NNReal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal instOneNNReal Real Real.instLE Real.instOne	Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal instPowReal Distrib.toMul	—	rpow_arith_mean_le_arith_mean_rpow Finset.sum_congr Fin.sum_univ_succ Finset.univ_unique Matrix.cons_val_succ Matrix.cons_val_fin_one Finset.sum_const Finset.card_singleton one_smul
rpow_arith_mean_le_arith_mean_rpow 📖	mathematical	Finset.sum NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal instOneNNReal Real Real.instLE Real.instOne	Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal instPowReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	Finset.sum_congr Real.rpow_arith_mean_le_arith_mean_rpow coe_nonneg Nat.cast_one

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_rpow_le_rpow_add 📖	mathematical	Real instLE instZero instOne	instAdd instPow	—	CanLift.prf NNReal.canLift NNReal.add_rpow_le_rpow_add
arith_mean_le_rpow_mean 📖	mathematical	Real instLE instZero Finset.sum instAddCommMonoid instOne	instMul instPow DivInvMonoid.toDiv instDivInvMonoid	—	lt_of_lt_of_le Mathlib.Meta.Positivity.pos_of_isNat instIsOrderedRing instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one rpow_le_rpow_iff Finset.sum_nonneg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid mul_nonneg IsOrderedRing.toPosMulMono rpow_nonneg rpow_mul one_div_mul_cancel ne_of_gt rpow_one rpow_arith_mean_le_arith_mean_rpow
pow_arith_mean_le_arith_mean_pow 📖	mathematical	Real instLE instZero Finset.sum instAddCommMonoid instOne	Monoid.toNatPow instMonoid instMul	—	ConvexOn.map_sum_le instIsStrictOrderedRing instIsOrderedAddMonoid IsStrictOrderedRing.toIsStrictOrderedModule convexOn_pow
pow_arith_mean_le_arith_mean_pow_of_even 📖	mathematical	Real instLE instZero Finset.sum instAddCommMonoid instOne Even	Monoid.toNatPow instMonoid instMul	—	ConvexOn.map_sum_le instIsStrictOrderedRing instIsOrderedAddMonoid IsStrictOrderedRing.toIsStrictOrderedModule Even.convexOn_pow Set.mem_univ
rpow_add_le_add_rpow 📖	mathematical	Real instLE instZero instOne	instPow instAdd	—	CanLift.prf NNReal.canLift NNReal.rpow_add_le_add_rpow
rpow_add_rpow_le 📖	mathematical	Real instLE instZero instLT	instPow instAdd DivInvMonoid.toDiv instDivInvMonoid instOne	—	CanLift.prf NNReal.canLift Nat.cast_one NNReal.rpow_add_rpow_le
rpow_add_rpow_le_add 📖	mathematical	Real instLE instZero instOne	instPow instAdd DivInvMonoid.toDiv instDivInvMonoid	—	CanLift.prf NNReal.canLift Nat.cast_one NNReal.rpow_add_rpow_le_add
rpow_arith_mean_le_arith_mean_rpow 📖	mathematical	Real instLE instZero Finset.sum instAddCommMonoid instOne	instPow instMul	—	ConvexOn.map_sum_le instIsStrictOrderedRing instIsOrderedAddMonoid IsStrictOrderedRing.toIsStrictOrderedModule convexOn_rpow
zpow_arith_mean_le_arith_mean_zpow 📖	mathematical	Real instLE instZero Finset.sum instAddCommMonoid instOne instLT	DivInvMonoid.toZPow instDivInvMonoid instMul	—	ConvexOn.map_sum_le instIsStrictOrderedRing instIsOrderedAddMonoid IsStrictOrderedRing.toIsStrictOrderedModule convexOn_zpow

---

← Back to Index