Commit 2024-06-23 16:19 2fc483bd

View on Github →

feat(SpecialFunctions/Log): add extended nonnegative real logarithm (#14018) This PR adds the SpecialFunctions/Log/ENNRealLog.lean file where we define log as an extension of the logarithm of a positive real to the extended nonnegative reals ℝ≥0∞. The function takes values in the extended reals EReal, with log 0 = ⊥ and log ⊤ = ⊤. Co-authored with @D-Thomine.

Estimated changes

added theorem ENNReal.log_bijective
added theorem ENNReal.log_bot_lt_iff
added theorem ENNReal.log_continuous
added theorem ENNReal.log_eq_bot_iff
added theorem ENNReal.log_eq_iff
added theorem ENNReal.log_eq_one_iff
added theorem ENNReal.log_eq_top_iff
added theorem ENNReal.log_injective
added theorem ENNReal.log_le_iff_le
added theorem ENNReal.log_le_one_iff
added theorem ENNReal.log_lt_iff_lt
added theorem ENNReal.log_lt_one_iff
added theorem ENNReal.log_lt_top_iff
added theorem ENNReal.log_monotone
added theorem ENNReal.log_mul_add
added theorem ENNReal.log_of_nnreal
added theorem ENNReal.log_one
added theorem ENNReal.log_one_le_iff
added theorem ENNReal.log_one_lt_iff
added theorem ENNReal.log_pos_real'
added theorem ENNReal.log_pos_real
added theorem ENNReal.log_pow
added theorem ENNReal.log_rpow
added theorem ENNReal.log_strictMono
added theorem ENNReal.log_surjective
added theorem ENNReal.log_top
added theorem ENNReal.log_zero