Commit 2025-03-19 07:35 67019e0b

View on Github →

chore(SpecialFunctions/Log): rename some Tendsto lemmas (#23083) Use nhdsNE/nhdsGT.

Estimated changes

Modified Mathlib/Analysis/Complex/Periodic.lean

Modified Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean

Modified Mathlib/Analysis/SpecialFunctions/Log/Base.lean

added theorem Real.tendsto_logb_nhdsGT_zero

added theorem Real.tendsto_logb_nhdsGT_zero_of_base_lt_one

added theorem Real.tendsto_logb_nhdsNE_zero

added theorem Real.tendsto_logb_nhdsNE_zero_of_base_lt_one

deleted theorem Real.tendsto_logb_nhdsWithin_zero

deleted theorem Real.tendsto_logb_nhdsWithin_zero_of_base_lt_one

deleted theorem Real.tendsto_logb_nhdsWithin_zero_right

deleted theorem Real.tendsto_logb_nhdsWithin_zero_right_of_base_lt_one

Modified Mathlib/Analysis/SpecialFunctions/Log/Basic.lean

added theorem Real.tendsto_log_nhdsGT_zero

added theorem Real.tendsto_log_nhdsLT_zero

added theorem Real.tendsto_log_nhdsNE_zero

deleted theorem Real.tendsto_log_nhdsWithin_zero

deleted theorem Real.tendsto_log_nhdsWithin_zero_left

deleted theorem Real.tendsto_log_nhdsWithin_zero_right

Modified Mathlib/Analysis/SpecialFunctions/Log/NegMulLog.lean

Modified Mathlib/Analysis/SpecialFunctions/NonIntegrable.lean

Modified Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean

Modified Mathlib/InformationTheory/KullbackLeibler/KLFun.lean