Feat(Log/Base): Adding 3 theorems related to Real.logb (#12110)

Mathlib/Analysis/SpecialFunctions/Log/Base.lean

@@ -113,6 +113,12 @@ theorem div_logb {a b c : ℝ} (h₁ : c ≠ 0) (h₂ : c ≠ 1) (h₃ : c ≠ -
   div_div_div_cancel_left' _ _ <| log_ne_zero.mpr ⟨h₁, h₂, h₃⟩
 #align real.div_logb Real.div_logb
 
+theorem logb_rpow_eq_mul_logb_of_pos (hx : 0 < x) : logb b (x ^ y) = y * logb b x := by
+  rw [logb, log_rpow hx, logb, mul_div_assoc]
+
+theorem logb_pow {k : ℕ} (hx : 0 < x) : logb b (x ^ k) = k * logb b x := by
+  rw [← rpow_nat_cast, logb_rpow_eq_mul_logb_of_pos hx]
+
 section BPosAndNeOne
 
 variable (b_pos : 0 < b) (b_ne_one : b ≠ 1)
@@ -148,6 +154,11 @@ theorem rpow_logb_of_neg (hx : x < 0) : b ^ logb b x = -x := by
   exact abs_of_neg hx
 #align real.rpow_logb_of_neg Real.rpow_logb_of_neg
 
+theorem logb_eq_iff_rpow_eq (hy : 0 < y) : logb b y = x ↔ b ^ x = y := by
+  constructor <;> rintro rfl
+  · exact rpow_logb b_pos b_ne_one hy
+  · exact logb_rpow b_pos b_ne_one
+
 theorem surjOn_logb : SurjOn (logb b) (Ioi 0) univ := fun x _ =>
   ⟨rpow b x, rpow_pos_of_pos b_pos x, logb_rpow b_pos b_ne_one⟩
 #align real.surj_on_logb Real.surjOn_logb