English
The map r ↦ log_b(r) is monotone increasing in r; more precisely, if 0 < r1 ≤ r2, then log_b(r1) ≤ log_b(r2.
Русский
Функция r ↦ log_b(r) монотонно возрастает; если 0 < r1 ≤ r2, то log_b(r1) ≤ log_b(r2).
LaTeX
$$$0 < r_1 \wedge r_1 \le r_2 \ \Rightarrow\ log_b r_1 \le log_b r_2$$$
Lean4
@[mono, gcongr]
theorem log_mono_right {b : ℕ} {r₁ r₂ : R} (h₀ : 0 < r₁) (h : r₁ ≤ r₂) : log b r₁ ≤ log b r₂ :=
by
rcases le_total r₁ 1 with h₁ | h₁ <;> rcases le_total r₂ 1 with h₂ | h₂
· have h₀' : 0 < r₂ := lt_of_lt_of_le h₀ h
rw [log_of_right_le_one _ h₁, log_of_right_le_one _ h₂, neg_le_neg_iff, Nat.cast_le]
exact Nat.clog_mono_right b <| Nat.ceil_mono <| (inv_le_inv₀ h₀' h₀).2 h
· rw [log_of_right_le_one _ h₁, log_of_one_le_right _ h₂]
exact (neg_nonpos.mpr (Int.natCast_nonneg _)).trans (Int.natCast_nonneg _)
· obtain rfl := le_antisymm h (h₂.trans h₁)
rfl
· rw [log_of_one_le_right _ h₁, log_of_one_le_right _ h₂, Nat.cast_le]
exact Nat.log_mono_right (Nat.floor_mono h)
