Commit 2023-05-20 14:05 e73b3d64

View on Github →

feat: port Analysis.SpecialFunctions.Log.Base (#4140)

Estimated changes

Modified Mathlib.lean

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

added theorem Real.ceil_logb_nat_cast

added theorem Real.eq_one_of_pos_of_logb_eq_zero

added theorem Real.eq_one_of_pos_of_logb_eq_zero_of_base_lt_one

added theorem Real.floor_logb_nat_cast

added theorem Real.le_logb_iff_rpow_le

added theorem Real.le_logb_iff_rpow_le_of_base_lt_one

added theorem Real.log_div_log

added theorem Real.logb_abs

added theorem Real.logb_div

added theorem Real.logb_eq_zero

added theorem Real.logb_injOn_pos

added theorem Real.logb_injOn_pos_of_base_lt_one

added theorem Real.logb_inv

added theorem Real.logb_le_iff_le_rpow

added theorem Real.logb_le_iff_le_rpow_of_base_lt_one

added theorem Real.logb_le_logb

added theorem Real.logb_le_logb_of_base_lt_one

added theorem Real.logb_lt_iff_lt_rpow

added theorem Real.logb_lt_iff_lt_rpow_of_base_lt_one

added theorem Real.logb_lt_logb

added theorem Real.logb_lt_logb_iff

added theorem Real.logb_lt_logb_iff_of_base_lt_one

added theorem Real.logb_lt_logb_of_base_lt_one

added theorem Real.logb_mul

added theorem Real.logb_ne_zero_of_pos_of_ne_one

added theorem Real.logb_ne_zero_of_pos_of_ne_one_of_base_lt_one

added theorem Real.logb_neg

added theorem Real.logb_neg_eq_logb

added theorem Real.logb_neg_iff

added theorem Real.logb_neg_iff_of_base_lt_one

added theorem Real.logb_neg_of_base_lt_one

added theorem Real.logb_nonneg

added theorem Real.logb_nonneg_iff

added theorem Real.logb_nonneg_iff_of_base_lt_one

added theorem Real.logb_nonneg_of_base_lt_one

added theorem Real.logb_nonpos

added theorem Real.logb_nonpos_iff'

added theorem Real.logb_nonpos_iff

added theorem Real.logb_nonpos_iff_of_base_lt_one

added theorem Real.logb_one

added theorem Real.logb_pos

added theorem Real.logb_pos_iff

added theorem Real.logb_pos_iff_of_base_lt_one

added theorem Real.logb_pos_of_base_lt_one

added theorem Real.logb_prod

added theorem Real.logb_rpow

added theorem Real.logb_surjective

added theorem Real.logb_zero

added theorem Real.lt_logb_iff_rpow_lt

added theorem Real.lt_logb_iff_rpow_lt_of_base_lt_one

added theorem Real.range_logb

added theorem Real.rpow_logb

added theorem Real.rpow_logb_eq_abs

added theorem Real.rpow_logb_of_neg

added theorem Real.strictAntiOn_logb

added theorem Real.strictAntiOn_logb_of_base_lt_one

added theorem Real.strictMonoOn_logb

added theorem Real.strictMonoOn_logb_of_base_lt_one

added theorem Real.surjOn_logb'

added theorem Real.surjOn_logb

added theorem Real.tendsto_logb_atTop

added theorem Real.tendsto_logb_atTop_of_base_lt_one