feat(analysis/special_functions/log/base): add real.logb_mul_base (#…

…18979)

Add proof that states `logb (a * b) c = ((logb a c)⁻¹ + (logb b c)⁻¹)⁻¹`.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/analysis/special_functions/log/base.lean

@@ -55,6 +55,39 @@ by simp_rw [logb, log_div hx hy, sub_div]
 
 @[simp] lemma logb_inv (x : ℝ) : logb b (x⁻¹) = -logb b x := by simp [logb, neg_div]
 
+lemma inv_logb (a b : ℝ) : (logb a b)⁻¹ = logb b a := by simp_rw [logb, inv_div]
+
+theorem inv_logb_mul_base {a b : ℝ} (h₁ : a ≠ 0) (h₂ : b ≠ 0) (c : ℝ) :
+  (logb (a * b) c)⁻¹ = (logb a c)⁻¹ + (logb b c)⁻¹ :=
+by simp_rw inv_logb; exact logb_mul h₁ h₂
+
+theorem inv_logb_div_base {a b : ℝ} (h₁ : a ≠ 0) (h₂ : b ≠ 0) (c : ℝ) :
+  (logb (a / b) c)⁻¹ = (logb a c)⁻¹ - (logb b c)⁻¹ :=
+by simp_rw inv_logb; exact logb_div h₁ h₂
+
+theorem logb_mul_base {a b : ℝ} (h₁ : a ≠ 0) (h₂ : b ≠ 0) (c : ℝ) :
+  logb (a * b) c = ((logb a c)⁻¹ + (logb b c)⁻¹)⁻¹ :=
+by rw [←inv_logb_mul_base h₁ h₂ c, inv_inv]
+
+theorem logb_div_base {a b : ℝ} (h₁ : a ≠ 0) (h₂ : b ≠ 0) (c : ℝ) :
+  logb (a / b) c = ((logb a c)⁻¹ - (logb b c)⁻¹)⁻¹ :=
+by rw [←inv_logb_div_base h₁ h₂ c, inv_inv]
+
+theorem mul_logb {a b c : ℝ} (h₁ : b ≠ 0) (h₂ : b ≠ 1) (h₃ : b ≠ -1) :
+  logb a b * logb b c = logb a c :=
+begin
+  unfold logb,
+  rw [mul_comm, div_mul_div_cancel _ (log_ne_zero.mpr ⟨h₁, h₂, h₃⟩)],
+end
+
+theorem div_logb {a b c : ℝ} (h₁ : c ≠ 0) (h₂ : c ≠ 1) (h₃ : c ≠ -1) :
+  logb a c / logb b c = logb a b :=
+begin
+  unfold logb,
+  -- TODO: div_div_div_cancel_left is missing for `group_with_zero`,
+  rw [div_div_div_eq, mul_comm, mul_div_mul_right _ _ (log_ne_zero.mpr ⟨h₁, h₂, h₃⟩)],
+end
+
 section b_pos_and_ne_one
 
 variable (b_pos : 0 < b)

src/analysis/special_functions/log/basic.lean

@@ -196,6 +196,9 @@ begin
   { rintro (rfl|rfl|rfl); simp only [log_one, log_zero, log_neg_eq_log], }
 end
 
+lemma log_ne_zero {x : ℝ} : log x ≠ 0 ↔ x ≠ 0 ∧ x ≠ 1 ∧ x ≠ -1 :=
+by simpa only [not_or_distrib] using log_eq_zero.not
+
 @[simp] lemma log_pow (x : ℝ) (n : ℕ) : log (x ^ n) = n * log x :=
 begin
   induction n with n ih,