Theorem: first_fourier (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
⊢ ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ (1 / (2 * π) * (↑n / x).log) =
    ∑' (n : ℕ), term f (↑σ') n * ∫ (v : ℝ), 𝐞 (-(v * (1 / (2 * π) * (↑n / x).log))) • ψ v
Tactic:
rfl
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
⊢ ∑' (n : ℕ), term f (↑σ') n * ∫ (v : ℝ), 𝐞 (-(v * (1 / (2 * π) * (↑n / x).log))) • ψ v =
    ∑' (n : ℕ), ∫ (v : ℝ), term f (↑σ') n * 𝐞 (-(v * (1 / (2 * π) * (↑n / x).log))) • ψ v
Tactic:
simp [integral_mul_left]
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
⊢ ∑' (n : ℕ), ∫ (v : ℝ), term f (↑σ') n * 𝐞 (-(v * (1 / (2 * π) * (↑n / x).log))) • ψ v =
    ∫ (v : ℝ), ∑' (n : ℕ), term f (↑σ') n * 𝐞 (-(v * (1 / (2 * π) * (↑n / x).log))) • ψ v
Tactic:
refine (integral_tsum ?_ ?_).symm
State after:
case refine_1
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
⊢ ∀ (i : ℕ), AEStronglyMeasurable (fun v => term f (↑σ') i * 𝐞 (-(v * (1 / (2 * π) * (↑i / x).log))) • ψ v) volume

case refine_2
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
⊢ ∑' (i : ℕ), ∫⁻ (a : ℝ), ↑‖term f (↑σ') i * 𝐞 (-(a * (1 / (2 * π) * (↑i / x).log))) • ψ a‖₊ ≠ ⊤

State before:
case refine_1
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
⊢ ∀ (i : ℕ), AEStronglyMeasurable (fun v => term f (↑σ') i * 𝐞 (-(v * (1 / (2 * π) * (↑i / x).log))) • ψ v) volume
Tactic:
refine fun _ ↦ Measurable.aestronglyMeasurable ?_
State after:
case refine_1
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
x✝ : ℕ
⊢ Measurable fun v => term f (↑σ') x✝ * 𝐞 (-(v * (1 / (2 * π) * (↑x✝ / x).log))) • ψ v

State before:
case refine_1
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
x✝ : ℕ
⊢ Measurable fun v => term f (↑σ') x✝ * 𝐞 (-(v * (1 / (2 * π) * (↑x✝ / x).log))) • ψ v
Tactic:
refine Measurable.mul (by fun_prop) ((Measurable.comp ?_ (by fun_prop)).smul (by fun_prop))
State after:
case refine_1
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
x✝ : ℕ
⊢ Measurable ⇑𝐞

State before:
case refine_1
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
x✝ : ℕ
⊢ Measurable ⇑𝐞
Tactic:
exact Continuous.measurable Real.continuous_fourierChar
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
x✝ : ℕ
⊢ Measurable fun v => term f (↑σ') x✝
Tactic:
fun_prop
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
x✝ : ℕ
⊢ Measurable fun v => -(v * (1 / (2 * π) * (↑x✝ / x).log))
Tactic:
fun_prop
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
x✝ : ℕ
⊢ Measurable fun v => ψ v
Tactic:
fun_prop
State after:
no goals

State before:
case refine_2
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
⊢ ∑' (i : ℕ), ∫⁻ (a : ℝ), ↑‖term f (↑σ') i * 𝐞 (-(a * (1 / (2 * π) * (↑i / x).log))) • ψ a‖₊ ≠ ⊤
Tactic:
simp_rw [nnnorm_mul]
State after:
case refine_2
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
⊢ ∑' (i : ℕ), ∫⁻ (a : ℝ), ↑(‖term f (↑σ') i‖₊ * ‖𝐞 (-(a * (1 / (2 * π) * (↑i / x).log))) • ψ a‖₊) ≠ ⊤

State before:
case refine_2
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
⊢ ∑' (i : ℕ), ∫⁻ (a : ℝ), ↑(‖term f (↑σ') i‖₊ * ‖𝐞 (-(a * (1 / (2 * π) * (↑i / x).log))) • ψ a‖₊) ≠ ⊤
Tactic:
push_cast
State after:
case refine_2
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
⊢ ∑' (i : ℕ), ∫⁻ (a : ℝ), ↑‖term f (↑σ') i‖₊ * ↑‖𝐞 (-(a * (1 / (2 * π) * (↑i / x).log))) • ψ a‖₊ ≠ ⊤

State before:
case refine_2
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
⊢ ∑' (i : ℕ), ∫⁻ (a : ℝ), ↑‖term f (↑σ') i‖₊ * ↑‖𝐞 (-(a * (1 / (2 * π) * (↑i / x).log))) • ψ a‖₊ ≠ ⊤
Tactic:
simp_rw [lintegral_const_mul _ (first_fourier_aux1 hcont _)]
State after:
case refine_2
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
⊢ ∑' (i : ℕ), ↑‖term f (↑σ') i‖₊ * ∫⁻ (a : ℝ), ↑‖𝐞 (-(a * (1 / (2 * π) * (↑i / x).log))) • ψ a‖₊ ∂volume ≠ ⊤

State before:
case refine_2
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
⊢ ∑' (i : ℕ), ↑‖term f (↑σ') i‖₊ * ∫⁻ (a : ℝ), ↑‖𝐞 (-(a * (1 / (2 * π) * (↑i / x).log))) • ψ a‖₊ ∂volume ≠ ⊤
Tactic:
calc
  _ = (∑' (i : ℕ), (‖term f σ' i‖₊ : ENNReal)) * ∫⁻ (a : ℝ), ‖ψ a‖₊ ∂volume := by
    simp [ENNReal.tsum_mul_right]
  _ ≠ ⊤ := ENNReal.mul_ne_top (hf_coe1 hf hσ)
    (ne_top_of_lt hsupp.2)
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
⊢ ∑' (i : ℕ), ↑‖term f (↑σ') i‖₊ * ∫⁻ (a : ℝ), ↑‖𝐞 (-(a * (1 / (2 * π) * (↑i / x).log))) • ψ a‖₊ ∂volume =
    (∑' (i : ℕ), ↑‖term f (↑σ') i‖₊) * ∫⁻ (a : ℝ), ↑‖ψ a‖₊
Tactic:
simp [ENNReal.tsum_mul_right]
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
⊢ ∫ (v : ℝ), ∑' (n : ℕ), term f (↑σ') n * 𝐞 (-(v * (1 / (2 * π) * (↑n / x).log))) • ψ v =
    ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ t * ↑x ^ (↑t * I)
Tactic:
congr 1
State after:
case e_f
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
⊢ (fun v => ∑' (n : ℕ), term f (↑σ') n * 𝐞 (-(v * (1 / (2 * π) * (↑n / x).log))) • ψ v) = fun t =>
    LSeries f (↑σ' + ↑t * I) * ψ t * ↑x ^ (↑t * I)

State before:
case e_f
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
⊢ (fun v => ∑' (n : ℕ), term f (↑σ') n * 𝐞 (-(v * (1 / (2 * π) * (↑n / x).log))) • ψ v) = fun t =>
    LSeries f (↑σ' + ↑t * I) * ψ t * ↑x ^ (↑t * I)
Tactic:
ext y
State after:
case e_f.h
n : ℕ
A a b c d u x y✝ t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
y : ℝ
⊢ ∑' (n : ℕ), term f (↑σ') n * 𝐞 (-(y * (1 / (2 * π) * (↑n / x).log))) • ψ y =
    LSeries f (↑σ' + ↑y * I) * ψ y * ↑x ^ (↑y * I)

State before:
case e_f.h
n : ℕ
A a b c d u x y✝ t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
y : ℝ
⊢ ∑' (n : ℕ), term f (↑σ') n * 𝐞 (-(y * (1 / (2 * π) * (↑n / x).log))) • ψ y =
    LSeries f (↑σ' + ↑y * I) * ψ y * ↑x ^ (↑y * I)
Tactic:
simp_rw [mul_assoc (LSeries _ _), ← smul_eq_mul (a := (LSeries _ _)), LSeries]
State after:
case e_f.h
n : ℕ
A a b c d u x y✝ t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
y : ℝ
⊢ ∑' (n : ℕ), term f (↑σ') n * 𝐞 (-(y * (1 / (2 * π) * (↑n / x).log))) • ψ y =
    (∑' (n : ℕ), term f (↑σ' + ↑y * I) n) • (ψ y * ↑x ^ (↑y * I))

State before:
case e_f.h
n : ℕ
A a b c d u x y✝ t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
y : ℝ
⊢ ∑' (n : ℕ), term f (↑σ') n * 𝐞 (-(y * (1 / (2 * π) * (↑n / x).log))) • ψ y =
    (∑' (n : ℕ), term f (↑σ' + ↑y * I) n) • (ψ y * ↑x ^ (↑y * I))
Tactic:
rw [← tsum_smul_const]
State after:
case e_f.h
n : ℕ
A a b c d u x y✝ t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
y : ℝ
⊢ ∑' (n : ℕ), term f (↑σ') n * 𝐞 (-(y * (1 / (2 * π) * (↑n / x).log))) • ψ y =
    ∑' (z : ℕ), term f (↑σ' + ↑y * I) z • (ψ y * ↑x ^ (↑y * I))

case e_f.h.hf
n : ℕ
A a b c d u x y✝ t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
y : ℝ
⊢ Summable fun n => term f (↑σ' + ↑y * I) n

State before:
case e_f.h
n : ℕ
A a b c d u x y✝ t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
y : ℝ
⊢ ∑' (n : ℕ), term f (↑σ') n * 𝐞 (-(y * (1 / (2 * π) * (↑n / x).log))) • ψ y =
    ∑' (z : ℕ), term f (↑σ' + ↑y * I) z • (ψ y * ↑x ^ (↑y * I))
Tactic:
congr with n
State after:
case e_f.h.e_f.h
n✝ : ℕ
A a b c d u x y✝ t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
y : ℝ
n : ℕ
⊢ term f (↑σ') n * 𝐞 (-(y * (1 / (2 * π) * (↑n / x).log))) • ψ y = term f (↑σ' + ↑y * I) n • (ψ y * ↑x ^ (↑y * I))

State before:
case e_f.h.e_f.h
n✝ : ℕ
A a b c d u x y✝ t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
y : ℝ
n : ℕ
⊢ term f (↑σ') n * 𝐞 (-(y * (1 / (2 * π) * (↑n / x).log))) • ψ y = term f (↑σ' + ↑y * I) n • (ψ y * ↑x ^ (↑y * I))
Tactic:
exact first_fourier_aux2 hx n
State after:
no goals

State before:
case e_f.h.hf
n : ℕ
A a b c d u x y✝ t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
y : ℝ
⊢ Summable fun n => term f (↑σ' + ↑y * I) n
Tactic:
apply Summable.of_norm
State after:
case e_f.h.hf.hf
n : ℕ
A a b c d u x y✝ t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
y : ℝ
⊢ Summable fun a => ‖term f (↑σ' + ↑y * I) a‖

State before:
case e_f.h.hf.hf
n : ℕ
A a b c d u x y✝ t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
y : ℝ
⊢ Summable fun a => ‖term f (↑σ' + ↑y * I) a‖
Tactic:
convert hf σ' hσ with n
State after:
case h.e'_5.h
n✝ : ℕ
A a b c d u x y✝ t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
y : ℝ
n : ℕ
⊢ ‖term f (↑σ' + ↑y * I) n‖ = nterm f σ' n

State before:
case h.e'_5.h
n✝ : ℕ
A a b c d u x y✝ t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
y : ℝ
n : ℕ
⊢ ‖term f (↑σ' + ↑y * 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 : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
y : ℝ
n : ℕ
h : n = 0
⊢ ‖term f (↑σ' + ↑y * 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 : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
y : ℝ
n : ℕ
h : ¬n = 0
⊢ ‖term f (↑σ' + ↑y * 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 : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
y : ℝ
n : ℕ
h : n = 0
⊢ ‖term f (↑σ' + ↑y * I) n‖ = nterm f σ' n
Tactic:
simp [nterm, term, h]
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 : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
y : ℝ
n : ℕ
h : ¬n = 0
⊢ ‖term f (↑σ' + ↑y * I) n‖ = nterm f σ' n
Tactic:
simp [nterm, term, h]
State after:
case neg
n✝ : ℕ
A a b c d u x y✝ t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
y : ℝ
n : ℕ
h : ¬n = 0
⊢ Complex.abs (f n) / Complex.abs (↑n ^ (↑σ' + ↑y * I)) = Complex.abs (f n) / ↑n ^ σ'

State before:
case neg
n✝ : ℕ
A a b c d u x y✝ t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
y : ℝ
n : ℕ
h : ¬n = 0
⊢ Complex.abs (f n) / Complex.abs (↑n ^ (↑σ' + ↑y * I)) = Complex.abs (f n) / ↑n ^ σ'
Tactic:
have : (n : ℂ) ≠ 0 := by simp [h]
State after:
case neg
n✝ : ℕ
A a b c d u x y✝ t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
y : ℝ
n : ℕ
h : ¬n = 0
this : ↑n ≠ 0
⊢ Complex.abs (f n) / Complex.abs (↑n ^ (↑σ' + ↑y * I)) = Complex.abs (f n) / ↑n ^ σ'

State before:
case neg
n✝ : ℕ
A a b c d u x y✝ t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
y : ℝ
n : ℕ
h : ¬n = 0
this : ↑n ≠ 0
⊢ Complex.abs (f n) / Complex.abs (↑n ^ (↑σ' + ↑y * I)) = Complex.abs (f n) / ↑n ^ σ'
Tactic:
simp [Complex.abs_cpow_of_ne_zero this]
State after:
no goals

State before:
n✝ : ℕ
A a b c d u x y✝ t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcont : Continuous ψ
hsupp : Integrable ψ volume
hx : 0 < x
hσ : 1 < σ'
y : ℝ
n : ℕ
h : ¬n = 0
⊢ ↑n ≠ 0
Tactic:
simp [h]
State after:
no goals