-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
@[aesop safe apply] lemma T_pos (n : ℕ) : 0 < T n

Proof state:
case ind.inl
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
h_ind : ∀ m < n, 0 < T m
hn : n < R.n₀
⊢ 0 < T n

Tactic:
exact R.T_gt_zero' n hn

Result:
no goals

Proof state:
case ind
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
h_ind : ∀ m < n, 0 < T m
⊢ 0 < T n

Tactic:
cases lt_or_le n R.n₀ with
| inl hn => exact R.T_gt_zero' n hn | inr hn => rw [R.h_rec n hn]
  have := R.g_nonneg
  refine add_pos_of_pos_of_nonneg (Finset.sum_pos ?sum_elems univ_nonempty) (by aesop)
  exact fun i _ => mul_pos (R.a_pos i) <| h_ind _ (R.r_lt_n i _ hn)

Result:
no goals

Proof state:
case ind.inr
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
h_ind : ∀ m < n, 0 < T m
hn : R.n₀ ≤ n
⊢ 0 < T n

Tactic:
rw [R.h_rec n hn]

Result:
case ind.inr
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
h_ind : ∀ m < n, 0 < T m
hn : R.n₀ ≤ n
⊢ 0 < ∑ i : α, a i * T (r i n) + g ↑n

Proof state:
case sum_elems
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
h_ind : ∀ m < n, 0 < T m
hn : R.n₀ ≤ n
this : ∀ x ≥ 0, 0 ≤ g x
⊢ ∀ i ∈ univ, 0 < a i * T (r i n)

Tactic:
exact fun i _ => mul_pos (R.a_pos i) <| h_ind _ (R.r_lt_n i _ hn)

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
⊢ 0 < T n

Tactic:
induction n using Nat.strongRecOn with
| ind n h_ind =>
  cases lt_or_le n R.n₀ with
  | inl hn => exact R.T_gt_zero' n hn | inr hn => rw [R.h_rec n hn]
    have := R.g_nonneg
    refine add_pos_of_pos_of_nonneg (Finset.sum_pos ?sum_elems univ_nonempty) (by aesop)
    exact fun i _ => mul_pos (R.a_pos i) <| h_ind _ (R.r_lt_n i _ hn)

Result:
no goals

Proof state:
case ind.inr
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
h_ind : ∀ m < n, 0 < T m
hn : R.n₀ ≤ n
this : ∀ x ≥ 0, 0 ≤ g x
⊢ 0 < ∑ i : α, a i * T (r i n) + g ↑n

Tactic:
refine add_pos_of_pos_of_nonneg (Finset.sum_pos ?sum_elems univ_nonempty) (by aesop)

Result:
case sum_elems
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
h_ind : ∀ m < n, 0 < T m
hn : R.n₀ ≤ n
this : ∀ x ≥ 0, 0 ≤ g x
⊢ ∀ i ∈ univ, 0 < a i * T (r i n)

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
h_ind : ∀ m < n, 0 < T m
hn : R.n₀ ≤ n
this : ∀ x ≥ 0, 0 ≤ g x
⊢ 0 ≤ g ↑n

Tactic:
aesop

Result:
no goals

Proof state:
case ind.inr
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
h_ind : ∀ m < n, 0 < T m
hn : R.n₀ ≤ n
⊢ 0 < ∑ i : α, a i * T (r i n) + g ↑n

Tactic:
have := R.g_nonneg

Result:
case ind.inr
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
h_ind : ∀ m < n, 0 < T m
hn : R.n₀ ≤ n
this : ∀ x ≥ 0, 0 ≤ g x
⊢ 0 < ∑ i : α, a i * T (r i n) + g ↑n