Theorem: dirichlet_test' (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℕ → ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hAb : atTop.BoundedAtFilter (shift (cumsum a) * b)
hbb : ∀ᶠ (n : ℕ) in atTop, b (n + 1) ≤ b n
h : Summable (shift (cumsum a) * nnabla b)
⊢ Summable (a * b)
Tactic:
have l1 : ∀ᶠ n in atTop, 0 ≤ (shift (cumsum a) * nnabla b) n := by
  filter_upwards [hbb] with n hb
  exact mul_nonneg (by simpa [shift] using Finset.sum_nonneg' ha) (sub_nonneg.mpr hb)
State after:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℕ → ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hAb : atTop.BoundedAtFilter (shift (cumsum a) * b)
hbb : ∀ᶠ (n : ℕ) in atTop, b (n + 1) ≤ b n
h : Summable (shift (cumsum a) * nnabla b)
l1 : ∀ᶠ (n : ℕ) in atTop, 0 ≤ (shift (cumsum a) * nnabla b) n
⊢ Summable (a * b)

State before:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℕ → ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hAb : atTop.BoundedAtFilter (shift (cumsum a) * b)
hbb : ∀ᶠ (n : ℕ) in atTop, b (n + 1) ≤ b n
h : Summable (shift (cumsum a) * nnabla b)
l1 : ∀ᶠ (n : ℕ) in atTop, 0 ≤ (shift (cumsum a) * nnabla b) n
⊢ Summable (a * b)
Tactic:
rw [summable_iff_bounded (mul_nonneg ha hb)]
State after:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℕ → ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hAb : atTop.BoundedAtFilter (shift (cumsum a) * b)
hbb : ∀ᶠ (n : ℕ) in atTop, b (n + 1) ≤ b n
h : Summable (shift (cumsum a) * nnabla b)
l1 : ∀ᶠ (n : ℕ) in atTop, 0 ≤ (shift (cumsum a) * nnabla b) n
⊢ atTop.BoundedAtFilter (cumsum (a * b))

State before:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℕ → ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hAb : atTop.BoundedAtFilter (shift (cumsum a) * b)
hbb : ∀ᶠ (n : ℕ) in atTop, b (n + 1) ≤ b n
h : Summable (shift (cumsum a) * nnabla b)
l1 : ∀ᶠ (n : ℕ) in atTop, 0 ≤ (shift (cumsum a) * nnabla b) n
⊢ atTop.BoundedAtFilter (cumsum (a * b))
Tactic:
rw [summable_iff_bounded' l1] at h
State after:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℕ → ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hAb : atTop.BoundedAtFilter (shift (cumsum a) * b)
hbb : ∀ᶠ (n : ℕ) in atTop, b (n + 1) ≤ b n
h : atTop.BoundedAtFilter (cumsum fun n => (shift (cumsum a) * nnabla b) n)
l1 : ∀ᶠ (n : ℕ) in atTop, 0 ≤ (shift (cumsum a) * nnabla b) n
⊢ atTop.BoundedAtFilter (cumsum (a * b))

State before:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℕ → ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hAb : atTop.BoundedAtFilter (shift (cumsum a) * b)
hbb : ∀ᶠ (n : ℕ) in atTop, b (n + 1) ≤ b n
h : atTop.BoundedAtFilter (cumsum fun n => (shift (cumsum a) * nnabla b) n)
l1 : ∀ᶠ (n : ℕ) in atTop, 0 ≤ (shift (cumsum a) * nnabla b) n
⊢ atTop.BoundedAtFilter (cumsum (a * b))
Tactic:
apply bounded_of_shift
State after:
case h
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℕ → ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hAb : atTop.BoundedAtFilter (shift (cumsum a) * b)
hbb : ∀ᶠ (n : ℕ) in atTop, b (n + 1) ≤ b n
h : atTop.BoundedAtFilter (cumsum fun n => (shift (cumsum a) * nnabla b) n)
l1 : ∀ᶠ (n : ℕ) in atTop, 0 ≤ (shift (cumsum a) * nnabla b) n
⊢ atTop.BoundedAtFilter (shift (cumsum (a * b)))

State before:
case h
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℕ → ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hAb : atTop.BoundedAtFilter (shift (cumsum a) * b)
hbb : ∀ᶠ (n : ℕ) in atTop, b (n + 1) ≤ b n
h : atTop.BoundedAtFilter (cumsum fun n => (shift (cumsum a) * nnabla b) n)
l1 : ∀ᶠ (n : ℕ) in atTop, 0 ≤ (shift (cumsum a) * nnabla b) n
⊢ atTop.BoundedAtFilter (shift (cumsum (a * b)))
Tactic:
simpa only [summation_by_parts'', sub_eq_add_neg, neg_cumsum, ← mul_neg, neg_nabla] using hAb.add h
State after:
no goals

State before:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℕ → ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hAb : atTop.BoundedAtFilter (shift (cumsum a) * b)
hbb : ∀ᶠ (n : ℕ) in atTop, b (n + 1) ≤ b n
h : Summable (shift (cumsum a) * nnabla b)
⊢ ∀ᶠ (n : ℕ) in atTop, 0 ≤ (shift (cumsum a) * nnabla b) n
Tactic:
filter_upwards [hbb] with n hb
State after:
case h
n✝ : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℕ → ℝ
ha : 0 ≤ a
hb✝ : 0 ≤ b
hAb : atTop.BoundedAtFilter (shift (cumsum a) * b)
hbb : ∀ᶠ (n : ℕ) in atTop, b (n + 1) ≤ b n
h : Summable (shift (cumsum a) * nnabla b)
n : ℕ
hb : b (n + 1) ≤ b n
⊢ 0 ≤ (shift (cumsum a) * nnabla b) n

State before:
case h
n✝ : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℕ → ℝ
ha : 0 ≤ a
hb✝ : 0 ≤ b
hAb : atTop.BoundedAtFilter (shift (cumsum a) * b)
hbb : ∀ᶠ (n : ℕ) in atTop, b (n + 1) ≤ b n
h : Summable (shift (cumsum a) * nnabla b)
n : ℕ
hb : b (n + 1) ≤ b n
⊢ 0 ≤ (shift (cumsum a) * nnabla b) n
Tactic:
exact mul_nonneg (by simpa [shift] using Finset.sum_nonneg' ha) (sub_nonneg.mpr hb)
State after:
no goals

State before:
n✝ : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℕ → ℝ
ha : 0 ≤ a
hb✝ : 0 ≤ b
hAb : atTop.BoundedAtFilter (shift (cumsum a) * b)
hbb : ∀ᶠ (n : ℕ) in atTop, b (n + 1) ≤ b n
h : Summable (shift (cumsum a) * nnabla b)
n : ℕ
hb : b (n + 1) ≤ b n
⊢ 0 ≤ shift (cumsum a) n
Tactic:
simpa [shift] using Finset.sum_nonneg' ha
State after:
no goals