English
For n,m>1, f(n) ≤ f(m)^{log_b m n}.
Русский
Для n,m>1 верно f(n) ≤ f(m)^{log_b m n}.
LaTeX
$$f(n) ≤ f(m)^{\\log_b m n}$$
Lean4
/-- If `f n > 1` for some `n` then `f n > 1` for all `n ≥ 2` -/
theorem one_lt_of_not_bounded (notbdd : ¬∀ n : ℕ, f n ≤ 1) {n₀ : ℕ} (hn₀ : 1 < n₀) : 1 < f n₀ :=
by
contrapose! notbdd with h
intro n
have h_ineq1 {m : ℕ} (hm : 1 ≤ m) : f m ≤ n₀ * (logb n₀ m + 1) := by
/- L is the string of digits of `n` in the base `n₀` -/
set L := Nat.digits n₀ m
calc
f m ≤ (L.mapIdx fun i _ ↦ n₀ * f n₀ ^ i).sum := apply_le_sum_digits m hn₀
_ ≤ (L.mapIdx fun _ _ ↦ (n₀ : ℝ)).sum :=
by
simp only [List.mapIdx_eq_zipIdx_map]
refine List.sum_le_sum fun ⟨i, a⟩ _ ↦ ?_
simp only
exact
(mul_le_mul_of_nonneg_right (mod_cast le_refl n₀) (by positivity)).trans <|
mul_le_of_le_one_right (by positivity) (pow_le_one₀ (by positivity) h)
_ = n₀ * (Nat.log n₀ m + 1) :=
by
rw [List.mapIdx_eq_zipIdx_map, List.eq_replicate_of_mem (a := (n₀ : ℝ)) (l := L.zipIdx.map _),
List.sum_replicate, List.length_map, List.length_zipIdx, nsmul_eq_mul, mul_comm,
Nat.digits_len n₀ m hn₀ (ne_zero_of_lt hm), Nat.cast_add_one]
simp +contextual
_ ≤ n₀ * (logb n₀ m + 1) := by gcongr;
exact
natLog_le_logb ..
-- For h_ineq2 we need to exclude the case n = 0.
rcases eq_or_ne n 0 with rfl | h₀
· simp
have h_ineq2 (k : ℕ) (hk : 0 < k) : f n ≤ (n₀ * (logb n₀ n + 1)) ^ (k : ℝ)⁻¹ * k ^ (k : ℝ)⁻¹ :=
by
have : 0 ≤ logb n₀ n := logb_nonneg (one_lt_cast.mpr hn₀) (mod_cast Nat.one_le_of_lt h₀.bot_lt)
calc
f n = (f ↑(n ^ k)) ^ (k : ℝ)⁻¹ := by
rw [Nat.cast_pow, map_pow, ← rpow_natCast, rpow_rpow_inv (by positivity) (by positivity)]
_ ≤ (n₀ * (logb n₀ ↑(n ^ k) + 1)) ^ (k : ℝ)⁻¹ := by
gcongr
exact h_ineq1 <| one_le_pow₀ (one_le_iff_ne_zero.mpr h₀)
_ = (n₀ * (k * logb n₀ n + 1)) ^ (k : ℝ)⁻¹ := by rw [Nat.cast_pow, logb_pow]
_ ≤ (n₀ * (k * logb n₀ n + k)) ^ (k : ℝ)⁻¹ := by
gcongr
exact one_le_cast.mpr hk
_ = (n₀ * (logb n₀ n + 1)) ^ (k : ℝ)⁻¹ * k ^ (k : ℝ)⁻¹ := by
rw [← mul_rpow (by positivity) (by positivity), mul_assoc, add_mul, one_mul, mul_comm _ (k : ℝ)]
-- For 0 < logb n₀ n below we also need to exclude n = 1.
rcases eq_or_ne n 1 with rfl | h₁
· simp
refine le_of_tendsto_of_tendsto tendsto_const_nhds ?_ (eventually_atTop.mpr ⟨1, h_ineq2⟩)
nth_rw 2 [← mul_one 1]
have : 0 < logb n₀ n := logb_pos (mod_cast hn₀) (by norm_cast; cutsat)
exact (tendsto_const_rpow_inv (by positivity)).mul tendsto_nat_rpow_inv
