Documentation Verification Report

SobolevInequality

📁 Source: Mathlib/Analysis/FunctionalSpaces/SobolevInequality.lean

Statistics

Metric	Count
Definitions `T`, `SNormLESNormFDerivOfEqConst`, `eLpNormLESNormFDerivOfEqInnerConst`, `eLpNormLESNormFDerivOfLeConst`, `eLpNormLESNormFDerivOneConst`, `lintegralPowLePowLIntegralFDerivConst`	6
Theorems `T_empty`, `T_insert_le_T_lmarginal_singleton`, `T_lmarginal_antitone`, `T_univ`, `SNormLESNormFDerivOfEqConst_def`, `eLpNormLESNormFDerivOfLeConst_def`, `eLpNormLESNormFDerivOneConst_def`, `eLpNorm_le_eLpNorm_fderiv`, `eLpNorm_le_eLpNorm_fderiv_of_eq`, `eLpNorm_le_eLpNorm_fderiv_of_eq_inner`, `eLpNorm_le_eLpNorm_fderiv_of_le`, `eLpNorm_le_eLpNorm_fderiv_one`, `lintegralPowLePowLIntegralFDerivConst_def`, `lintegral_mul_prod_lintegral_pow_le`, `lintegral_pow_le_pow_lintegral_fderiv`, `lintegral_pow_le_pow_lintegral_fderiv_aux`, `lintegral_prod_lintegral_pow_le`	17
Total	23

MeasureTheory

Definitions

Name	Category	Theorems
`SNormLESNormFDerivOfEqConst` 📖	CompOp	2 math math: `SNormLESNormFDerivOfEqConst_def`, `eLpNorm_le_eLpNorm_fderiv_of_eq`
`eLpNormLESNormFDerivOfEqInnerConst` 📖	CompOp	1 math math: `eLpNorm_le_eLpNorm_fderiv_of_eq_inner`
`eLpNormLESNormFDerivOfLeConst` 📖	CompOp	3 math math: `eLpNormLESNormFDerivOfLeConst_def`, `eLpNorm_le_eLpNorm_fderiv_of_le`, `eLpNorm_le_eLpNorm_fderiv`
`eLpNormLESNormFDerivOneConst` 📖	CompOp	2 math math: `eLpNorm_le_eLpNorm_fderiv_one`, `eLpNormLESNormFDerivOneConst_def`
`lintegralPowLePowLIntegralFDerivConst` 📖	CompOp	3 math math: `lintegral_pow_le_pow_lintegral_fderiv`, `lintegralPowLePowLIntegralFDerivConst_def`, `eLpNormLESNormFDerivOneConst_def`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`SNormLESNormFDerivOfEqConst_def` 📖	mathematical	—	`SNormLESNormFDerivOfEqConst`	—	`RingHomInvPair.ids` `fact_one_le_two_ennreal`
`eLpNormLESNormFDerivOfLeConst_def` 📖	mathematical	—	`eLpNormLESNormFDerivOfLeConst`	—	—
`eLpNormLESNormFDerivOneConst_def` 📖	mathematical	—	`eLpNormLESNormFDerivOneConst` `NNReal` `Real` `NNReal.instPowReal` `lintegralPowLePowLIntegralFDerivConst` `Real.instInv`	—	—
`eLpNorm_le_eLpNorm_fderiv` 📖	mathematical	`ContDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `WithTop` `ENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Set` `Set.instHasSubset` `Function.support` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instOneNNReal` `Preorder.toLT` `AddMonoidWithOne.toNatCast` `instSemiringNNReal` `Module.finrank` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `Bornology.IsBounded` `PseudoMetricSpace.toBornology`	`ENNReal` `ENNReal.instPartialOrder` `eLpNorm` `ContinuousENorm.toENorm` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `SeminormedAddGroup.toContinuousENorm` `ENNReal.ofNNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `ENNReal.instCommSemiring` `eLpNormLESNormFDerivOfLeConst` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.toSeminormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `fderiv`	—	`eLpNorm_le_eLpNorm_fderiv_of_le` `AddGroup.toOrderedSub` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `inv_nonneg_of_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Nat.cast_nonneg'` `Real.instZeroLEOneClass`
`eLpNorm_le_eLpNorm_fderiv_of_eq` 📖	mathematical	`ContDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `WithTop` `ENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `HasCompactSupport` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instOneNNReal` `Module.finrank` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `Real.instInv` `NNReal.toReal` `Real.instSub` `NNReal.instInv` `Real.instNatCast`	`ENNReal` `ENNReal.instPartialOrder` `eLpNorm` `ContinuousENorm.toENorm` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `SeminormedAddGroup.toContinuousENorm` `ENNReal.ofNNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `ENNReal.instCommSemiring` `SNormLESNormFDerivOfEqConst` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.toSeminormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `fderiv`	—	`RingHomInvPair.ids` `fact_one_le_two_ennreal` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `RingHomIsometric.ids` `ContDiff.comp` `ContinuousLinearEquiv.contDiff` `HasCompactSupport.comp_left` `ContinuousLinearEquiv.map_zero` `eLpNorm_le_eLpNorm_fderiv_of_eq_inner` `RingHomCompTriple.ids` `fderiv_comp` `ContinuousLinearEquiv.differentiableAt` `ContDiff.differentiable` `one_ne_zero` `NeZero.charZero_one` `WithTop.charZero` `ContinuousLinearMap.opNorm_comp_le` `ContinuousLinearEquiv.fderiv` `ContinuousLinearEquiv.symm_apply_apply` `eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul` `Filter.Eventually.of_forall` `Measure.instOuterMeasureClass` `ContinuousLinearMap.le_opNNNorm` `mul_assoc` `mul_le_mul_right` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid` `SNormLESNormFDerivOfEqConst_def`
`eLpNorm_le_eLpNorm_fderiv_of_eq_inner` 📖	mathematical	`ContDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `WithTop` `ENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `HasCompactSupport` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instOneNNReal` `Module.finrank` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `Real.instInv` `NNReal.toReal` `Real.instSub` `NNReal.instInv` `Real.instNatCast`	`ENNReal` `ENNReal.instPartialOrder` `eLpNorm` `ContinuousENorm.toENorm` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `SeminormedAddGroup.toContinuousENorm` `ENNReal.ofNNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `ENNReal.instCommSemiring` `eLpNormLESNormFDerivOfEqInnerConst` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.toSeminormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `fderiv`	—	`RingHomIsometric.ids` `eLpNorm_exponent_zero` `ENNReal.instCanonicallyOrderedAdd` `LT.lt.trans_eq` `NNReal.coe_lt_coe` `pos_iff_ne_zero` `NNReal.instCanonicallyOrderedAdd` `inv_ne_zero` `inv_lt_inv₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Nat.cast_zero` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `RCLike.charZero_rclike` `LT.lt.trans_le` `zero_lt_one` `NeZero.charZero_one` `NNReal.coe_le_coe` `sub_pos` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `NNReal.coe_inv` `Nat.one_lt_cast` `NNReal.addLeftMono` `LinearOrderedCommMonoidWithZero.toZeroLeOneClass` `IsStrictOrderedRing.toCharZero` `NNReal.instIsStrictOrderedRing` `LE.le.trans_lt` `NNReal.HolderConjugate.conjExponent` `Nat.cast_one` `LT.lt.le` `NNReal.HolderTriple.lt` `Real.HolderTriple.lt` `NNReal.HolderConjugate.coe` `LE.le.eq_or_lt` `inv_one` `NNReal.coe_natCast` `NNReal.coe_sub` `inv_div` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.subst_sub` `Mathlib.Tactic.FieldSimp.NF.one_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `ne_of_gt` `Nat.cast_pos'` `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.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `eLpNormLESNormFDerivOfEqInnerConst.congr_simp` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.eval_cons_eq_eval_of_eq_of_eq` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `Real.toNNReal_one` `eLpNorm_le_eLpNorm_fderiv_one` `Real.HolderConjugate.conjExponent` `LT.lt.ne'` `LT.lt.trans` `sub_ne_zero_of_ne` `one_div` `Real.HolderConjugate.one_sub_inv` `sub_sub_sub_cancel_left` `le_of_lt` `div_pos` `mul_pos` `Mathlib.Meta.Positivity.nnreal_coe_pos` `lt_of_lt_of_le` `Mathlib.Meta.Positivity.pos_of_isNat` `NNReal.instIsOrderedRing` `Mathlib.Meta.NormNum.isNat_ofNat` `one_lt_div` `mul_sub` `sub_lt_sub_iff_right` `lt_mul_iff_one_lt_left` `Real.HolderTriple.pos` `NNReal.coe_mul` `Real.HolderConjugate.conjugate_eq` `mul_inv_rev` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `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.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `eLpNorm_nnreal_eq_lintegral` `ENNReal.zero_rpow_of_pos` `Real.instIsOrderedRing` `Real.instNontrivial` `lt_of_le_of_ne'` `zero_le` `mul_nonneg` `IsOrderedRing.toPosMulMono` `ENNReal.instIsOrderedRing` `LT.lt.ne` `lintegral_rpow_enorm_lt_top_of_eLpNorm'_lt_top` `NNReal.coe_pos` `eLpNorm_nnreal_eq_eLpNorm'` `MemLp.eLpNorm_lt_top` `Continuous.memLp_of_hasCompactSupport` `Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `BorelSpace.opensMeasurable` `ContDiff.continuous` `ENNReal.rpow_pos` `ENNReal.rpow_ne_top_of_nonneg'` `ContDiff.norm_rpow` `HasCompactSupport.rpow_const` `HasCompactSupport.norm` `NNReal.HolderTriple.pos` `NNReal.HolderConjugate.symm` `ENNReal.rpow_mul` `Real.enorm_rpow_of_nonneg` `norm_nonneg` `lt_trans` `enorm_norm` `eLpNorm_one_eq_lintegral_enorm` `mul_assoc` `lintegral_const_mul` `Measurable.fun_comp` `Measurable.mul` `ENNReal.instMeasurableMul₂` `Measurable.fst` `measurable_id'` `Measurable.snd` `Continuous.measurable` `Prod.borelSpace` `ENNReal.borelSpace` `secondCountableTopologyEither_of_right` `ENNReal.instSecondCountableTopology` `Continuous.prodMk` `Continuous.comp'` `ENNReal.continuous_rpow_const` `ENNReal.continuous_coe` `Continuous.nnnorm` `Continuous.fderiv_one` `ContDiff.fun_comp` `ContDiff.snd` `contDiff_fun_id` `continuous_id'` `mul_le_mul_right` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid` `lintegral_mono_fn'` `le_refl` `enorm_fderiv_norm_rpow_le` `ContDiff.differentiable` `WithTop.charZero` `ENNReal.lintegral_mul_le_Lp_mul_Lq` `Real.HolderConjugate.symm` `AEMeasurable.pow_const` `ENNReal.hasMeasurablePow` `AEStronglyMeasurable.enorm` `Continuous.aestronglyMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `secondCountableTopologyEither_of_left` `secondCountable_of_proper` `FiniteDimensional.proper_real` `ENNReal.rpow_sub` `ENNReal.div_le_iff` `Real.coe_toNNReal'` `mul_eq_mul_left_iff` `IsDomain.toIsCancelMulZero` `Real.instIsDomain` `max_eq_left_iff`
`eLpNorm_le_eLpNorm_fderiv_of_le` 📖	mathematical	`ContDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `WithTop` `ENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Set` `Set.instHasSubset` `Function.support` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instOneNNReal` `Preorder.toLT` `AddMonoidWithOne.toNatCast` `instSemiringNNReal` `Module.finrank` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `Real.instLE` `Real.instSub` `NNReal.toReal` `NNReal.instInv` `Real.instInv` `Real.instNatCast` `Bornology.IsBounded` `PseudoMetricSpace.toBornology`	`ENNReal` `ENNReal.instPartialOrder` `eLpNorm` `ContinuousENorm.toENorm` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `SeminormedAddGroup.toContinuousENorm` `ENNReal.ofNNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `ENNReal.instCommSemiring` `eLpNormLESNormFDerivOfLeConst` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.toSeminormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `fderiv`	—	`RingHomIsometric.ids` `eLpNorm_exponent_zero` `eLpNormLESNormFDerivOfLeConst.congr_simp` `ENNReal.instCanonicallyOrderedAdd` `inv_inv` `NNReal.coe_sub` `inv_anti₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `NNReal.instIsStrictOrderedRing` `lt_of_lt_of_le` `Mathlib.Meta.Positivity.pos_of_isNat` `NNReal.instIsOrderedRing` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `le_of_lt` `NNReal.coe_natCast` `inv_le_inv₀` `NNReal.instCanonicallyOrderedAdd` `NNReal.instOrderedSub` `inv_strictAnti₀` `inv_pos_of_pos` `lt_of_le_of_ne'` `zero_le` `eLpNorm_restrict_eq_of_support_subset` `ENNReal.coe_rpow_of_nonneg` `one_div` `Nat.cast_zero` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `AddGroup.toOrderedSub` `ENNReal.coe_toNNReal` `LT.lt.ne` `Bornology.IsBounded.measure_lt_top` `FiniteDimensional.proper_real` `Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `Measure.restrict_apply` `Set.univ_inter` `eLpNorm_le_eLpNorm_mul_rpow_measure_univ` `Continuous.aestronglyMeasurable` `BorelSpace.opensMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `secondCountableTopologyEither_of_right` `secondCountable_of_proper` `ContDiff.continuous` `HasCompactSupport.of_support_subset_isCompact` `instR1Space` `TopologicalSpace.PseudoMetrizableSpace.regularSpace` `Bornology.IsBounded.isCompact_closure` `HasSubset.Subset.trans` `Set.instIsTransSubset` `subset_closure` `mul_le_mul_left` `covariant_swap_mul_of_covariant_mul` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid` `eLpNorm_le_eLpNorm_fderiv_of_eq` `NNReal.addLeftMono` `LinearOrderedCommMonoidWithZero.toZeroLeOneClass` `IsStrictOrderedRing.toCharZero` `LE.le.trans_lt` `eLpNormLESNormFDerivOfLeConst_def` `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`
`eLpNorm_le_eLpNorm_fderiv_one` 📖	mathematical	`ContDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `WithTop` `ENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `HasCompactSupport` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NNReal.HolderConjugate` `NNReal` `AddMonoidWithOne.toNatCast` `instSemiringNNReal` `Module.finrank` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `eLpNorm` `ContinuousENorm.toENorm` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `SeminormedAddGroup.toContinuousENorm` `ENNReal.ofNNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `ENNReal.instCommSemiring` `eLpNormLESNormFDerivOneConst` `NNReal.toReal` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.toSeminormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `fderiv` `instAddCommMonoidWithOneENNReal`	—	`Real.HolderTriple.pos` `Real.HolderConjugate.symm` `NNReal.HolderConjugate.coe` `RingHomIsometric.ids` `eLpNorm_one_eq_lintegral_enorm` `ENNReal.rpow_le_rpow_iff` `ENNReal.mul_rpow_of_nonneg` `LT.lt.le` `ENNReal.coe_rpow_of_nonneg` `eLpNormLESNormFDerivOneConst_def` `NNReal.rpow_mul` `eLpNorm_nnreal_pow_eq_lintegral` `LT.lt.ne'` `NNReal.HolderTriple.pos` `NNReal.HolderConjugate.symm` `inv_mul_cancel₀` `NNReal.rpow_one` `lintegral_pow_le_pow_lintegral_fderiv`
`lintegralPowLePowLIntegralFDerivConst_def` 📖	mathematical	—	`lintegralPowLePowLIntegralFDerivConst`	—	`RingHomInvPair.ids` `Real.instCompleteSpace`
`lintegral_mul_prod_lintegral_pow_le` 📖	mathematical	`SigmaFinite` `Real` `Real.instLE` `Real.instZero` `Real.instMul` `Real.instSub` `Real.instNatCast` `Fintype.card` `Real.instOne` `Measurable` `ENNReal` `MeasurableSpace.pi` `ENNReal.measurableSpace`	`Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `lintegral` `Measure.pi` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instPowReal` `Finset.prod` `CommSemiring.toCommMonoid` `Finset.univ` `Function.update` `Real.instAdd`	—	`isEmpty_or_nonempty` `lintegral_of_isEmpty` `zero_le` `ENNReal.instCanonicallyOrderedAdd` `Finset.empty_subset` `GridLines.T.congr_simp` `Finset.compl_univ` `lmarginal_empty` `GridLines.T_univ` `Finset.compl_empty` `lmarginal_univ` `GridLines.T_empty` `GridLines.T_lmarginal_antitone`
`lintegral_pow_le_pow_lintegral_fderiv` 📖	mathematical	`ContDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `WithTop` `ENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `HasCompactSupport` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Real.HolderConjugate` `Real.instNatCast` `Module.finrank` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `lintegral` `ENNReal.instPowReal` `ENorm.enorm` `ContinuousENorm.toENorm` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `SeminormedAddGroup.toContinuousENorm` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `ENNReal.instCommSemiring` `ENNReal.ofNNReal` `lintegralPowLePowLIntegralFDerivConst` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.toSeminormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `fderiv`	—	`RingHomIsometric.ids` `Fintype.card_fin` `Module.finrank_fintype_fun_eq_card` `commRing_strongRankCondition` `Real.instNontrivial` `RingHomInvPair.ids` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Pi.topologicalAddGroup` `instIsTopologicalAddGroupReal` `instContinuousSMulForall` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Real.instCompleteSpace` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Pi.t2Space` `FiniteDimensional.finiteDimensional_pi'` `Finite.of_fintype` `FiniteDimensional.rclike_to_real` `Real.HolderTriple.nonneg` `Real.HolderConjugate.symm` `ContinuousLinearEquiv.isAddHaarMeasure_map` `Pi.borelSpace` `instCountableFin` `instSecondCountableTopologyReal` `Real.borelSpace` `Measure.instIsAddHaarMeasureForallVolumeOfMeasurableAddOfSigmaFinite` `ContinuousAdd.measurableAdd` `IsTopologicalSemiring.toContinuousAdd` `Measure.IsAddHaarMeasure.sigmaFinite` `instIsAddHaarMeasureVolume` `SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `locallyCompact_of_proper` `instProperSpaceReal` `Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `Measure.IsAddHaarMeasure.toIsAddLeftInvariant` `Measure.addHaarScalarFactor_pos_of_isAddHaarMeasure` `IsScalarTower.right` `Measure.isAddLeftInvariant_eq_smul` `FiniteDimensional.proper_real` `secondCountable_of_proper` `LT.lt.ne'` `lintegralPowLePowLIntegralFDerivConst_def` `inv_mul_cancel_right₀` `NNReal.rpow_pos` `lintegral_smul_measure` `ContDiff.comp` `ContinuousLinearEquiv.contDiff` `HasCompactSupport.comp_homeomorph` `RingHomCompTriple.ids` `lintegral_map` `Measurable.pow_const` `ENNReal.hasMeasurablePow` `Measurable.coe_nnreal_ennreal` `Measurable.nnnorm` `BorelSpace.opensMeasurable` `Continuous.measurable` `ContDiff.continuous` `Pi.opensMeasurableSpace` `ContinuousLinearEquiv.continuous` `lintegral_pow_le_pow_lintegral_fderiv_aux` `fderiv_comp` `ContDiff.differentiable` `one_ne_zero` `NeZero.charZero_one` `WithTop.charZero` `ContinuousLinearEquiv.differentiableAt` `ENNReal.rpow_le_rpow` `lintegral_mono_fn'` `le_refl` `ContinuousLinearEquiv.fderiv` `ContinuousLinearMap.opENorm_comp_le` `lintegral_mul_const` `Measurable.fun_comp` `measurable_enorm` `ContinuousLinearMap.instBorelSpace` `Continuous.fderiv_one` `ContDiff.fun_comp` `ContDiff.snd` `contDiff_fun_id` `continuous_id'` `ContinuousMapClass.map_continuous` `ContinuousSemilinearMapClass.toContinuousMapClass` `ContinuousSemilinearEquivClass.continuousSemilinearMapClass` `ContinuousLinearEquiv.continuousSemilinearEquivClass` `mul_comm` `ENNReal.mul_rpow_of_nonneg` `enorm_eq_nnnorm` `ENNReal.coe_rpow_of_nonneg` `mul_assoc` `ENNReal.coe_rpow_of_ne_zero` `ENNReal.coe_mul` `ENNReal.mul_le_mul_iff_right` `ENNReal.coe_ne_top`
`lintegral_pow_le_pow_lintegral_fderiv_aux` 📖	mathematical	`Real.HolderConjugate` `Real` `Real.instNatCast` `Fintype.card` `ContDiff` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Pi.normedAddCommGroup` `Real.normedAddCommGroup` `Pi.normedSpace` `NontriviallyNormedField.toNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `WithTop` `ENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `HasCompactSupport` `Pi.topologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `lintegral` `MeasureSpace.toMeasurableSpace` `MeasureSpace.pi` `Real.measureSpace` `MeasureSpace.volume` `ENNReal.instPowReal` `ENorm.enorm` `ContinuousENorm.toENorm` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `AddCommGroup.toAddCommMonoid` `Pi.addCommGroup` `Real.instAddCommGroup` `SeminormedAddCommGroup.toPseudoMetricSpace` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `Real.instRing` `NormedSpace.toModule` `Real.normedField` `ContinuousLinearMap.toSeminormedAddCommGroup` `Pi.seminormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `fderiv`	—	`Nat.instAtLeastTwoHAddOfNat` `Nat.cast_one` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `RCLike.charZero_rclike` `Real.HolderTriple.lt` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `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_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Linarith.add_lt_of_le_of_neg` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `RingHomIsometric.ids` `ENNReal.rpow_mul` `Real.HolderConjugate.conjugate_eq` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.one_eq_eval` `Mathlib.Tactic.FieldSimp.subst_sub` `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` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.eval_cons_eq_eval_of_eq_of_eq` `Mathlib.Tactic.FieldSimp.eq_div_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div'` `Finset.prod_const` `Int.cast_one` `ENNReal.rpow_natCast` `lintegral_mono_fn'` `le_refl` `Finset.prod_le_prod` `IsOrderedRing.toZeroLEOneClass` `ENNReal.instIsOrderedRing` `IsOrderedRing.toPosMulMono` `zero_le` `ENNReal.instCanonicallyOrderedAdd` `ENNReal.rpow_le_rpow` `le_trans` `Function.update_eq_self` `HasCompactSupport.enorm_le_lintegral_Ici_deriv` `ContDiff.comp` `contDiff_update` `HasCompactSupport.comp_isClosedEmbedding` `isClosedEmbedding_update` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `Measure.restrict_le_self` `fderiv_comp_deriv` `Differentiable.differentiableAt` `ContDiff.differentiable` `one_ne_zero` `NeZero.charZero_one` `WithTop.charZero` `HasDerivAt.differentiableAt` `hasDerivAt_update` `Finite.of_fintype` `ContinuousLinearMap.le_opENorm` `deriv_update` `Pi.enorm_single` `enorm_one` `NormedDivisionRing.to_normOneClass` `mul_one` `le_of_lt` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `lt_of_lt_of_le` `lintegral_prod_lintegral_pow_le` `Measure.IsAddHaarMeasure.sigmaFinite` `instIsAddHaarMeasureVolume` `FiniteDimensional.rclike_to_real` `Real.borelSpace` `SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace` `instIsTopologicalAddGroupReal` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `instSecondCountableTopologyReal` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `locallyCompact_of_proper` `instProperSpaceReal` `Measurable.fun_comp` `measurable_enorm` `BorelSpace.opensMeasurable` `ContinuousLinearMap.instBorelSpace` `Continuous.measurable` `Pi.opensMeasurableSpace` `Finite.to_countable` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Continuous.fderiv_one` `ContDiff.fun_comp` `ContDiff.snd` `contDiff_fun_id` `continuous_id'`
`lintegral_prod_lintegral_pow_le` 📖	mathematical	`SigmaFinite` `Real.HolderConjugate` `Real` `Real.instNatCast` `Fintype.card` `Measurable` `ENNReal` `MeasurableSpace.pi` `ENNReal.measurableSpace`	`Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `lintegral` `Measure.pi` `Finset.prod` `CommSemiring.toCommMonoid` `ENNReal.instCommSemiring` `Finset.univ` `ENNReal.instPowReal` `Function.update` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `Real.instSub`	—	`Fintype.one_lt_card_iff_nontrivial` `Nat.cast_one` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `RCLike.charZero_rclike` `Real.HolderTriple.lt` `Fintype.one_lt_card` `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.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `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_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `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.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `le_of_lt` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `Mathlib.Tactic.FieldSimp.le_eq_cancel_le` `PosMulStrictMono.toPosMulMono` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.subst_sub` `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` `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.NF.mul_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `ne_of_gt` `zero_lt_one` `NeZero.one` `GroupWithZero.toNontrivial` `le_refl` `one_div` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `Mathlib.Tactic.FieldSimp.subst_add` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `one_ne_zero` `sub_add_cancel` `mul_comm` `Real.HolderConjugate.sub_one_mul_conj` `Finset.prod_congr` `Mathlib.Tactic.FieldSimp.NF.eval_cons_eq_eval_of_eq_of_eq` `sub_self` `ENNReal.rpow_zero` `lintegral_mul_prod_lintegral_pow_le`

MeasureTheory.GridLines

Definitions

Name	Category	Theorems
`T` 📖	CompOp	4 math math: `T_lmarginal_antitone`, `T_empty`, `T_univ`, `T_insert_le_T_lmarginal_singleton`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`T_empty` 📖	mathematical	—	`T` `Finset` `Finset.instEmptyCollection` `ENNReal` `Real` `ENNReal.instPowReal` `Real.instAdd` `Real.instOne`	—	`MeasureTheory.lmarginal.congr_simp` `CharP.cast_eq_zero` `CharP.ofCharZero` `RCLike.charZero_rclike` `zero_sub` `neg_mul` `one_mul` `sub_neg_eq_add` `mul_one` `MeasureTheory.lmarginal_empty`
`T_insert_le_T_lmarginal_singleton` 📖	mathematical	`MeasureTheory.SigmaFinite` `Real` `Real.instLE` `Real.instZero` `Real.instMul` `Real.instNatCast` `Finset.card` `Real.instOne` `Finset` `Finset.instMembership` `Measurable` `ENNReal` `MeasurableSpace.pi` `ENNReal.measurableSpace`	`Pi.hasLe` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `T` `Finset.instInsert` `MeasureTheory.lmarginal` `Finset.instSingleton`	—	`Finset.card_insert_of_notMem` `Nat.cast_add` `Nat.cast_one` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `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_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `MeasureTheory.lmarginal_insert'` `Finset.prod_apply` `Finset.prod_congr` `Measurable.mul` `ENNReal.instMeasurableMul₂` `Measurable.pow_const` `ENNReal.hasMeasurablePow` `Finset.measurable_fun_prod` `Measurable.lmarginal` `MeasureTheory.lmarginal_mono` `Measurable.comp` `measurable_update` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.mul_congr` `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.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Finset.prod_insert` `Mathlib.Tactic.RingNF.nat_rawCast_1` `pow_one` `mul_one` `Mathlib.Tactic.RingNF.mul_assoc_rev` `add_zero` `MeasureTheory.lmarginal_update_of_mem` `Finset.mem_singleton` `MeasureTheory.lintegral_const_mul` `mul_le_mul_right` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid` `ENNReal.lintegral_mul_prod_norm_pow_le` `Measurable.aemeasurable` `Finset.sum_const` `nsmul_eq_mul` `MeasureTheory.lmarginal_singleton` `MeasureTheory.lmarginal_insert` `ENNReal.rpow_add_of_nonneg` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `MeasureTheory.lmarginal_union` `Finset.disjoint_singleton` `Finset.union_comm` `le_refl`
`T_lmarginal_antitone` 📖	mathematical	`MeasureTheory.SigmaFinite` `Real` `Real.instLE` `Real.instZero` `Real.instMul` `Real.instSub` `Real.instNatCast` `Fintype.card` `Real.instOne` `Measurable` `ENNReal` `MeasurableSpace.pi` `ENNReal.measurableSpace`	`Antitone` `Finset` `PartialOrder.toPreorder` `Finset.partialOrder` `Pi.preorder` `ENNReal.instPartialOrder` `T` `MeasureTheory.lmarginal` `Compl.compl` `BooleanAlgebra.toCompl` `Finset.booleanAlgebra`	—	`Finset.antitone_iff_forall_insert_le` `MeasureTheory.lmarginal_union` `Finset.disjoint_singleton_left` `Finset.notMem_compl` `Finset.mem_insert_self` `Finset.insert_compl_insert` `T_insert_le_T_lmarginal_singleton` `le_trans` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `Finset.card_add_card_compl` `Nat.cast_one` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `RCLike.charZero_rclike` `add_le_add_right` `Nat.instIsOrderedAddMonoid` `Finset.mem_compl` `Finset.card_pos` `le_of_not_gt` `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.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `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_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Linarith.add_lt_of_le_of_neg` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Measurable.lmarginal`
`T_univ` 📖	mathematical	`MeasureTheory.SigmaFinite`	`T` `Finset.univ` `MeasureTheory.lintegral` `MeasurableSpace.pi` `MeasureTheory.Measure.pi` `ENNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `Real` `ENNReal.instPowReal` `Real.instSub` `Real.instOne` `Real.instMul` `Real.instNatCast` `Fintype.card` `Finset.prod` `CommSemiring.toCommMonoid` `Function.update`	—	`MeasureTheory.lmarginal.congr_simp` `Finset.prod_congr` `MeasureTheory.lmarginal_singleton` `MeasureTheory.lmarginal_univ` `Finset.prod_apply`

---

← Back to Index