ENNRealLog

📁 Source: Mathlib/Analysis/SpecialFunctions/Log/ENNRealLog.lean

Statistics

Metric	Count
Definitions	0
Theorems `bot_lt_log_iff`, `log_bijective`, `log_eq_bot_iff`, `log_eq_iff`, `log_eq_one_iff`, `log_eq_top_iff`, `log_injective`, `log_inv`, `log_le_log`, `log_le_log_iff`, `log_le_zero_iff`, `log_lt_log`, `log_lt_log_iff`, `log_lt_top_iff`, `log_lt_zero_iff`, `log_monotone`, `log_mul_add`, `log_ofReal`, `log_ofReal_of_pos`, `log_of_nnreal`, `log_one`, `log_pos_real`, `log_pos_real'`, `log_pow`, `log_rpow`, `log_strictMono`, `log_surjective`, `log_top`, `log_zero`, `zero_le_log_iff`, `zero_lt_log_iff`	31
Total	31

ENNReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bot_lt_log_iff` 📖	mathematical	—	`EReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderEReal` `Bot.bot` `instBotEReal` `log` `ENNReal` `instPartialOrder` `instZeroENNReal`	—	`log_lt_log_iff` `log_zero`
`log_bijective` 📖	mathematical	—	`Function.Bijective` `ENNReal` `EReal` `log`	—	`log_injective` `log_surjective`
`log_eq_bot_iff` 📖	mathematical	—	`log` `Bot.bot` `EReal` `instBotEReal` `ENNReal` `instZeroENNReal`	—	`log_eq_iff` `log_zero`
`log_eq_iff` 📖	mathematical	—	`log`	—	`log_injective`
`log_eq_one_iff` 📖	mathematical	—	`log` `EReal` `instZeroEReal` `ENNReal` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`log_eq_iff` `log_one`
`log_eq_top_iff` 📖	mathematical	—	`log` `Top.top` `EReal` `EReal.instTop` `ENNReal` `instTopENNReal`	—	`log_eq_iff` `log_top`
`log_injective` 📖	mathematical	—	`ENNReal` `EReal` `log`	—	`StrictMono.injective` `log_strictMono`
`log_inv` 📖	mathematical	—	`log` `ENNReal` `instInv` `EReal` `EReal.instNeg`	—	`log_rpow` `neg_mul` `one_mul`
`log_le_log` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`EReal` `instPartialOrderEReal` `log`	—	`log_monotone`
`log_le_log_iff` 📖	mathematical	—	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `log` `ENNReal` `instPartialOrder`	—	`StrictMono.le_iff_le` `log_strictMono`
`log_le_zero_iff` 📖	mathematical	—	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `log` `instZeroEReal` `ENNReal` `instPartialOrder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`log_le_log_iff` `log_one`
`log_lt_log` 📖	mathematical	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder`	`EReal` `instPartialOrderEReal` `log`	—	`log_strictMono`
`log_lt_log_iff` 📖	mathematical	—	`EReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderEReal` `log` `ENNReal` `instPartialOrder`	—	`StrictMono.lt_iff_lt` `log_strictMono`
`log_lt_top_iff` 📖	mathematical	—	`EReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderEReal` `log` `Top.top` `EReal.instTop` `ENNReal` `instPartialOrder` `instTopENNReal`	—	`log_lt_log_iff` `log_top`
`log_lt_zero_iff` 📖	mathematical	—	`EReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderEReal` `log` `instZeroEReal` `ENNReal` `instPartialOrder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`log_lt_log_iff` `log_one`
`log_monotone` 📖	mathematical	—	`Monotone` `ENNReal` `EReal` `PartialOrder.toPreorder` `instPartialOrder` `instPartialOrderEReal` `log`	—	`StrictMono.monotone` `log_strictMono`
`log_mul_add` 📖	mathematical	—	`log` `ENNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring` `EReal` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoidEReal`	—	`trichotomy` `MulZeroClass.zero_mul` `log_zero` `EReal.bot_add` `log_top` `MulZeroClass.mul_zero` `EReal.add_bot` `mul_top` `EReal.add_top_of_ne_bot` `log_pos_real'` `top_mul'` `EReal.top_add_coe` `log_eq_top_iff` `LT.lt.ne'` `toReal_pos_iff` `toReal_mul` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Nat.cast_zero` `Real.log_mul`
`log_ofReal` 📖	mathematical	—	`log` `ofReal` `EReal` `Real` `Real.instLE` `Real.instZero` `Real.decidableLE` `Bot.bot` `instBotEReal` `Real.toEReal` `Real.log`	—	`toReal_ofReal` `LT.lt.le` `not_le`
`log_ofReal_of_pos` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`log` `ofReal` `Real.toEReal` `Real.log`	—	`log_ofReal` `LT.lt.not_ge`
`log_of_nnreal` 📖	mathematical	—	`log` `ofNNReal` `Real.toEReal` `Real.log` `NNReal.toReal`	—	—
`log_one` 📖	mathematical	—	`log` `ENNReal` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `EReal` `instZeroEReal`	—	`NeZero.charZero_one` `instCharZero` `Real.log_one`
`log_pos_real` 📖	mathematical	—	`log` `Real.toEReal` `Real.log` `toReal`	—	—
`log_pos_real'` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `toReal`	`log` `Real.toEReal` `Real.log`	—	`LT.lt.ne'` `toReal_pos_iff` `LT.lt.ne`
`log_pow` 📖	mathematical	—	`log` `ENNReal` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `instCommSemiring` `EReal` `EReal.instMul` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal`	—	`rpow_natCast` `log_rpow` `EReal.coe_natCast`
`log_rpow` 📖	mathematical	—	`log` `ENNReal` `Real` `instPowReal` `EReal` `EReal.instMul` `Real.toEReal`	—	`lt_trichotomy` `trichotomy` `zero_rpow_def` `not_lt_of_gt` `LT.lt.ne` `log_zero` `EReal.coe_mul_bot_of_neg` `top_rpow_of_neg` `log_top` `EReal.coe_mul_top_of_neg` `LT.lt.ne'` `toReal_pos_iff` `Real.log_rpow` `toReal_rpow` `rpow_zero` `log_one` `MulZeroClass.zero_mul` `zero_rpow_of_pos` `EReal.mul_bot_of_pos` `Nat.cast_zero` `top_rpow_of_pos` `EReal.mul_top_of_pos`
`log_strictMono` 📖	mathematical	—	`StrictMono` `ENNReal` `EReal` `PartialOrder.toPreorder` `instPartialOrder` `instPartialOrderEReal` `log`	—	`instCanonicallyOrderedAdd`
`log_surjective` 📖	mathematical	—	`ENNReal` `EReal` `log`	—	`log_zero` `log_ofReal` `Real.log_exp`
`log_top` 📖	mathematical	—	`log` `Top.top` `ENNReal` `instTopENNReal` `EReal` `EReal.instTop`	—	—
`log_zero` 📖	mathematical	—	`log` `ENNReal` `instZeroENNReal` `Bot.bot` `EReal` `instBotEReal`	—	—
`zero_le_log_iff` 📖	mathematical	—	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `instZeroEReal` `log` `ENNReal` `instPartialOrder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`log_le_log_iff` `log_one`
`zero_lt_log_iff` 📖	mathematical	—	`EReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderEReal` `instZeroEReal` `log` `ENNReal` `instPartialOrder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`log_lt_log_iff` `log_one`

---

← Back to Index