Theorem: limiting_fourier_aux (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
⊢ ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
      ↑A * ↑(x ^ (1 - σ')) * ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
    ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
Tactic:
have hint : Integrable ψ := ψ.h1.continuous.integrable_of_hasCompactSupport ψ.h2
State after:
n : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
⊢ ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
      ↑A * ↑(x ^ (1 - σ')) * ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
    ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)

State before:
n : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
⊢ ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
      ↑A * ↑(x ^ (1 - σ')) * ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
    ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
Tactic:
have l3 : 0 < x := zero_lt_one.trans_le hx
State after:
n : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
⊢ ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
      ↑A * ↑(x ^ (1 - σ')) * ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
    ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)

State before:
n : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
⊢ ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
      ↑A * ↑(x ^ (1 - σ')) * ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
    ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
Tactic:
have l1 (σ') (hσ' : 1 < σ') := first_fourier hf ψ.h1.continuous hint l3 hσ'
State after:
n : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
⊢ ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
      ↑A * ↑(x ^ (1 - σ')) * ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
    ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)

State before:
n : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
⊢ ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
      ↑A * ↑(x ^ (1 - σ')) * ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
    ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
Tactic:
have l2 (σ') (hσ' : 1 < σ') := second_fourier ψ.h1.continuous hint l3 hσ'
State after:
n : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
⊢ ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
      ↑A * ↑(x ^ (1 - σ')) * ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
    ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)

State before:
n : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
⊢ ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
      ↑A * ↑(x ^ (1 - σ')) * ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
    ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
Tactic:
have l8 : Continuous fun t : ℝ ↦ (x : ℂ) ^ (t * I) :=
  continuous_const.cpow (continuous_ofReal.mul continuous_const) (by simp [l3])
State after:
n : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
l8 : Continuous fun t => ↑x ^ (↑t * I)
⊢ ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
      ↑A * ↑(x ^ (1 - σ')) * ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
    ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)

State before:
n : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
l8 : Continuous fun t => ↑x ^ (↑t * I)
⊢ ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
      ↑A * ↑(x ^ (1 - σ')) * ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
    ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
Tactic:
have l6 : Continuous fun t : ℝ ↦ LSeries f (↑σ' + ↑t * I) * ψ t * ↑x ^ (↑t * I) := by
  apply ((continuous_LSeries_aux (hf _ hσ')).mul ψ.h1.continuous).mul l8
State after:
n : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
l8 : Continuous fun t => ↑x ^ (↑t * I)
l6 : Continuous fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
⊢ ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
      ↑A * ↑(x ^ (1 - σ')) * ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
    ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)

State before:
n : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
l8 : Continuous fun t => ↑x ^ (↑t * I)
l6 : Continuous fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
⊢ ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
      ↑A * ↑(x ^ (1 - σ')) * ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
    ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
Tactic:
have l4 : Integrable fun t : ℝ ↦ LSeries f (↑σ' + ↑t * I) * ψ t * ↑x ^ (↑t * I) := by
  exact l6.integrable_of_hasCompactSupport ψ.h2.mul_left.mul_right
State after:
n : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
l8 : Continuous fun t => ↑x ^ (↑t * I)
l6 : Continuous fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l4 : Integrable (fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) volume
⊢ ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
      ↑A * ↑(x ^ (1 - σ')) * ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
    ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)

State before:
n : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
l8 : Continuous fun t => ↑x ^ (↑t * I)
l6 : Continuous fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l4 : Integrable (fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) volume
⊢ ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
      ↑A * ↑(x ^ (1 - σ')) * ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
    ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
Tactic:
have e2 (u : ℝ) : σ' + u * I - 1 ≠ 0 := by
  intro h ; have := congr_arg Complex.re h ; simp at this ; linarith
State after:
n : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
l8 : Continuous fun t => ↑x ^ (↑t * I)
l6 : Continuous fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l4 : Integrable (fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) volume
e2 : ∀ (u : ℝ), ↑σ' + ↑u * I - 1 ≠ 0
⊢ ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
      ↑A * ↑(x ^ (1 - σ')) * ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
    ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)

State before:
n : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
l8 : Continuous fun t => ↑x ^ (↑t * I)
l6 : Continuous fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l4 : Integrable (fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) volume
e2 : ∀ (u : ℝ), ↑σ' + ↑u * I - 1 ≠ 0
⊢ ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
      ↑A * ↑(x ^ (1 - σ')) * ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
    ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
Tactic:
have l7 : Continuous fun a ↦ A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (σ' + a * I - 1) * ψ a * x ^ (a * I))) := by
  simp [← mul_assoc]
  refine ((continuous_const.mul <| Continuous.inv₀ ?_ e2).mul ψ.h1.continuous).mul l8
  continuity
State after:
n : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
l8 : Continuous fun t => ↑x ^ (↑t * I)
l6 : Continuous fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l4 : Integrable (fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) volume
e2 : ∀ (u : ℝ), ↑σ' + ↑u * I - 1 ≠ 0
l7 : Continuous fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I)))
⊢ ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
      ↑A * ↑(x ^ (1 - σ')) * ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
    ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)

State before:
n : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
l8 : Continuous fun t => ↑x ^ (↑t * I)
l6 : Continuous fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l4 : Integrable (fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) volume
e2 : ∀ (u : ℝ), ↑σ' + ↑u * I - 1 ≠ 0
l7 : Continuous fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I)))
⊢ ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
      ↑A * ↑(x ^ (1 - σ')) * ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
    ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
Tactic:
have l5 : Integrable fun a ↦ A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (σ' + a * I - 1) * ψ a * x ^ (a * I))) := by
  apply l7.integrable_of_hasCompactSupport
  exact ψ.h2.mul_left.mul_right.mul_left.mul_left
State after:
n : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
l8 : Continuous fun t => ↑x ^ (↑t * I)
l6 : Continuous fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l4 : Integrable (fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) volume
e2 : ∀ (u : ℝ), ↑σ' + ↑u * I - 1 ≠ 0
l7 : Continuous fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I)))
l5 :
  Integrable (fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I))))
    volume
⊢ ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
      ↑A * ↑(x ^ (1 - σ')) * ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
    ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)

State before:
n : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
l8 : Continuous fun t => ↑x ^ (↑t * I)
l6 : Continuous fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l4 : Integrable (fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) volume
e2 : ∀ (u : ℝ), ↑σ' + ↑u * I - 1 ≠ 0
l7 : Continuous fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I)))
l5 :
  Integrable (fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I))))
    volume
⊢ ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
      ↑A * ↑(x ^ (1 - σ')) * ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
    ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
Tactic:
simp_rw [l1 σ' hσ', l2 σ' hσ', ← integral_mul_left, ← integral_sub l4 l5]
State after:
n : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
l8 : Continuous fun t => ↑x ^ (↑t * I)
l6 : Continuous fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l4 : Integrable (fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) volume
e2 : ∀ (u : ℝ), ↑σ' + ↑u * I - 1 ≠ 0
l7 : Continuous fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I)))
l5 :
  Integrable (fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I))))
    volume
⊢ ∫ (a : ℝ),
      LSeries f (↑σ' + ↑a * I) * ψ.toFun a * ↑x ^ (↑a * I) -
        ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I))) =
    ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)

State before:
n : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
l8 : Continuous fun t => ↑x ^ (↑t * I)
l6 : Continuous fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l4 : Integrable (fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) volume
e2 : ∀ (u : ℝ), ↑σ' + ↑u * I - 1 ≠ 0
l7 : Continuous fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I)))
l5 :
  Integrable (fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I))))
    volume
⊢ ∫ (a : ℝ),
      LSeries f (↑σ' + ↑a * I) * ψ.toFun a * ↑x ^ (↑a * I) -
        ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I))) =
    ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
Tactic:
apply integral_congr_ae
State after:
case h
n : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
l8 : Continuous fun t => ↑x ^ (↑t * I)
l6 : Continuous fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l4 : Integrable (fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) volume
e2 : ∀ (u : ℝ), ↑σ' + ↑u * I - 1 ≠ 0
l7 : Continuous fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I)))
l5 :
  Integrable (fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I))))
    volume
⊢ (fun a =>
      LSeries f (↑σ' + ↑a * I) * ψ.toFun a * ↑x ^ (↑a * I) -
        ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I)))) =ᶠ[ae volume]
    fun a => G (↑σ' + ↑a * I) * ψ.toFun a * ↑x ^ (↑a * I)

State before:
case h
n : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
l8 : Continuous fun t => ↑x ^ (↑t * I)
l6 : Continuous fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l4 : Integrable (fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) volume
e2 : ∀ (u : ℝ), ↑σ' + ↑u * I - 1 ≠ 0
l7 : Continuous fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I)))
l5 :
  Integrable (fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I))))
    volume
⊢ (fun a =>
      LSeries f (↑σ' + ↑a * I) * ψ.toFun a * ↑x ^ (↑a * I) -
        ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I)))) =ᶠ[ae volume]
    fun a => G (↑σ' + ↑a * I) * ψ.toFun a * ↑x ^ (↑a * I)
Tactic:
apply eventually_of_forall
State after:
case h.hp
n : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
l8 : Continuous fun t => ↑x ^ (↑t * I)
l6 : Continuous fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l4 : Integrable (fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) volume
e2 : ∀ (u : ℝ), ↑σ' + ↑u * I - 1 ≠ 0
l7 : Continuous fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I)))
l5 :
  Integrable (fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I))))
    volume
⊢ ∀ (x_1 : ℝ),
    (fun a =>
          LSeries f (↑σ' + ↑a * I) * ψ.toFun a * ↑x ^ (↑a * I) -
            ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I))))
        x_1 =
      (fun a => G (↑σ' + ↑a * I) * ψ.toFun a * ↑x ^ (↑a * I)) x_1

State before:
case h.hp
n : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
l8 : Continuous fun t => ↑x ^ (↑t * I)
l6 : Continuous fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l4 : Integrable (fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) volume
e2 : ∀ (u : ℝ), ↑σ' + ↑u * I - 1 ≠ 0
l7 : Continuous fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I)))
l5 :
  Integrable (fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I))))
    volume
⊢ ∀ (x_1 : ℝ),
    (fun a =>
          LSeries f (↑σ' + ↑a * I) * ψ.toFun a * ↑x ^ (↑a * I) -
            ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I))))
        x_1 =
      (fun a => G (↑σ' + ↑a * I) * ψ.toFun a * ↑x ^ (↑a * I)) x_1
Tactic:
intro u
State after:
case h.hp
n : ℕ
A a b c d u✝ x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
l8 : Continuous fun t => ↑x ^ (↑t * I)
l6 : Continuous fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l4 : Integrable (fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) volume
e2 : ∀ (u : ℝ), ↑σ' + ↑u * I - 1 ≠ 0
l7 : Continuous fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I)))
l5 :
  Integrable (fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I))))
    volume
u : ℝ
⊢ (fun a =>
        LSeries f (↑σ' + ↑a * I) * ψ.toFun a * ↑x ^ (↑a * I) -
          ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I))))
      u =
    (fun a => G (↑σ' + ↑a * I) * ψ.toFun a * ↑x ^ (↑a * I)) u

State before:
case h.hp
n : ℕ
A a b c d u✝ x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
l8 : Continuous fun t => ↑x ^ (↑t * I)
l6 : Continuous fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l4 : Integrable (fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) volume
e2 : ∀ (u : ℝ), ↑σ' + ↑u * I - 1 ≠ 0
l7 : Continuous fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I)))
l5 :
  Integrable (fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I))))
    volume
u : ℝ
⊢ (fun a =>
        LSeries f (↑σ' + ↑a * I) * ψ.toFun a * ↑x ^ (↑a * I) -
          ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I))))
      u =
    (fun a => G (↑σ' + ↑a * I) * ψ.toFun a * ↑x ^ (↑a * I)) u
Tactic:
have e1 : 1 < ((σ' : ℂ) + (u : ℂ) * I).re := by simp [hσ']
State after:
case h.hp
n : ℕ
A a b c d u✝ x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
l8 : Continuous fun t => ↑x ^ (↑t * I)
l6 : Continuous fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l4 : Integrable (fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) volume
e2 : ∀ (u : ℝ), ↑σ' + ↑u * I - 1 ≠ 0
l7 : Continuous fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I)))
l5 :
  Integrable (fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I))))
    volume
u : ℝ
e1 : 1 < (↑σ' + ↑u * I).re
⊢ (fun a =>
        LSeries f (↑σ' + ↑a * I) * ψ.toFun a * ↑x ^ (↑a * I) -
          ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I))))
      u =
    (fun a => G (↑σ' + ↑a * I) * ψ.toFun a * ↑x ^ (↑a * I)) u

State before:
case h.hp
n : ℕ
A a b c d u✝ x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
l8 : Continuous fun t => ↑x ^ (↑t * I)
l6 : Continuous fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l4 : Integrable (fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) volume
e2 : ∀ (u : ℝ), ↑σ' + ↑u * I - 1 ≠ 0
l7 : Continuous fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I)))
l5 :
  Integrable (fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I))))
    volume
u : ℝ
e1 : 1 < (↑σ' + ↑u * I).re
⊢ (fun a =>
        LSeries f (↑σ' + ↑a * I) * ψ.toFun a * ↑x ^ (↑a * I) -
          ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I))))
      u =
    (fun a => G (↑σ' + ↑a * I) * ψ.toFun a * ↑x ^ (↑a * I)) u
Tactic:
simp_rw [hG' e1, sub_mul, ← mul_assoc]
State after:
case h.hp
n : ℕ
A a b c d u✝ x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
l8 : Continuous fun t => ↑x ^ (↑t * I)
l6 : Continuous fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l4 : Integrable (fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) volume
e2 : ∀ (u : ℝ), ↑σ' + ↑u * I - 1 ≠ 0
l7 : Continuous fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I)))
l5 :
  Integrable (fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I))))
    volume
u : ℝ
e1 : 1 < (↑σ' + ↑u * I).re
⊢ LSeries f (↑σ' + ↑u * I) * ψ.toFun u * ↑x ^ (↑u * I) -
      ↑A * ↑(x ^ (1 - σ')) * ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑u * I - 1)) * ψ.toFun u * ↑x ^ (↑u * I) =
    LSeries f (↑σ' + ↑u * I) * ψ.toFun u * ↑x ^ (↑u * I) - ↑A / (↑σ' + ↑u * I - 1) * ψ.toFun u * ↑x ^ (↑u * I)

State before:
case h.hp
n : ℕ
A a b c d u✝ x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
l8 : Continuous fun t => ↑x ^ (↑t * I)
l6 : Continuous fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l4 : Integrable (fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) volume
e2 : ∀ (u : ℝ), ↑σ' + ↑u * I - 1 ≠ 0
l7 : Continuous fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I)))
l5 :
  Integrable (fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I))))
    volume
u : ℝ
e1 : 1 < (↑σ' + ↑u * I).re
⊢ LSeries f (↑σ' + ↑u * I) * ψ.toFun u * ↑x ^ (↑u * I) -
      ↑A * ↑(x ^ (1 - σ')) * ↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑u * I - 1)) * ψ.toFun u * ↑x ^ (↑u * I) =
    LSeries f (↑σ' + ↑u * I) * ψ.toFun u * ↑x ^ (↑u * I) - ↑A / (↑σ' + ↑u * I - 1) * ψ.toFun u * ↑x ^ (↑u * I)
Tactic:
field_simp [e2]
State after:
case h.hp
n : ℕ
A a b c d u✝ x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
l8 : Continuous fun t => ↑x ^ (↑t * I)
l6 : Continuous fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l4 : Integrable (fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) volume
e2 : ∀ (u : ℝ), ↑σ' + ↑u * I - 1 ≠ 0
l7 : Continuous fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I)))
l5 :
  Integrable (fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I))))
    volume
u : ℝ
e1 : 1 < (↑σ' + ↑u * I).re
⊢ (↑A * ↑(x ^ (1 - σ')) * ↑(x ^ (σ' - 1)) = ↑A ∨ ψ.toFun u = 0) ∨ x = 0 ∧ ¬↑u * I = 0

State before:
case h.hp
n : ℕ
A a b c d u✝ x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
l8 : Continuous fun t => ↑x ^ (↑t * I)
l6 : Continuous fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l4 : Integrable (fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) volume
e2 : ∀ (u : ℝ), ↑σ' + ↑u * I - 1 ≠ 0
l7 : Continuous fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I)))
l5 :
  Integrable (fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I))))
    volume
u : ℝ
e1 : 1 < (↑σ' + ↑u * I).re
⊢ (↑A * ↑(x ^ (1 - σ')) * ↑(x ^ (σ' - 1)) = ↑A ∨ ψ.toFun u = 0) ∨ x = 0 ∧ ¬↑u * I = 0
Tactic:
left
State after:
case h.hp.h
n : ℕ
A a b c d u✝ x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
l8 : Continuous fun t => ↑x ^ (↑t * I)
l6 : Continuous fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l4 : Integrable (fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) volume
e2 : ∀ (u : ℝ), ↑σ' + ↑u * I - 1 ≠ 0
l7 : Continuous fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I)))
l5 :
  Integrable (fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I))))
    volume
u : ℝ
e1 : 1 < (↑σ' + ↑u * I).re
⊢ ↑A * ↑(x ^ (1 - σ')) * ↑(x ^ (σ' - 1)) = ↑A ∨ ψ.toFun u = 0

State before:
case h.hp.h
n : ℕ
A a b c d u✝ x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
l8 : Continuous fun t => ↑x ^ (↑t * I)
l6 : Continuous fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l4 : Integrable (fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) volume
e2 : ∀ (u : ℝ), ↑σ' + ↑u * I - 1 ≠ 0
l7 : Continuous fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I)))
l5 :
  Integrable (fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I))))
    volume
u : ℝ
e1 : 1 < (↑σ' + ↑u * I).re
⊢ ↑A * ↑(x ^ (1 - σ')) * ↑(x ^ (σ' - 1)) = ↑A ∨ ψ.toFun u = 0
Tactic:
left
State after:
case h.hp.h.h
n : ℕ
A a b c d u✝ x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
l8 : Continuous fun t => ↑x ^ (↑t * I)
l6 : Continuous fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l4 : Integrable (fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) volume
e2 : ∀ (u : ℝ), ↑σ' + ↑u * I - 1 ≠ 0
l7 : Continuous fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I)))
l5 :
  Integrable (fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I))))
    volume
u : ℝ
e1 : 1 < (↑σ' + ↑u * I).re
⊢ ↑A * ↑(x ^ (1 - σ')) * ↑(x ^ (σ' - 1)) = ↑A

State before:
case h.hp.h.h
n : ℕ
A a b c d u✝ x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
l8 : Continuous fun t => ↑x ^ (↑t * I)
l6 : Continuous fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l4 : Integrable (fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) volume
e2 : ∀ (u : ℝ), ↑σ' + ↑u * I - 1 ≠ 0
l7 : Continuous fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I)))
l5 :
  Integrable (fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I))))
    volume
u : ℝ
e1 : 1 < (↑σ' + ↑u * I).re
⊢ ↑A * ↑(x ^ (1 - σ')) * ↑(x ^ (σ' - 1)) = ↑A
Tactic:
norm_cast
State after:
case h.hp.h.h
n : ℕ
A a b c d u✝ x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
l8 : Continuous fun t => ↑x ^ (↑t * I)
l6 : Continuous fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l4 : Integrable (fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) volume
e2 : ∀ (u : ℝ), ↑σ' + ↑u * I - 1 ≠ 0
l7 : Continuous fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I)))
l5 :
  Integrable (fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I))))
    volume
u : ℝ
e1 : 1 < (↑σ' + ↑u * I).re
⊢ A * x ^ (1 - σ') * x ^ (σ' - 1) = A

State before:
case h.hp.h.h
n : ℕ
A a b c d u✝ x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
l8 : Continuous fun t => ↑x ^ (↑t * I)
l6 : Continuous fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l4 : Integrable (fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) volume
e2 : ∀ (u : ℝ), ↑σ' + ↑u * I - 1 ≠ 0
l7 : Continuous fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I)))
l5 :
  Integrable (fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I))))
    volume
u : ℝ
e1 : 1 < (↑σ' + ↑u * I).re
⊢ A * x ^ (1 - σ') * x ^ (σ' - 1) = A
Tactic:
simp [mul_assoc, ← rpow_add l3]
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
⊢ ℝ → ↑x ∈ slitPlane
Tactic:
simp [l3]
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
l8 : Continuous fun t => ↑x ^ (↑t * I)
⊢ Continuous fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
Tactic:
apply ((continuous_LSeries_aux (hf _ hσ')).mul ψ.h1.continuous).mul l8
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
l8 : Continuous fun t => ↑x ^ (↑t * I)
l6 : Continuous fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
⊢ Integrable (fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) volume
Tactic:
exact l6.integrable_of_hasCompactSupport ψ.h2.mul_left.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 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
l8 : Continuous fun t => ↑x ^ (↑t * I)
l6 : Continuous fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l4 : Integrable (fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) volume
u : ℝ
⊢ ↑σ' + ↑u * I - 1 ≠ 0
Tactic:
intro h
State after:
n : ℕ
A a b c d u✝ x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
l8 : Continuous fun t => ↑x ^ (↑t * I)
l6 : Continuous fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l4 : Integrable (fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) volume
u : ℝ
h : ↑σ' + ↑u * I - 1 = 0
⊢ False

State before:
n : ℕ
A a b c d u✝ x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
l8 : Continuous fun t => ↑x ^ (↑t * I)
l6 : Continuous fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l4 : Integrable (fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) volume
u : ℝ
h : ↑σ' + ↑u * I - 1 = 0
⊢ False
Tactic:
have := congr_arg Complex.re h
State after:
n : ℕ
A a b c d u✝ x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
l8 : Continuous fun t => ↑x ^ (↑t * I)
l6 : Continuous fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l4 : Integrable (fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) volume
u : ℝ
h : ↑σ' + ↑u * I - 1 = 0
this : (↑σ' + ↑u * I - 1).re = re 0
⊢ False

State before:
n : ℕ
A a b c d u✝ x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
l8 : Continuous fun t => ↑x ^ (↑t * I)
l6 : Continuous fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l4 : Integrable (fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) volume
u : ℝ
h : ↑σ' + ↑u * I - 1 = 0
this : (↑σ' + ↑u * I - 1).re = re 0
⊢ False
Tactic:
simp at this
State after:
n : ℕ
A a b c d u✝ x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
l8 : Continuous fun t => ↑x ^ (↑t * I)
l6 : Continuous fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l4 : Integrable (fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) volume
u : ℝ
h : ↑σ' + ↑u * I - 1 = 0
this : σ' - 1 = 0
⊢ False

State before:
n : ℕ
A a b c d u✝ x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
l8 : Continuous fun t => ↑x ^ (↑t * I)
l6 : Continuous fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l4 : Integrable (fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) volume
u : ℝ
h : ↑σ' + ↑u * I - 1 = 0
this : σ' - 1 = 0
⊢ False
Tactic:
linarith
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
l8 : Continuous fun t => ↑x ^ (↑t * I)
l6 : Continuous fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l4 : Integrable (fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) volume
e2 : ∀ (u : ℝ), ↑σ' + ↑u * I - 1 ≠ 0
⊢ Continuous fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I)))
Tactic:
simp [← mul_assoc]
State after:
n : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
l8 : Continuous fun t => ↑x ^ (↑t * I)
l6 : Continuous fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l4 : Integrable (fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) volume
e2 : ∀ (u : ℝ), ↑σ' + ↑u * I - 1 ≠ 0
⊢ Continuous fun a => ↑A * ↑(x ^ (1 - σ')) * ↑(x ^ (σ' - 1)) * (↑σ' + ↑a * I - 1)⁻¹ * ψ.toFun a * ↑x ^ (↑a * I)

State before:
n : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
l8 : Continuous fun t => ↑x ^ (↑t * I)
l6 : Continuous fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l4 : Integrable (fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) volume
e2 : ∀ (u : ℝ), ↑σ' + ↑u * I - 1 ≠ 0
⊢ Continuous fun a => ↑A * ↑(x ^ (1 - σ')) * ↑(x ^ (σ' - 1)) * (↑σ' + ↑a * I - 1)⁻¹ * ψ.toFun a * ↑x ^ (↑a * I)
Tactic:
refine ((continuous_const.mul <| Continuous.inv₀ ?_ e2).mul ψ.h1.continuous).mul l8
State after:
n : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
l8 : Continuous fun t => ↑x ^ (↑t * I)
l6 : Continuous fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l4 : Integrable (fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) volume
e2 : ∀ (u : ℝ), ↑σ' + ↑u * I - 1 ≠ 0
⊢ Continuous fun x => ↑σ' + ↑x * I - 1

State before:
n : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
l8 : Continuous fun t => ↑x ^ (↑t * I)
l6 : Continuous fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l4 : Integrable (fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) volume
e2 : ∀ (u : ℝ), ↑σ' + ↑u * I - 1 ≠ 0
⊢ Continuous fun x => ↑σ' + ↑x * I - 1
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 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
l8 : Continuous fun t => ↑x ^ (↑t * I)
l6 : Continuous fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l4 : Integrable (fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) volume
e2 : ∀ (u : ℝ), ↑σ' + ↑u * I - 1 ≠ 0
l7 : Continuous fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I)))
⊢ Integrable (fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I))))
    volume
Tactic:
apply l7.integrable_of_hasCompactSupport
State after:
n : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
l8 : Continuous fun t => ↑x ^ (↑t * I)
l6 : Continuous fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l4 : Integrable (fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) volume
e2 : ∀ (u : ℝ), ↑σ' + ↑u * I - 1 ≠ 0
l7 : Continuous fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I)))
⊢ HasCompactSupport fun a =>
    ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I)))

State before:
n : ℕ
A a b c d u x y t σ'✝ : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
l8 : Continuous fun t => ↑x ^ (↑t * I)
l6 : Continuous fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l4 : Integrable (fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) volume
e2 : ∀ (u : ℝ), ↑σ' + ↑u * I - 1 ≠ 0
l7 : Continuous fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I)))
⊢ HasCompactSupport fun a =>
    ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I)))
Tactic:
exact ψ.h2.mul_left.mul_right.mul_left.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 𝕜
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
σ' : ℝ
hσ' : 1 < σ'
hint : Integrable ψ.toFun volume
l3 : 0 < x
l1 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∑' (n : ℕ), term f (↑σ') n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) =
        ∫ (t : ℝ), LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l2 :
  ∀ (σ' : ℝ),
    1 < σ' →
      ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 ψ.toFun (u / (2 * π)) =
        ↑(x ^ (σ' - 1)) * ∫ (t : ℝ), 1 / (↑σ' + ↑t * I - 1) * ψ.toFun t * ↑x ^ (↑t * I)
l8 : Continuous fun t => ↑x ^ (↑t * I)
l6 : Continuous fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
l4 : Integrable (fun t => LSeries f (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) volume
e2 : ∀ (u : ℝ), ↑σ' + ↑u * I - 1 ≠ 0
l7 : Continuous fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I)))
l5 :
  Integrable (fun a => ↑A * ↑(x ^ (1 - σ')) * (↑(x ^ (σ' - 1)) * (1 / (↑σ' + ↑a * I - 1) * ψ.toFun a * ↑x ^ (↑a * I))))
    volume
u : ℝ
⊢ 1 < (↑σ' + ↑u * I).re
Tactic:
simp [hσ']
State after:
no goals