-- 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:
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
⊢ f ↑n ≤ (↑n₀ * (logb ↑n₀ ↑n + 1)) ^ (↑k)⁻¹ * ↑k ^ (↑k)⁻¹

Tactic:
have : 0 ≤ logb n₀ n := logb_nonneg (one_lt_cast.mpr hn₀) (mod_cast Nat.one_le_of_lt h₀.bot_lt)

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
k : ℕ
hk : 0 < k
this : 0 ≤ logb ↑n₀ ↑n
⊢ f ↑n ≤ (↑n₀ * (logb ↑n₀ ↑n + 1)) ^ (↑k)⁻¹ * ↑k ^ (↑k)⁻¹

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₀ * (↑k * logb ↑n₀ ↑n + 1)) ^ (↑k)⁻¹ ≤ (↑n₀ * (↑k * logb ↑n₀ ↑n + ↑k)) ^ (↑k)⁻¹

Tactic:
gcongr

Result:
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

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
⊢ f ↑n ≤ 1

Tactic:
refine le_of_tendsto_of_tendsto tendsto_const_nhds ?_ (eventually_atTop.mpr ⟨1, h_ineq2⟩)

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)

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

Tactic:
simp only [List.mapIdx_eq_zipIdx_map, List.map_map]

Result:
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

Proof state:
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)

Tactic:
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, List.map_map]
  refine List.sum_le_sum fun ⟨i, a⟩ _ ↦ ?_
  simp only [Function.comp_apply, Function.uncurry_apply_pair]
  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₀ (not_eq_zero_of_lt hm), Nat.cast_add_one]
  simp +contextual
_ ≤ n₀ * (logb n₀ m + 1) := by gcongr; exact natLog_le_logb ..

Result:
no goals

Proof state:
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n : ℕ
⊢ f ↑n ≤ 1

Tactic:
have h_ineq1 {m : ℕ} (hm : 1 ≤ m) : f m ≤ n₀ * (logb n₀ m + 1) := by
  
  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, List.map_map]
    refine List.sum_le_sum fun ⟨i, a⟩ _ ↦ ?_
    simp only [Function.comp_apply, Function.uncurry_apply_pair]
    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₀ (not_eq_zero_of_lt hm), Nat.cast_add_one]
    simp +contextual
  _ ≤ n₀ * (logb n₀ m + 1) := by gcongr; exact natLog_le_logb ..

Result:
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

Proof state:
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
n₀ : ℕ
hn₀ : 1 < n₀
⊢ 1 < f ↑n₀

Tactic:
contrapose! notbdd with h

Result:
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
⊢ ∀ (n : ℕ), f ↑n ≤ 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
⊢ f ↑n = f ↑(n ^ k) ^ (↑k)⁻¹

Tactic:
rw [Nat.cast_pow, map_pow, ← rpow_natCast, rpow_rpow_inv (by positivity) (by 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 ≤ f ↑n₀

Tactic:
positivity

Result:
no goals

Proof state:
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
⊢ ∀ (n : ℕ), f ↑n ≤ 1

Tactic:
intro n

Result:
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n : ℕ
⊢ f ↑n ≤ 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
⊢ f ↑n ≤ (↑n₀ * (logb ↑n₀ ↑n + 1)) ^ (↑k)⁻¹ * ↑k ^ (↑k)⁻¹

Tactic:
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:
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
⊢ 0 ≤ ↑n₀ * (logb ↑n₀ ↑n + 1)

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)
h₀ : n ≠ 0
h_ineq2 : ∀ (k : ℕ), 0 < k → f ↑n ≤ (↑n₀ * (logb ↑n₀ ↑n + 1)) ^ (↑k)⁻¹ * ↑k ^ (↑k)⁻¹
h₁ : n ≠ 1
⊢ 1 < n

Tactic:
omega

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
⊢ ↑n₀ * f ↑n₀ ^ a ≤ ↑n₀

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

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
⊢ 0 ≤ f ↑n

Tactic:
positivity

Result:
no goals

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
this : 0 < logb ↑n₀ ↑n
⊢ Tendsto (fun b => (↑n₀ * (logb ↑n₀ ↑n + 1)) ^ (↑b)⁻¹ * ↑b ^ (↑b)⁻¹) atTop (𝓝 (1 * 1))

Tactic:
exact (tendsto_const_rpow_inv (by positivity)).mul tendsto_nat_rpow_inv

Result:
no goals