Theorem: cancel_main' (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hf0 : f 0 = 0
hg : 0 ≤ g
hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n
hg' : Antitone g
n : ℕ
⊢ cumsum (f * g) n ≤ C * cumsum g n
Tactic:
match n with
| 0 => simp [cumsum]
| 1 => specialize hg 0 ; specialize hf' 1 ; simp [cumsum, hf0] at hf' hg ⊢ ; positivity
| n + 2 => convert cancel_aux' hf hg hf' hg' (n + 2) using 1 ; simp [cumsum_succ] ; ring
State after:
no goals

State before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hf0 : f 0 = 0
hg : 0 ≤ g
hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n
hg' : Antitone g
n : ℕ
⊢ cumsum (f * g) 0 ≤ C * cumsum g 0
Tactic:
simp [cumsum]
State after:
no goals

State before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hf0 : f 0 = 0
hg : 0 ≤ g
hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n
hg' : Antitone g
n : ℕ
⊢ cumsum (f * g) 1 ≤ C * cumsum g 1
Tactic:
specialize hg 0
State after:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hf0 : f 0 = 0
hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n
hg' : Antitone g
n : ℕ
hg : 0 0 ≤ g 0
⊢ cumsum (f * g) 1 ≤ C * cumsum g 1

State before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hf0 : f 0 = 0
hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n
hg' : Antitone g
n : ℕ
hg : 0 0 ≤ g 0
⊢ cumsum (f * g) 1 ≤ C * cumsum g 1
Tactic:
specialize hf' 1
State after:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hf0 : f 0 = 0
hg' : Antitone g
n : ℕ
hg : 0 0 ≤ g 0
hf' : cumsum f 1 ≤ C * ↑1
⊢ cumsum (f * g) 1 ≤ C * cumsum g 1

State before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hf0 : f 0 = 0
hg' : Antitone g
n : ℕ
hg : 0 0 ≤ g 0
hf' : cumsum f 1 ≤ C * ↑1
⊢ cumsum (f * g) 1 ≤ C * cumsum g 1
Tactic:
simp [cumsum, hf0] at hf' hg ⊢
State after:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hf0 : f 0 = 0
hg' : Antitone g
n : ℕ
hg : 0 ≤ g 0
hf' : 0 ≤ C
⊢ 0 ≤ C * g 0

State before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hf0 : f 0 = 0
hg' : Antitone g
n : ℕ
hg : 0 ≤ g 0
hf' : 0 ≤ C
⊢ 0 ≤ C * g 0
Tactic:
positivity
State after:
no goals

State before:
n✝¹ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hf0 : f 0 = 0
hg : 0 ≤ g
hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n
hg' : Antitone g
n✝ n : ℕ
⊢ cumsum (f * g) (n + 2) ≤ C * cumsum g (n + 2)
Tactic:
convert cancel_aux' hf hg hf' hg' (n + 2) using 1
State after:
case h.e'_4
n✝¹ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hf0 : f 0 = 0
hg : 0 ≤ g
hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n
hg' : Antitone g
n✝ n : ℕ
⊢ C * cumsum g (n + 2) =
    C * ↑(n + 2) * g (n + 2 - 1) + C * cumsum g (n + 2 - 1 - 1 + 1) - C * (↑(n + 2 - 1 - 1) + 1) * g (n + 2 - 1)

State before:
case h.e'_4
n✝¹ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hf0 : f 0 = 0
hg : 0 ≤ g
hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n
hg' : Antitone g
n✝ n : ℕ
⊢ C * cumsum g (n + 2) =
    C * ↑(n + 2) * g (n + 2 - 1) + C * cumsum g (n + 2 - 1 - 1 + 1) - C * (↑(n + 2 - 1 - 1) + 1) * g (n + 2 - 1)
Tactic:
simp [cumsum_succ]
State after:
case h.e'_4
n✝¹ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hf0 : f 0 = 0
hg : 0 ≤ g
hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n
hg' : Antitone g
n✝ n : ℕ
⊢ C * (cumsum g n + g n + g (n + 1)) = C * (↑n + 2) * g (n + 1) + C * (cumsum g n + g n) - C * (↑n + 1) * g (n + 1)

State before:
case h.e'_4
n✝¹ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hf0 : f 0 = 0
hg : 0 ≤ g
hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n
hg' : Antitone g
n✝ n : ℕ
⊢ C * (cumsum g n + g n + g (n + 1)) = C * (↑n + 2) * g (n + 1) + C * (cumsum g n + g n) - C * (↑n + 1) * g (n + 1)
Tactic:
ring
State after:
no goals