Theorem: limiting_fourier (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
hG : ContinuousOn G {s | 1 ≤ s.re}
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
⊢ ∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
      ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π)) =
    ∫ (t : ℝ), G (1 + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
Tactic:
have l1 := limiting_fourier_lim1 hcheby ψ (by linarith)
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
hG : ContinuousOn G {s | 1 ≤ s.re}
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
l1 :
  Tendsto (fun σ' => ∑' (n : ℕ), term f (↑σ') n * 𝓕 (W21.ofCS2 ψ).toFun (1 / (2 * π) * (↑n / x).log)) (𝓝[>] 1)
    (𝓝 (∑' (n : ℕ), f n / ↑n * 𝓕 (W21.ofCS2 ψ).toFun (1 / (2 * π) * (↑n / x).log)))
⊢ ∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
      ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π)) =
    ∫ (t : ℝ), G (1 + ↑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 𝕜
hcheby : cheby f
hG : ContinuousOn G {s | 1 ≤ s.re}
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
l1 :
  Tendsto (fun σ' => ∑' (n : ℕ), term f (↑σ') n * 𝓕 (W21.ofCS2 ψ).toFun (1 / (2 * π) * (↑n / x).log)) (𝓝[>] 1)
    (𝓝 (∑' (n : ℕ), f n / ↑n * 𝓕 (W21.ofCS2 ψ).toFun (1 / (2 * π) * (↑n / x).log)))
⊢ ∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
      ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π)) =
    ∫ (t : ℝ), G (1 + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
Tactic:
have l2 := limiting_fourier_lim2 A ψ hx
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
hG : ContinuousOn G {s | 1 ≤ s.re}
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
l1 :
  Tendsto (fun σ' => ∑' (n : ℕ), term f (↑σ') n * 𝓕 (W21.ofCS2 ψ).toFun (1 / (2 * π) * (↑n / x).log)) (𝓝[>] 1)
    (𝓝 (∑' (n : ℕ), f n / ↑n * 𝓕 (W21.ofCS2 ψ).toFun (1 / (2 * π) * (↑n / x).log)))
l2 :
  Tendsto
    (fun σ' =>
      ↑A * ↑(x ^ (1 - σ')) * ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 (W21.ofCS2 ψ).toFun (u / (2 * π)))
    (𝓝[>] 1) (𝓝 (↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 (W21.ofCS2 ψ).toFun (u / (2 * π))))
⊢ ∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
      ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π)) =
    ∫ (t : ℝ), G (1 + ↑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 𝕜
hcheby : cheby f
hG : ContinuousOn G {s | 1 ≤ s.re}
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
l1 :
  Tendsto (fun σ' => ∑' (n : ℕ), term f (↑σ') n * 𝓕 (W21.ofCS2 ψ).toFun (1 / (2 * π) * (↑n / x).log)) (𝓝[>] 1)
    (𝓝 (∑' (n : ℕ), f n / ↑n * 𝓕 (W21.ofCS2 ψ).toFun (1 / (2 * π) * (↑n / x).log)))
l2 :
  Tendsto
    (fun σ' =>
      ↑A * ↑(x ^ (1 - σ')) * ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 (W21.ofCS2 ψ).toFun (u / (2 * π)))
    (𝓝[>] 1) (𝓝 (↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 (W21.ofCS2 ψ).toFun (u / (2 * π))))
⊢ ∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
      ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π)) =
    ∫ (t : ℝ), G (1 + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
Tactic:
have l3 := limiting_fourier_lim3 hG ψ hx
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
hG : ContinuousOn G {s | 1 ≤ s.re}
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
l1 :
  Tendsto (fun σ' => ∑' (n : ℕ), term f (↑σ') n * 𝓕 (W21.ofCS2 ψ).toFun (1 / (2 * π) * (↑n / x).log)) (𝓝[>] 1)
    (𝓝 (∑' (n : ℕ), f n / ↑n * 𝓕 (W21.ofCS2 ψ).toFun (1 / (2 * π) * (↑n / x).log)))
l2 :
  Tendsto
    (fun σ' =>
      ↑A * ↑(x ^ (1 - σ')) * ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 (W21.ofCS2 ψ).toFun (u / (2 * π)))
    (𝓝[>] 1) (𝓝 (↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 (W21.ofCS2 ψ).toFun (u / (2 * π))))
l3 :
  Tendsto (fun σ' => ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) (𝓝[>] 1)
    (𝓝 (∫ (t : ℝ), G (1 + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)))
⊢ ∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
      ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π)) =
    ∫ (t : ℝ), G (1 + ↑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 𝕜
hcheby : cheby f
hG : ContinuousOn G {s | 1 ≤ s.re}
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
l1 :
  Tendsto (fun σ' => ∑' (n : ℕ), term f (↑σ') n * 𝓕 (W21.ofCS2 ψ).toFun (1 / (2 * π) * (↑n / x).log)) (𝓝[>] 1)
    (𝓝 (∑' (n : ℕ), f n / ↑n * 𝓕 (W21.ofCS2 ψ).toFun (1 / (2 * π) * (↑n / x).log)))
l2 :
  Tendsto
    (fun σ' =>
      ↑A * ↑(x ^ (1 - σ')) * ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 (W21.ofCS2 ψ).toFun (u / (2 * π)))
    (𝓝[>] 1) (𝓝 (↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 (W21.ofCS2 ψ).toFun (u / (2 * π))))
l3 :
  Tendsto (fun σ' => ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) (𝓝[>] 1)
    (𝓝 (∫ (t : ℝ), G (1 + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)))
⊢ ∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
      ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π)) =
    ∫ (t : ℝ), G (1 + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
Tactic:
apply tendsto_nhds_unique_of_eventuallyEq (l1.sub l2) l3
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
hG : ContinuousOn G {s | 1 ≤ s.re}
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
l1 :
  Tendsto (fun σ' => ∑' (n : ℕ), term f (↑σ') n * 𝓕 (W21.ofCS2 ψ).toFun (1 / (2 * π) * (↑n / x).log)) (𝓝[>] 1)
    (𝓝 (∑' (n : ℕ), f n / ↑n * 𝓕 (W21.ofCS2 ψ).toFun (1 / (2 * π) * (↑n / x).log)))
l2 :
  Tendsto
    (fun σ' =>
      ↑A * ↑(x ^ (1 - σ')) * ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 (W21.ofCS2 ψ).toFun (u / (2 * π)))
    (𝓝[>] 1) (𝓝 (↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 (W21.ofCS2 ψ).toFun (u / (2 * π))))
l3 :
  Tendsto (fun σ' => ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) (𝓝[>] 1)
    (𝓝 (∫ (t : ℝ), G (1 + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)))
⊢ (fun x_1 =>
      ∑' (n : ℕ), term f (↑x_1) n * 𝓕 (W21.ofCS2 ψ).toFun (1 / (2 * π) * (↑n / x).log) -
        ↑A * ↑(x ^ (1 - x_1)) *
          ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (x_1 - 1))) * 𝓕 (W21.ofCS2 ψ).toFun (u / (2 * π))) =ᶠ[𝓝[>] 1]
    fun σ' => ∫ (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 𝕜
hcheby : cheby f
hG : ContinuousOn G {s | 1 ≤ s.re}
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
l1 :
  Tendsto (fun σ' => ∑' (n : ℕ), term f (↑σ') n * 𝓕 (W21.ofCS2 ψ).toFun (1 / (2 * π) * (↑n / x).log)) (𝓝[>] 1)
    (𝓝 (∑' (n : ℕ), f n / ↑n * 𝓕 (W21.ofCS2 ψ).toFun (1 / (2 * π) * (↑n / x).log)))
l2 :
  Tendsto
    (fun σ' =>
      ↑A * ↑(x ^ (1 - σ')) * ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 (W21.ofCS2 ψ).toFun (u / (2 * π)))
    (𝓝[>] 1) (𝓝 (↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 (W21.ofCS2 ψ).toFun (u / (2 * π))))
l3 :
  Tendsto (fun σ' => ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) (𝓝[>] 1)
    (𝓝 (∫ (t : ℝ), G (1 + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)))
⊢ (fun x_1 =>
      ∑' (n : ℕ), term f (↑x_1) n * 𝓕 (W21.ofCS2 ψ).toFun (1 / (2 * π) * (↑n / x).log) -
        ↑A * ↑(x ^ (1 - x_1)) *
          ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (x_1 - 1))) * 𝓕 (W21.ofCS2 ψ).toFun (u / (2 * π))) =ᶠ[𝓝[>] 1]
    fun σ' => ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
Tactic:
simpa [eventuallyEq_nhdsWithin_iff] using eventually_of_forall (limiting_fourier_aux hG' hf ψ hx)
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
hG : ContinuousOn G {s | 1 ≤ s.re}
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
⊢ 0 < ?m.1975794
Tactic:
linarith
State after:
no goals