MeanInequalities

📁 Source: Mathlib/Analysis/MeanInequalities.lean

Statistics

Metric	Count
Definitions	0
Theorems Lp_add_le, inner_le_Lp_mul_Lq, inner_le_weight_mul_Lp_of_nonneg, rpow_sum_le_const_mul_sum_rpow, young_inequality, Lp_add_le, Lp_add_le_hasSum, Lp_add_le_tsum, Lp_add_le_tsum', geom_mean_le_arith_mean2_weighted, geom_mean_le_arith_mean3_weighted, geom_mean_le_arith_mean4_weighted, geom_mean_le_arith_mean_weighted, inner_le_Lp_mul_Lq, inner_le_Lp_mul_Lq_hasSum, inner_le_Lp_mul_Lq_tsum, inner_le_Lp_mul_Lq_tsum', inner_le_weight_mul_Lp, isGreatest_Lp, rpow_sum_le_const_mul_sum_rpow, summable_Lp_add, summable_mul_of_Lp_Lq, young_inequality, young_inequality_real, Lp_add_le, Lp_add_le_hasSum_of_nonneg, Lp_add_le_of_nonneg, Lp_add_le_tsum_of_nonneg, Lp_add_le_tsum_of_nonneg', arith_mean_weighted_of_constant, compact_inner_le_weight_mul_Lp_of_nonneg, geom_mean_eq_arith_mean_weighted_iff, geom_mean_eq_arith_mean_weighted_iff', geom_mean_eq_arith_mean_weighted_of_constant, geom_mean_le_arith_mean, geom_mean_le_arith_mean2_weighted, geom_mean_le_arith_mean3_weighted, geom_mean_le_arith_mean4_weighted, geom_mean_le_arith_mean_weighted, geom_mean_lt_arith_mean_weighted_iff_of_pos, geom_mean_weighted_of_constant, harm_mean_le_geom_mean, harm_mean_le_geom_mean_weighted, inner_le_Lp_mul_Lq, inner_le_Lp_mul_Lq_hasSum_of_nonneg, inner_le_Lp_mul_Lq_of_nonneg, inner_le_Lp_mul_Lq_tsum_of_nonneg, inner_le_Lp_mul_Lq_tsum_of_nonneg', inner_le_weight_mul_Lp_of_nonneg, rpow_sum_le_const_mul_sum_rpow, rpow_sum_le_const_mul_sum_rpow_of_nonneg, summable_Lp_add_of_nonneg, summable_mul_of_Lp_Lq_of_nonneg, young_inequality, young_inequality_of_nonneg	55
Total	55

ENNReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Lp_add_le 📖	mathematical	Real Real.instLE Real.instOne	ENNReal Preorder.toLE PartialOrder.toPreorder instPartialOrder instPowReal Finset.sum instAddCommMonoid Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring DivInvMonoid.toDiv Real.instDivInvMonoid	—	top_add add_top lt_of_lt_of_le zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike one_div Unique.instSubsingleton asymm instAsymmLt IsOrderedRing.toPosMulMono Real.instIsOrderedRing PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing coe_le_coe NNReal.Lp_add_le Finset.sum_congr coe_toNNReal coe_rpow_of_nonneg le_of_lt one_div_pos coe_finset_sum
inner_le_Lp_mul_Lq 📖	mathematical	Real.HolderConjugate	ENNReal Preorder.toLE PartialOrder.toPreorder instPartialOrder Finset.sum instAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring Real instPowReal DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne	—	one_div Unique.instSubsingleton Real.HolderTriple.pos asymm instAsymmLt PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsOrderedRing.toPosMulMono Real.instIsOrderedRing Real.HolderConjugate.symm MulZeroClass.zero_mul MulZeroClass.mul_zero Finset.sum_eq_zero instCanonicallyOrderedAdd top_mul mul_top coe_le_coe NNReal.inner_le_Lp_mul_Lq Finset.sum_congr coe_toNNReal coe_finset_sum coe_rpow_of_nonneg LT.lt.le
inner_le_weight_mul_Lp_of_nonneg 📖	mathematical	Real Real.instLE Real.instOne	ENNReal Preorder.toLE PartialOrder.toPreorder instPartialOrder Finset.sum instAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring instPowReal Real.instSub Real.instInv	—	LE.le.eq_or_lt inv_one sub_self rpow_zero Finset.sum_congr rpow_one one_mul lt_of_lt_of_le Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one inv_lt_one_of_one_lt₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.instZeroLEOneClass Unique.instSubsingleton IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid LT.lt.not_gt instNoZeroDivisors IsOrderedRing.toPosMulMono MulZeroClass.zero_mul Finset.sum_eq_zero instCanonicallyOrderedAdd top_mul mul_top coe_le_coe NNReal.inner_le_weight_mul_Lp LT.lt.le eq_or_ne coe_toNNReal toNNReal_mul coe_rpow_of_nonneg coe_finset_sum inv_nonneg coe_mul
rpow_sum_le_const_mul_sum_rpow 📖	mathematical	Real Real.instLE Real.instOne	ENNReal Preorder.toLE PartialOrder.toPreorder instPartialOrder instPowReal Finset.sum instAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Finset.card Real.instSub	—	eq_or_lt_of_le rpow_one sub_self rpow_zero Finset.sum_congr one_mul Real.HolderConjugate.conjExponent one_div_mul_cancel Real.HolderTriple.ne_zero Real.HolderConjugate.div_conj_eq_sub_one Mathlib.Tactic.Ring.of_eq 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.sub_congr Mathlib.Tactic.Ring.sub_pf 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.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.div_pf 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.zero_mul 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 one_rpow Finset.sum_const Nat.smul_one_eq_cast mul_rpow_of_nonneg Real.HolderTriple.nonneg rpow_le_rpow inner_le_Lp_mul_Lq Real.HolderConjugate.symm
young_inequality 📖	mathematical	Real.HolderConjugate	ENNReal Preorder.toLE PartialOrder.toPreorder instPartialOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring Distrib.toAdd DivInvMonoid.toDiv instDivInvMonoid Real instPowReal ofReal	—	le_trans le_top le_of_eq div_eq_mul_inv top_rpow_of_pos Real.HolderTriple.pos top_mul top_add Real.HolderConjugate.symm add_top coe_toNNReal coe_mul coe_rpow_of_nonneg Real.HolderTriple.nonneg ofReal.eq_1 coe_div coe_add coe_le_coe NNReal.young_inequality_real

NNReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Lp_add_le 📖	mathematical	Real Real.instLE Real.instOne	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal instPowReal Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib DivInvMonoid.toDiv Real.instDivInvMonoid	—	eq_or_lt_of_le Finset.sum_congr rpow_one Finset.sum_add_distrib div_self NeZero.charZero_one RCLike.charZero_rclike Real.HolderConjugate.conjExponent isGreatest_Lp Set.image_congr add_mul Distrib.rightDistribClass add_le_add addLeftMono covariant_swap_add_of_covariant_add
Lp_add_le_hasSum 📖	mathematical	Real Real.instLE Real.instOne HasSum NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal instTopologicalSpace instPowReal SummationFilter.unconditional	Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib	—	LT.lt.ne' lt_of_lt_of_le zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Lp_add_le_tsum HasSum.summable HasSum.tsum_eq TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace SummationFilter.instNeBotUnconditional rpow_inv_rpow_self one_div rpow_self_rpow_inv Summable.hasSum
Lp_add_le_tsum 📖	mathematical	Real Real.instLE Real.instOne Summable NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal instTopologicalSpace instPowReal SummationFilter.unconditional	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal tsum DivInvMonoid.toDiv Real.instDivInvMonoid	—	lt_of_lt_of_le zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike one_div rpow_inv_le_iff le_trans Lp_add_le add_le_add addLeftMono covariant_swap_add_of_covariant_add rpow_le_rpow_iff one_div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Summable.sum_le_tsum IsOrderedRing.toIsOrderedAddMonoid instIsOrderedRing OrderTopology.to_orderClosedTopology instOrderTopology SummationFilter.instNeBotUnconditional SummationFilter.instLeAtTopUnconditional zero_le instCanonicallyOrderedAdd HasSum.summable hasSum_of_isLUB isLUB_ciSup Summable.tsum_le_of_sum_le
Lp_add_le_tsum' 📖	mathematical	Real Real.instLE Real.instOne Summable NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal instTopologicalSpace instPowReal SummationFilter.unconditional	Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal tsum Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib DivInvMonoid.toDiv Real.instDivInvMonoid	—	Lp_add_le_tsum
geom_mean_le_arith_mean2_weighted 📖	mathematical	NNReal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal instOneNNReal	Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal Distrib.toMul Real instPowReal toReal	—	Fin.sum_univ_succ Finset.sum_congr Finset.univ_eq_empty Fin.isEmpty' add_zero Fin.prod_univ_succ Finset.prod_congr mul_one geom_mean_le_arith_mean_weighted
geom_mean_le_arith_mean3_weighted 📖	mathematical	NNReal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal instOneNNReal	Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal Distrib.toMul Real instPowReal toReal	—	mul_assoc Fin.sum_univ_succ Finset.sum_congr Finset.univ_eq_empty Fin.isEmpty' add_zero Fin.prod_univ_succ Finset.prod_congr mul_one geom_mean_le_arith_mean_weighted
geom_mean_le_arith_mean4_weighted 📖	mathematical	NNReal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal instOneNNReal	Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal Distrib.toMul Real instPowReal toReal	—	mul_assoc Fin.sum_univ_succ Finset.sum_congr Finset.univ_eq_empty Fin.isEmpty' add_zero Fin.prod_univ_succ Finset.prod_congr mul_one geom_mean_le_arith_mean_weighted
geom_mean_le_arith_mean_weighted 📖	mathematical	Finset.sum NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal instOneNNReal	Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal Finset.prod CommSemiring.toCommMonoid instCommSemiringNNReal Real instPowReal toReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	Finset.prod_congr Finset.sum_congr Real.geom_mean_le_arith_mean_weighted coe_nonneg Nat.cast_one
inner_le_Lp_mul_Lq 📖	mathematical	Real.HolderConjugate	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Real instPowReal DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne	—	eq_zero_or_pos instCanonicallyOrderedAdd eq mul_comm Real.HolderConjugate.symm le_of_eq Finset.sum_congr div_rpow one_div inv_mul_cancel₀ Real.HolderTriple.ne_zero rpow_one div_self LT.lt.ne' one_mul div_le_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono instIsStrictOrderedRing mul_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono rpow_pos div_mul_div_comm
inner_le_Lp_mul_Lq_hasSum 📖	mathematical	Real.HolderConjugate HasSum NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal instTopologicalSpace Real instPowReal SummationFilter.unconditional	Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	inner_le_Lp_mul_Lq_tsum HasSum.summable HasSum.tsum_eq TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace SummationFilter.instNeBotUnconditional rpow_inv_rpow_self Real.HolderTriple.ne_zero Real.HolderConjugate.symm one_div Summable.hasSum
inner_le_Lp_mul_Lq_tsum 📖	mathematical	Real.HolderConjugate Summable NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal instTopologicalSpace Real instPowReal SummationFilter.unconditional	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal tsum DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne	—	le_trans inner_le_Lp_mul_Lq mul_le_mul IsOrderedRing.toPosMulMono instIsOrderedRing IsOrderedRing.toMulPosMono rpow_le_rpow_iff one_div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.HolderTriple.pos Summable.sum_le_tsum IsOrderedRing.toIsOrderedAddMonoid OrderTopology.to_orderClosedTopology instOrderTopology SummationFilter.instNeBotUnconditional SummationFilter.instLeAtTopUnconditional zero_le instCanonicallyOrderedAdd Real.HolderConjugate.symm bot_le HasSum.summable hasSum_of_isLUB isLUB_ciSup Summable.tsum_le_of_sum_le
inner_le_Lp_mul_Lq_tsum' 📖	mathematical	Real.HolderConjugate Summable NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal instTopologicalSpace Real instPowReal SummationFilter.unconditional	Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal tsum Distrib.toMul NonUnitalNonAssocSemiring.toDistrib DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne	—	inner_le_Lp_mul_Lq_tsum
inner_le_weight_mul_Lp 📖	mathematical	Real Real.instLE Real.instOne	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib instPowReal Real.instSub Real.instInv	—	LE.le.eq_or_lt inv_one sub_self rpow_zero Finset.sum_congr rpow_one one_mul eq mul_assoc rpow_of_add_eq one_ne_zero NeZero.charZero_one RCLike.charZero_rclike sub_add_cancel inner_le_Lp_mul_Lq Real.HolderConjugate.symm Real.holderConjugate_iff inv_inv add_sub_cancel ne_of_gt lt_of_lt_of_le Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one LT.lt.ne' rpow_rpow_inv div_inv_eq_mul mul_rpow rpow_inv_rpow one_div
isGreatest_Lp 📖	mathematical	Real.HolderConjugate	IsGreatest NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal Set.image Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib setOf Real instPowReal instOneNNReal DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne	—	eq_zero_or_pos instCanonicallyOrderedAdd one_div zero_rpow Real.HolderTriple.ne_zero Real.HolderConjugate.symm div_zero Finset.sum_congr Finset.sum_const_zero MulZeroClass.mul_zero add_sub_cancel_right mul_div_cancel_left_of_imp div_rpow Real.HolderConjugate.mul_eq_add rpow_sub' div_mul_cancel₀ rpow_one div_le_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono instIsStrictOrderedRing one_mul div_eq_iff Unique.instSubsingleton LT.lt.ne' rpow_add Real.HolderConjugate.inv_add_inv_eq_one le_trans inner_le_Lp_mul_Lq mul_one mul_le_mul_right mulLeftMono rpow_le_one le_of_lt Real.HolderTriple.one_div_pos
rpow_sum_le_const_mul_sum_rpow 📖	mathematical	Real Real.instLE Real.instOne	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal instPowReal Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Finset.card Real.instSub	—	eq_or_lt_of_le rpow_one sub_self rpow_zero Finset.sum_congr one_mul Real.HolderConjugate.conjExponent one_div_mul_cancel Real.HolderTriple.ne_zero Real.HolderConjugate.div_conj_eq_sub_one Mathlib.Tactic.Ring.of_eq 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.sub_congr Mathlib.Tactic.Ring.sub_pf 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.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.div_pf 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.zero_mul 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 one_rpow Finset.sum_const Nat.smul_one_eq_cast mul_rpow rpow_le_rpow inner_le_Lp_mul_Lq Real.HolderConjugate.symm Real.HolderTriple.nonneg
summable_Lp_add 📖	mathematical	Real Real.instLE Real.instOne Summable NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal instTopologicalSpace instPowReal SummationFilter.unconditional	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib	—	Lp_add_le_tsum
summable_mul_of_Lp_Lq 📖	mathematical	Real.HolderConjugate Summable NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal instTopologicalSpace Real instPowReal SummationFilter.unconditional	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	inner_le_Lp_mul_Lq_tsum
young_inequality 📖	mathematical	HolderConjugate	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal Distrib.toAdd instDiv Real instPowReal toReal	—	Real.young_inequality_of_nonneg coe_nonneg HolderConjugate.coe
young_inequality_real 📖	mathematical	Real.HolderConjugate	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal Distrib.toAdd instDiv Real instPowReal Real.toNNReal	—	sup_of_le_left Real.HolderTriple.nonneg Real.HolderConjugate.symm young_inequality Real.HolderConjugate.toNNReal

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Lp_add_le 📖	mathematical	Real instLE instOne	instPow Finset.sum instAddCommMonoid abs lattice instAddGroup instAdd DivInvMonoid.toDiv instDivInvMonoid	—	abs_nonneg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid covariant_swap_add_of_covariant_add NNReal.coe_le_coe NNReal.Lp_add_le le_trans rpow_le_rpow Finset.sum_le_sum zero_le_one instZeroLEOneClass one_div PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing Finset.sum_congr NNReal.coe_sum
Lp_add_le_hasSum_of_nonneg 📖	mathematical	Real instLE instOne instZero HasSum instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instPow SummationFilter.unconditional	instAdd	—	CanLift.prf Pi.canLift NNReal.canLift NNReal.Lp_add_le_hasSum Nat.cast_zero zero_le NNReal.instCanonicallyOrderedAdd
Lp_add_le_of_nonneg 📖	mathematical	Real instLE instOne instZero	instPow Finset.sum instAddCommMonoid instAdd DivInvMonoid.toDiv instDivInvMonoid	—	Finset.sum_congr abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid Lp_add_le
Lp_add_le_tsum_of_nonneg 📖	mathematical	Real instLE instOne instZero Summable instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instPow SummationFilter.unconditional	instAdd tsum DivInvMonoid.toDiv instDivInvMonoid	—	CanLift.prf Pi.canLift NNReal.canLift Nat.cast_one NNReal.Lp_add_le_tsum
Lp_add_le_tsum_of_nonneg' 📖	mathematical	Real instLE instOne instZero Summable instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instPow SummationFilter.unconditional	tsum instAdd DivInvMonoid.toDiv instDivInvMonoid	—	Lp_add_le_tsum_of_nonneg
arith_mean_weighted_of_constant 📖	mathematical	Finset.sum Real instAddCommMonoid instOne	instMul	—	Finset.sum_congr eq_or_ne MulZeroClass.zero_mul Finset.sum_mul one_mul
compact_inner_le_weight_mul_Lp_of_nonneg 📖	mathematical	Real instLE instOne instZero	Finset.expect instAddCommMonoid Algebra.toModule NNRat instCommSemiringNNRat semiring DivisionSemiring.toNNRatAlgebra Semifield.toDivisionSemiring Field.toSemifield instField RCLike.charZero_rclike instRCLike instMul instPow instSub instInv	—	RCLike.charZero_rclike Finset.expect_eq_sum_div_card div_rpow Finset.sum_nonneg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid instIsOrderedRing mul_nonneg IsOrderedRing.toPosMulMono rpow_nonneg div_mul_div_comm rpow_add' sub_add_cancel NeZero.charZero_one rpow_one div_le_div_of_nonneg_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono instIsStrictOrderedRing inner_le_weight_mul_Lp_of_nonneg Nat.cast_nonneg' instZeroLEOneClass
geom_mean_eq_arith_mean_weighted_iff 📖	mathematical	Real instLE instZero Finset.sum instAddCommMonoid instOne	Finset.prod instCommMonoid instPow instMul	—	left_ne_zero_of_mul rpow_zero Finset.sum_filter_of_ne Finset.prod_filter_of_ne geom_mean_eq_arith_mean_weighted_iff' LE.le.lt_iff_ne' Finset.sum_filter_ne_zero
geom_mean_eq_arith_mean_weighted_iff' 📖	mathematical	Real instLT instZero Finset.sum instAddCommMonoid instOne instLE	Finset.prod instCommMonoid instPow instMul	—	Finset.prod_eq_zero zero_rpow eq_zero_of_ne_zero_of_mul_left_eq_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass ne_of_lt Finset.sum_eq_zero_iff_of_nonneg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid mul_nonneg_iff_of_pos_left IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing lt_of_le_of_ne ne_of_gt Mathlib.Tactic.Push.not_and_eq StrictConvexOn.map_sum_eq_iff IsStrictOrderedRing.toIsStrictOrderedModule strictConvexOn_exp Set.mem_univ Finset.prod_congr exp_mul exp_log Finset.sum_congr arith_mean_weighted_of_constant mul_comm log_injOn_pos exp_sum
geom_mean_eq_arith_mean_weighted_of_constant 📖	mathematical	Real instLE instZero Finset.sum instAddCommMonoid instOne	Finset.prod instCommMonoid instPow instMul	—	geom_mean_weighted_of_constant arith_mean_weighted_of_constant
geom_mean_le_arith_mean 📖	mathematical	Real instLE instZero instLT Finset.sum instAddCommMonoid	instPow Finset.prod instCommMonoid instInv DivInvMonoid.toDiv instDivInvMonoid instMul	—	finset_prod_rpow rpow_nonneg Finset.prod_congr div_eq_mul_inv rpow_mul Finset.sum_congr mul_assoc mul_comm geom_mean_le_arith_mean_weighted div_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing le_of_lt mul_inv_cancel₀ Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero 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_zero_add Mathlib.Tactic.Ring.add_pf_add_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.lt_of_lt_of_eq Mathlib.Tactic.Linarith.sub_neg_of_lt instIsOrderedRing sub_eq_zero_of_eq
geom_mean_le_arith_mean2_weighted 📖	mathematical	Real instLE instZero instAdd instOne	instMul instPow	—	NNReal.geom_mean_le_arith_mean2_weighted
geom_mean_le_arith_mean3_weighted 📖	mathematical	Real instLE instZero instAdd instOne	instMul instPow	—	NNReal.geom_mean_le_arith_mean3_weighted
geom_mean_le_arith_mean4_weighted 📖	mathematical	Real instLE instZero instAdd instOne	instMul instPow	—	NNReal.geom_mean_le_arith_mean4_weighted
geom_mean_le_arith_mean_weighted 📖	mathematical	Real instLE instZero Finset.sum instAddCommMonoid instOne	Finset.prod instCommMonoid instPow instMul	—	Finset.prod_eq_zero zero_rpow Finset.sum_nonneg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid mul_nonneg IsOrderedRing.toPosMulMono instIsOrderedRing ConvexOn.map_sum_le instIsStrictOrderedRing IsStrictOrderedRing.toIsStrictOrderedModule convexOn_exp Set.mem_univ Finset.prod_congr eq_or_lt_of_le Mathlib.Tactic.Push.not_and_eq rpow_zero MulZeroClass.mul_zero exp_zero rpow_def_of_pos Finset.sum_congr MulZeroClass.zero_mul exp_log mul_comm exp_sum
geom_mean_lt_arith_mean_weighted_iff_of_pos 📖	mathematical	Real instLT instZero Finset.sum instAddCommMonoid instOne instLE	Finset.prod instCommMonoid instPow instMul Finset Finset.instMembership	—	lt_self_iff_false geom_mean_eq_arith_mean_weighted_iff' arith_mean_weighted_of_constant Finset.sum_congr Mathlib.Tactic.Push.not_and_eq geom_mean_le_arith_mean_weighted le_of_lt le_antisymm
geom_mean_weighted_of_constant 📖	mathematical	Real instLE instZero Finset.sum instAddCommMonoid instOne	Finset.prod instCommMonoid instPow	—	Finset.prod_congr eq_or_ne rpow_zero rpow_sum_of_nonneg one_ne_zero NeZero.charZero_one RCLike.charZero_rclike Finset.exists_ne_zero_of_sum_ne_zero rpow_one
harm_mean_le_geom_mean 📖	mathematical	Finset.Nonempty Real instLT instZero Finset.sum instAddCommMonoid	instLE DivInvMonoid.toDiv instDivInvMonoid instPow Finset.prod instCommMonoid instInv	—	harm_mean_le_geom_mean_weighted div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing Finset.sum_congr div_eq_mul_inv Finset.sum_mul mul_inv_cancel₀ LT.lt.ne' inv_inv mul_inv Finset.mul_sum inv_mul_eq_div div_right_comm finset_prod_rpow rpow_nonneg le_of_lt Finset.prod_congr rpow_mul
harm_mean_le_geom_mean_weighted 📖	mathematical	Finset.Nonempty Real instLT instZero Finset.sum instAddCommMonoid instOne	instLE instInv DivInvMonoid.toDiv instDivInvMonoid Finset.prod instCommMonoid instPow	—	geom_mean_le_arith_mean_weighted le_of_lt one_div_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing Finset.prod_pos instZeroLEOneClass instNontrivial rpow_pos_of_pos inv_pos Finset.sum_pos instIsOrderedCancelAddMonoid mul_pos le_trans inv_le_inv₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Finset.prod_congr one_div Finset.sum_congr inv_inv Finset.prod_inv_distrib Finset.prod_le_prod IsOrderedRing.toPosMulMono instIsOrderedRing inv_nonneg rpow_nonneg inv_rpow le_refl
inner_le_Lp_mul_Lq 📖	mathematical	HolderConjugate	Real instLE Finset.sum instAddCommMonoid instMul instPow abs lattice instAddGroup DivInvMonoid.toDiv instDivInvMonoid instOne	—	abs_nonneg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid covariant_swap_add_of_covariant_add NNReal.coe_le_coe NNReal.inner_le_Lp_mul_Lq le_trans Finset.sum_le_sum instIsOrderedRing Finset.sum_congr NNReal.coe_sum
inner_le_Lp_mul_Lq_hasSum_of_nonneg 📖	mathematical	HolderConjugate Real instLE instZero HasSum instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instPow SummationFilter.unconditional	instMul	—	CanLift.prf Pi.canLift NNReal.canLift NNReal.inner_le_Lp_mul_Lq_hasSum Subtype.prop
inner_le_Lp_mul_Lq_of_nonneg 📖	mathematical	HolderConjugate Real instLE instZero	Finset.sum instAddCommMonoid instMul instPow DivInvMonoid.toDiv instDivInvMonoid instOne	—	Finset.sum_congr abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid inner_le_Lp_mul_Lq
inner_le_Lp_mul_Lq_tsum_of_nonneg 📖	mathematical	HolderConjugate Real instLE instZero Summable instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instPow SummationFilter.unconditional	instMul tsum DivInvMonoid.toDiv instDivInvMonoid instOne	—	CanLift.prf Pi.canLift NNReal.canLift Nat.cast_one NNReal.inner_le_Lp_mul_Lq_tsum
inner_le_Lp_mul_Lq_tsum_of_nonneg' 📖	mathematical	HolderConjugate Real instLE instZero Summable instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instPow SummationFilter.unconditional	tsum instMul DivInvMonoid.toDiv instDivInvMonoid instOne	—	inner_le_Lp_mul_Lq_tsum_of_nonneg
inner_le_weight_mul_Lp_of_nonneg 📖	mathematical	Real instLE instOne instZero	Finset.sum instAddCommMonoid instMul instPow instSub instInv	—	CanLift.prf Pi.canLift NNReal.canLift Nat.cast_one Finset.sum_congr NNReal.inner_le_weight_mul_Lp
rpow_sum_le_const_mul_sum_rpow 📖	mathematical	Real instLE instOne	instPow Finset.sum instAddCommMonoid abs lattice instAddGroup instMul instNatCast Finset.card instSub	—	abs_nonneg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid covariant_swap_add_of_covariant_add NNReal.coe_le_coe NNReal.rpow_sum_le_const_mul_sum_rpow Finset.sum_congr NNReal.coe_sum NNReal.coe_natCast
rpow_sum_le_const_mul_sum_rpow_of_nonneg 📖	mathematical	Real instLE instOne instZero	instPow Finset.sum instAddCommMonoid instMul instNatCast Finset.card instSub	—	Finset.sum_congr abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid rpow_sum_le_const_mul_sum_rpow
summable_Lp_add_of_nonneg 📖	mathematical	Real instLE instOne instZero Summable instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instPow SummationFilter.unconditional	instAdd	—	Lp_add_le_tsum_of_nonneg
summable_mul_of_Lp_Lq_of_nonneg 📖	mathematical	HolderConjugate Real instLE instZero Summable instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instPow SummationFilter.unconditional	instMul	—	inner_le_Lp_mul_Lq_tsum_of_nonneg
young_inequality 📖	mathematical	HolderConjugate	Real instLE instMul instAdd DivInvMonoid.toDiv instDivInvMonoid instPow abs lattice instAddGroup	—	le_abs_self abs_mul instIsOrderedRing young_inequality_of_nonneg abs_nonneg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid covariant_swap_add_of_covariant_add
young_inequality_of_nonneg 📖	mathematical	Real instLE instZero HolderConjugate	instMul instAdd DivInvMonoid.toDiv instDivInvMonoid instPow	—	div_eq_inv_mul mul_inv_cancel₀ HolderTriple.ne_zero rpow_one HolderConjugate.symm geom_mean_le_arith_mean2_weighted HolderTriple.inv_nonneg rpow_nonneg HolderConjugate.inv_add_inv_eq_one

---

← Back to Index