ConjExponents

📁 Source: Mathlib/Data/Real/ConjExponents.lean

Statistics

Metric	Count
Definitions `conjExponent`, `HolderConjugate`, `HolderTriple`, `conjExponent`, `HolderConjugate`, `HolderTriple`, `conjExponent`	7
Theorems `conjExponent`, `conjExponent_eq`, `conj_eq`, `div_conj_eq_sub_one`, `instConjExponentOfFactLeOfNat`, `inv_inv`, `inv_one_sub_inv`, `inv_one_sub_inv'`, `mul_eq_add`, `of_toNNReal`, `of_toReal`, `one_sub_inv_inv`, `one_top`, `toNNReal`, `toNNReal_iff`, `toReal`, `toReal_iff`, `top_one`, `of_toNNReal`, `of_toReal`, `toNNReal`, `toNNReal_iff`, `toReal`, `toReal_iff`, `coe_conjExponent`, `holderConjugate_coe_iff`, `holderTriple_coe_iff`, `isConjExponent_comm`, `isConjExponent_iff_eq_conjExponent`, `coe_ennreal`, `conjExponent`, `conjExponent_eq`, `conjugate_eq`, `div_conj_eq_sub_one`, `inv_add_inv_ennreal`, `inv_add_inv_eq_one`, `inv_inv`, `inv_one_sub_inv`, `mul_eq_add`, `one_sub_inv`, `one_sub_inv_inv`, `sub_one_mul_conj`, `sub_one_ne_zero`, `sub_one_pos`, `two_two`, `coe_ennreal`, `holderConjugate_div_div`, `inv_add_inv_eq_inv`, `inv_eq`, `inv_inv_add_inv`, `inv_lt_inv`, `inv_ne_zero`, `inv_ne_zero'`, `inv_nonneg`, `inv_nonneg'`, `inv_pos`, `inv_pos'`, `inv_sub_inv_eq_inv`, `left_pos`, `lt`, `ne_zero`, `ne_zero'`, `nonneg`, `nonneg'`, `of_pos`, `one_div_add_one_div`, `one_div_eq`, `one_div_ne_zero`, `one_div_ne_zero'`, `one_div_nonneg`, `one_div_nonneg'`, `one_div_pos`, `one_div_pos'`, `pos`, `pos'`, `right_pos`, `holderConjugate_coe_iff`, `holderConjugate_comm`, `holderConjugate_iff`, `holderConjugate_iff_eq_conjExponent`, `holderConjugate_one_div`, `holderTriple_coe_iff`, `holderTriple_iff`, `conjExponent`, `conjExponent_eq`, `conjugate_eq`, `div_conj_eq_sub_one`, `ennrealOfReal`, `inv_add_inv_ennreal`, `inv_add_inv_eq_one`, `inv_inv`, `inv_one_sub_inv`, `inv_sub_one`, `mul_eq_add`, `one_sub_inv`, `one_sub_inv_inv`, `sub_one_mul_conj`, `sub_one_ne_zero`, `sub_one_pos`, `toNNReal`, `two_two`, `ennrealOfReal`, `holderConjugate_div_div`, `inv_add_inv_eq_inv`, `inv_eq`, `inv_inv_add_inv`, `inv_lt_inv`, `inv_ne_zero`, `inv_ne_zero'`, `inv_nonneg`, `inv_nonneg'`, `inv_pos`, `inv_pos'`, `inv_sub_inv_eq_inv`, `left_pos`, `lt`, `ne_zero`, `ne_zero'`, `nonneg`, `nonneg'`, `of_pos`, `one_div_add_one_div`, `one_div_eq`, `one_div_ne_zero`, `one_div_ne_zero'`, `one_div_nonneg`, `one_div_nonneg'`, `one_div_pos`, `one_div_pos'`, `pos`, `pos'`, `right_pos`, `toNNReal`, `holderConjugate_comm`, `holderConjugate_iff`, `holderConjugate_iff_eq_conjExponent`, `holderConjugate_one_div`, `holderTriple_iff`	138
Total	145

ENNReal

Definitions

Name	Category	Theorems
`conjExponent` 📖	CompOp	4 math math: `HolderConjugate.instConjExponentOfFactLeOfNat`, `HolderConjugate.conjExponent`, `coe_conjExponent`, `HolderConjugate.conjExponent_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_conjExponent` 📖	mathematical	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instOneNNReal`	`ofNNReal` `NNReal.conjExponent` `conjExponent`	—	`NNReal.conjExponent.eq_1` `conjExponent.eq_1` `Nat.cast_one` `coe_inv` `LT.lt.ne'` `tsub_pos_of_lt` `NNReal.instCanonicallyOrderedAdd` `NNReal.instOrderedSub` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_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` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.subst_add` `Mathlib.Tactic.FieldSimp.NF.one_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `tsub_add_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `NNReal.addLeftMono` `LT.lt.le`
`holderConjugate_coe_iff` 📖	mathematical	—	`HolderConjugate` `ofNNReal` `NNReal.HolderConjugate`	—	`holderTriple_coe_iff` `one_ne_zero` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `NNReal.instIsStrictOrderedRing`
`holderTriple_coe_iff` 📖	mathematical	—	`HolderTriple` `ofNNReal` `NNReal.HolderTriple`	—	`NNReal.holderTriple_iff` `Nat.cast_zero` `HolderTriple.unique` `coe_zero` `HolderTriple.symm` `HolderTriple.instZero` `HolderTriple.inv_add_inv_eq_inv` `Ne.bot_lt` `holderTriple_iff` `NNReal.HolderTriple.ne_zero` `NNReal.HolderTriple.symm` `NNReal.HolderTriple.inv_add_inv_eq_inv`
`isConjExponent_comm` 📖	mathematical	—	`HolderConjugate`	—	`HolderConjugate.symm`
`isConjExponent_iff_eq_conjExponent` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	`HolderConjugate` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring` `instInv` `instSub`	—	`HolderConjugate.conj_eq` `HolderConjugate.conjExponent`

ENNReal.HolderConjugate

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`conjExponent` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	`ENNReal.HolderConjugate` `ENNReal.conjExponent`	—	`LT.lt.ne'` `LT.lt.trans_le` `zero_lt_one` `IsOrderedRing.toZeroLEOneClass` `ENNReal.instIsOrderedRing` `NeZero.charZero_one` `ENNReal.instCharZero` `eq_1` `ENNReal.holderTriple_iff` `ENNReal.conjExponent.eq_1` `add_comm` `AddLECancellable.eq_tsub_iff_add_eq_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `ENNReal.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `ENNReal.instOrderedSub` `inv_one` `inv_eq_iff_eq_inv` `LE.le.eq_or_lt` `tsub_self` `ENNReal.inv_zero` `add_top` `eq_or_ne` `ENNReal.top_sub` `ENNReal.inv_top` `add_zero` `tsub_zero` `ENNReal.add_div` `ENNReal.div_self` `tsub_pos_of_lt` `ENNReal.sub_ne_top` `one_div` `tsub_add_cancel_of_le` `div_eq_mul_inv` `ENNReal.mul_inv` `inv_inv` `ENNReal.mul_sub` `ENNReal.inv_mul_cancel` `mul_one`
`conjExponent_eq` 📖	mathematical	—	`ENNReal.conjExponent`	—	`one_le` `unique` `instConjExponentOfFactLeOfNat`
`conj_eq` 📖	mathematical	—	`ENNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `ENNReal.instInv` `ENNReal.instSub`	—	`conjExponent_eq`
`div_conj_eq_sub_one` 📖	mathematical	—	`ENNReal` `DivInvMonoid.toDiv` `ENNReal.instDivInvMonoid` `ENNReal.instSub` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`eq_or_ne` `one_div` `ENNReal.inv_top` `tsub_self` `ENNReal.instCanonicallyOrderedAdd` `ENNReal.instOrderedSub` `unique` `symm` `instOneInfty` `ENNReal.eq_sub_of_add_eq` `ENNReal.one_ne_top` `ENNReal.div_self` `ne_zero` `ENNReal.add_div` `mul_eq_add` `mul_div_assoc` `mul_one`
`instConjExponentOfFactLeOfNat` 📖	mathematical	—	`ENNReal.HolderConjugate` `ENNReal.conjExponent`	—	`conjExponent` `Fact.out`
`inv_inv` 📖	mathematical	`ENNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	`ENNReal.HolderConjugate` `ENNReal.instInv`	—	`inv_inv` `inv_one`
`inv_one_sub_inv` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	`ENNReal.HolderConjugate` `ENNReal.instInv` `ENNReal.instSub`	—	`inv_inv` `add_tsub_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `ENNReal.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `ENNReal.instOrderedSub`
`inv_one_sub_inv'` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	`ENNReal.HolderConjugate` `ENNReal.instInv` `ENNReal.instSub`	—	`inv_inv` `inv_one_sub_inv` `ENNReal.inv_le_one`
`mul_eq_add` 📖	mathematical	—	`ENNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `Distrib.toAdd`	—	`eq_or_ne` `ENNReal.top_mul` `ne_zero` `symm` `top_add` `ENNReal.mul_top` `add_top` `add_comm` `mul_one` `mul_add` `Distrib.leftDistribClass` `ENNReal.mul_inv_cancel` `add_mul` `Distrib.rightDistribClass` `one_mul` `ENNReal.inv_mul_cancel_right` `inv_add_inv_eq_one`
`of_toNNReal` 📖	mathematical	`NNReal.HolderConjugate` `ENNReal.toNNReal`	`ENNReal.HolderConjugate`	—	`of_toReal` `NNReal.HolderConjugate.coe`
`of_toReal` 📖	mathematical	`Real.HolderConjugate` `ENNReal.toReal`	`ENNReal.HolderConjugate`	—	`ENNReal.HolderTriple.of_toReal` `Real.HolderConjugate.eq_1` `ENNReal.toReal_one`
`one_sub_inv_inv` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	`ENNReal.HolderConjugate` `ENNReal.instInv` `ENNReal.instSub`	—	`symm` `inv_one_sub_inv`
`one_top` 📖	mathematical	—	`ENNReal.HolderConjugate` `ENNReal` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Top.top` `instTopENNReal`	—	`inv_one` `ENNReal.inv_top` `add_zero`
`toNNReal` 📖	mathematical	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instOneNNReal` `ENNReal.toNNReal`	`NNReal.HolderConjugate`	—	`toNNReal_iff`
`toNNReal_iff` 📖	mathematical	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instOneNNReal` `ENNReal.toNNReal`	`NNReal.HolderConjugate` `ENNReal.HolderConjugate`	—	`toReal_iff`
`toReal` 📖	mathematical	`Real` `Real.instLT` `Real.instOne` `ENNReal.toReal`	`Real.HolderConjugate`	—	`toReal_iff`
`toReal_iff` 📖	mathematical	`Real` `Real.instLT` `Real.instOne` `ENNReal.toReal`	`Real.HolderConjugate` `ENNReal.HolderConjugate`	—	`of_toReal` `ENNReal.toReal_pos_iff` `pos` `symm` `lt_top_iff_one_lt` `Mathlib.Tactic.Contrapose.contrapose₁` `ENNReal.toReal_mono` `ENNReal.one_ne_top` `ENNReal.HolderTriple.toReal` `LT.lt.trans` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing`
`top_one` 📖	mathematical	—	`ENNReal.HolderConjugate` `Top.top` `ENNReal` `instTopENNReal` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`ENNReal.inv_top` `inv_one` `zero_add`

ENNReal.HolderTriple

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_toNNReal` 📖	mathematical	`NNReal.HolderTriple` `ENNReal.toNNReal`	`ENNReal.HolderTriple`	—	`of_toReal` `NNReal.HolderTriple.coe`
`of_toReal` 📖	mathematical	`Real.HolderTriple` `ENNReal.toReal`	`ENNReal.HolderTriple`	—	`Real.HolderTriple.pos` `Real.HolderTriple.symm` `Real.HolderTriple.pos'` `ENNReal.ofReal_toReal` `LT.lt.ne` `ENNReal.toReal_pos_iff` `Real.HolderTriple.ennrealOfReal`
`toNNReal` 📖	mathematical	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `ENNReal.toNNReal`	`NNReal.HolderTriple`	—	`toNNReal_iff`
`toNNReal_iff` 📖	mathematical	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `ENNReal.toNNReal`	`NNReal.HolderTriple` `ENNReal.HolderTriple`	—	`toReal_iff`
`toReal` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `ENNReal.toReal`	`Real.HolderTriple`	—	`toReal_iff`
`toReal_iff` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `ENNReal.toReal`	`Real.HolderTriple` `ENNReal.HolderTriple`	—	`of_toReal` `ENNReal.toReal_add` `LT.lt.ne'` `ENNReal.toReal_pos_iff` `ENNReal.toReal_inv` `inv_add_inv_eq_inv`

NNReal

Definitions

Name	Category	Theorems
`HolderConjugate` 📖	MathDef	15 math math: `Real.HolderConjugate.toNNReal`, `holderConjugate_comm`, `ENNReal.holderConjugate_coe_iff`, `HolderConjugate.conjExponent`, `holderConjugate_one_div`, `HolderConjugate.two_two`, `HolderConjugate.one_sub_inv_inv`, `HolderTriple.holderConjugate_div_div`, `holderConjugate_iff_eq_conjExponent`, `ENNReal.HolderConjugate.toNNReal_iff`, `HolderConjugate.inv_inv`, `holderConjugate_coe_iff`, `HolderConjugate.inv_one_sub_inv`, `holderConjugate_iff`, `ENNReal.HolderConjugate.toNNReal`
`HolderTriple` 📖	CompData	7 math math: `ENNReal.holderTriple_coe_iff`, `ENNReal.HolderTriple.toNNReal_iff`, `ENNReal.HolderTriple.toNNReal`, `HolderTriple.of_pos`, `Real.HolderTriple.toNNReal`, `holderTriple_coe_iff`, `holderTriple_iff`
`conjExponent` 📖	CompOp	3 math math: `HolderConjugate.conjExponent`, `HolderConjugate.conjExponent_eq`, `ENNReal.coe_conjExponent`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`holderConjugate_coe_iff` 📖	mathematical	—	`Real.HolderConjugate` `toReal` `HolderConjugate`	—	`holderTriple_coe_iff`
`holderConjugate_comm` 📖	mathematical	—	`HolderConjugate`	—	`HolderConjugate.symm`
`holderConjugate_iff` 📖	mathematical	—	`HolderConjugate` `NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instOneNNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `instInv`	—	`holderConjugate_coe_iff` `Real.holderConjugate_iff` `coe_one` `Nat.cast_one`
`holderConjugate_iff_eq_conjExponent` 📖	mathematical	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instOneNNReal`	`HolderConjugate` `instDiv` `instSub`	—	`holderConjugate_coe_iff` `Real.holderConjugate_iff_eq_conjExponent` `Nat.cast_one` `coe_one` `coe_sub` `LT.lt.le`
`holderConjugate_one_div` 📖	mathematical	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `instOneNNReal`	`HolderConjugate` `instDiv`	—	`one_div` `HolderConjugate.inv_inv`
`holderTriple_coe_iff` 📖	mathematical	—	`Real.HolderTriple` `toReal` `HolderTriple`	—	`Real.holderTriple_iff` `Nat.cast_zero` `holderTriple_iff`
`holderTriple_iff` 📖	mathematical	—	`HolderTriple` `NNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `instInv` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal`	—	—

NNReal.HolderConjugate

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_ennreal` 📖	mathematical	`NNReal.HolderConjugate`	`ENNReal.HolderConjugate` `ENNReal.ofNNReal`	—	`ENNReal.holderConjugate_coe_iff`
`conjExponent` 📖	mathematical	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instOneNNReal`	`NNReal.HolderConjugate` `NNReal.conjExponent`	—	`NNReal.holderConjugate_iff_eq_conjExponent`
`conjExponent_eq` 📖	mathematical	`NNReal.HolderConjugate`	`NNReal.conjExponent`	—	`conjugate_eq`
`conjugate_eq` 📖	mathematical	`NNReal.HolderConjugate`	`NNReal` `NNReal.instDiv` `NNReal.instSub` `instOneNNReal`	—	`LT.lt.le` `Real.HolderTriple.lt` `coe` `Nat.cast_one` `Real.HolderConjugate.conjugate_eq` `NNReal.coe_one` `NNReal.coe_sub`
`div_conj_eq_sub_one` 📖	mathematical	`NNReal.HolderConjugate`	`NNReal` `NNReal.instDiv` `NNReal.instSub` `instOneNNReal`	—	`Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_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` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `NNReal.HolderTriple.ne_zero` `symm` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.LinearCombination.eq_of_eq` `AddRightCancelSemigroup.toIsRightCancelAdd` `sub_one_mul_conj` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.atom_pf` `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.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_gt`
`inv_add_inv_ennreal` 📖	mathematical	`NNReal.HolderConjugate`	`ENNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofNNReal` `NNReal` `NNReal.instInv` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`Nat.cast_one` `inv_add_inv_eq_one`
`inv_add_inv_eq_one` 📖	mathematical	`NNReal.HolderConjugate`	`NNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `NNReal.instInv` `instOneNNReal`	—	`NNReal.HolderTriple.inv_add_inv_eq_inv` `inv_one`
`inv_inv` 📖	mathematical	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `instOneNNReal`	`NNReal.HolderConjugate` `NNReal.instInv`	—	`inv_inv` `inv_one` `inv_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono`
`inv_one_sub_inv` 📖	mathematical	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `instOneNNReal`	`NNReal.HolderConjugate` `NNReal.instInv` `NNReal.instSub`	—	`NNReal.holderConjugate_iff` `one_lt_inv₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `inv_inv` `add_tsub_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `NNReal.instCanonicallyOrderedAdd` `NNReal.addLeftMono` `NNReal.instOrderedSub` `LT.lt.le`
`mul_eq_add` 📖	mathematical	`NNReal.HolderConjugate`	`NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `Distrib.toAdd`	—	`inv_one` `mul_one` `mul_add` `Distrib.leftDistribClass` `mul_inv_cancel₀` `NNReal.HolderTriple.ne_zero` `add_mul` `Distrib.rightDistribClass` `one_mul` `inv_mul_cancel_right₀` `symm` `add_comm` `NNReal.HolderTriple.inv_eq`
`one_sub_inv` 📖	mathematical	`NNReal.HolderConjugate`	`NNReal` `NNReal.instSub` `instOneNNReal` `NNReal.instInv`	—	`tsub_eq_of_eq_add` `NNReal.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `NNReal.addLeftReflectLT` `inv_add_inv_eq_one` `symm`
`one_sub_inv_inv` 📖	mathematical	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `instOneNNReal`	`NNReal.HolderConjugate` `NNReal.instInv` `NNReal.instSub`	—	`symm` `inv_one_sub_inv`
`sub_one_mul_conj` 📖	mathematical	`NNReal.HolderConjugate`	`NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `NNReal.instSub` `instOneNNReal`	—	`eq_div_iff` `sub_one_ne_zero` `conjugate_eq` `mul_comm`
`sub_one_ne_zero` 📖	—	`NNReal.HolderConjugate`	—	—	`LT.lt.ne'` `sub_one_pos`
`sub_one_pos` 📖	mathematical	`NNReal.HolderConjugate`	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `NNReal.instSub` `instOneNNReal`	—	`tsub_pos_of_lt` `NNReal.instCanonicallyOrderedAdd` `NNReal.instOrderedSub` `NNReal.HolderTriple.lt`
`two_two` 📖	mathematical	—	`NNReal.HolderConjugate` `NNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `inv_one` `one_div` `add_halves` `ZeroLEOneClass.neZero.two` `LinearOrderedCommMonoidWithZero.toZeroLeOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `NNReal.instIsStrictOrderedRing` `NNReal.addLeftMono` `zero_lt_two`

NNReal.HolderTriple

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_ennreal` 📖	mathematical	`NNReal.HolderTriple`	`ENNReal.HolderTriple` `ENNReal.ofNNReal`	—	`ENNReal.holderTriple_coe_iff`
`holderConjugate_div_div` 📖	mathematical	`NNReal.HolderTriple`	`NNReal.HolderConjugate` `NNReal` `NNReal.instDiv`	—	`div_eq_mul_inv` `mul_inv_rev` `inv_inv` `Distrib.leftDistribClass` `inv_add_inv_eq_inv` `mul_inv_cancel₀` `ne_zero'` `inv_one` `left_pos` `pos'` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `right_pos`
`inv_add_inv_eq_inv` 📖	mathematical	`NNReal.HolderTriple`	`NNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `NNReal.instInv`	—	—
`inv_eq` 📖	mathematical	`NNReal.HolderTriple`	`NNReal` `NNReal.instInv` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`inv_add_inv_eq_inv`
`inv_inv_add_inv` 📖	mathematical	`NNReal.HolderTriple`	`NNReal` `NNReal.instInv` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`Real.HolderTriple.inv_inv_add_inv` `coe`
`inv_lt_inv` 📖	mathematical	`NNReal.HolderTriple`	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `NNReal.instInv`	—	`Real.HolderTriple.inv_lt_inv` `coe`
`inv_ne_zero` 📖	—	`NNReal.HolderTriple`	—	—	`LT.lt.ne'` `inv_pos`
`inv_ne_zero'` 📖	—	`NNReal.HolderTriple`	—	—	`LT.lt.ne'` `inv_pos'`
`inv_nonneg` 📖	mathematical	`NNReal.HolderTriple`	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `NNReal.instInv`	—	`LT.lt.le` `inv_pos`
`inv_nonneg'` 📖	mathematical	`NNReal.HolderTriple`	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `NNReal.instInv`	—	`LT.lt.le` `inv_pos'`
`inv_pos` 📖	mathematical	`NNReal.HolderTriple`	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `NNReal.instInv`	—	`inv_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `pos`
`inv_pos'` 📖	mathematical	`NNReal.HolderTriple`	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `NNReal.instInv`	—	`inv_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `pos'`
`inv_sub_inv_eq_inv` 📖	mathematical	`NNReal.HolderTriple`	`NNReal` `NNReal.instSub` `NNReal.instInv`	—	`LT.lt.le` `inv_lt_inv` `symm` `Real.HolderTriple.inv_sub_inv_eq_inv` `coe`
`left_pos` 📖	mathematical	`NNReal.HolderTriple`	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal`	—	—
`lt` 📖	mathematical	`NNReal.HolderTriple`	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal`	—	`Real.HolderTriple.lt` `coe`
`ne_zero` 📖	—	`NNReal.HolderTriple`	—	—	`LT.lt.ne'` `pos`
`ne_zero'` 📖	—	`NNReal.HolderTriple`	—	—	`LT.lt.ne'` `pos'`
`nonneg` 📖	mathematical	`NNReal.HolderTriple`	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal`	—	`LT.lt.le` `pos`
`nonneg'` 📖	mathematical	`NNReal.HolderTriple`	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal`	—	`LT.lt.le` `pos'`
`of_pos` 📖	mathematical	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal`	`NNReal.HolderTriple` `NNReal.instInv` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`inv_inv`
`one_div_add_one_div` 📖	mathematical	`NNReal.HolderTriple`	`NNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `NNReal.instDiv` `instOneNNReal`	—	`Nat.cast_one` `Real.HolderTriple.one_div_add_one_div` `coe`
`one_div_eq` 📖	mathematical	`NNReal.HolderTriple`	`NNReal` `NNReal.instDiv` `instOneNNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`one_div_add_one_div`
`one_div_ne_zero` 📖	—	`NNReal.HolderTriple`	—	—	`ne_of_gt` `one_div_pos`
`one_div_ne_zero'` 📖	—	`NNReal.HolderTriple`	—	—	`ne_of_gt` `one_div_pos'`
`one_div_nonneg` 📖	mathematical	`NNReal.HolderTriple`	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `NNReal.instDiv` `instOneNNReal`	—	`le_of_lt` `one_div_pos`
`one_div_nonneg'` 📖	mathematical	`NNReal.HolderTriple`	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `NNReal.instDiv` `instOneNNReal`	—	`le_of_lt` `one_div_pos'`
`one_div_pos` 📖	mathematical	`NNReal.HolderTriple`	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `NNReal.instDiv` `instOneNNReal`	—	`one_div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `pos`
`one_div_pos'` 📖	mathematical	`NNReal.HolderTriple`	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `NNReal.instDiv` `instOneNNReal`	—	`one_div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `pos'`
`pos` 📖	mathematical	`NNReal.HolderTriple`	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal`	—	`left_pos`
`pos'` 📖	mathematical	`NNReal.HolderTriple`	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal`	—	`inv_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `add_pos` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `NNReal.addLeftMono` `inv_pos` `symm` `inv_add_inv_eq_inv`
`right_pos` 📖	mathematical	`NNReal.HolderTriple`	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal`	—	—

Real

Definitions

Name	Category	Theorems
`HolderConjugate` 📖	MathDef	14 math math: `ENNReal.HolderConjugate.toReal_iff`, `HolderTriple.holderConjugate_div_div`, `HolderConjugate.inv_inv`, `HolderConjugate.two_two`, `NNReal.HolderConjugate.coe`, `holderConjugate_iff`, `NNReal.holderConjugate_coe_iff`, `HolderConjugate.one_sub_inv_inv`, `HolderConjugate.inv_one_sub_inv`, `ENNReal.HolderConjugate.toReal`, `holderConjugate_comm`, `holderConjugate_one_div`, `holderConjugate_iff_eq_conjExponent`, `HolderConjugate.conjExponent`
`HolderTriple` 📖	CompData	6 math math: `holderTriple_iff`, `HolderTriple.of_pos`, `ENNReal.HolderTriple.toReal_iff`, `NNReal.HolderTriple.coe`, `NNReal.holderTriple_coe_iff`, `ENNReal.HolderTriple.toReal`
`conjExponent` 📖	CompOp	2 math math: `HolderConjugate.conjExponent_eq`, `HolderConjugate.conjExponent`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`holderConjugate_comm` 📖	mathematical	—	`HolderConjugate`	—	`HolderConjugate.symm`
`holderConjugate_iff` 📖	mathematical	—	`HolderConjugate` `Real` `instLT` `instOne` `instAdd` `instInv`	—	`HolderTriple.lt` `HolderConjugate.inv_add_inv_eq_one` `LT.lt.trans` `zero_lt_one` `instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `instIsStrictOrderedRing` `inv_one` `inv_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `sub_pos` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `inv_lt_one₀` `eq_sub_of_add_eq'`
`holderConjugate_iff_eq_conjExponent` 📖	mathematical	`Real` `instLT` `instOne`	`HolderConjugate` `DivInvMonoid.toDiv` `instDivInvMonoid` `instSub`	—	`HolderConjugate.conjugate_eq` `holderConjugate_iff` `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_add` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `div_one` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.subst_sub` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `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₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `ne_of_gt` `lt_trans` `Mathlib.Meta.Positivity.pos_of_isNat` `instIsOrderedRing` `instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `add_sub_cancel`
`holderConjugate_one_div` 📖	mathematical	`Real` `instLT` `instZero` `instAdd` `instOne`	`HolderConjugate` `DivInvMonoid.toDiv` `instDivInvMonoid`	—	`one_div` `HolderConjugate.inv_inv`
`holderTriple_iff` 📖	mathematical	—	`HolderTriple` `Real` `instAdd` `instInv` `instLT` `instZero`	—	—

Real.HolderConjugate

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`conjExponent` 📖	mathematical	`Real` `Real.instLT` `Real.instOne`	`Real.HolderConjugate` `Real.conjExponent`	—	`Real.holderConjugate_iff_eq_conjExponent`
`conjExponent_eq` 📖	mathematical	`Real.HolderConjugate`	`Real.conjExponent`	—	`conjugate_eq`
`conjugate_eq` 📖	mathematical	`Real.HolderConjugate`	`Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instSub` `Real.instOne`	—	`Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.subst_sub` `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.eval_cons_mul_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.eval_cons_mul_eval_cons_neg` `Real.HolderTriple.ne_zero` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `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_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.zero_mul` `Real.HolderTriple.inv_sub_inv_eq_inv` `symm` `inv_inv`
`div_conj_eq_sub_one` 📖	mathematical	`Real.HolderConjugate`	`Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instSub` `Real.instOne`	—	`Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_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` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.subst_sub` `Mathlib.Tactic.FieldSimp.NF.one_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `Real.HolderTriple.ne_zero` `symm` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.LinearCombination.eq_of_eq` `AddRightCancelSemigroup.toIsRightCancelAdd` `sub_one_mul_conj` `Mathlib.Tactic.LinearCombination.eq_rearrange` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.mul_congr` `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.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `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.Ring.cast_zero` `Nat.cast_zero`
`ennrealOfReal` 📖	mathematical	`Real.HolderConjugate`	`ENNReal.HolderConjugate` `ENNReal.ofReal`	—	`ENNReal.ofReal_one` `Real.HolderTriple.ennrealOfReal`
`inv_add_inv_ennreal` 📖	mathematical	`Real.HolderConjugate`	`ENNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instInv` `ENNReal.ofReal` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`ENNReal.ofReal_one` `ENNReal.ofReal_inv_of_pos` `Real.HolderTriple.pos` `symm` `ENNReal.ofReal_add` `Real.HolderTriple.inv_nonneg` `inv_add_inv_eq_one`
`inv_add_inv_eq_one` 📖	mathematical	`Real.HolderConjugate`	`Real` `Real.instAdd` `Real.instInv` `Real.instOne`	—	`Real.HolderTriple.inv_add_inv_eq_inv` `inv_one`
`inv_inv` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Real.instAdd` `Real.instOne`	`Real.HolderConjugate` `Real.instInv`	—	`inv_inv` `inv_one` `inv_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing`
`inv_one_sub_inv` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Real.instOne`	`Real.HolderConjugate` `Real.instInv` `Real.instSub`	—	`Real.holderConjugate_iff` `one_lt_inv₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `inv_inv` `add_sub_cancel`
`inv_sub_one` 📖	mathematical	`Real.HolderConjugate`	`Real` `Real.instSub` `Real.instInv` `Real.instOne` `Real.instNeg`	—	`neg_sub` `one_sub_inv`
`mul_eq_add` 📖	mathematical	`Real.HolderConjugate`	`Real` `Real.instMul` `Real.instAdd`	—	`sub_mul` `one_mul` `sub_one_mul_conj`
`one_sub_inv` 📖	mathematical	`Real.HolderConjugate`	`Real` `Real.instSub` `Real.instOne` `Real.instInv`	—	`sub_eq_of_eq_add` `inv_add_inv_eq_one` `symm`
`one_sub_inv_inv` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Real.instOne`	`Real.HolderConjugate` `Real.instInv` `Real.instSub`	—	`symm` `inv_one_sub_inv`
`sub_one_mul_conj` 📖	mathematical	`Real.HolderConjugate`	`Real` `Real.instMul` `Real.instSub` `Real.instOne`	—	`eq_div_iff` `sub_one_ne_zero` `conjugate_eq` `mul_comm`
`sub_one_ne_zero` 📖	—	`Real.HolderConjugate`	—	—	`LT.lt.ne'` `sub_one_pos`
`sub_one_pos` 📖	mathematical	`Real.HolderConjugate`	`Real` `Real.instLT` `Real.instZero` `Real.instSub` `Real.instOne`	—	`sub_pos` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.HolderTriple.lt`
`toNNReal` 📖	mathematical	`Real.HolderConjugate`	`NNReal.HolderConjugate` `Real.toNNReal`	—	`Real.toNNReal_one` `Real.HolderTriple.toNNReal`
`two_two` 📖	mathematical	—	`Real.HolderConjugate` `Real` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_add` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Nat.cast_one` `zero_lt_two` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid`

Real.HolderTriple

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ennrealOfReal` 📖	mathematical	`Real.HolderTriple`	`ENNReal.HolderTriple` `ENNReal.ofReal`	—	`ENNReal.ofReal_add` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `nonneg` `symm` `ENNReal.ofReal_inv_of_pos` `pos` `pos'` `inv_add_inv_eq_inv`
`holderConjugate_div_div` 📖	mathematical	`Real.HolderTriple`	`Real.HolderConjugate` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid`	—	`div_eq_mul_inv` `mul_inv_rev` `inv_inv` `Distrib.leftDistribClass` `inv_add_inv_eq_inv` `mul_inv_cancel₀` `ne_zero'` `inv_one` `left_pos` `pos'` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `right_pos`
`inv_add_inv_eq_inv` 📖	mathematical	`Real.HolderTriple`	`Real` `Real.instAdd` `Real.instInv`	—	—
`inv_eq` 📖	mathematical	`Real.HolderTriple`	`Real` `Real.instInv` `Real.instAdd`	—	`inv_add_inv_eq_inv`
`inv_inv_add_inv` 📖	mathematical	`Real.HolderTriple`	`Real` `Real.instInv` `Real.instAdd`	—	`inv_add_inv_eq_inv` `inv_inv`
`inv_lt_inv` 📖	mathematical	`Real.HolderTriple`	`Real` `Real.instLT` `Real.instInv`	—	`add_zero` `add_lt_add_right` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `inv_pos` `symm` `inv_add_inv_eq_inv`
`inv_ne_zero` 📖	—	`Real.HolderTriple`	—	—	`LT.lt.ne'` `inv_pos`
`inv_ne_zero'` 📖	—	`Real.HolderTriple`	—	—	`LT.lt.ne'` `inv_pos'`
`inv_nonneg` 📖	mathematical	`Real.HolderTriple`	`Real` `Real.instLE` `Real.instZero` `Real.instInv`	—	`LT.lt.le` `inv_pos`
`inv_nonneg'` 📖	mathematical	`Real.HolderTriple`	`Real` `Real.instLE` `Real.instZero` `Real.instInv`	—	`LT.lt.le` `inv_pos'`
`inv_pos` 📖	mathematical	`Real.HolderTriple`	`Real` `Real.instLT` `Real.instZero` `Real.instInv`	—	`inv_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `pos`
`inv_pos'` 📖	mathematical	`Real.HolderTriple`	`Real` `Real.instLT` `Real.instZero` `Real.instInv`	—	`inv_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `pos'`
`inv_sub_inv_eq_inv` 📖	mathematical	`Real.HolderTriple`	`Real` `Real.instSub` `Real.instInv`	—	`sub_eq_of_eq_add` `inv_eq`
`left_pos` 📖	mathematical	`Real.HolderTriple`	`Real` `Real.instLT` `Real.instZero`	—	—
`lt` 📖	mathematical	`Real.HolderTriple`	`Real` `Real.instLT`	—	`inv_inv` `inv_strictAnti₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `inv_pos` `inv_lt_inv`
`ne_zero` 📖	—	`Real.HolderTriple`	—	—	`LT.lt.ne'` `pos`
`ne_zero'` 📖	—	`Real.HolderTriple`	—	—	`LT.lt.ne'` `pos'`
`nonneg` 📖	mathematical	`Real.HolderTriple`	`Real` `Real.instLE` `Real.instZero`	—	`LT.lt.le` `pos`
`nonneg'` 📖	mathematical	`Real.HolderTriple`	`Real` `Real.instLE` `Real.instZero`	—	`LT.lt.le` `pos'`
`of_pos` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Real.HolderTriple` `Real.instInv` `Real.instAdd`	—	`inv_inv`
`one_div_add_one_div` 📖	mathematical	`Real.HolderTriple`	`Real` `Real.instAdd` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne`	—	`one_div` `inv_add_inv_eq_inv`
`one_div_eq` 📖	mathematical	`Real.HolderTriple`	`Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `Real.instAdd`	—	`one_div_add_one_div`
`one_div_ne_zero` 📖	—	`Real.HolderTriple`	—	—	`ne_of_gt` `one_div_pos`
`one_div_ne_zero'` 📖	—	`Real.HolderTriple`	—	—	`ne_of_gt` `one_div_pos'`
`one_div_nonneg` 📖	mathematical	`Real.HolderTriple`	`Real` `Real.instLE` `Real.instZero` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne`	—	`le_of_lt` `one_div_pos`
`one_div_nonneg'` 📖	mathematical	`Real.HolderTriple`	`Real` `Real.instLE` `Real.instZero` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne`	—	`le_of_lt` `one_div_pos'`
`one_div_pos` 📖	mathematical	`Real.HolderTriple`	`Real` `Real.instLT` `Real.instZero` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne`	—	`one_div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `pos`
`one_div_pos'` 📖	mathematical	`Real.HolderTriple`	`Real` `Real.instLT` `Real.instZero` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne`	—	`one_div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `pos'`
`pos` 📖	mathematical	`Real.HolderTriple`	`Real` `Real.instLT` `Real.instZero`	—	`left_pos`
`pos'` 📖	mathematical	`Real.HolderTriple`	`Real` `Real.instLT` `Real.instZero`	—	`inv_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `add_pos` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `inv_pos` `symm` `inv_add_inv_eq_inv`
`right_pos` 📖	mathematical	`Real.HolderTriple`	`Real` `Real.instLT` `Real.instZero`	—	—
`toNNReal` 📖	mathematical	`Real.HolderTriple`	`NNReal.HolderTriple` `Real.toNNReal`	—	`sup_of_le_left` `nonneg` `symm` `nonneg'`

---

← Back to Index