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', Lr_le_Lp_mul_Lq, Lr_le_Lp_mul_Lq_tsum, Lr_rpow_le_Lp_mul_Lq, Lr_rpow_le_Lp_mul_Lq_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_and_Lr_rpow_le_Lp_mul_Lq_tsum, summable_and_inner_le_Lp_mul_Lq_tsum, summable_mul_of_Lp_Lq, summable_mul_rpow_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', Lr_le_Lp_mul_Lq_tsum_of_nonneg, Lr_rpow_le_Lp_mul_Lq, Lr_rpow_le_Lp_mul_Lq_of_nonneg, Lr_rpow_le_Lp_mul_Lq_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_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_Lr_of_Lp_Lq_of_nonneg, summable_and_Lr_rpow_le_Lp_mul_Lq_tsum_of_nonneg, summable_and_inner_le_Lp_mul_Lq_tsum_of_nonneg, summable_mul_of_Lp_Lq_of_nonneg, young_inequality, young_inequality_of_nonneg	69
Total	69

ENNReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Lp_add_le 📖	mathematical	Real Real.instLE Real.instOne	ENNReal Preorder.toLE PartialOrder.toPreorder instPartialOrder Real instPowReal Finset.sum instAddCommMonoid Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne	—	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 Real instPowReal Real.instSub Real.instOne Real.instInv	—	LE.le.eq_or_lt inv_one sub_self rpow_zero Finset.sum_congr rpow_one one_mul instReflLe 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 instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add 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 Real instPowReal Finset.sum instAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Finset.card Real.instSub Real.instOne	—	eq_or_lt_of_le rpow_one sub_self rpow_zero Finset.sum_congr one_mul instReflLe 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 instPartialOrder Real instPowReal Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiring Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne	—	eq_or_lt_of_le Finset.sum_congr rpow_one Finset.sum_add_distrib div_self NeZero.charZero_one RCLike.charZero_rclike instReflLe 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 instSemiring instTopologicalSpace instPowReal SummationFilter.unconditional	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrder Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiring HasSum NonUnitalNonAssocSemiring.toAddCommMonoid instTopologicalSpace Real instPowReal SummationFilter.unconditional	—	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 instSemiring instTopologicalSpace instPowReal SummationFilter.unconditional	Summable NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiring instTopologicalSpace Real instPowReal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib SummationFilter.unconditional Preorder.toLE PartialOrder.toPreorder instPartialOrder tsum DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne	—	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 OrderTopology.to_orderClosedTopology instOrderTopology SummationFilter.instNeBotUnconditional SummationFilter.instLeAtTopUnconditional zero_le 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 instSemiring instTopologicalSpace instPowReal SummationFilter.unconditional	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrder Real instPowReal tsum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiring instTopologicalSpace Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib SummationFilter.unconditional DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne	—	Lp_add_le_tsum
Lr_le_Lp_mul_Lq 📖	mathematical	Real.HolderTriple	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrder Real instPowReal Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne	—	LT.lt.ne' Real.HolderTriple.pos' mul_rpow Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one 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 div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_cons_eq_eval_of_eq_of_eq Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero Mathlib.Tactic.FieldSimp.eq_div_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div' one_ne_zero NeZero.one GroupWithZero.toNontrivial rpow_le_rpow_iff inv_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing inv_eq_one_div Lr_rpow_le_Lp_mul_Lq
Lr_le_Lp_mul_Lq_tsum 📖	mathematical	Real.HolderTriple Summable NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiring instTopologicalSpace Real instPowReal SummationFilter.unconditional	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrder Real instPowReal tsum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiring instTopologicalSpace Distrib.toMul NonUnitalNonAssocSemiring.toDistrib SummationFilter.unconditional DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne	—	LT.lt.ne' Real.HolderTriple.pos' mul_rpow Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one 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 div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_cons_eq_eval_of_eq_of_eq Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero Mathlib.Tactic.FieldSimp.eq_div_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div' one_ne_zero NeZero.one GroupWithZero.toNontrivial rpow_le_rpow_iff inv_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing inv_eq_one_div Lr_rpow_le_Lp_mul_Lq_tsum
Lr_rpow_le_Lp_mul_Lq 📖	mathematical	Real.HolderTriple	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrder Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiring Real instPowReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib DivInvMonoid.toDiv Real.instDivInvMonoid	—	Real.HolderTriple.holderConjugate_div_div Finset.sum_congr mul_rpow LE.le.trans_eq inner_le_Lp_mul_Lq Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.atom_eq_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 div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one one_ne_zero NeZero.one GroupWithZero.toNontrivial mul_div_cancel_left₀ GroupWithZero.toMulDivCancelClass LT.lt.ne' Real.HolderTriple.pos' Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.eq_div_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div' Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁
Lr_rpow_le_Lp_mul_Lq_tsum 📖	mathematical	Real.HolderTriple Summable NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiring instTopologicalSpace Real instPowReal SummationFilter.unconditional	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrder tsum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiring instTopologicalSpace Real instPowReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib SummationFilter.unconditional DivInvMonoid.toDiv Real.instDivInvMonoid	—	summable_and_Lr_rpow_le_Lp_mul_Lq_tsum
geom_mean_le_arith_mean2_weighted 📖	mathematical	NNReal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiring instOne	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiring Real instPowReal toReal Distrib.toAdd	—	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 instSemiring instOne	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiring Real instPowReal toReal Distrib.toAdd	—	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 instSemiring instOne	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiring Real instPowReal toReal Distrib.toAdd	—	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 instSemiring instOne	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrder Finset.prod CommSemiring.toCommMonoid instCommSemiring Real instPowReal toReal Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiring 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 instPartialOrder Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Real instPowReal DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne	—	eq_zero_or_pos 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 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 instSemiring instTopologicalSpace Real instPowReal SummationFilter.unconditional	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiring HasSum NonUnitalNonAssocSemiring.toAddCommMonoid instTopologicalSpace SummationFilter.unconditional	—	summable_and_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 instSemiring instTopologicalSpace Real instPowReal SummationFilter.unconditional	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrder tsum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiring instTopologicalSpace Distrib.toMul NonUnitalNonAssocSemiring.toDistrib SummationFilter.unconditional Real instPowReal DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne	—	summable_and_inner_le_Lp_mul_Lq_tsum
inner_le_Lp_mul_Lq_tsum' 📖	mathematical	Real.HolderConjugate Summable NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiring instTopologicalSpace Real instPowReal SummationFilter.unconditional	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrder tsum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiring instTopologicalSpace Distrib.toMul NonUnitalNonAssocSemiring.toDistrib SummationFilter.unconditional Real instPowReal 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 instPartialOrder Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Real instPowReal Real.instSub Real.instOne Real.instInv	—	LE.le.eq_or_lt inv_one sub_self rpow_zero Finset.sum_congr rpow_one one_mul instReflLe 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 instPartialOrder Set.image Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib setOf Real instPowReal instOne DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne	—	eq_zero_or_pos 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 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 instPartialOrder Real instPowReal Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Finset.card Real.instSub Real.instOne	—	eq_or_lt_of_le rpow_one sub_self rpow_zero Finset.sum_congr one_mul instReflLe 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 instSemiring instTopologicalSpace instPowReal SummationFilter.unconditional	Summable NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiring instTopologicalSpace Real instPowReal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib SummationFilter.unconditional	—	Lp_add_le_tsum
summable_and_Lr_rpow_le_Lp_mul_Lq_tsum 📖	mathematical	Real.HolderTriple Summable NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiring instTopologicalSpace Real instPowReal SummationFilter.unconditional	Summable NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiring instTopologicalSpace Real instPowReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib SummationFilter.unconditional Preorder.toLE PartialOrder.toPreorder instPartialOrder tsum DivInvMonoid.toDiv Real.instDivInvMonoid	—	Real.HolderTriple.all_pos le_trans Lr_rpow_le_Lp_mul_Lq mul_le_mul IsOrderedRing.toPosMulMono IsOrderedRing.toMulPosMono rpow_le_rpow_iff div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Summable.sum_le_tsum IsOrderedRing.toIsOrderedAddMonoid OrderTopology.to_orderClosedTopology instOrderTopology SummationFilter.instNeBotUnconditional SummationFilter.instLeAtTopUnconditional zero_le bot_le HasSum.summable hasSum_of_isLUB isLUB_ciSup Summable.tsum_le_of_sum_le
summable_and_inner_le_Lp_mul_Lq_tsum 📖	mathematical	Real.HolderConjugate Summable NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiring instTopologicalSpace Real instPowReal SummationFilter.unconditional	Summable NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiring instTopologicalSpace Distrib.toMul NonUnitalNonAssocSemiring.toDistrib SummationFilter.unconditional Preorder.toLE PartialOrder.toPreorder instPartialOrder tsum Real instPowReal DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne	—	one_div rpow_one summable_and_Lr_rpow_le_Lp_mul_Lq_tsum
summable_mul_of_Lp_Lq 📖	mathematical	Real.HolderConjugate Summable NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiring instTopologicalSpace Real instPowReal SummationFilter.unconditional	Summable NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiring instTopologicalSpace Distrib.toMul NonUnitalNonAssocSemiring.toDistrib SummationFilter.unconditional	—	summable_and_inner_le_Lp_mul_Lq_tsum
summable_mul_rpow_of_Lp_Lq 📖	mathematical	Real.HolderTriple Summable NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiring instTopologicalSpace Real instPowReal SummationFilter.unconditional	Summable NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiring instTopologicalSpace Real instPowReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib SummationFilter.unconditional	—	summable_and_Lr_rpow_le_Lp_mul_Lq_tsum
young_inequality 📖	mathematical	HolderConjugate	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiring 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 instPartialOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiring 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	Real instLE instPow Finset.sum instAddCommMonoid abs lattice instAddGroup instAdd DivInvMonoid.toDiv instDivInvMonoid instOne	—	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	Real instLE instZero instAdd HasSum instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instPow SummationFilter.unconditional	—	CanLift.prf Pi.canLift NNReal.canLift NNReal.Lp_add_le_hasSum Nat.cast_zero zero_le
Lp_add_le_of_nonneg 📖	mathematical	Real instLE instOne instZero	Real instLE instPow Finset.sum instAddCommMonoid instAdd DivInvMonoid.toDiv instDivInvMonoid instOne	—	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	Summable Real instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instPow instAdd SummationFilter.unconditional instLE tsum DivInvMonoid.toDiv instDivInvMonoid instOne	—	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	Real instLE instPow tsum instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instAdd SummationFilter.unconditional DivInvMonoid.toDiv instDivInvMonoid instOne	—	Lp_add_le_tsum_of_nonneg
Lr_le_Lp_mul_Lq_tsum_of_nonneg 📖	mathematical	HolderTriple Real instLE instZero Summable instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instPow SummationFilter.unconditional	Real instLE instPow tsum instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instMul SummationFilter.unconditional DivInvMonoid.toDiv instDivInvMonoid instOne	—	tsum_nonneg instIsOrderedAddMonoid HasSolidNorm.orderClosedTopology instHasSolidNormReal rpow_nonneg HolderTriple.pos' mul_rpow rpow_mul Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one 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 div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_cons_eq_eval_of_eq_of_eq Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero ne_of_gt Mathlib.Tactic.FieldSimp.eq_div_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div' one_ne_zero NeZero.one GroupWithZero.toNontrivial rpow_le_rpow_iff mul_nonneg IsOrderedRing.toPosMulMono instIsOrderedRing inv_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing inv_eq_one_div Lr_rpow_le_Lp_mul_Lq_tsum_of_nonneg
Lr_rpow_le_Lp_mul_Lq 📖	mathematical	HolderTriple	Real instLE Finset.sum instAddCommMonoid instPow abs lattice instAddGroup instMul DivInvMonoid.toDiv instDivInvMonoid	—	Finset.sum_congr abs_mul instIsOrderedRing abs_nonneg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid covariant_swap_add_of_covariant_add NNReal.coe_sum NNReal.coe_le_coe NNReal.Lr_rpow_le_Lp_mul_Lq
Lr_rpow_le_Lp_mul_Lq_of_nonneg 📖	mathematical	HolderTriple Real instLE instZero	Real instLE Finset.sum instAddCommMonoid instPow instMul DivInvMonoid.toDiv instDivInvMonoid	—	Finset.sum_congr abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid mul_nonneg IsOrderedRing.toPosMulMono instIsOrderedRing Lr_rpow_le_Lp_mul_Lq
Lr_rpow_le_Lp_mul_Lq_tsum_of_nonneg 📖	mathematical	HolderTriple Real instLE instZero Summable instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instPow SummationFilter.unconditional	Real instLE tsum instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instPow instMul SummationFilter.unconditional DivInvMonoid.toDiv instDivInvMonoid	—	summable_and_Lr_rpow_le_Lp_mul_Lq_tsum_of_nonneg
arith_mean_weighted_of_constant 📖	mathematical	Finset.sum Real instAddCommMonoid instOne	Finset.sum Real instAddCommMonoid 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	Real instLE Finset.expect instAddCommMonoid Algebra.toModule NNRat instCommSemiringNNRat semiring DivisionSemiring.toNNRatAlgebra Semifield.toDivisionSemiring Field.toSemifield instField RCLike.charZero_rclike instRCLike instMul instPow instSub instOne 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 Real instCommMonoid instPow Finset.sum instAddCommMonoid 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 Real instCommMonoid instPow Finset.sum instAddCommMonoid 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 Real instCommMonoid instPow Finset.sum instAddCommMonoid instMul	—	geom_mean_weighted_of_constant arith_mean_weighted_of_constant
geom_mean_le_arith_mean 📖	mathematical	Real instLE instZero instLT Finset.sum instAddCommMonoid	Real instLE instPow Finset.prod instCommMonoid instInv Finset.sum instAddCommMonoid 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	Real instLE instMul instPow instAdd	—	NNReal.geom_mean_le_arith_mean2_weighted
geom_mean_le_arith_mean3_weighted 📖	mathematical	Real instLE instZero instAdd instOne	Real instLE instMul instPow instAdd	—	NNReal.geom_mean_le_arith_mean3_weighted
geom_mean_le_arith_mean4_weighted 📖	mathematical	Real instLE instZero instAdd instOne	Real instLE instMul instPow instAdd	—	NNReal.geom_mean_le_arith_mean4_weighted
geom_mean_le_arith_mean_weighted 📖	mathematical	Real instLE instZero Finset.sum instAddCommMonoid instOne	Real instLE Finset.prod instCommMonoid instPow Finset.sum instAddCommMonoid 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	Real instLT Finset.prod instCommMonoid instPow Finset.sum instAddCommMonoid instMul Finset SetLike.instMembership Finset.instSetLike	—	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 Real 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	Real instLE DivInvMonoid.toDiv instDivInvMonoid Finset.sum instAddCommMonoid 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	Real instLE instInv Finset.sum instAddCommMonoid 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 IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid 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	—	le_trans Finset.sum_le_sum IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid instIsOrderedRing one_div Finset.sum_congr abs_mul rpow_one Lr_rpow_le_Lp_mul_Lq
inner_le_Lp_mul_Lq_hasSum_of_nonneg 📖	mathematical	HolderConjugate Real instLE instZero HasSum instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instPow SummationFilter.unconditional	Real instLE instZero instMul HasSum instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace SummationFilter.unconditional	—	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	Real instLE 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_of_nonneg' 📖	mathematical	HolderConjugate Real instLE instZero	Real instLE Finset.sum instAddCommMonoid instMul instPow DivInvMonoid.toDiv instDivInvMonoid instOne	—	inner_le_Lp_mul_Lq_of_nonneg
inner_le_Lp_mul_Lq_tsum_of_nonneg 📖	mathematical	HolderConjugate Real instLE instZero Summable instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instPow SummationFilter.unconditional	Real instLE tsum instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instMul SummationFilter.unconditional instPow DivInvMonoid.toDiv instDivInvMonoid instOne	—	summable_and_inner_le_Lp_mul_Lq_tsum_of_nonneg
inner_le_weight_mul_Lp_of_nonneg 📖	mathematical	Real instLE instOne instZero	Real instLE Finset.sum instAddCommMonoid instMul instPow instSub instOne 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	Real instLE instPow Finset.sum instAddCommMonoid abs lattice instAddGroup instMul instNatCast Finset.card instSub instOne	—	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	Real instLE instPow Finset.sum instAddCommMonoid instMul instNatCast Finset.card instSub instOne	—	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	Summable Real instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instPow instAdd SummationFilter.unconditional	—	Lp_add_le_tsum_of_nonneg
summable_Lr_of_Lp_Lq_of_nonneg 📖	mathematical	HolderTriple Real instLE instZero Summable instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instPow SummationFilter.unconditional	Summable Real instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instPow instMul SummationFilter.unconditional	—	summable_and_Lr_rpow_le_Lp_mul_Lq_tsum_of_nonneg
summable_and_Lr_rpow_le_Lp_mul_Lq_tsum_of_nonneg 📖	mathematical	HolderTriple Real instLE instZero Summable instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instPow SummationFilter.unconditional	Summable Real instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instPow instMul SummationFilter.unconditional instLE tsum DivInvMonoid.toDiv instDivInvMonoid	—	CanLift.prf Pi.canLift NNReal.canLift NNReal.summable_and_Lr_rpow_le_Lp_mul_Lq_tsum
summable_and_inner_le_Lp_mul_Lq_tsum_of_nonneg 📖	mathematical	HolderConjugate Real instLE instZero Summable instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instPow SummationFilter.unconditional	Summable Real instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instMul SummationFilter.unconditional instLE tsum instPow DivInvMonoid.toDiv instDivInvMonoid instOne	—	one_div rpow_one summable_and_Lr_rpow_le_Lp_mul_Lq_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	Summable Real instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instMul SummationFilter.unconditional	—	summable_and_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	Real instLE 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