Commit 2024-07-12 14:35 c2057164

View on Github →

feat(SpecialFunctions/Log): Add extended exp (#14107) We define an extended version of the exponential from EReal to ENNReal and prove some properties in relation to the extended log.

  • Rename ENNReal.lean to ENNRealLog.lean
  • Add ENNRealExp.lean
  • Add ENNRealLogExp.lean See this Zulip discussion.

Estimated changes

added theorem ENNReal.bot_lt_log_iff
deleted theorem ENNReal.log_bot_lt_iff
deleted theorem ENNReal.log_continuous
modified theorem ENNReal.log_eq_bot_iff
modified theorem ENNReal.log_eq_one_iff
modified theorem ENNReal.log_eq_top_iff
modified theorem ENNReal.log_injective
added theorem ENNReal.log_inv
deleted theorem ENNReal.log_le_iff_le
added theorem ENNReal.log_le_log_iff
deleted theorem ENNReal.log_le_one_iff
deleted theorem ENNReal.log_lt_iff_lt
added theorem ENNReal.log_lt_log_iff
deleted theorem ENNReal.log_lt_one_iff
modified theorem ENNReal.log_lt_top_iff
modified theorem ENNReal.log_monotone
added theorem ENNReal.log_ofReal
modified theorem ENNReal.log_one
deleted theorem ENNReal.log_one_le_iff
deleted theorem ENNReal.log_one_lt_iff
modified theorem ENNReal.log_top
modified theorem ENNReal.log_zero
added theorem ENNReal.continuous_exp
added theorem ENNReal.continuous_log
added theorem ENNReal.exp_log
added theorem ENNReal.measurable_log
added theorem EReal.expOrderIso_symm
added theorem EReal.exp_mul
added theorem EReal.exp_nmul
added theorem EReal.log_exp
added theorem EReal.measurable_exp
added theorem Measurable.ennreal_log
added theorem Measurable.ereal_exp
added def EReal.exp
added theorem EReal.exp_add
added theorem EReal.exp_bot
added theorem EReal.exp_coe
added theorem EReal.exp_eq_top_iff
added theorem EReal.exp_eq_zero_iff
added theorem EReal.exp_le_exp_iff
added theorem EReal.exp_le_one_iff
added theorem EReal.exp_lt_exp_iff
added theorem EReal.exp_lt_one_iff
added theorem EReal.exp_lt_top_iff
added theorem EReal.exp_monotone
added theorem EReal.exp_neg
added theorem EReal.exp_strictMono
added theorem EReal.exp_top
added theorem EReal.exp_zero
added theorem EReal.one_le_exp_iff
added theorem EReal.one_lt_exp_iff
added theorem EReal.zero_lt_exp_iff