Commit 2024-11-11 16:21 16c47564

View on Github →

chore(SpecialFunctions/Log): transfer results from log to logb (#18621) These are mostly transferred directly, except for continuousAt_logb_iff which needs different handling since it's not always true.

Estimated changes

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

added theorem Real.continuousAt_logb

added theorem Real.continuousAt_logb_iff

added theorem Real.continuousOn_logb

added theorem Real.continuous_logb'

added theorem Real.continuous_logb

added theorem Real.logb_nat_eq_sum_factorization

modified theorem Real.logb_pow

added theorem Real.tendsto_logb_nhdsWithin_zero

added theorem Real.tendsto_logb_nhdsWithin_zero_of_base_lt_one

added theorem Real.tendsto_logb_nhdsWithin_zero_right

added theorem Real.tendsto_logb_nhdsWithin_zero_right_of_base_lt_one

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

Modified Mathlib/NumberTheory/Ostrowski.lean