Documentation Verification Report

ENNRealLogExp

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

Statistics

Metric	Count
Definitions `logHomeomorph`, `logOrderIso`, `expHomeomorph`, `expOrderIso`	4
Theorems `continuous_exp`, `continuous_log`, `exp_log`, `logHomeomorph_apply`, `logHomeomorph_symm`, `logOrderIso_apply`, `logOrderIso_symm`, `measurable_log`, `tendsto_rpow_atBot_of_base_lt_one`, `tendsto_rpow_atBot_of_one_lt_base`, `tendsto_rpow_atTop_of_base_lt_one`, `tendsto_rpow_atTop_of_one_lt_base`, `rpow_eq_exp_mul_log`, `expHomeomorph_apply`, `expHomeomorph_symm`, `expOrderIso_apply`, `expOrderIso_symm`, `exp_mul`, `exp_nmul`, `log_exp`, `measurable_exp`, `tendsto_exp_nhds_bot_nhds_zero`, `tendsto_exp_nhds_top_nhds_top`, `tendsto_exp_nhds_zero_nhds_one`, `ennreal_log`, `ereal_exp`, `instPolishSpaceEReal`	27
Total	31

ENNReal

Definitions

Name	Category	Theorems
`logHomeomorph` 📖	CompOp	3 math math: `EReal.expHomeomorph_symm`, `logHomeomorph_symm`, `logHomeomorph_apply`
`logOrderIso` 📖	CompOp	3 math math: `EReal.expOrderIso_symm`, `logOrderIso_symm`, `logOrderIso_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_exp` 📖	mathematical	—	`Continuous` `EReal` `ENNReal` `EReal.instTopologicalSpace` `instTopologicalSpace` `EReal.exp`	—	`OrderIso.continuous` `EReal.instOrderTopology` `instOrderTopology`
`continuous_log` 📖	mathematical	—	`Continuous` `ENNReal` `EReal` `instTopologicalSpace` `EReal.instTopologicalSpace` `log`	—	`OrderIso.continuous` `instOrderTopology` `EReal.instOrderTopology`
`exp_log` 📖	mathematical	—	`EReal.exp` `log`	—	`log_zero` `toReal_pos` `ofReal_toReal` `log_ofReal_of_pos` `EReal.exp_coe` `Real.exp_log`
`logHomeomorph_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `ENNReal` `EReal` `instTopologicalSpace` `EReal.instTopologicalSpace` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `logHomeomorph` `log`	—	—
`logHomeomorph_symm` 📖	mathematical	—	`Homeomorph.symm` `ENNReal` `EReal` `instTopologicalSpace` `EReal.instTopologicalSpace` `logHomeomorph` `EReal.expHomeomorph`	—	—
`logOrderIso_apply` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `ENNReal` `EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instPartialOrderEReal` `instFunLikeOrderIso` `logOrderIso` `log`	—	—
`logOrderIso_symm` 📖	mathematical	—	`OrderIso.symm` `ENNReal` `EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instPartialOrderEReal` `logOrderIso` `EReal.expOrderIso`	—	—
`measurable_log` 📖	mathematical	—	`Measurable` `ENNReal` `EReal` `measurableSpace` `EReal.measurableSpace` `log`	—	`Continuous.measurable` `BorelSpace.opensMeasurable` `borelSpace` `EReal.borelSpace` `continuous_log`
`tendsto_rpow_atBot_of_base_lt_one` 📖	mathematical	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	`Filter.Tendsto` `Real` `instPowReal` `Filter.atBot` `Real.instPreorder` `nhds` `instTopologicalSpace` `Top.top` `instTopENNReal`	—	`EReal.ENNReal.rpow_eq_exp_mul_log` `Filter.Tendsto.comp` `EReal.tendsto_exp_nhds_top_nhds_top` `EReal.bot_mul_of_neg` `log_lt_zero_iff` `EReal.Tendsto.mul_const` `EReal.tendsto_coe_atBot`
`tendsto_rpow_atBot_of_one_lt_base` 📖	mathematical	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	`Filter.Tendsto` `Real` `instPowReal` `Filter.atBot` `Real.instPreorder` `nhds` `instTopologicalSpace` `instZeroENNReal`	—	`EReal.ENNReal.rpow_eq_exp_mul_log` `Filter.Tendsto.comp` `EReal.tendsto_exp_nhds_bot_nhds_zero` `EReal.bot_mul_of_pos` `zero_lt_log_iff` `EReal.Tendsto.mul_const` `EReal.tendsto_coe_atBot`
`tendsto_rpow_atTop_of_base_lt_one` 📖	mathematical	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	`Filter.Tendsto` `Real` `instPowReal` `Filter.atTop` `Real.instPreorder` `nhds` `instTopologicalSpace` `instZeroENNReal`	—	`EReal.ENNReal.rpow_eq_exp_mul_log` `Filter.Tendsto.comp` `EReal.tendsto_exp_nhds_bot_nhds_zero` `EReal.top_mul_of_neg` `log_lt_zero_iff` `EReal.Tendsto.mul_const` `EReal.tendsto_coe_atTop`
`tendsto_rpow_atTop_of_one_lt_base` 📖	mathematical	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	`Filter.Tendsto` `Real` `instPowReal` `Filter.atTop` `Real.instPreorder` `nhds` `instTopologicalSpace` `Top.top` `instTopENNReal`	—	`EReal.ENNReal.rpow_eq_exp_mul_log` `Filter.Tendsto.comp` `EReal.tendsto_exp_nhds_top_nhds_top` `EReal.top_mul_of_pos` `zero_lt_log_iff` `EReal.Tendsto.mul_const` `EReal.tendsto_coe_atTop`

EReal

Definitions

Name	Category	Theorems
`expHomeomorph` 📖	CompOp	3 math math: `expHomeomorph_symm`, `ENNReal.logHomeomorph_symm`, `expHomeomorph_apply`
`expOrderIso` 📖	CompOp	3 math math: `expOrderIso_symm`, `ENNReal.logOrderIso_symm`, `expOrderIso_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`expHomeomorph_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `EReal` `ENNReal` `instTopologicalSpace` `ENNReal.instTopologicalSpace` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `expHomeomorph` `exp`	—	—
`expHomeomorph_symm` 📖	mathematical	—	`Homeomorph.symm` `EReal` `ENNReal` `instTopologicalSpace` `ENNReal.instTopologicalSpace` `expHomeomorph` `ENNReal.logHomeomorph`	—	—
`expOrderIso_apply` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `EReal` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `ENNReal.instPartialOrder` `instFunLikeOrderIso` `expOrderIso` `exp`	—	—
`expOrderIso_symm` 📖	mathematical	—	`OrderIso.symm` `EReal` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `ENNReal.instPartialOrder` `expOrderIso` `ENNReal.logOrderIso`	—	—
`exp_mul` 📖	mathematical	—	`exp` `EReal` `instMul` `Real.toEReal` `ENNReal` `Real` `ENNReal.instPowReal`	—	`ENNReal.log_eq_iff` `ENNReal.log_rpow` `log_exp` `mul_comm`
`exp_nmul` 📖	mathematical	—	`exp` `EReal` `instMul` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal` `ENNReal` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	—	`ENNReal.log_pow` `log_exp`
`log_exp` 📖	mathematical	—	`ENNReal.log` `exp`	—	`ENNReal.log_zero` `exp_coe` `ENNReal.log_ofReal` `not_le` `Real.exp_pos` `Real.log_exp`
`measurable_exp` 📖	mathematical	—	`Measurable` `EReal` `ENNReal` `measurableSpace` `ENNReal.measurableSpace` `exp`	—	`Continuous.measurable` `BorelSpace.opensMeasurable` `borelSpace` `ENNReal.borelSpace` `ENNReal.continuous_exp`
`tendsto_exp_nhds_bot_nhds_zero` 📖	mathematical	—	`Filter.Tendsto` `EReal` `ENNReal` `exp` `nhds` `instTopologicalSpace` `Bot.bot` `instBotEReal` `ENNReal.instTopologicalSpace` `instZeroENNReal`	—	`Continuous.tendsto` `ENNReal.continuous_exp`
`tendsto_exp_nhds_top_nhds_top` 📖	mathematical	—	`Filter.Tendsto` `EReal` `ENNReal` `exp` `nhds` `instTopologicalSpace` `Top.top` `instTop` `ENNReal.instTopologicalSpace` `instTopENNReal`	—	`Continuous.tendsto` `ENNReal.continuous_exp`
`tendsto_exp_nhds_zero_nhds_one` 📖	mathematical	—	`Filter.Tendsto` `EReal` `ENNReal` `exp` `nhds` `instTopologicalSpace` `instZeroEReal` `ENNReal.instTopologicalSpace` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`exp_zero` `Continuous.tendsto` `ENNReal.continuous_exp`

EReal.ENNReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`rpow_eq_exp_mul_log` 📖	mathematical	—	`ENNReal` `Real` `ENNReal.instPowReal` `EReal.exp` `EReal` `EReal.instMul` `Real.toEReal` `ENNReal.log`	—	`mul_comm` `EReal.exp_mul` `ENNReal.exp_log`

Measurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ennreal_log` 📖	mathematical	`Measurable` `ENNReal` `ENNReal.measurableSpace`	`EReal` `EReal.measurableSpace` `ENNReal.log`	—	`comp` `ENNReal.measurable_log`
`ereal_exp` 📖	mathematical	`Measurable` `EReal` `EReal.measurableSpace`	`ENNReal` `ENNReal.measurableSpace` `EReal.exp`	—	`comp` `EReal.measurable_exp`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instPolishSpaceEReal` 📖	mathematical	—	`PolishSpace` `EReal` `EReal.instTopologicalSpace`	—	`Topology.IsClosedEmbedding.polishSpace` `PolishSpace.instENNReal` `EReal.instOrderTopology` `ENNReal.instOrderTopology` `Homeomorph.isClosedEmbedding`

---

← Back to Index