Theorem: limiting_cor_W21
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
S1 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ∑' (n : ℕ), f n / ↑n * 𝓕 ψ (1 / (2 * π) * (↑n / x).log)
S2 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ (u / (2 * π))
S : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => S1 x ψ - S2 x ψ
g : trunc
Ψ : ℝ → CS 2 ℂ := fun R => g.scale R * ψ
C : ℝ
hcheby : chebyWith C f
hC : 0 ≤ C
key2 : ∀ ε > 0, ∀ᶠ (x : ℝ) in atTop, dist (W21.norm (ψ.toFun - (Ψ x).toFun)) 0 < ε
ε : ℝ
hε : ε > 0
M : ℝ := C * (1 + 2 * π ^ 2) + ‖↑A‖ * (2 * π ^ 2)
R : ℝ
hRψ : W21.norm (ψ.toFun - (Ψ R).toFun) < ε / 2 / (1 + M)
key✝ : ∀ (R ε : ℝ), ε > 0 → ∀ᶠ (x : ℝ) in atTop, ‖S x (Ψ R).toFun‖ < ε
x : ℝ
hx : 1 ≤ x
key : ‖S x (Ψ R).toFun‖ < ε / 2
key3 : ‖S x (ψ.toFun - (Ψ R).toFun)‖ < ε / 2
S1_sub_1 : ∀ (x : ℝ), 𝓕 (ψ.toFun - (Ψ R).toFun) x = 𝓕 ψ.toFun x - 𝓕 (Ψ R).toFun x
S1_sub : S1 x (ψ.toFun - (Ψ R).toFun) = S1 x ψ.toFun - S1 x (Ψ R).toFun
⊢ ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π)) - 𝓕 (Ψ R).toFun (u / (2 * π)) =
    (↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π))) -
      ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 (Ψ R).toFun (u / (2 * π))
Tactic:
rw [integral_sub]
Proof state after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
S1 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ∑' (n : ℕ), f n / ↑n * 𝓕 ψ (1 / (2 * π) * (↑n / x).log)
S2 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ (u / (2 * π))
S : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => S1 x ψ - S2 x ψ
g : trunc
Ψ : ℝ → CS 2 ℂ := fun R => g.scale R * ψ
C : ℝ
hcheby : chebyWith C f
hC : 0 ≤ C
key2 : ∀ ε > 0, ∀ᶠ (x : ℝ) in atTop, dist (W21.norm (ψ.toFun - (Ψ x).toFun)) 0 < ε
ε : ℝ
hε : ε > 0
M : ℝ := C * (1 + 2 * π ^ 2) + ‖↑A‖ * (2 * π ^ 2)
R : ℝ
hRψ : W21.norm (ψ.toFun - (Ψ R).toFun) < ε / 2 / (1 + M)
key✝ : ∀ (R ε : ℝ), ε > 0 → ∀ᶠ (x : ℝ) in atTop, ‖S x (Ψ R).toFun‖ < ε
x : ℝ
hx : 1 ≤ x
key : ‖S x (Ψ R).toFun‖ < ε / 2
key3 : ‖S x (ψ.toFun - (Ψ R).toFun)‖ < ε / 2
S1_sub_1 : ∀ (x : ℝ), 𝓕 (ψ.toFun - (Ψ R).toFun) x = 𝓕 ψ.toFun x - 𝓕 (Ψ R).toFun x
S1_sub : S1 x (ψ.toFun - (Ψ R).toFun) = S1 x ψ.toFun - S1 x (Ψ R).toFun
⊢ ↑A * ((∫ (a : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (a / (2 * π))) - ∫ (a : ℝ) in Ici (-x.log), 𝓕 (Ψ R).toFun (a / (2 * π))) =
    (↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π))) -
      ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 (Ψ R).toFun (u / (2 * π))

case hf
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
S1 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ∑' (n : ℕ), f n / ↑n * 𝓕 ψ (1 / (2 * π) * (↑n / x).log)
S2 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ (u / (2 * π))
S : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => S1 x ψ - S2 x ψ
g : trunc
Ψ : ℝ → CS 2 ℂ := fun R => g.scale R * ψ
C : ℝ
hcheby : chebyWith C f
hC : 0 ≤ C
key2 : ∀ ε > 0, ∀ᶠ (x : ℝ) in atTop, dist (W21.norm (ψ.toFun - (Ψ x).toFun)) 0 < ε
ε : ℝ
hε : ε > 0
M : ℝ := C * (1 + 2 * π ^ 2) + ‖↑A‖ * (2 * π ^ 2)
R : ℝ
hRψ : W21.norm (ψ.toFun - (Ψ R).toFun) < ε / 2 / (1 + M)
key✝ : ∀ (R ε : ℝ), ε > 0 → ∀ᶠ (x : ℝ) in atTop, ‖S x (Ψ R).toFun‖ < ε
x : ℝ
hx : 1 ≤ x
key : ‖S x (Ψ R).toFun‖ < ε / 2
key3 : ‖S x (ψ.toFun - (Ψ R).toFun)‖ < ε / 2
S1_sub_1 : ∀ (x : ℝ), 𝓕 (ψ.toFun - (Ψ R).toFun) x = 𝓕 ψ.toFun x - 𝓕 (Ψ R).toFun x
S1_sub : S1 x (ψ.toFun - (Ψ R).toFun) = S1 x ψ.toFun - S1 x (Ψ R).toFun
⊢ Integrable (fun u => 𝓕 ψ.toFun (u / (2 * π))) (volume.restrict (Ici (-x.log)))

case hg
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
S1 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ∑' (n : ℕ), f n / ↑n * 𝓕 ψ (1 / (2 * π) * (↑n / x).log)
S2 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ (u / (2 * π))
S : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => S1 x ψ - S2 x ψ
g : trunc
Ψ : ℝ → CS 2 ℂ := fun R => g.scale R * ψ
C : ℝ
hcheby : chebyWith C f
hC : 0 ≤ C
key2 : ∀ ε > 0, ∀ᶠ (x : ℝ) in atTop, dist (W21.norm (ψ.toFun - (Ψ x).toFun)) 0 < ε
ε : ℝ
hε : ε > 0
M : ℝ := C * (1 + 2 * π ^ 2) + ‖↑A‖ * (2 * π ^ 2)
R : ℝ
hRψ : W21.norm (ψ.toFun - (Ψ R).toFun) < ε / 2 / (1 + M)
key✝ : ∀ (R ε : ℝ), ε > 0 → ∀ᶠ (x : ℝ) in atTop, ‖S x (Ψ R).toFun‖ < ε
x : ℝ
hx : 1 ≤ x
key : ‖S x (Ψ R).toFun‖ < ε / 2
key3 : ‖S x (ψ.toFun - (Ψ R).toFun)‖ < ε / 2
S1_sub_1 : ∀ (x : ℝ), 𝓕 (ψ.toFun - (Ψ R).toFun) x = 𝓕 ψ.toFun x - 𝓕 (Ψ R).toFun x
S1_sub : S1 x (ψ.toFun - (Ψ R).toFun) = S1 x ψ.toFun - S1 x (Ψ R).toFun
⊢ Integrable (fun u => 𝓕 (Ψ R).toFun (u / (2 * π))) (volume.restrict (Ici (-x.log)))