-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
/-- The main proof of the upper bound part of the Akra-Bazzi theorem. The factor
`1 - ε n` does not change the asymptotic order, but is needed for the induction step to go
through. -/
lemma T_isBigO_smoothingFn_mul_asympBound :
    T =O[atTop] (fun n => (1 - ε n) * asympBound g a b n)

Proof state:
case bc.h.h.a0
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
c₁ : ℝ
hc₁ : c₁ > 0
h_sumTransform_aux : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * g ↑n ≤ sumTransform (p a b) g (r i n) n
n₀ : ℕ
n₀_ge_Rn₀ : R.n₀ ≤ n₀
h_smoothing_pos : ∀ (y : ℕ), n₀ ≤ y → 0 < 1 - ε ↑y
h_smoothing_gt_half : ∀ (y : ℕ), n₀ ≤ y → 1 / 2 < 1 - ε ↑y
h_asympBound_pos : ∀ (y : ℕ), n₀ ≤ y → 0 < asympBound g a b y
h_asympBound_r_pos : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), 0 < asympBound g a b (r i y)
h_asympBound_floor : ∀ (y : ℕ), ⌊b' * ↑n₀⌋₊ ≤ y → 0 < asympBound g a b y
n₀_pos : 0 < n₀
h_smoothing_r_pos : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), 0 < 1 - ε ↑(r i y)
bound1 : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), ↑(r i y) ^ p a b * (1 - ε ↑(r i y)) ≤ b i ^ p a b * ↑y ^ p a b * (1 - ε ↑y)
h_smoothingFn_floor : ∀ (y : ℕ), ⌊b' * ↑n₀⌋₊ ≤ y → 0 < 1 - ε ↑y
h_sumTransform : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), c₁ * g ↑y ≤ sumTransform (p a b) g (r i y) y
h_bi_le_r : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), b (min_bi b) / 2 * ↑y ≤ ↑(r i y)
h_base_nonempty : (Ico ⌊b (min_bi b) / 2 * ↑n₀⌋₊ n₀).Nonempty
base_max : ℝ := (Ico ⌊b' * ↑n₀⌋₊ n₀).sup' h_base_nonempty fun n => T n / ((1 - ε ↑n) * asympBound g a b n)
C : ℝ := 2 * c₁⁻¹ ⊔ base_max
hC : C = 2 * c₁⁻¹ ⊔ base_max
h_base : ∀ n ∈ Ico ⌊b' * ↑n₀⌋₊ n₀, T n ≤ C * ((1 - ε ↑n) * asympBound g a b n)
n : ℕ
h_ind : ∀ m < n, m ≥ n₀ → 0 < asympBound g a b m → 0 < 1 - ε ↑m → T m ≤ C * ((1 - ε ↑m) * asympBound g a b m)
hn : n ≥ n₀
h_asympBound_pos' : 0 < asympBound g a b n
h_one_sub_smoothingFn_pos' : 0 < 1 - ε ↑n
b_mul_n₀_le_ri : ∀ (i : α), ⌊b' * ↑n₀⌋₊ ≤ r i n
g_pos : 0 ≤ g ↑n
i : α
a✝ : i ∈ univ
⊢ 0 ≤ 1 + ∑ u ∈ range (r i n), g ↑u / ↑u ^ (p a b + 1)

Tactic:
refine add_nonneg zero_le_one <| Finset.sum_nonneg fun j _ => ?_

Result:
case bc.h.h.a0
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
c₁ : ℝ
hc₁ : c₁ > 0
h_sumTransform_aux : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * g ↑n ≤ sumTransform (p a b) g (r i n) n
n₀ : ℕ
n₀_ge_Rn₀ : R.n₀ ≤ n₀
h_smoothing_pos : ∀ (y : ℕ), n₀ ≤ y → 0 < 1 - ε ↑y
h_smoothing_gt_half : ∀ (y : ℕ), n₀ ≤ y → 1 / 2 < 1 - ε ↑y
h_asympBound_pos : ∀ (y : ℕ), n₀ ≤ y → 0 < asympBound g a b y
h_asympBound_r_pos : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), 0 < asympBound g a b (r i y)
h_asympBound_floor : ∀ (y : ℕ), ⌊b' * ↑n₀⌋₊ ≤ y → 0 < asympBound g a b y
n₀_pos : 0 < n₀
h_smoothing_r_pos : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), 0 < 1 - ε ↑(r i y)
bound1 : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), ↑(r i y) ^ p a b * (1 - ε ↑(r i y)) ≤ b i ^ p a b * ↑y ^ p a b * (1 - ε ↑y)
h_smoothingFn_floor : ∀ (y : ℕ), ⌊b' * ↑n₀⌋₊ ≤ y → 0 < 1 - ε ↑y
h_sumTransform : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), c₁ * g ↑y ≤ sumTransform (p a b) g (r i y) y
h_bi_le_r : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), b (min_bi b) / 2 * ↑y ≤ ↑(r i y)
h_base_nonempty : (Ico ⌊b (min_bi b) / 2 * ↑n₀⌋₊ n₀).Nonempty
base_max : ℝ := (Ico ⌊b' * ↑n₀⌋₊ n₀).sup' h_base_nonempty fun n => T n / ((1 - ε ↑n) * asympBound g a b n)
C : ℝ := 2 * c₁⁻¹ ⊔ base_max
hC : C = 2 * c₁⁻¹ ⊔ base_max
h_base : ∀ n ∈ Ico ⌊b' * ↑n₀⌋₊ n₀, T n ≤ C * ((1 - ε ↑n) * asympBound g a b n)
n : ℕ
h_ind : ∀ m < n, m ≥ n₀ → 0 < asympBound g a b m → 0 < 1 - ε ↑m → T m ≤ C * ((1 - ε ↑m) * asympBound g a b m)
hn : n ≥ n₀
h_asympBound_pos' : 0 < asympBound g a b n
h_one_sub_smoothingFn_pos' : 0 < 1 - ε ↑n
b_mul_n₀_le_ri : ∀ (i : α), ⌊b' * ↑n₀⌋₊ ≤ r i n
g_pos : 0 ≤ g ↑n
i : α
a✝ : i ∈ univ
j : ℕ
x✝ : j ∈ range (r i n)
⊢ 0 ≤ g ↑j / ↑j ^ (p a b + 1)

Proof state:
case bc
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
c₁ : ℝ
hc₁ : c₁ > 0
h_sumTransform_aux : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * g ↑n ≤ sumTransform (p a b) g (r i n) n
n₀ : ℕ
n₀_ge_Rn₀ : R.n₀ ≤ n₀
h_smoothing_pos : ∀ (y : ℕ), n₀ ≤ y → 0 < 1 - ε ↑y
h_smoothing_gt_half : ∀ (y : ℕ), n₀ ≤ y → 1 / 2 < 1 - ε ↑y
h_asympBound_pos : ∀ (y : ℕ), n₀ ≤ y → 0 < asympBound g a b y
h_asympBound_r_pos : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), 0 < asympBound g a b (r i y)
h_asympBound_floor : ∀ (y : ℕ), ⌊b' * ↑n₀⌋₊ ≤ y → 0 < asympBound g a b y
n₀_pos : 0 < n₀
h_smoothing_r_pos : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), 0 < 1 - ε ↑(r i y)
bound1 : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), ↑(r i y) ^ p a b * (1 - ε ↑(r i y)) ≤ b i ^ p a b * ↑y ^ p a b * (1 - ε ↑y)
h_smoothingFn_floor : ∀ (y : ℕ), ⌊b' * ↑n₀⌋₊ ≤ y → 0 < 1 - ε ↑y
h_sumTransform : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), c₁ * g ↑y ≤ sumTransform (p a b) g (r i y) y
h_bi_le_r : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), b (min_bi b) / 2 * ↑y ≤ ↑(r i y)
h_base_nonempty : (Ico ⌊b (min_bi b) / 2 * ↑n₀⌋₊ n₀).Nonempty
base_max : ℝ := (Ico ⌊b' * ↑n₀⌋₊ n₀).sup' h_base_nonempty fun n => T n / ((1 - ε ↑n) * asympBound g a b n)
C : ℝ := 2 * c₁⁻¹ ⊔ base_max
hC : C = 2 * c₁⁻¹ ⊔ base_max
h_base : ∀ n ∈ Ico ⌊b' * ↑n₀⌋₊ n₀, T n ≤ C * ((1 - ε ↑n) * asympBound g a b n)
n : ℕ
h_ind : ∀ m < n, m ≥ n₀ → 0 < asympBound g a b m → 0 < 1 - ε ↑m → T m ≤ C * ((1 - ε ↑m) * asympBound g a b m)
hn : n ≥ n₀
h_asympBound_pos' : 0 < asympBound g a b n
h_one_sub_smoothingFn_pos' : 0 < 1 - ε ↑n
b_mul_n₀_le_ri : ∀ (i : α), ⌊b' * ↑n₀⌋₊ ≤ r i n
g_pos : 0 ≤ g ↑n
⊢ (1 - C * c₁ * (1 - ε ↑n)) * g ↑n ≤ 0

Tactic:
refine mul_nonpos_of_nonpos_of_nonneg ?_ g_pos

Result:
case bc
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
c₁ : ℝ
hc₁ : c₁ > 0
h_sumTransform_aux : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * g ↑n ≤ sumTransform (p a b) g (r i n) n
n₀ : ℕ
n₀_ge_Rn₀ : R.n₀ ≤ n₀
h_smoothing_pos : ∀ (y : ℕ), n₀ ≤ y → 0 < 1 - ε ↑y
h_smoothing_gt_half : ∀ (y : ℕ), n₀ ≤ y → 1 / 2 < 1 - ε ↑y
h_asympBound_pos : ∀ (y : ℕ), n₀ ≤ y → 0 < asympBound g a b y
h_asympBound_r_pos : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), 0 < asympBound g a b (r i y)
h_asympBound_floor : ∀ (y : ℕ), ⌊b' * ↑n₀⌋₊ ≤ y → 0 < asympBound g a b y
n₀_pos : 0 < n₀
h_smoothing_r_pos : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), 0 < 1 - ε ↑(r i y)
bound1 : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), ↑(r i y) ^ p a b * (1 - ε ↑(r i y)) ≤ b i ^ p a b * ↑y ^ p a b * (1 - ε ↑y)
h_smoothingFn_floor : ∀ (y : ℕ), ⌊b' * ↑n₀⌋₊ ≤ y → 0 < 1 - ε ↑y
h_sumTransform : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), c₁ * g ↑y ≤ sumTransform (p a b) g (r i y) y
h_bi_le_r : ∀ (y : ℕ), n₀ ≤ y → ∀ (i : α), b (min_bi b) / 2 * ↑y ≤ ↑(r i y)
h_base_nonempty : (Ico ⌊b (min_bi b) / 2 * ↑n₀⌋₊ n₀).Nonempty
base_max : ℝ := (Ico ⌊b' * ↑n₀⌋₊ n₀).sup' h_base_nonempty fun n => T n / ((1 - ε ↑n) * asympBound g a b n)
C : ℝ := 2 * c₁⁻¹ ⊔ base_max
hC : C = 2 * c₁⁻¹ ⊔ base_max
h_base : ∀ n ∈ Ico ⌊b' * ↑n₀⌋₊ n₀, T n ≤ C * ((1 - ε ↑n) * asympBound g a b n)
n : ℕ
h_ind : ∀ m < n, m ≥ n₀ → 0 < asympBound g a b m → 0 < 1 - ε ↑m → T m ≤ C * ((1 - ε ↑m) * asympBound g a b m)
hn : n ≥ n₀
h_asympBound_pos' : 0 < asympBound g a b n
h_one_sub_smoothingFn_pos' : 0 < 1 - ε ↑n
b_mul_n₀_le_ri : ∀ (i : α), ⌊b' * ↑n₀⌋₊ ≤ r i n
g_pos : 0 ≤ g ↑n
⊢ 1 - C * c₁ * (1 - ε ↑n) ≤ 0