induction_Ico_mul — Mathlib

English

An induction principle for intervals of the form [x0, r^n x0). If a property P holds on [x0, r x0) and, whenever it holds on [x0, r^n x0), it also holds on [r^n x0, r^{n+1} x0), then P holds for every x ≥ x0.

Русский

Принцип математической индукции по интервалам вида [x0, r^n x0). Если P верно на [x0, r x0) и если P верно на [x0, r^n x0) тогда P верно на [r^n x0, r^{n+1} x0), то P верна для всех x ≥ x0.

LaTeX

$$$\forall P:\\mathbb{R} \to \mathrm{Prop},\ (x_0,r\in \mathbb{R})\ (1

Lean4

/-- 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₀`. -/
theorem 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
    by
    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₀, ← rpow_natCast, ← logb_lt_iff_lt_rpow hr hx', Nat.cast_add, Nat.cast_one]
    exact ⟨hx, Nat.lt_floor_add_one _⟩
  intro n
  induction n with
  | zero => simpa using base
  | succ n ih => exact fun x hx => (Ico_subset_Ico_union_Ico hx).elim (ih x) (step (n + 1) (by simp) ih _)

Похожие утверждения