Documentation Verification Report

MeanInequalities

📁 Source: Mathlib/MeasureTheory/Integral/MeanInequalities.lean

Statistics

Metric	Count
Definitions `funMulInvSnorm`	1
Theorems `ae_eq_zero_of_lintegral_rpow_eq_zero`, `funMulInvSnorm_rpow`, `fun_eq_funMulInvSnorm_mul_eLpNorm`, `lintegral_Lp_add_le`, `lintegral_Lp_add_le_of_le_one`, `lintegral_Lp_mul_le_Lq_mul_Lr`, `lintegral_mul_eq_zero_of_lintegral_rpow_eq_zero`, `lintegral_mul_le_Lp_mul_Lq`, `lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_eq_top`, `lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_ne_top`, `lintegral_mul_le_one_of_lintegral_rpow_eq_one`, `lintegral_mul_norm_pow_le`, `lintegral_mul_prod_norm_pow_le`, `lintegral_mul_rpow_le_lintegral_rpow_mul_lintegral_rpow`, `lintegral_prod_norm_pow_le`, `lintegral_rpow_add_le_add_eLpNorm_mul_lintegral_rpow_add`, `lintegral_rpow_add_lt_top_of_lintegral_rpow_lt_top`, `lintegral_rpow_funMulInvSnorm_eq_one`, `lintegral_mul_le_Lp_mul_Lq`	19
Total	20

ENNReal

Definitions

Name	Category	Theorems
`funMulInvSnorm` 📖	CompOp	3 math math: `lintegral_rpow_funMulInvSnorm_eq_one`, `funMulInvSnorm_rpow`, `fun_eq_funMulInvSnorm_mul_eLpNorm`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ae_eq_zero_of_lintegral_rpow_eq_zero` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `AEMeasurable` `ENNReal` `measurableSpace` `MeasureTheory.lintegral` `instPowReal` `instZeroENNReal`	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `Pi.instZero`	—	`Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.lintegral_eq_zero_iff'` `AEMeasurable.pow_const` `hasMeasurablePow` `Filter.univ_mem'` `Pi.zero_apply` `not_imp_not` `LT.lt.ne'` `rpow_pos_of_nonneg` `pos_iff_ne_zero` `instCanonicallyOrderedAdd`
`funMulInvSnorm_rpow` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`ENNReal` `instPowReal` `funMulInvSnorm` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring` `instInv` `MeasureTheory.lintegral`	—	`funMulInvSnorm.eq_1` `mul_rpow_of_nonneg` `le_of_lt` `inv_rpow` `rpow_mul` `one_div_mul_cancel` `LT.lt.ne'` `rpow_one`
`fun_eq_funMulInvSnorm_mul_eLpNorm` 📖	mathematical	—	`ENNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring` `funMulInvSnorm` `Real` `instPowReal` `MeasureTheory.lintegral` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne`	—	`one_div` `mul_assoc` `inv_mul_cancel` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `mul_one`
`lintegral_Lp_add_le` 📖	mathematical	`AEMeasurable` `ENNReal` `measurableSpace` `Real` `Real.instLE` `Real.instOne`	`Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instPowReal` `MeasureTheory.lintegral` `Pi.instAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring` `DivInvMonoid.toDiv` `Real.instDivInvMonoid`	—	`lt_of_lt_of_le` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `eq_top_or_lt_top` `one_div` `top_rpow_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `top_add` `add_top` `le_of_eq` `one_div_one` `rpow_one` `MeasureTheory.lintegral_add_left'` `lt_of_le_of_ne` `Real.HolderConjugate.conjExponent` `zero_rpow_of_pos` `zero_le` `instCanonicallyOrderedAdd` `LT.lt.ne` `lintegral_rpow_add_lt_top_of_lintegral_rpow_lt_top`
`lintegral_Lp_add_le_of_le_one` 📖	mathematical	`AEMeasurable` `ENNReal` `measurableSpace` `Real` `Real.instLE` `Real.instZero` `Real.instOne`	`Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instPowReal` `MeasureTheory.lintegral` `Pi.instAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Distrib.toMul` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `Real.instSub`	—	`Nat.instAtLeastTwoHAddOfNat` `eq_or_lt_of_le` `rpow_zero` `MeasureTheory.lintegral_one` `div_zero` `zero_sub` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `rpow_neg` `rpow_one` `inv_mul_cancel` `two_ne_zero` `CharZero.NeZero.two` `instCharZero` `ofNat_ne_top` `le_refl` `MeasureTheory.lintegral_add_left'` `AEMeasurable.pow_const` `hasMeasurablePow` `rpow_le_rpow` `MeasureTheory.lintegral_mono_fn'` `rpow_add_le_add_rpow` `le_of_lt` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `rpow_add_le_mul_rpow_add_rpow` `one_le_div`
`lintegral_Lp_mul_le_Lq_mul_Lr` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `Real.instAdd` `AEMeasurable` `ENNReal` `measurableSpace`	`Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instPowReal` `MeasureTheory.lintegral` `Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring`	—	`ne_of_lt` `le_of_lt` `lt_of_le_of_lt` `one_div` `add_sub_cancel_left` `Real.HolderConjugate.conjExponent` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `one_mul` `mul_rpow_of_nonneg` `rpow_le_rpow` `rpow_mul` `lintegral_mul_le_Lp_mul_Lq` `AEMeasurable.pow_const` `hasMeasurablePow` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `mul_comm` `div_eq_iff` `inv_inv` `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.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.subst_sub` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `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.one_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `Mathlib.Tactic.FieldSimp.eq_div_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div'` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `div_mul_div_comm`
`lintegral_mul_eq_zero_of_lintegral_rpow_eq_zero` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `AEMeasurable` `ENNReal` `measurableSpace` `MeasureTheory.lintegral` `instPowReal` `instZeroENNReal`	`Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring`	—	`MeasureTheory.lintegral_zero_fun` `MeasureTheory.lintegral_congr_ae` `MeasureTheory.Measure.instOuterMeasureClass` `ae_eq_zero_of_lintegral_rpow_eq_zero` `Filter.EventuallyEq.mul` `MeasureTheory.ae_eq_refl` `MulZeroClass.zero_mul`
`lintegral_mul_le_Lp_mul_Lq` 📖	mathematical	`Real.HolderConjugate` `AEMeasurable` `ENNReal` `measurableSpace`	`Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `MeasureTheory.lintegral` `Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring` `Real` `instPowReal` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne`	—	`Eq.trans_le` `lintegral_mul_eq_zero_of_lintegral_rpow_eq_zero` `Real.HolderTriple.nonneg` `zero_le` `instCanonicallyOrderedAdd` `mul_comm` `Real.HolderConjugate.symm` `lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_eq_top` `Real.HolderTriple.pos` `lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_ne_top`
`lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_eq_top` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Real.instLE` `MeasureTheory.lintegral` `ENNReal` `instPowReal` `Top.top` `instTopENNReal`	`Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne`	—	`one_div` `top_rpow_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `top_mul` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing`
`lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_ne_top` 📖	mathematical	`Real.HolderConjugate` `AEMeasurable` `ENNReal` `measurableSpace`	`Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `MeasureTheory.lintegral` `Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring` `Real` `instPowReal` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne`	—	`MeasureTheory.lintegral_congr` `Pi.mul_apply` `fun_eq_funMulInvSnorm_mul_eLpNorm` `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` `MeasureTheory.lintegral_mul_const'` `one_div` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `mul_le_of_le_one_left'` `covariant_swap_mul_of_covariant_mul` `IsOrderedMonoid.toMulLeftMono` `instIsOrderedMonoid` `lintegral_rpow_funMulInvSnorm_eq_one` `Real.HolderTriple.pos` `Real.HolderConjugate.symm` `lintegral_mul_le_one_of_lintegral_rpow_eq_one` `AEMeasurable.mul_const` `MeasurableMul₂.toMeasurableMul` `instMeasurableMul₂`
`lintegral_mul_le_one_of_lintegral_rpow_eq_one` 📖	mathematical	`Real.HolderConjugate` `AEMeasurable` `ENNReal` `measurableSpace` `MeasureTheory.lintegral` `Real` `instPowReal` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	`Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring`	—	`MeasureTheory.lintegral_mono` `young_inequality` `div_eq_mul_inv` `MeasureTheory.lintegral_add_left'` `AEMeasurable.mul_const` `MeasurableMul₂.toMeasurableMul` `instMeasurableMul₂` `AEMeasurable.pow_const` `hasMeasurablePow` `MeasureTheory.lintegral_mul_const''` `MeasureTheory.lintegral_mul_const'` `Real.HolderTriple.pos` `Real.HolderConjugate.symm` `one_mul` `Real.HolderConjugate.inv_add_inv_ennreal`
`lintegral_mul_norm_pow_le` 📖	mathematical	`AEMeasurable` `ENNReal` `measurableSpace` `Real` `Real.instLE` `Real.instZero` `Real.instAdd` `Real.instOne`	`Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `MeasureTheory.lintegral` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring` `instPowReal`	—	`LE.le.eq_or_lt` `rpow_zero` `zero_add` `rpow_one` `one_mul` `add_zero` `mul_one` `one_div` `one_lt_inv₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `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.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Mathlib.Tactic.Linarith.lt_of_eq_of_lt` `sub_eq_zero_of_eq` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `inv_inv` `lintegral_mul_le_Lp_mul_Lq` `Real.holderConjugate_iff` `AEMeasurable.pow_const` `hasMeasurablePow` `mul_inv_cancel₀` `LT.lt.ne'` `div_inv_eq_mul`
`lintegral_mul_prod_norm_pow_le` 📖	mathematical	`AEMeasurable` `ENNReal` `measurableSpace` `Real` `Real.instAdd` `Finset.sum` `Real.instAddCommMonoid` `Real.instOne` `Real.instLE` `Real.instZero`	`Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `MeasureTheory.lintegral` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring` `instPowReal` `Finset.prod` `CommSemiring.toCommMonoid`	—	`lintegral_prod_norm_pow_le` `Finset.sum_insertNone` `Finset.sum_congr` `Finset.prod_insertNone` `Finset.prod_congr`
`lintegral_mul_rpow_le_lintegral_rpow_mul_lintegral_rpow` 📖	mathematical	`Real.HolderConjugate` `AEMeasurable` `ENNReal` `measurableSpace`	`Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `MeasureTheory.lintegral` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring` `Real` `instPowReal` `Real.instSub` `Real.instOne` `DivInvMonoid.toDiv` `Real.instDivInvMonoid`	—	`LE.le.trans_eq` `lintegral_mul_le_Lp_mul_Lq` `AEMeasurable.pow_const` `hasMeasurablePow` `one_div` `Real.HolderConjugate.sub_one_mul_conj`
`lintegral_prod_norm_pow_le` 📖	mathematical	`AEMeasurable` `ENNReal` `measurableSpace` `Finset.sum` `Real` `Real.instAddCommMonoid` `Real.instOne` `Real.instLE` `Real.instZero`	`Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `MeasureTheory.lintegral` `Finset.prod` `CommSemiring.toCommMonoid` `instCommSemiring` `instPowReal`	—	`Finset.induction` `NeZero.charZero_one` `RCLike.charZero_rclike` `eq_or_ne` `Finset.prod_insert` `Finset.sum_insert` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Finset.sum_eq_zero_iff_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Finset.mem_insert_of_mem` `Finset.prod_congr` `rpow_zero` `rpow_one` `Finset.prod_const_one` `mul_one` `covariant_swap_add_of_covariant_add` `Finset.single_le_sum` `Finset.mem_insert_self` `sub_ne_zero` `Finset.sum_div` `Finset.sum_insert_sub` `div_self` `div_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `prod_rpow_of_nonneg` `div_mul_cancel₀` `lintegral_mul_norm_pow_le` `Finset.aemeasurable_fun_prod` `instMeasurableMul₂` `AEMeasurable.pow_const` `hasMeasurablePow` `add_sub_cancel` `mul_le_mul_right` `IsOrderedMonoid.toMulLeftMono` `instIsOrderedMonoid` `rpow_le_rpow` `le_of_lt` `lt_of_le_of_ne'`
`lintegral_rpow_add_le_add_eLpNorm_mul_lintegral_rpow_add` 📖	mathematical	`Real.HolderConjugate` `AEMeasurable` `ENNReal` `measurableSpace`	`Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `MeasureTheory.lintegral` `Real` `instPowReal` `Pi.instAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring` `Distrib.toMul` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne`	—	`MeasureTheory.lintegral_mono_fn'` `le_refl` `zero_rpow_of_pos` `Real.HolderTriple.pos` `zero_le` `instCanonicallyOrderedAdd` `top_rpow_of_pos` `Real.HolderConjugate.sub_one_pos` `top_mul_top` `le_top` `le_of_eq` `rpow_one` `rpow_add` `add_sub_cancel` `AEMeasurable.pow_const` `hasMeasurablePow` `AEMeasurable.add` `ContinuousAdd.measurableMul₂` `borelSpace` `instSecondCountableTopology` `instContinuousAdd` `add_mul` `Distrib.rightDistribClass` `MeasureTheory.lintegral_add_left'` `AEMeasurable.mul` `instMeasurableMul₂` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `lintegral_mul_rpow_le_lintegral_rpow_mul_lintegral_rpow`
`lintegral_rpow_add_lt_top_of_lintegral_rpow_lt_top` 📖	mathematical	`AEMeasurable` `ENNReal` `measurableSpace` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `MeasureTheory.lintegral` `Real` `instPowReal` `Top.top` `instTopENNReal` `Real.instLE` `Real.instOne`	`Pi.instAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring`	—	`lt_of_lt_of_le` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `le_of_lt` `Nat.instAtLeastTwoHAddOfNat` `MeasureTheory.lintegral_mono` `zero_rpow_of_pos` `rpow_lt_rpow` `one_div` `sub_eq_add_neg` `rpow_add` `two_ne_zero` `CharZero.NeZero.two` `instCharZero` `coe_ne_top` `mul_assoc` `mul_rpow_of_nonneg` `inv_mul_cancel` `one_rpow` `one_mul` `rpow_neg_one` `mul_le_mul_iff_right` `LT.lt.ne'` `rpow_ne_top_of_nonneg` `div_ne_top` `one_ne_top` `ne_of_gt` `Mathlib.Meta.Positivity.pos_of_isNat` `instIsOrderedRing` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `mul_add` `Distrib.leftDistribClass` `rpow_arith_mean_le_arith_mean2_rpow` `div_add_div_same` `one_add_one_eq_two` `div_self` `MeasureTheory.lintegral_add_left'` `AEMeasurable.const_mul` `MeasurableMul₂.toMeasurableMul` `instMeasurableMul₂` `AEMeasurable.pow_const` `hasMeasurablePow` `MeasureTheory.lintegral_const_mul''` `MeasureTheory.lintegral_const_mul'` `rpow_ne_top_of_nonneg'` `ofNat_ne_top` `add_lt_top` `Ne.lt_top` `mul_ne_top` `rpow_ne_top_of_ne_zero` `ne_top_of_lt`
`lintegral_rpow_funMulInvSnorm_eq_one` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`MeasureTheory.lintegral` `ENNReal` `instPowReal` `funMulInvSnorm` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`funMulInvSnorm_rpow` `MeasureTheory.lintegral_mul_const'` `inv_ne_top` `mul_inv_cancel`

NNReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lintegral_mul_le_Lp_mul_Lq` 📖	mathematical	`Real.HolderConjugate` `AEMeasurable` `NNReal` `measurableSpace`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `MeasureTheory.lintegral` `ENNReal.ofNNReal` `Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `Real` `ENNReal.instPowReal` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne`	—	`ENNReal.lintegral_mul_le_Lp_mul_Lq` `AEMeasurable.coe_nnreal_ennreal`

---

← Back to Index