-- Mathlib/NumberTheory/Ostrowski.lean
/-- If `f n > 1` for some `n` then `f n > 1` for all `n ≥ 2` -/
lemma one_lt_of_not_bounded (notbdd : ¬ ∀ n : ℕ, f n ≤ 1) {n₀ : ℕ} (hn₀ : 1 < n₀) : 1 < f n₀

Proof state:
case inl
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
h_ineq1 : ∀ {m : ℕ}, 1 ≤ m → f ↑m ≤ ↑n₀ * (logb ↑n₀ ↑m + 1)
⊢ f ↑0 ≤ 1

Tactic:
simp

Result:
no goals

Proof state:
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n : ℕ
h_ineq1 : ∀ {m : ℕ}, 1 ≤ m → f ↑m ≤ ↑n₀ * (logb ↑n₀ ↑m + 1)
h₀ : n ≠ 0
h_ineq2 : ∀ (k : ℕ), 0 < k → f ↑n ≤ (↑n₀ * (logb ↑n₀ ↑n + 1)) ^ (↑k)⁻¹ * ↑k ^ (↑k)⁻¹
h₁ : n ≠ 1
this : 0 < logb ↑n₀ ↑n
⊢ 0 < ↑n₀ * (logb ↑n₀ ↑n + 1)

Tactic:
positivity

Result:
no goals

Proof state:
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n m : ℕ
hm : 1 ≤ m
L : List ℕ := n₀.digits m
x✝¹ : ℕ × ℕ
i a : ℕ
x✝ : (i, a) ∈ L.zipIdx
⊢ 0 ≤ ↑n₀

Tactic:
positivity

Result:
no goals

Proof state:
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n m : ℕ
hm : 1 ≤ m
⊢ f ↑m ≤ ↑n₀ * (logb ↑n₀ ↑m + 1)

Tactic:
set L := Nat.digits n₀ m

Result:
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n m : ℕ
hm : 1 ≤ m
L : List ℕ := n₀.digits m
⊢ f ↑m ≤ ↑n₀ * (logb ↑n₀ ↑m + 1)

Proof state:
case h.bc
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n m : ℕ
hm : 1 ≤ m
L : List ℕ := n₀.digits m
⊢ ↑(Nat.log n₀ m) ≤ logb ↑n₀ ↑m

Tactic:
exact natLog_le_logb ..

Result:
no goals

Proof state:
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n m : ℕ
hm : 1 ≤ m
L : List ℕ := n₀.digits m
⊢ (List.map (fun x => ↑n₀ * f ↑n₀ ^ x.2) L.zipIdx).sum ≤ (List.map (fun x => ↑n₀) L.zipIdx).sum

Tactic:
refine List.sum_le_sum fun ⟨i, a⟩ _ ↦ ?_

Result:
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n m : ℕ
hm : 1 ≤ m
L : List ℕ := n₀.digits m
x✝¹ : ℕ × ℕ
i a : ℕ
x✝ : (i, a) ∈ L.zipIdx
⊢ ↑n₀ * f ↑n₀ ^ (i, a).2 ≤ ↑n₀

Proof state:
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n : ℕ
h_ineq1 : ∀ {m : ℕ}, 1 ≤ m → f ↑m ≤ ↑n₀ * (logb ↑n₀ ↑m + 1)
h₀ : n ≠ 0
k : ℕ
hk : 0 < k
this : 0 ≤ logb ↑n₀ ↑n
⊢ (↑n₀ * (logb ↑n₀ ↑(n ^ k) + 1)) ^ (↑k)⁻¹ = (↑n₀ * (↑k * logb ↑n₀ ↑n + 1)) ^ (↑k)⁻¹

Tactic:
rw [Nat.cast_pow, logb_pow]

Result:
no goals

Proof state:
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n m : ℕ
hm : 1 ≤ m
L : List ℕ := n₀.digits m
⊢ ∀
    b ∈
      List.map
        (fun x =>
          match x with
          | (a, i) => ↑n₀)
        L.zipIdx,
    b = ↑n₀

Tactic:
simp +contextual

Result:
no goals

Proof state:
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n : ℕ
h_ineq1 : ∀ {m : ℕ}, 1 ≤ m → f ↑m ≤ ↑n₀ * (logb ↑n₀ ↑m + 1)
h₀ : n ≠ 0
k : ℕ
hk : 0 < k
this : 0 ≤ logb ↑n₀ ↑n
⊢ f ↑(n ^ k) ^ (↑k)⁻¹ ≤ (↑n₀ * (logb ↑n₀ ↑(n ^ k) + 1)) ^ (↑k)⁻¹

Tactic:
gcongr

Result:
case h₁
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n : ℕ
h_ineq1 : ∀ {m : ℕ}, 1 ≤ m → f ↑m ≤ ↑n₀ * (logb ↑n₀ ↑m + 1)
h₀ : n ≠ 0
k : ℕ
hk : 0 < k
this : 0 ≤ logb ↑n₀ ↑n
⊢ f ↑(n ^ k) ≤ ↑n₀ * (logb ↑n₀ ↑(n ^ k) + 1)

Proof state:
case h₁.h.bc
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n : ℕ
h_ineq1 : ∀ {m : ℕ}, 1 ≤ m → f ↑m ≤ ↑n₀ * (logb ↑n₀ ↑m + 1)
h₀ : n ≠ 0
k : ℕ
hk : 0 < k
this : 0 ≤ logb ↑n₀ ↑n
⊢ 1 ≤ ↑k

Tactic:
exact one_le_cast.mpr hk

Result:
no goals

Proof state:
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n : ℕ
h_ineq1 : ∀ {m : ℕ}, 1 ≤ m → f ↑m ≤ ↑n₀ * (logb ↑n₀ ↑m + 1)
h₀ : n ≠ 0
k : ℕ
hk : 0 < k
this : 0 ≤ logb ↑n₀ ↑n
⊢ ↑k ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n : ℕ
h_ineq1 : ∀ {m : ℕ}, 1 ≤ m → f ↑m ≤ ↑n₀ * (logb ↑n₀ ↑m + 1)
⊢ f ↑n ≤ 1

Tactic:
rcases eq_or_ne n 0 with rfl | h₀

Result:
case inl
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
h_ineq1 : ∀ {m : ℕ}, 1 ≤ m → f ↑m ≤ ↑n₀ * (logb ↑n₀ ↑m + 1)
⊢ f ↑0 ≤ 1

case inr
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n : ℕ
h_ineq1 : ∀ {m : ℕ}, 1 ≤ m → f ↑m ≤ ↑n₀ * (logb ↑n₀ ↑m + 1)
h₀ : n ≠ 0
⊢ f ↑n ≤ 1

Proof state:
case inr.inr
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n : ℕ
h_ineq1 : ∀ {m : ℕ}, 1 ≤ m → f ↑m ≤ ↑n₀ * (logb ↑n₀ ↑m + 1)
h₀ : n ≠ 0
h_ineq2 : ∀ (k : ℕ), 0 < k → f ↑n ≤ (↑n₀ * (logb ↑n₀ ↑n + 1)) ^ (↑k)⁻¹ * ↑k ^ (↑k)⁻¹
h₁ : n ≠ 1
⊢ Tendsto (fun b => (↑n₀ * (logb ↑n₀ ↑n + 1)) ^ (↑b)⁻¹ * ↑b ^ (↑b)⁻¹) atTop (𝓝 (1 * 1))

Tactic:
have : 0 < logb n₀ n := logb_pos (mod_cast hn₀) (by norm_cast; omega)

Result:
case inr.inr
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n : ℕ
h_ineq1 : ∀ {m : ℕ}, 1 ≤ m → f ↑m ≤ ↑n₀ * (logb ↑n₀ ↑m + 1)
h₀ : n ≠ 0
h_ineq2 : ∀ (k : ℕ), 0 < k → f ↑n ≤ (↑n₀ * (logb ↑n₀ ↑n + 1)) ^ (↑k)⁻¹ * ↑k ^ (↑k)⁻¹
h₁ : n ≠ 1
this : 0 < logb ↑n₀ ↑n
⊢ Tendsto (fun b => (↑n₀ * (logb ↑n₀ ↑n + 1)) ^ (↑b)⁻¹ * ↑b ^ (↑b)⁻¹) atTop (𝓝 (1 * 1))

Proof state:
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n : ℕ
h_ineq1 : ∀ {m : ℕ}, 1 ≤ m → f ↑m ≤ ↑n₀ * (logb ↑n₀ ↑m + 1)
h₀ : n ≠ 0
h_ineq2 : ∀ (k : ℕ), 0 < k → f ↑n ≤ (↑n₀ * (logb ↑n₀ ↑n + 1)) ^ (↑k)⁻¹ * ↑k ^ (↑k)⁻¹
h₁ : n ≠ 1
⊢ 1 < ↑n

Tactic:
norm_cast

Result:
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n : ℕ
h_ineq1 : ∀ {m : ℕ}, 1 ≤ m → f ↑m ≤ ↑n₀ * (logb ↑n₀ ↑m + 1)
h₀ : n ≠ 0
h_ineq2 : ∀ (k : ℕ), 0 < k → f ↑n ≤ (↑n₀ * (logb ↑n₀ ↑n + 1)) ^ (↑k)⁻¹ * ↑k ^ (↑k)⁻¹
h₁ : n ≠ 1
⊢ 1 < n

Proof state:
case inr.inr
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n : ℕ
h_ineq1 : ∀ {m : ℕ}, 1 ≤ m → f ↑m ≤ ↑n₀ * (logb ↑n₀ ↑m + 1)
h₀ : n ≠ 0
h_ineq2 : ∀ (k : ℕ), 0 < k → f ↑n ≤ (↑n₀ * (logb ↑n₀ ↑n + 1)) ^ (↑k)⁻¹ * ↑k ^ (↑k)⁻¹
h₁ : n ≠ 1
⊢ Tendsto (fun b => (↑n₀ * (logb ↑n₀ ↑n + 1)) ^ (↑b)⁻¹ * ↑b ^ (↑b)⁻¹) atTop (𝓝 1)

Tactic:
nth_rw 2 [← mul_one 1]

Result:
case inr.inr
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n : ℕ
h_ineq1 : ∀ {m : ℕ}, 1 ≤ m → f ↑m ≤ ↑n₀ * (logb ↑n₀ ↑m + 1)
h₀ : n ≠ 0
h_ineq2 : ∀ (k : ℕ), 0 < k → f ↑n ≤ (↑n₀ * (logb ↑n₀ ↑n + 1)) ^ (↑k)⁻¹ * ↑k ^ (↑k)⁻¹
h₁ : n ≠ 1
⊢ Tendsto (fun b => (↑n₀ * (logb ↑n₀ ↑n + 1)) ^ (↑b)⁻¹ * ↑b ^ (↑b)⁻¹) atTop (𝓝 (1 * 1))

Proof state:
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n : ℕ
h_ineq1 : ∀ {m : ℕ}, 1 ≤ m → f ↑m ≤ ↑n₀ * (logb ↑n₀ ↑m + 1)
h₀ : n ≠ 0
k : ℕ
hk : 0 < k
this : 0 ≤ logb ↑n₀ ↑n
⊢ 0 ≤ ↑k

Tactic:
positivity

Result:
no goals

Proof state:
case inr
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n : ℕ
h_ineq1 : ∀ {m : ℕ}, 1 ≤ m → f ↑m ≤ ↑n₀ * (logb ↑n₀ ↑m + 1)
h₀ : n ≠ 0
⊢ f ↑n ≤ 1

Tactic:
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 : ℝ)]

Result:
case inr
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n : ℕ
h_ineq1 : ∀ {m : ℕ}, 1 ≤ m → f ↑m ≤ ↑n₀ * (logb ↑n₀ ↑m + 1)
h₀ : n ≠ 0
h_ineq2 : ∀ (k : ℕ), 0 < k → f ↑n ≤ (↑n₀ * (logb ↑n₀ ↑n + 1)) ^ (↑k)⁻¹ * ↑k ^ (↑k)⁻¹
⊢ f ↑n ≤ 1

Proof state:
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n m : ℕ
hm : 1 ≤ m
L : List ℕ := n₀.digits m
x✝¹ : ℕ × ℕ
i a : ℕ
x✝ : (i, a) ∈ L.zipIdx
⊢ 0 ≤ f ↑n₀ ^ a

Tactic:
positivity

Result:
no goals