-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
lemma tendsto_atTop_sumCoeffsExp : Tendsto (fun (p : ℝ) => ∑ i, a i * (b i) ^ p) atBot atTop

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
h₁✝ : Tendsto (fun p => a (max_bi b) * b (max_bi b) ^ p) atBot atTop
p : ℝ
i : α
x✝ : i ∈ univ
h₁ : 0 < a i
h₂ : 0 < b i
⊢ 0 ≤ (fun i => a i * b i ^ p) i

Tactic:
positivity

Result:
no goals

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

Tactic:
linarith

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ Tendsto (fun p => a (max_bi b)) atBot (𝓝 (a (max_bi b)))

Tactic:
simp

Result:
no goals

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

Tactic:
have := R.b_pos (max_bi b)

Result:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
this : 0 < b (max_bi b)
⊢ 0 < b (max_bi b)

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
h₁ : Tendsto (fun p => a (max_bi b) * b (max_bi b) ^ p) atBot atTop
p : ℝ
⊢ a (max_bi b) * b (max_bi b) ^ p ≤ ∑ i : α, a i * b i ^ p

Tactic:
refine Finset.single_le_sum (f := fun i => (a i : ℝ) * b i ^ p) (fun i _ => ?_) (mem_univ _)

Result:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
h₁ : Tendsto (fun p => a (max_bi b) * b (max_bi b) ^ p) atBot atTop
p : ℝ
i : α
x✝ : i ∈ univ
⊢ 0 ≤ (fun i => a i * b i ^ p) i

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
h₁ : Tendsto (fun p => a (max_bi b) * b (max_bi b) ^ p) atBot atTop
p : ℝ
i : α
x✝ : i ∈ univ
⊢ 0 ≤ (fun i => a i * b i ^ p) i

Tactic:
have h₁ : 0 < a i := R.a_pos i

Result:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
h₁✝ : Tendsto (fun p => a (max_bi b) * b (max_bi b) ^ p) atBot atTop
p : ℝ
i : α
x✝ : i ∈ univ
h₁ : 0 < a i
⊢ 0 ≤ (fun i => a i * b i ^ p) i

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ Tendsto (fun p => ∑ i : α, a i * b i ^ p) atBot atTop

Tactic:
have h₁ : Tendsto (fun p : ℝ => (a (max_bi b) : ℝ) * b (max_bi b) ^ p) atBot atTop :=
  Tendsto.mul_atTop (R.a_pos (max_bi b)) (by simp)
    <| tendsto_rpow_atBot_of_base_lt_one _
    (by have := R.b_pos (max_bi b); linarith) (R.b_lt_one _)

Result:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
h₁ : Tendsto (fun p => a (max_bi b) * b (max_bi b) ^ p) atBot atTop
⊢ Tendsto (fun p => ∑ i : α, a i * b i ^ p) atBot atTop

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
h₁✝ : Tendsto (fun p => a (max_bi b) * b (max_bi b) ^ p) atBot atTop
p : ℝ
i : α
x✝ : i ∈ univ
h₁ : 0 < a i
⊢ 0 ≤ (fun i => a i * b i ^ p) i

Tactic:
have h₂ : 0 < b i := R.b_pos i

Result:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
h₁✝ : Tendsto (fun p => a (max_bi b) * b (max_bi b) ^ p) atBot atTop
p : ℝ
i : α
x✝ : i ∈ univ
h₁ : 0 < a i
h₂ : 0 < b i
⊢ 0 ≤ (fun i => a i * b i ^ p) i

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
h₁ : Tendsto (fun p => a (max_bi b) * b (max_bi b) ^ p) atBot atTop
⊢ Tendsto (fun p => ∑ i : α, a i * b i ^ p) atBot atTop

Tactic:
refine tendsto_atTop_mono (fun p => ?_) h₁

Result:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
h₁ : Tendsto (fun p => a (max_bi b) * b (max_bi b) ^ p) atBot atTop
p : ℝ
⊢ a (max_bi b) * b (max_bi b) ^ p ≤ ∑ i : α, a i * b i ^ p