Commit 2024-09-08 09:20 b63d3d7b

View on Github →

feat: Nat.log is less than or equal to Real.logb (#16450) We add

lemma nat_log_le_real_logb {a b : ℕ} (_ : 0 < a)  : Nat.log b a ≤ Real.logb b a

and remove some (hb : 1 < b) not needed hypotheses in previous lemmas

Estimated changes

modified theorem Real.ceil_logb_natCast
modified theorem Real.floor_logb_natCast
added theorem Real.logb_one_left
added theorem Real.logb_zero_left
added theorem Real.natLog_le_logb
added theorem Int.clog_one_left
added theorem Int.clog_zero_left
added theorem Int.log_one_left
added theorem Int.log_zero_left