internlm/Lean-Github huggingface dataset:
Theorem: limiting_fourier_aux
Proof 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
Proof 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
Theorem: limiting_fourier_aux
Proof 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
Proof 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
Theorem: limiting_fourier_aux
Proof 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
Proof 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
Theorem: limiting_fourier_aux
Proof 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
Proof state after:
no goals
Theorem: limiting_fourier_aux
Proof 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]
Proof 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)
Theorem: limiting_fourier_aux
Proof 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
Proof 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
Theorem: limiting_fourier_aux
Proof 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
Proof state after:
no goals
Theorem: limiting_fourier_aux
Proof 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
Proof 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)))
Theorem: limiting_fourier_aux
Proof 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
Proof state after:
no goals
Theorem: limiting_fourier_aux
Proof 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σ']
Proof state after:
no goals
Theorem: cumsum_zero
Proof state before:
n : ℕ
A a b c d u✝¹ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝⁴ : _root_.RCLike 𝕜
α : Type u_1
E : Type u_2
inst✝³ : OfNat α 1
inst✝² : Add α
inst✝¹ : Sub α
u✝ : α → ℂ
inst✝ : AddCommMonoid E
u : ℕ → E
⊢ cumsum u 0 = 0
Tactic:
simp [cumsum]
Proof state after:
no goals
Theorem: cumsum_succ
Proof state before:
n✝ : ℕ
A a b c d u✝¹ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝⁴ : _root_.RCLike 𝕜
α : Type u_1
E : Type u_2
inst✝³ : OfNat α 1
inst✝² : Add α
inst✝¹ : Sub α
u✝ : α → ℂ
inst✝ : AddCommMonoid E
u : ℕ → E
n : ℕ
⊢ cumsum u (n + 1) = cumsum u n + u n
Tactic:
simp [cumsum, Finset.sum_range_succ]
Proof state after:
no goals
Theorem: nabla_cumsum
Proof state before:
n : ℕ
A a b c d u✝¹ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝⁴ : _root_.RCLike 𝕜
α : Type u_1
E : Type u_2
inst✝³ : OfNat α 1
inst✝² : Add α
inst✝¹ : Sub α
u✝ : α → ℂ
inst✝ : AddCommGroup E
u : ℕ → E
⊢ nabla (cumsum u) = u
Tactic:
ext n
Proof state after:
case h
n✝ : ℕ
A a b c d u✝¹ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝⁴ : _root_.RCLike 𝕜
α : Type u_1
E : Type u_2
inst✝³ : OfNat α 1
inst✝² : Add α
inst✝¹ : Sub α
u✝ : α → ℂ
inst✝ : AddCommGroup E
u : ℕ → E
n : ℕ
⊢ nabla (cumsum u) n = u n
Theorem: nabla_cumsum
Proof state before:
case h
n✝ : ℕ
A a b c d u✝¹ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝⁴ : _root_.RCLike 𝕜
α : Type u_1
E : Type u_2
inst✝³ : OfNat α 1
inst✝² : Add α
inst✝¹ : Sub α
u✝ : α → ℂ
inst✝ : AddCommGroup E
u : ℕ → E
n : ℕ
⊢ nabla (cumsum u) n = u n
Tactic:
simp [nabla, cumsum, Finset.range_succ]
Proof state after:
no goals
Theorem: neg_cumsum
Proof state before:
n✝ : ℕ
A a b c d u✝¹ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝⁴ : _root_.RCLike 𝕜
α : Type u_1
E : Type u_2
inst✝³ : OfNat α 1
inst✝² : Add α
inst✝¹ : Sub α
u✝ : α → ℂ
inst✝ : AddCommGroup E
u : ℕ → E
n : ℕ
⊢ (-cumsum u) n = cumsum (-u) n
Tactic:
simp [cumsum]
Proof state after:
no goals
Theorem: neg_nabla
Proof state before:
n : ℕ
A a b c d u✝¹ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝⁴ : _root_.RCLike 𝕜
α : Type u_1
E : Type u_2
inst✝³ : OfNat α 1
inst✝² : Add α
inst✝¹ : Sub α
u✝ : α → ℂ
inst✝ : Ring E
u : α → E
⊢ -nabla u = nnabla u
Tactic:
ext n
Proof state after:
case h
n✝ : ℕ
A a b c d u✝¹ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝⁴ : _root_.RCLike 𝕜
α : Type u_1
E : Type u_2
inst✝³ : OfNat α 1
inst✝² : Add α
inst✝¹ : Sub α
u✝ : α → ℂ
inst✝ : Ring E
u : α → E
n : α
⊢ (-nabla u) n = nnabla u n
Theorem: neg_nabla
Proof state before:
case h
n✝ : ℕ
A a b c d u✝¹ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝⁴ : _root_.RCLike 𝕜
α : Type u_1
E : Type u_2
inst✝³ : OfNat α 1
inst✝² : Add α
inst✝¹ : Sub α
u✝ : α → ℂ
inst✝ : Ring E
u : α → E
n : α
⊢ (-nabla u) n = nnabla u n
Tactic:
simp [nabla, nnabla]
Proof state after:
no goals
Theorem: nabla_mul
Proof state before:
n : ℕ
A a b c✝ d u✝¹ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝⁴ : _root_.RCLike 𝕜
α : Type u_1
E : Type u_2
inst✝³ : OfNat α 1
inst✝² : Add α
inst✝¹ : Sub α
u✝ : α → ℂ
inst✝ : Ring E
u : α → E
c : E
⊢ (nabla fun n => c * u n) = c • nabla u
Tactic:
ext n
Proof state after:
case h
n✝ : ℕ
A a b c✝ d u✝¹ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝⁴ : _root_.RCLike 𝕜
α : Type u_1
E : Type u_2
inst✝³ : OfNat α 1
inst✝² : Add α
inst✝¹ : Sub α
u✝ : α → ℂ
inst✝ : Ring E
u : α → E
c : E
n : α
⊢ nabla (fun n => c * u n) n = (c • nabla u) n
Theorem: nabla_mul
Proof state before:
case h
n✝ : ℕ
A a b c✝ d u✝¹ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝⁴ : _root_.RCLike 𝕜
α : Type u_1
E : Type u_2
inst✝³ : OfNat α 1
inst✝² : Add α
inst✝¹ : Sub α
u✝ : α → ℂ
inst✝ : Ring E
u : α → E
c : E
n : α
⊢ nabla (fun n => c * u n) n = (c • nabla u) n
Tactic:
simp [nabla, mul_sub]
Proof state after:
no goals
Theorem: nnabla_mul
Proof state before:
n : ℕ
A a b c✝ d u✝¹ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝⁴ : _root_.RCLike 𝕜
α : Type u_1
E : Type u_2
inst✝³ : OfNat α 1
inst✝² : Add α
inst✝¹ : Sub α
u✝ : α → ℂ
inst✝ : Ring E
u : α → E
c : E
⊢ (nnabla fun n => c * u n) = c • nnabla u
Tactic:
ext n
Proof state after:
case h
n✝ : ℕ
A a b c✝ d u✝¹ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝⁴ : _root_.RCLike 𝕜
α : Type u_1
E : Type u_2
inst✝³ : OfNat α 1
inst✝² : Add α
inst✝¹ : Sub α
u✝ : α → ℂ
inst✝ : Ring E
u : α → E
c : E
n : α
⊢ nnabla (fun n => c * u n) n = (c • nnabla u) n
Theorem: nnabla_mul
Proof state before:
case h
n✝ : ℕ
A a b c✝ d u✝¹ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝⁴ : _root_.RCLike 𝕜
α : Type u_1
E : Type u_2
inst✝³ : OfNat α 1
inst✝² : Add α
inst✝¹ : Sub α
u✝ : α → ℂ
inst✝ : Ring E
u : α → E
c : E
n : α
⊢ nnabla (fun n => c * u n) n = (c • nnabla u) n
Tactic:
simp [nnabla, mul_sub]
Proof state after:
no goals
Theorem: nnabla_cast
Proof state before:
n : ℕ
A a b c d u✝¹ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝⁴ : _root_.RCLike 𝕜
α : Type u_1
E : Type u_2
inst✝³ : OfNat α 1
inst✝² : Add α
inst✝¹ : Sub α
u✝ : α → ℂ
u : ℝ → E
inst✝ : Sub E
⊢ nnabla u ∘ Nat.cast = nnabla (u ∘ Nat.cast)
Tactic:
ext n
Proof state after:
case h
n✝ : ℕ
A a b c d u✝¹ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝⁴ : _root_.RCLike 𝕜
α : Type u_1
E : Type u_2
inst✝³ : OfNat α 1
inst✝² : Add α
inst✝¹ : Sub α
u✝ : α → ℂ
u : ℝ → E
inst✝ : Sub E
n : ℕ
⊢ (nnabla u ∘ Nat.cast) n = nnabla (u ∘ Nat.cast) n
Theorem: nnabla_cast
Proof state before:
case h
n✝ : ℕ
A a b c d u✝¹ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝⁴ : _root_.RCLike 𝕜
α : Type u_1
E : Type u_2
inst✝³ : OfNat α 1
inst✝² : Add α
inst✝¹ : Sub α
u✝ : α → ℂ
u : ℝ → E
inst✝ : Sub E
n : ℕ
⊢ (nnabla u ∘ Nat.cast) n = nnabla (u ∘ Nat.cast) n
Tactic:
simp [nnabla]
Proof state after:
no goals
Theorem: Finset.sum_shift_front
Proof state before:
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝¹ : _root_.RCLike 𝕜
E : Type u_1
inst✝ : Ring E
u : ℕ → E
n : ℕ
⊢ cumsum u (n + 1) = u 0 + cumsum (shift u) n
Tactic:
simp_rw [add_comm n, cumsum, sum_range_add, sum_range_one, add_comm 1]
Proof state after:
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝¹ : _root_.RCLike 𝕜
E : Type u_1
inst✝ : Ring E
u : ℕ → E
n : ℕ
⊢ u 0 + ∑ x ∈ range n, u (x + 1) = u 0 + ∑ i ∈ range n, shift u i
Theorem: Finset.sum_shift_front
Proof state before:
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝¹ : _root_.RCLike 𝕜
E : Type u_1
inst✝ : Ring E
u : ℕ → E
n : ℕ
⊢ u 0 + ∑ x ∈ range n, u (x + 1) = u 0 + ∑ i ∈ range n, shift u i
Tactic:
rfl
Proof state after:
no goals