feat: add induction principle for intervals (#8350)

This PR adds an induction principle that says that if a proposition `P` is true on `[x₀, r * x₀)` and if `P` for `[x₀, r^n * x₀)` implies `P` for `[r^n * x₀, r^(n+1) * x₀)`, then `P` is true for all `x ≥ x₀`.

It also adds a few missing lemmas about `logb`.



Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>

Mathlib/Analysis/SpecialFunctions/Log/Base.lean

@@ -53,6 +53,13 @@ theorem logb_zero : logb b 0 = 0 := by simp [logb]
 theorem logb_one : logb b 1 = 0 := by simp [logb]
 #align real.logb_one Real.logb_one
 
+@[simp]
+lemma logb_self_eq_one (hb : 1 < b) : logb b b = 1 :=
+   div_self (log_pos hb).ne'
+
+lemma logb_self_eq_one_iff : logb b b = 1 ↔ b ≠ 0 ∧ b ≠ 1 ∧ b ≠ -1 :=
+  Iff.trans ⟨fun h h' => by simp [logb, h'] at h, div_self⟩ log_ne_zero
+
 @[simp]
 theorem logb_abs (x : ℝ) : logb b |x| = logb b x := by rw [logb, logb, log_abs]
 #align real.logb_abs Real.logb_abs
@@ -178,6 +185,11 @@ theorem logb_le_logb (h : 0 < x) (h₁ : 0 < y) : logb b x ≤ logb b y ↔ x 
   rw [logb, logb, div_le_div_right (log_pos hb), log_le_log h h₁]
 #align real.logb_le_logb Real.logb_le_logb
 
+@[gcongr]
+theorem logb_le_logb_of_le (h : 0 < x) (hxy : x ≤ y) : logb b x ≤ logb b y :=
+  (logb_le_logb hb h (by linarith)).mpr hxy
+
+@[gcongr]
 theorem logb_lt_logb (hx : 0 < x) (hxy : x < y) : logb b x < logb b y := by
   rw [logb, logb, div_lt_div_right (log_pos hb)]
   exact log_lt_log hx hxy
@@ -427,3 +439,29 @@ theorem logb_prod {α : Type*} (s : Finset α) (f : α → ℝ) (hf : ∀ x ∈
 #align real.logb_prod Real.logb_prod
 
 end Real
+
+section Induction
+
+/-- Induction principle for intervals of real numbers: if a proposition `P` is true
+on `[x₀, r * x₀)` and if `P` for `[x₀, r^n * x₀)` implies `P` for `[r^n * x₀, r^(n+1) * x₀)`,
+then `P` is true for all `x ≥ x₀`. -/
+lemma Real.induction_Ico_mul {P : ℝ → Prop} (x₀ r : ℝ) (hr : 1 < r) (hx₀ : 0 < x₀)
+    (base : ∀ x ∈ Set.Ico x₀ (r * x₀), P x)
+    (step : ∀ n : ℕ, n ≥ 1 → (∀ z ∈ Set.Ico x₀ (r ^ n * x₀), P z) →
+      (∀ z ∈ Set.Ico (r ^ n * x₀) (r ^ (n+1) * x₀), P z)) :
+    ∀ x ≥ x₀, P x := by
+  suffices : ∀ n : ℕ, ∀ x ∈ Set.Ico x₀ (r ^ (n + 1) * x₀), P x
+  · intro x hx
+    have hx' : 0 < x / x₀ := div_pos (hx₀.trans_le hx) hx₀
+    refine this ⌊logb r (x / x₀)⌋₊ x ?_
+    rw [mem_Ico, ←div_lt_iff hx₀, ←logb_lt_iff_lt_rpow hr hx']
+    exact ⟨hx, Nat.lt_floor_add_one _⟩
+  intro n
+  induction n
+  case zero => simpa using base
+  case succ n ih =>
+    specialize step (n + 1) (by simp)
+    simp only [Nat.cast_add_one] at step ⊢
+    exact fun x hx => (Ico_subset_Ico_union_Ico hx).elim (ih x) (step ih _)
+
+end Induction