-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
lemma eventually_bi_mul_le_r : ∀ᶠ (n : ℕ) in atTop, ∀ i, (b (min_bi b) / 2) * n ≤ r i n

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
gt_zero : 0 < b (min_bi b)
hlo : (fun n => ↑n / log ↑n ^ 2) =o[atTop] fun n => ↑n
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)

Tactic:
rw [Asymptotics.isLittleO_iff] at hlo

Result:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
gt_zero : 0 < b (min_bi b)
hlo : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ c * ‖↑x‖
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
gt_zero : 0 < b (min_bi b)
hlo : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ c * ‖↑x‖
hlo' : ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ b (min_bi b) / 2 * ‖↑x‖
n : ℕ
hn' : ∀ (i : α), b i * ↑n - ↑n / log ↑n ^ 2 ≤ ↑(r i n)
i : α
hn : ‖↑n / log ↑n ^ 2‖ ≤ b (min_bi b) / 2 * ↑n
⊢ b (min_bi b) * ↑n - b (min_bi b) / 2 * ↑n ≤ b (min_bi b) * ↑n - ‖↑n / log ↑n ^ 2‖

Tactic:
gcongr

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
gt_zero : 0 < b (min_bi b)
hlo : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ c * ‖↑x‖
hlo' : ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ b (min_bi b) / 2 * ‖↑x‖
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)

Tactic:
filter_upwards [hlo', R.eventually_b_le_r] with n hn hn'

Result:
case h
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
gt_zero : 0 < b (min_bi b)
hlo : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ c * ‖↑x‖
hlo' : ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ b (min_bi b) / 2 * ‖↑x‖
n : ℕ
hn : ‖↑n / log ↑n ^ 2‖ ≤ b (min_bi b) / 2 * ‖↑n‖
hn' : ∀ (i : α), b i * ↑n - ↑n / log ↑n ^ 2 ≤ ↑(r i n)
⊢ ∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)

Proof state:
case h
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
gt_zero : 0 < b (min_bi b)
hlo : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ c * ‖↑x‖
hlo' : ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ b (min_bi b) / 2 * ‖↑x‖
n : ℕ
hn' : ∀ (i : α), b i * ↑n - ↑n / log ↑n ^ 2 ≤ ↑(r i n)
i : α
hn : ‖↑n / log ↑n ^ 2‖ ≤ b (min_bi b) / 2 * ↑n
⊢ b (min_bi b) / 2 * ↑n ≤ ↑(r i n)

Tactic:
calc b (min_bi b) / 2 * n = b (min_bi b) * n - b (min_bi b) / 2 * n := by ring
                        _ ≤ b (min_bi b) * n - ‖n / log n ^ 2‖ := by gcongr
                        _ ≤ b i * n - ‖n / log n ^ 2‖ := by gcongr; aesop
                        _ = b i * n - n / log n ^ 2 := by
                              congr
                              exact Real.norm_of_nonneg <| by positivity
                        _ ≤ r i n := hn' i

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
gt_zero : 0 < b (min_bi b)
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)

Tactic:
have hlo := isLittleO_self_div_log_id

Result:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
gt_zero : 0 < b (min_bi b)
hlo : (fun n => ↑n / log ↑n ^ 2) =o[atTop] fun n => ↑n
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
gt_zero : 0 < b (min_bi b)
hlo : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ c * ‖↑x‖
hlo' : ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ b (min_bi b) / 2 * ‖↑x‖
n : ℕ
hn' : ∀ (i : α), b i * ↑n - ↑n / log ↑n ^ 2 ≤ ↑(r i n)
i : α
hn : ‖↑n / log ↑n ^ 2‖ ≤ b (min_bi b) / 2 * ↑n
⊢ b (min_bi b) / 2 * ↑n = b (min_bi b) * ↑n - b (min_bi b) / 2 * ↑n

Tactic:
ring

Result:
no goals