Documentation Verification Report

Holder

📁 Source: Mathlib/Data/ENNReal/Holder.lean

Statistics

Metric	Count
Definitions `HolderConjugate`, `HolderTriple`	2
Theorems `eq_top_iff_eq_one`, `instOneInfty`, `instTwoTwo`, `inv_add_inv_eq_one`, `lt_top_iff_one_lt`, `ne_top_iff_ne_one`, `ne_zero`, `one_le`, `one_sub_inv`, `pos`, `sub_one_mul_inv`, `unique`, `holderConjugate_div_div`, `instInfty`, `instZero`, `inv_add_inv_eq_inv`, `inv_eq`, `inv_inv_add_inv`, `inv_le_inv`, `inv_sub_inv_eq_inv`, `inv_sub_inv_eq_inv'`, `le`, `of`, `one_div_add_one_div`, `one_div_eq`, `unique`, `unique_of_ne_zero`, `holderConjugate_iff`, `holderTriple_iff`	29
Total	31

ENNReal

Definitions

Name	Category	Theorems
`HolderConjugate` 📖	MathDef	22 math math: `HolderConjugate.instOneInfty`, `HolderConjugate.toReal_iff`, `HolderConjugate.inv_one_sub_inv'`, `HolderConjugate.of_toNNReal`, `holderConjugate_coe_iff`, `HolderConjugate.symm`, `Real.HolderConjugate.ennrealOfReal`, `holderConjugate_iff`, `HolderConjugate.instConjExponentOfFactLeOfNat`, `HolderTriple.holderConjugate_div_div`, `HolderConjugate.instTwoTwo`, `HolderConjugate.one_sub_inv_inv`, `HolderConjugate.of_toReal`, `HolderConjugate.conjExponent`, `HolderConjugate.toNNReal_iff`, `NNReal.HolderConjugate.coe_ennreal`, `isConjExponent_comm`, `HolderConjugate.top_one`, `HolderConjugate.inv_inv`, `HolderConjugate.one_top`, `HolderConjugate.inv_one_sub_inv`, `isConjExponent_iff_eq_conjExponent`
`HolderTriple` 📖	CompData	12 math math: `holderTriple_coe_iff`, `HolderTriple.toNNReal_iff`, `holderTriple_iff`, `NNReal.HolderTriple.coe_ennreal`, `HolderTriple.of_toNNReal`, `HolderTriple.symm`, `HolderTriple.toReal_iff`, `HolderTriple.of_toReal`, `Real.HolderTriple.ennrealOfReal`, `HolderTriple.instZero`, `HolderTriple.instInfty`, `HolderTriple.of`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`holderConjugate_iff` 📖	mathematical	—	`HolderConjugate` `ENNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring` `instInv` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`inv_one`
`holderTriple_iff` 📖	mathematical	—	`HolderTriple` `ENNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring` `instInv`	—	—

ENNReal.HolderConjugate

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_top_iff_eq_one` 📖	mathematical	—	`Top.top` `ENNReal` `instTopENNReal` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`inv_inv` `one_sub_inv` `ENNReal.inv_top` `tsub_zero` `ENNReal.instOrderedSub` `inv_one` `symm` `tsub_self` `ENNReal.instCanonicallyOrderedAdd` `ENNReal.inv_zero`
`instOneInfty` 📖	mathematical	—	`ENNReal.HolderConjugate` `ENNReal` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Top.top` `instTopENNReal`	—	`ENNReal.HolderTriple.instInfty`
`instTwoTwo` 📖	mathematical	—	`ENNReal.HolderConjugate` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `two_mul` `ENNReal.mul_inv_cancel` `Mathlib.Meta.NormNum.isNat_eq_false` `ENNReal.instCharZero` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Nat.cast_zero` `inv_one`
`inv_add_inv_eq_one` 📖	mathematical	—	`ENNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instInv` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`ENNReal.HolderTriple.inv_add_inv_eq_inv` `inv_one`
`lt_top_iff_one_lt` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Top.top` `instTopENNReal` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`lt_top_iff_ne_top` `ne_top_iff_ne_one` `lt_iff_le_and_ne` `one_le` `symm`
`ne_top_iff_ne_one` 📖	—	—	—	—	`not_iff_not` `eq_top_iff_eq_one`
`ne_zero` 📖	—	—	—	—	`LT.lt.ne'` `pos`
`one_le` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`ENNReal.HolderTriple.le`
`one_sub_inv` 📖	mathematical	—	`ENNReal` `ENNReal.instSub` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `ENNReal.instInv`	—	`ENNReal.HolderTriple.inv_sub_inv_eq_inv` `symm` `one_ne_zero` `NeZero.charZero_one` `ENNReal.instCharZero` `inv_one`
`pos` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal`	—	`LT.lt.trans_le` `zero_lt_one` `IsOrderedRing.toZeroLEOneClass` `ENNReal.instIsOrderedRing` `NeZero.charZero_one` `ENNReal.instCharZero` `one_le`
`sub_one_mul_inv` 📖	mathematical	—	`ENNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instSub` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `ENNReal.instInv`	—	`LT.lt.ne'` `pos` `ENNReal.sub_mul` `IsOrderedRing.toZeroLEOneClass` `ENNReal.instIsOrderedRing` `NeZero.charZero_one` `ENNReal.instCharZero` `ENNReal.mul_inv_cancel` `one_mul` `one_sub_inv`
`unique` 📖	—	—	—	—	`ENNReal.HolderTriple.unique_of_ne_zero` `one_ne_zero` `NeZero.charZero_one` `ENNReal.instCharZero`

ENNReal.HolderTriple

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`holderConjugate_div_div` 📖	mathematical	—	`ENNReal.HolderConjugate` `ENNReal` `DivInvMonoid.toDiv` `ENNReal.instDivInvMonoid`	—	`ENNReal.inv_div` `div_eq_mul_inv` `mul_add` `Distrib.leftDistribClass` `inv_add_inv_eq_inv` `ENNReal.mul_inv_cancel` `inv_one`
`instInfty` 📖	mathematical	—	`ENNReal.HolderTriple` `Top.top` `ENNReal` `instTopENNReal`	—	`ENNReal.inv_top` `add_zero`
`instZero` 📖	mathematical	—	`ENNReal.HolderTriple` `ENNReal` `instZeroENNReal`	—	`ENNReal.inv_zero` `add_top`
`inv_add_inv_eq_inv` 📖	mathematical	—	`ENNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instInv`	—	—
`inv_eq` 📖	mathematical	—	`ENNReal` `ENNReal.instInv` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	—	`inv_add_inv_eq_inv`
`inv_inv_add_inv` 📖	mathematical	—	`ENNReal` `ENNReal.instInv` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	—	`inv_add_inv_eq_inv` `inv_inv`
`inv_le_inv` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ENNReal.instInv`	—	`le`
`inv_sub_inv_eq_inv` 📖	mathematical	—	`ENNReal` `ENNReal.instSub` `ENNReal.instInv`	—	`ENNReal.sub_eq_of_eq_add` `ne_of_lt` `inv_le_inv` `symm` `pos_iff_ne_zero` `ENNReal.instCanonicallyOrderedAdd` `inv_eq`
`inv_sub_inv_eq_inv'` 📖	mathematical	—	`ENNReal` `ENNReal.instSub` `ENNReal.instInv`	—	`eq_zero_or_pos` `ENNReal.instCanonicallyOrderedAdd` `inv_eq` `add_top` `ENNReal.inv_zero` `inv_sub_inv_eq_inv` `LT.lt.ne'`
`le` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder`	—	`inv_inv_add_inv` `inv_inv` `ENNReal.instCanonicallyOrderedAdd`
`of` 📖	mathematical	—	`ENNReal.HolderTriple` `ENNReal` `ENNReal.instInv` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	—	`inv_inv`
`one_div_add_one_div` 📖	mathematical	—	`ENNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `DivInvMonoid.toDiv` `ENNReal.instDivInvMonoid` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`one_div` `inv_add_inv_eq_inv`
`one_div_eq` 📖	mathematical	—	`ENNReal` `DivInvMonoid.toDiv` `ENNReal.instDivInvMonoid` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	—	`one_div_add_one_div`
`unique` 📖	—	—	—	—	`inv_eq`
`unique_of_ne_zero` 📖	—	—	—	—	`inv_sub_inv_eq_inv` `symm`

---

← Back to Index