Documentation Verification Report

TriangleInequality

📁 Source: Mathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean

Statistics

Metric	Count
Definitions `LpAddConst`	1
Theorems `LpAddConst_lt_top`, `LpAddConst_of_one_le`, `LpAddConst_zero`, `add`, `sub`, `eLpNorm'_add_le`, `eLpNorm'_add_le_of_le_one`, `eLpNorm'_sum_le`, `eLpNormEssSup_add_le`, `eLpNorm_add_le`, `eLpNorm_add_le'`, `eLpNorm_add_lt_top`, `eLpNorm_sub_le`, `eLpNorm_sub_le'`, `eLpNorm_sum_le`, `exists_Lp_half`, `memLp_finset_sum`, `memLp_finset_sum'`	18
Total	19

MeasureTheory

Definitions

Name	Category	Theorems
`LpAddConst` 📖	CompOp	5 math math: `LpAddConst_of_one_le`, `LpAddConst_lt_top`, `eLpNorm_sub_le'`, `eLpNorm_add_le'`, `LpAddConst_zero`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`LpAddConst_lt_top` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `LpAddConst` `Top.top` `instTopENNReal`	—	`LpAddConst.eq_1` `ENNReal.rpow_lt_top_of_nonneg` `one_div` `sub_nonneg` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `ENNReal.toReal_inv` `ENNReal.toReal_one` `ENNReal.toReal_mono` `LT.lt.ne'` `ENNReal.one_le_inv` `LT.lt.le` `ENNReal.ofNat_ne_top` `ENNReal.one_lt_top`
`LpAddConst_of_one_le` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	`LpAddConst`	—	`LpAddConst.eq_1` `lt_irrefl` `LT.lt.trans_le`
`LpAddConst_zero` 📖	mathematical	—	`LpAddConst` `ENNReal` `instZeroENNReal` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`LpAddConst.eq_1` `lt_irrefl`
`eLpNorm'_add_le` 📖	mathematical	`AEStronglyMeasurable` `Real` `Real.instLE` `Real.instOne`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `eLpNorm'` `ContinuousENorm.toENorm` `ESeminormedAddMonoid.toContinuousENorm` `Pi.instAdd` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `ESeminormedAddMonoid.toAddMonoid` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	—	`ENNReal.rpow_le_rpow` `lintegral_mono_fn'` `le_refl` `le_of_lt` `lt_of_lt_of_le` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `ENNReal.lintegral_Lp_add_le` `AEStronglyMeasurable.enorm`
`eLpNorm'_add_le_of_le_one` 📖	mathematical	`AEStronglyMeasurable` `Real` `Real.instLE` `Real.instZero` `Real.instOne`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `eLpNorm'` `ContinuousENorm.toENorm` `ESeminormedAddMonoid.toContinuousENorm` `Pi.instAdd` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `ESeminormedAddMonoid.toAddMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instPowReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `Real.instSub` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Distrib.toAdd`	—	`Nat.instAtLeastTwoHAddOfNat` `ENNReal.rpow_le_rpow` `lintegral_mono_fn'` `le_refl` `Mathlib.Meta.Positivity.div_nonneg_of_pos_of_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `ENNReal.lintegral_Lp_add_le_of_le_one` `AEStronglyMeasurable.enorm`
`eLpNorm'_sum_le` 📖	mathematical	`AEStronglyMeasurable` `Real` `Real.instLE` `Real.instOne`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `eLpNorm'` `ContinuousENorm.toENorm` `ESeminormedAddMonoid.toContinuousENorm` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `Finset.sum` `Pi.addCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENNReal.instAddCommMonoid`	—	`Finset.le_sum_of_subadditive_on_pred` `ENNReal.instIsOrderedAddMonoid` `Eq.le` `eLpNorm'_zero` `LT.lt.trans_le` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `eLpNorm'_add_le` `AEStronglyMeasurable.add`
`eLpNormEssSup_add_le` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `eLpNormEssSup` `ContinuousENorm.toENorm` `ESeminormedAddMonoid.toContinuousENorm` `Pi.instAdd` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `ESeminormedAddMonoid.toAddMonoid` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	—	`le_trans` `essSup_mono_ae` `Filter.Eventually.of_forall` `Measure.instOuterMeasureClass` `enorm_add_le` `ENNReal.essSup_add_le`
`eLpNorm_add_le` 📖	mathematical	`AEStronglyMeasurable` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	`eLpNorm` `ContinuousENorm.toENorm` `ESeminormedAddMonoid.toContinuousENorm` `Pi.instAdd` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `ESeminormedAddMonoid.toAddMonoid` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	—	`eLpNorm_exponent_zero` `add_zero` `eLpNorm_exponent_top` `ENNReal.toReal_one` `ENNReal.toReal_le_toReal` `ENNReal.one_ne_top` `eLpNorm_eq_eLpNorm'` `eLpNorm'_add_le`
`eLpNorm_add_le'` 📖	mathematical	`AEStronglyMeasurable`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `eLpNorm` `ContinuousENorm.toENorm` `ESeminormedAddMonoid.toContinuousENorm` `Pi.instAdd` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `ESeminormedAddMonoid.toAddMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `LpAddConst` `Distrib.toAdd`	—	`eq_or_ne` `eLpNorm_exponent_zero` `add_zero` `MulZeroClass.mul_zero` `lt_or_ge` `eLpNorm_eq_eLpNorm'` `LT.lt.ne` `LT.lt.trans` `ENNReal.one_lt_top` `Nat.instAtLeastTwoHAddOfNat` `Ne.bot_lt` `eLpNorm'_add_le_of_le_one` `ENNReal.toReal_nonneg` `ENNReal.toReal_mono` `ENNReal.one_ne_top` `LT.lt.le` `LpAddConst_of_one_le` `one_mul` `eLpNorm_add_le`
`eLpNorm_add_lt_top` 📖	mathematical	`MemLp` `ContinuousENorm.toENorm` `ESeminormedAddMonoid.toContinuousENorm`	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `eLpNorm` `Pi.instAdd` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `ESeminormedAddMonoid.toAddMonoid` `Top.top` `instTopENNReal`	—	`eLpNorm_add_le'` `MemLp.aestronglyMeasurable` `ENNReal.mul_lt_top` `LpAddConst_lt_top` `ENNReal.add_lt_top`
`eLpNorm_sub_le` 📖	mathematical	`AEStronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	`eLpNorm` `ContinuousENorm.toENorm` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `SeminormedAddGroup.toContinuousENorm` `Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	—	`LpAddConst_of_one_le` `one_mul` `eLpNorm_sub_le'`
`eLpNorm_sub_le'` 📖	mathematical	`AEStronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `eLpNorm` `ContinuousENorm.toENorm` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `SeminormedAddGroup.toContinuousENorm` `Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `LpAddConst` `Distrib.toAdd`	—	`sub_eq_add_neg` `eLpNorm_neg` `eLpNorm_add_le'` `AEStronglyMeasurable.neg` `IsTopologicalAddGroup.toContinuousNeg` `SeminormedAddCommGroup.toIsTopologicalAddGroup`
`eLpNorm_sum_le` 📖	mathematical	`AEStronglyMeasurable` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	`eLpNorm` `ContinuousENorm.toENorm` `ESeminormedAddMonoid.toContinuousENorm` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `Finset.sum` `Pi.addCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENNReal.instAddCommMonoid`	—	`Finset.le_sum_of_subadditive_on_pred` `ENNReal.instIsOrderedAddMonoid` `Eq.le` `eLpNorm_zero` `eLpNorm_add_le` `AEStronglyMeasurable.add`
`exists_Lp_half` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal` `eLpNorm` `ContinuousENorm.toENorm` `ESeminormedAddMonoid.toContinuousENorm` `Pi.instAdd` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `ESeminormedAddMonoid.toAddMonoid`	—	`Filter.Tendsto.mono_left` `ENNReal.Tendsto.const_mul` `Filter.Tendsto.add` `ENNReal.instContinuousAdd` `Filter.tendsto_id` `LT.lt.ne` `LpAddConst_lt_top` `nhdsWithin_le_nhds` `Filter.Eventually.exists` `ENNReal.nhdsGT_zero_neBot` `Filter.Eventually.and` `tendsto_order` `ENNReal.instOrderTopology` `add_zero` `MulZeroClass.mul_zero` `Ne.bot_lt` `self_mem_nhdsWithin` `eLpNorm_add_le'` `mul_le_mul_right` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add`
`memLp_finset_sum` 📖	mathematical	`MemLp` `ContinuousENorm.toENorm` `ESeminormedAddMonoid.toContinuousENorm` `ESeminormedAddCommMonoid.toESeminormedAddMonoid`	`Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid`	—	`Finset.induction_on` `Finset.sum_insert` `MemLp.add` `Finset.mem_insert_self` `Finset.mem_insert_of_mem`
`memLp_finset_sum'` 📖	mathematical	`MemLp` `ContinuousENorm.toENorm` `ESeminormedAddMonoid.toContinuousENorm` `ESeminormedAddCommMonoid.toESeminormedAddMonoid`	`Finset.sum` `Pi.addCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid`	—	`Finset.sum_apply` `memLp_finset_sum`

MeasureTheory.MemLp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`MeasureTheory.MemLp` `ContinuousENorm.toENorm` `ESeminormedAddMonoid.toContinuousENorm`	`Pi.instAdd` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `ESeminormedAddMonoid.toAddMonoid`	—	`MeasureTheory.AEStronglyMeasurable.add` `MeasureTheory.eLpNorm_add_lt_top`
`sub` 📖	mathematical	`MeasureTheory.MemLp` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toPseudoMetricSpace`	`Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`sub_eq_add_neg` `add` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `neg`

---

← Back to Index