[GOAL]
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n => u n / ↑n)
n : ℕ
hn : n ≠ 0
⊢ Subadditive.lim h ≤ u n / ↑n
[PROOFSTEP]
rw [Subadditive.lim]
[GOAL]
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n => u n / ↑n)
n : ℕ
hn : n ≠ 0
⊢ sInf ((fun n => u n / ↑n) '' Ici 1) ≤ u n / ↑n
[PROOFSTEP]
exact csInf_le (hbdd.mono <| image_subset_range _ _) ⟨n, hn.bot_lt, rfl⟩
[GOAL]
u : ℕ → ℝ
h : Subadditive u
k n r : ℕ
⊢ u (k * n + r) ≤ ↑k * u n + u r
[PROOFSTEP]
induction k with
| zero => simp only [Nat.zero_eq, Nat.cast_zero, zero_mul, zero_add]; rfl
| succ k IH =>
  calc
    u ((k + 1) * n + r) = u (n + (k * n + r)) := by congr 1; ring
    _ ≤ u n + u (k * n + r) := (h _ _)
    _ ≤ u n + (k * u n + u r) := (add_le_add_left IH _)
    _ = (k + 1 : ℕ) * u n + u r := by simp; ring
[GOAL]
u : ℕ → ℝ
h : Subadditive u
k n r : ℕ
⊢ u (k * n + r) ≤ ↑k * u n + u r
[PROOFSTEP]
induction k with
| zero => simp only [Nat.zero_eq, Nat.cast_zero, zero_mul, zero_add]; rfl
| succ k IH =>
  calc
    u ((k + 1) * n + r) = u (n + (k * n + r)) := by congr 1; ring
    _ ≤ u n + u (k * n + r) := (h _ _)
    _ ≤ u n + (k * u n + u r) := (add_le_add_left IH _)
    _ = (k + 1 : ℕ) * u n + u r := by simp; ring
[GOAL]
case zero
u : ℕ → ℝ
h : Subadditive u
n r : ℕ
⊢ u (Nat.zero * n + r) ≤ ↑Nat.zero * u n + u r
[PROOFSTEP]

| zero => simp only [Nat.zero_eq, Nat.cast_zero, zero_mul, zero_add]; rfl
[GOAL]
case zero
u : ℕ → ℝ
h : Subadditive u
n r : ℕ
⊢ u (Nat.zero * n + r) ≤ ↑Nat.zero * u n + u r
[PROOFSTEP]
simp only [Nat.zero_eq, Nat.cast_zero, zero_mul, zero_add]
[GOAL]
case zero
u : ℕ → ℝ
h : Subadditive u
n r : ℕ
⊢ u r ≤ u r
[PROOFSTEP]
rfl
[GOAL]
case succ
u : ℕ → ℝ
h : Subadditive u
n r k : ℕ
IH : u (k * n + r) ≤ ↑k * u n + u r
⊢ u (Nat.succ k * n + r) ≤ ↑(Nat.succ k) * u n + u r
[PROOFSTEP]

| succ k IH =>
  calc
    u ((k + 1) * n + r) = u (n + (k * n + r)) := by congr 1; ring
    _ ≤ u n + u (k * n + r) := (h _ _)
    _ ≤ u n + (k * u n + u r) := (add_le_add_left IH _)
    _ = (k + 1 : ℕ) * u n + u r := by simp; ring
[GOAL]
case succ
u : ℕ → ℝ
h : Subadditive u
n r k : ℕ
IH : u (k * n + r) ≤ ↑k * u n + u r
⊢ u (Nat.succ k * n + r) ≤ ↑(Nat.succ k) * u n + u r
[PROOFSTEP]
calc
  u ((k + 1) * n + r) = u (n + (k * n + r)) := by congr 1; ring
  _ ≤ u n + u (k * n + r) := (h _ _)
  _ ≤ u n + (k * u n + u r) := (add_le_add_left IH _)
  _ = (k + 1 : ℕ) * u n + u r := by simp; ring
[GOAL]
u : ℕ → ℝ
h : Subadditive u
n r k : ℕ
IH : u (k * n + r) ≤ ↑k * u n + u r
⊢ u ((k + 1) * n + r) = u (n + (k * n + r))
[PROOFSTEP]
congr 1
[GOAL]
case e_a
u : ℕ → ℝ
h : Subadditive u
n r k : ℕ
IH : u (k * n + r) ≤ ↑k * u n + u r
⊢ (k + 1) * n + r = n + (k * n + r)
[PROOFSTEP]
ring
[GOAL]
u : ℕ → ℝ
h : Subadditive u
n r k : ℕ
IH : u (k * n + r) ≤ ↑k * u n + u r
⊢ u n + (↑k * u n + u r) = ↑(k + 1) * u n + u r
[PROOFSTEP]
simp
[GOAL]
u : ℕ → ℝ
h : Subadditive u
n r k : ℕ
IH : u (k * n + r) ≤ ↑k * u n + u r
⊢ u n + (↑k * u n + u r) = (↑k + 1) * u n + u r
[PROOFSTEP]
ring
[GOAL]
u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / ↑n < L
⊢ ∀ᶠ (p : ℕ) in atTop, u p / ↑p < L
[PROOFSTEP]
refine
  .atTop_of_arithmetic hn fun r _ =>
    ?_
      /- `(k * u n + u r) / (k * n + r)` tends to `u n / n < L`, hence
        `(k * u n + u r) / (k * n + r) < L` for sufficiently large `k`. -/
[GOAL]
u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / ↑n < L
r : ℕ
x✝ : r < n
⊢ ∀ᶠ (a : ℕ) in atTop, u (n * a + r) / ↑(n * a + r) < L
[PROOFSTEP]
have A : Tendsto (fun x : ℝ => (u n + u r / x) / (n + r / x)) atTop (𝓝 ((u n + 0) / (n + 0))) :=
  (tendsto_const_nhds.add <| tendsto_const_nhds.div_atTop tendsto_id).div
      (tendsto_const_nhds.add <| tendsto_const_nhds.div_atTop tendsto_id) <|
    by simpa
[GOAL]
u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / ↑n < L
r : ℕ
x✝ : r < n
⊢ ↑n + 0 ≠ 0
[PROOFSTEP]
simpa
[GOAL]
u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / ↑n < L
r : ℕ
x✝ : r < n
A : Tendsto (fun x => (u n + u r / x) / (↑n + ↑r / x)) atTop (𝓝 ((u n + 0) / (↑n + 0)))
⊢ ∀ᶠ (a : ℕ) in atTop, u (n * a + r) / ↑(n * a + r) < L
[PROOFSTEP]
have B : Tendsto (fun x => (x * u n + u r) / (x * n + r)) atTop (𝓝 (u n / n)) :=
  by
  rw [add_zero, add_zero] at A 
  refine A.congr' <| (eventually_ne_atTop 0).mono fun x hx => ?_
  simp only [(· ∘ ·), add_div' _ _ _ hx, div_div_div_cancel_right _ hx, mul_comm]
[GOAL]
u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / ↑n < L
r : ℕ
x✝ : r < n
A : Tendsto (fun x => (u n + u r / x) / (↑n + ↑r / x)) atTop (𝓝 ((u n + 0) / (↑n + 0)))
⊢ Tendsto (fun x => (x * u n + u r) / (x * ↑n + ↑r)) atTop (𝓝 (u n / ↑n))
[PROOFSTEP]
rw [add_zero, add_zero] at A 
[GOAL]
u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / ↑n < L
r : ℕ
x✝ : r < n
A : Tendsto (fun x => (u n + u r / x) / (↑n + ↑r / x)) atTop (𝓝 (u n / ↑n))
⊢ Tendsto (fun x => (x * u n + u r) / (x * ↑n + ↑r)) atTop (𝓝 (u n / ↑n))
[PROOFSTEP]
refine A.congr' <| (eventually_ne_atTop 0).mono fun x hx => ?_
[GOAL]
u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / ↑n < L
r : ℕ
x✝ : r < n
A : Tendsto (fun x => (u n + u r / x) / (↑n + ↑r / x)) atTop (𝓝 (u n / ↑n))
x : ℝ
hx : x ≠ 0
⊢ (u n + u r / x) / (↑n + ↑r / x) = (fun x => (x * u n + u r) / (x * ↑n + ↑r)) x
[PROOFSTEP]
simp only [(· ∘ ·), add_div' _ _ _ hx, div_div_div_cancel_right _ hx, mul_comm]
[GOAL]
u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / ↑n < L
r : ℕ
x✝ : r < n
A : Tendsto (fun x => (u n + u r / x) / (↑n + ↑r / x)) atTop (𝓝 ((u n + 0) / (↑n + 0)))
B : Tendsto (fun x => (x * u n + u r) / (x * ↑n + ↑r)) atTop (𝓝 (u n / ↑n))
⊢ ∀ᶠ (a : ℕ) in atTop, u (n * a + r) / ↑(n * a + r) < L
[PROOFSTEP]
refine
  ((B.comp tendsto_nat_cast_atTop_atTop).eventually (gt_mem_nhds hL)).mono fun k hk =>
    ?_
      /- Finally, we use an upper estimate on `u (k * n + r)` to get an estimate on
        `u (k * n + r) / (k * n + r)`. -/
[GOAL]
u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / ↑n < L
r : ℕ
x✝ : r < n
A : Tendsto (fun x => (u n + u r / x) / (↑n + ↑r / x)) atTop (𝓝 ((u n + 0) / (↑n + 0)))
B : Tendsto (fun x => (x * u n + u r) / (x * ↑n + ↑r)) atTop (𝓝 (u n / ↑n))
k : ℕ
hk : ((fun x => (x * u n + u r) / (x * ↑n + ↑r)) ∘ Nat.cast) k < L
⊢ u (n * k + r) / ↑(n * k + r) < L
[PROOFSTEP]
rw [mul_comm]
[GOAL]
u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / ↑n < L
r : ℕ
x✝ : r < n
A : Tendsto (fun x => (u n + u r / x) / (↑n + ↑r / x)) atTop (𝓝 ((u n + 0) / (↑n + 0)))
B : Tendsto (fun x => (x * u n + u r) / (x * ↑n + ↑r)) atTop (𝓝 (u n / ↑n))
k : ℕ
hk : ((fun x => (x * u n + u r) / (x * ↑n + ↑r)) ∘ Nat.cast) k < L
⊢ u (k * n + r) / ↑(k * n + r) < L
[PROOFSTEP]
refine lt_of_le_of_lt ?_ hk
[GOAL]
u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / ↑n < L
r : ℕ
x✝ : r < n
A : Tendsto (fun x => (u n + u r / x) / (↑n + ↑r / x)) atTop (𝓝 ((u n + 0) / (↑n + 0)))
B : Tendsto (fun x => (x * u n + u r) / (x * ↑n + ↑r)) atTop (𝓝 (u n / ↑n))
k : ℕ
hk : ((fun x => (x * u n + u r) / (x * ↑n + ↑r)) ∘ Nat.cast) k < L
⊢ u (k * n + r) / ↑(k * n + r) ≤ ((fun x => (x * u n + u r) / (x * ↑n + ↑r)) ∘ Nat.cast) k
[PROOFSTEP]
simp only [(· ∘ ·), ← Nat.cast_add, ← Nat.cast_mul]
[GOAL]
u : ℕ → ℝ
h : Subadditive u
L : ℝ
n : ℕ
hn : n ≠ 0
hL : u n / ↑n < L
r : ℕ
x✝ : r < n
A : Tendsto (fun x => (u n + u r / x) / (↑n + ↑r / x)) atTop (𝓝 ((u n + 0) / (↑n + 0)))
B : Tendsto (fun x => (x * u n + u r) / (x * ↑n + ↑r)) atTop (𝓝 (u n / ↑n))
k : ℕ
hk : ((fun x => (x * u n + u r) / (x * ↑n + ↑r)) ∘ Nat.cast) k < L
⊢ u (k * n + r) / ↑(k * n + r) ≤ (↑k * u n + u r) / ↑(k * n + r)
[PROOFSTEP]
exact div_le_div_of_le (Nat.cast_nonneg _) (h.apply_mul_add_le _ _ _)
[GOAL]
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n => u n / ↑n)
⊢ Tendsto (fun n => u n / ↑n) atTop (𝓝 (Subadditive.lim h))
[PROOFSTEP]
refine' tendsto_order.2 ⟨fun l hl => _, fun L hL => _⟩
[GOAL]
case refine'_1
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n => u n / ↑n)
l : ℝ
hl : l < Subadditive.lim h
⊢ ∀ᶠ (b : ℕ) in atTop, l < u b / ↑b
[PROOFSTEP]
refine' eventually_atTop.2 ⟨1, fun n hn => hl.trans_le (h.lim_le_div hbdd (zero_lt_one.trans_le hn).ne')⟩
[GOAL]
case refine'_2
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n => u n / ↑n)
L : ℝ
hL : L > Subadditive.lim h
⊢ ∀ᶠ (b : ℕ) in atTop, u b / ↑b < L
[PROOFSTEP]
obtain ⟨n, npos, hn⟩ : ∃ n : ℕ, 0 < n ∧ u n / n < L :=
  by
  rw [Subadditive.lim] at hL 
  rcases exists_lt_of_csInf_lt (by simp) hL with ⟨x, hx, xL⟩
  rcases(mem_image _ _ _).1 hx with ⟨n, hn, rfl⟩
  exact ⟨n, zero_lt_one.trans_le hn, xL⟩
[GOAL]
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n => u n / ↑n)
L : ℝ
hL : L > Subadditive.lim h
⊢ ∃ n, 0 < n ∧ u n / ↑n < L
[PROOFSTEP]
rw [Subadditive.lim] at hL 
[GOAL]
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n => u n / ↑n)
L : ℝ
hL : L > sInf ((fun n => u n / ↑n) '' Ici 1)
⊢ ∃ n, 0 < n ∧ u n / ↑n < L
[PROOFSTEP]
rcases exists_lt_of_csInf_lt (by simp) hL with ⟨x, hx, xL⟩
[GOAL]
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n => u n / ↑n)
L : ℝ
hL : L > sInf ((fun n => u n / ↑n) '' Ici 1)
⊢ Set.Nonempty ((fun n => u n / ↑n) '' Ici 1)
[PROOFSTEP]
simp
[GOAL]
case intro.intro
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n => u n / ↑n)
L : ℝ
hL : L > sInf ((fun n => u n / ↑n) '' Ici 1)
x : ℝ
hx : x ∈ (fun n => u n / ↑n) '' Ici 1
xL : x < L
⊢ ∃ n, 0 < n ∧ u n / ↑n < L
[PROOFSTEP]
rcases(mem_image _ _ _).1 hx with ⟨n, hn, rfl⟩
[GOAL]
case intro.intro.intro.intro
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n => u n / ↑n)
L : ℝ
hL : L > sInf ((fun n => u n / ↑n) '' Ici 1)
n : ℕ
hn : n ∈ Ici 1
hx : u n / ↑n ∈ (fun n => u n / ↑n) '' Ici 1
xL : u n / ↑n < L
⊢ ∃ n, 0 < n ∧ u n / ↑n < L
[PROOFSTEP]
exact ⟨n, zero_lt_one.trans_le hn, xL⟩
[GOAL]
case refine'_2.intro.intro
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n => u n / ↑n)
L : ℝ
hL : L > Subadditive.lim h
n : ℕ
npos : 0 < n
hn : u n / ↑n < L
⊢ ∀ᶠ (b : ℕ) in atTop, u b / ↑b < L
[PROOFSTEP]
exact h.eventually_div_lt_of_div_lt npos.ne' hn
