Theorem: continuous_LSeries_aux (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : Summable (nterm f σ')
l1 : ∀ (i : ℕ), Continuous fun x => term f (↑σ' + ↑x * I) i
l2 : ∀ (n : ℕ) (x : ℝ), ‖term f (↑σ' + ↑x * I) n‖ = nterm f σ' n
⊢ Continuous fun x => LSeries f (↑σ' + ↑x * I)
Tactic:
exact continuous_tsum l1 hf (fun n x => le_of_eq (l2 n x))
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : Summable (nterm f σ')
i : ℕ
⊢ Continuous fun x => term f (↑σ' + ↑x * I) i
Tactic:
by_cases h : i = 0
State after:
case pos
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : Summable (nterm f σ')
i : ℕ
h : i = 0
⊢ Continuous fun x => term f (↑σ' + ↑x * I) i

case neg
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : Summable (nterm f σ')
i : ℕ
h : ¬i = 0
⊢ Continuous fun x => term f (↑σ' + ↑x * I) i

State before:
case pos
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : Summable (nterm f σ')
i : ℕ
h : i = 0
⊢ Continuous fun x => term f (↑σ' + ↑x * I) i
Tactic:
simpa [h] using continuous_const
State after:
no goals

State before:
case neg
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : Summable (nterm f σ')
i : ℕ
h : ¬i = 0
⊢ Continuous fun x => term f (↑σ' + ↑x * I) i
Tactic:
simpa [h] using continuous_const.div (continuous_const.cpow (by continuity) (by simp [h])) (fun x => by simp [h])
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : Summable (nterm f σ')
i : ℕ
h : ¬i = 0
⊢ Continuous fun x => ↑σ' + ↑x * I
Tactic:
continuity
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : Summable (nterm f σ')
i : ℕ
h : ¬i = 0
⊢ ℝ → ↑i ∈ slitPlane
Tactic:
simp [h]
State after:
no goals

State before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : Summable (nterm f σ')
i : ℕ
h : ¬i = 0
x : ℝ
⊢ ↑i ^ (↑σ' + ↑x * I) ≠ 0
Tactic:
simp [h]
State after:
no goals

State before:
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : Summable (nterm f σ')
l1 : ∀ (i : ℕ), Continuous fun x => term f (↑σ' + ↑x * I) i
n : ℕ
x : ℝ
⊢ ‖term f (↑σ' + ↑x * I) n‖ = nterm f σ' n
Tactic:
by_cases h : n = 0
State after:
case pos
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : Summable (nterm f σ')
l1 : ∀ (i : ℕ), Continuous fun x => term f (↑σ' + ↑x * I) i
n : ℕ
x : ℝ
h : n = 0
⊢ ‖term f (↑σ' + ↑x * I) n‖ = nterm f σ' n

case neg
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : Summable (nterm f σ')
l1 : ∀ (i : ℕ), Continuous fun x => term f (↑σ' + ↑x * I) i
n : ℕ
x : ℝ
h : ¬n = 0
⊢ ‖term f (↑σ' + ↑x * I) n‖ = nterm f σ' n

State before:
case pos
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : Summable (nterm f σ')
l1 : ∀ (i : ℕ), Continuous fun x => term f (↑σ' + ↑x * I) i
n : ℕ
x : ℝ
h : n = 0
⊢ ‖term f (↑σ' + ↑x * I) n‖ = nterm f σ' n
Tactic:
simp [h, nterm]
State after:
no goals

State before:
case neg
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : Summable (nterm f σ')
l1 : ∀ (i : ℕ), Continuous fun x => term f (↑σ' + ↑x * I) i
n : ℕ
x : ℝ
h : ¬n = 0
⊢ ‖term f (↑σ' + ↑x * I) n‖ = nterm f σ' n
Tactic:
field_simp [h, nterm, cpow_add _ _ (Nat.cast_ne_zero.mpr h)]
State after:
case neg
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : Summable (nterm f σ')
l1 : ∀ (i : ℕ), Continuous fun x => term f (↑σ' + ↑x * I) i
n : ℕ
x : ℝ
h : ¬n = 0
⊢ Complex.abs (↑n ^ (↑x * I)) = 1 ∨ f n = 0

State before:
case neg
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : Summable (nterm f σ')
l1 : ∀ (i : ℕ), Continuous fun x => term f (↑σ' + ↑x * I) i
n : ℕ
x : ℝ
h : ¬n = 0
⊢ Complex.abs (↑n ^ (↑x * I)) = 1 ∨ f n = 0
Tactic:
rw [← Complex.norm_eq_abs, Complex.norm_natCast_cpow_of_pos (Nat.pos_of_ne_zero h)]
State after:
case neg
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : Summable (nterm f σ')
l1 : ∀ (i : ℕ), Continuous fun x => term f (↑σ' + ↑x * I) i
n : ℕ
x : ℝ
h : ¬n = 0
⊢ ↑n ^ (↑x * I).re = 1 ∨ f n = 0

State before:
case neg
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : Summable (nterm f σ')
l1 : ∀ (i : ℕ), Continuous fun x => term f (↑σ' + ↑x * I) i
n : ℕ
x : ℝ
h : ¬n = 0
⊢ ↑n ^ (↑x * I).re = 1 ∨ f n = 0
Tactic:
simp
State after:
no goals