English
If hb > 1, hv ≠ 0, and w < b^u, then log_b (b^u v + w) = u + log_b v when v ≠ 0.
Русский
Если hb > 1, hv ≠ 0 и w < b^u, то log_b (b^u v + w) = u + log_b v при v ≠ 0.
LaTeX
$$$ \log_b (b^u \cdot v + w) = u + \log_b v \quad\text{provided } hv \neq 0 \text{ and } w < b^u $$$
Lean4
theorem log_opow_mul_add {b u v w : Ordinal} (hb : 1 < b) (hv : v ≠ 0) (hw : w < b ^ u) :
log b (b ^ u * v + w) = u + log b v := by
rw [log_eq_iff hb]
· constructor
· rw [opow_add]
exact (mul_le_mul_left' (opow_log_le_self b hv) _).trans (le_add_right _ w)
· apply (add_lt_add_left hw _).trans_le
rw [← mul_succ, ← add_succ, opow_add]
apply mul_le_mul_left'
rw [succ_le_iff]
exact lt_opow_succ_log_self hb _
· exact fun h ↦ mul_ne_zero (opow_ne_zero u (bot_lt_of_lt hb).ne') hv <| left_eq_zero_of_add_eq_zero h
