Theorem: limiting_cor_W21 (PrimeNumberTheoremAnd/Wiener.lean)

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 σ')
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}
⊢ Tendsto
    (fun x =>
      ∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
        ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π)))
    atTop (𝓝 0)
Tactic:
let S1 x (ψ : ℝ → ℂ) := ∑' (n : ℕ), f n / ↑n * 𝓕 ψ (1 / (2 * π) * Real.log (↑n / x))
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 σ')
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}
S1 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ∑' (n : ℕ), f n / ↑n * 𝓕 ψ (1 / (2 * π) * (↑n / x).log)
⊢ Tendsto
    (fun x =>
      ∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
        ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π)))
    atTop (𝓝 0)

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 σ')
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}
S1 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ∑' (n : ℕ), f n / ↑n * 𝓕 ψ (1 / (2 * π) * (↑n / x).log)
⊢ Tendsto
    (fun x =>
      ∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
        ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π)))
    atTop (𝓝 0)
Tactic:
let S2 x (ψ : ℝ → ℂ) := ↑A * ∫ (u : ℝ) in Ici (-Real.log x), 𝓕 ψ (u / (2 * π))
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 σ')
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}
S1 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ∑' (n : ℕ), f n / ↑n * 𝓕 ψ (1 / (2 * π) * (↑n / x).log)
S2 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ (u / (2 * π))
⊢ Tendsto
    (fun x =>
      ∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
        ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π)))
    atTop (𝓝 0)

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 σ')
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}
S1 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ∑' (n : ℕ), f n / ↑n * 𝓕 ψ (1 / (2 * π) * (↑n / x).log)
S2 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ (u / (2 * π))
⊢ Tendsto
    (fun x =>
      ∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
        ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π)))
    atTop (𝓝 0)
Tactic:
let S x ψ := S1 x ψ - S2 x ψ
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 σ')
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}
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 ψ
⊢ Tendsto
    (fun x =>
      ∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
        ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π)))
    atTop (𝓝 0)

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 σ')
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}
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 ψ
⊢ Tendsto
    (fun x =>
      ∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
        ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π)))
    atTop (𝓝 0)
Tactic:
change Tendsto (fun x ↦ S x ψ) atTop (𝓝 0)
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 σ')
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}
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 ψ
⊢ Tendsto (fun x => S x ψ.toFun) atTop (𝓝 0)

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 σ')
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}
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 ψ
⊢ Tendsto (fun x => S x ψ.toFun) atTop (𝓝 0)
Tactic:
obtain g := exists_trunc
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 σ')
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}
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
⊢ Tendsto (fun x => S x ψ.toFun) atTop (𝓝 0)

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 σ')
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}
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
⊢ Tendsto (fun x => S x ψ.toFun) atTop (𝓝 0)
Tactic:
let Ψ R := g.scale R * ψ
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 σ')
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}
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 * ψ
⊢ Tendsto (fun x => S x ψ.toFun) atTop (𝓝 0)

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 σ')
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}
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 * ψ
⊢ Tendsto (fun x => S x ψ.toFun) atTop (𝓝 0)
Tactic:
have key R : Tendsto (fun x ↦ S x (Ψ R)) atTop (𝓝 0) := limiting_cor (Ψ R) hf hcheby hG hG'
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 σ')
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}
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 * ψ
key : ∀ (R : ℝ), Tendsto (fun x => S x (Ψ R).toFun) atTop (𝓝 0)
⊢ Tendsto (fun x => S x ψ.toFun) atTop (𝓝 0)

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 σ')
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}
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 * ψ
key : ∀ (R : ℝ), Tendsto (fun x => S x (Ψ R).toFun) atTop (𝓝 0)
⊢ Tendsto (fun x => S x ψ.toFun) atTop (𝓝 0)
Tactic:
obtain ⟨C, hcheby⟩ := hcheby
State after:
case intro
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 * ψ
key : ∀ (R : ℝ), Tendsto (fun x => S x (Ψ R).toFun) atTop (𝓝 0)
C : ℝ
hcheby : chebyWith C f
⊢ Tendsto (fun x => S x ψ.toFun) atTop (𝓝 0)

State before:
case intro
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 * ψ
key : ∀ (R : ℝ), Tendsto (fun x => S x (Ψ R).toFun) atTop (𝓝 0)
C : ℝ
hcheby : chebyWith C f
⊢ Tendsto (fun x => S x ψ.toFun) atTop (𝓝 0)
Tactic:
have hC : 0 ≤ C := by
  have : ‖f 0‖ ≤ C := by simpa [cumsum] using hcheby 1
  have : 0 ≤ ‖f 0‖ := by positivity
  linarith
State after:
case intro
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 * ψ
key : ∀ (R : ℝ), Tendsto (fun x => S x (Ψ R).toFun) atTop (𝓝 0)
C : ℝ
hcheby : chebyWith C f
hC : 0 ≤ C
⊢ Tendsto (fun x => S x ψ.toFun) atTop (𝓝 0)

State before:
case intro
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 * ψ
key : ∀ (R : ℝ), Tendsto (fun x => S x (Ψ R).toFun) atTop (𝓝 0)
C : ℝ
hcheby : chebyWith C f
hC : 0 ≤ C
⊢ Tendsto (fun x => S x ψ.toFun) atTop (𝓝 0)
Tactic:
have key2 : Tendsto (fun R ↦ W21.norm (ψ - Ψ R)) atTop (𝓝 0) := W21_approximation ψ g
State after:
case intro
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 * ψ
key : ∀ (R : ℝ), Tendsto (fun x => S x (Ψ R).toFun) atTop (𝓝 0)
C : ℝ
hcheby : chebyWith C f
hC : 0 ≤ C
key2 : Tendsto (fun R => W21.norm (ψ.toFun - (Ψ R).toFun)) atTop (𝓝 0)
⊢ Tendsto (fun x => S x ψ.toFun) atTop (𝓝 0)

State before:
case intro
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 * ψ
key : ∀ (R : ℝ), Tendsto (fun x => S x (Ψ R).toFun) atTop (𝓝 0)
C : ℝ
hcheby : chebyWith C f
hC : 0 ≤ C
key2 : Tendsto (fun R => W21.norm (ψ.toFun - (Ψ R).toFun)) atTop (𝓝 0)
⊢ Tendsto (fun x => S x ψ.toFun) atTop (𝓝 0)
Tactic:
simp_rw [Metric.tendsto_nhds] at key key2 ⊢
State after:
case intro
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
key : ∀ (R ε : ℝ), ε > 0 → ∀ᶠ (x : ℝ) in atTop, dist (S x (Ψ R).toFun) 0 < ε
key2 : ∀ ε > 0, ∀ᶠ (x : ℝ) in atTop, dist (W21.norm (ψ.toFun - (Ψ x).toFun)) 0 < ε
⊢ ∀ ε > 0, ∀ᶠ (x : ℝ) in atTop, dist (S x ψ.toFun) 0 < ε

State before:
case intro
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
key : ∀ (R ε : ℝ), ε > 0 → ∀ᶠ (x : ℝ) in atTop, dist (S x (Ψ R).toFun) 0 < ε
key2 : ∀ ε > 0, ∀ᶠ (x : ℝ) in atTop, dist (W21.norm (ψ.toFun - (Ψ x).toFun)) 0 < ε
⊢ ∀ ε > 0, ∀ᶠ (x : ℝ) in atTop, dist (S x ψ.toFun) 0 < ε
Tactic:
intro ε hε
State after:
case intro
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
key : ∀ (R ε : ℝ), ε > 0 → ∀ᶠ (x : ℝ) in atTop, dist (S x (Ψ R).toFun) 0 < ε
key2 : ∀ ε > 0, ∀ᶠ (x : ℝ) in atTop, dist (W21.norm (ψ.toFun - (Ψ x).toFun)) 0 < ε
ε : ℝ
hε : ε > 0
⊢ ∀ᶠ (x : ℝ) in atTop, dist (S x ψ.toFun) 0 < ε

State before:
case intro
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
key : ∀ (R ε : ℝ), ε > 0 → ∀ᶠ (x : ℝ) in atTop, dist (S x (Ψ R).toFun) 0 < ε
key2 : ∀ ε > 0, ∀ᶠ (x : ℝ) in atTop, dist (W21.norm (ψ.toFun - (Ψ x).toFun)) 0 < ε
ε : ℝ
hε : ε > 0
⊢ ∀ᶠ (x : ℝ) in atTop, dist (S x ψ.toFun) 0 < ε
Tactic:
let M := C * (1 + 2 * π ^ 2) + ‖(A : ℂ)‖ * (2 * π ^ 2)
State after:
case intro
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
key : ∀ (R ε : ℝ), ε > 0 → ∀ᶠ (x : ℝ) in atTop, dist (S x (Ψ R).toFun) 0 < ε
key2 : ∀ ε > 0, ∀ᶠ (x : ℝ) in atTop, dist (W21.norm (ψ.toFun - (Ψ x).toFun)) 0 < ε
ε : ℝ
hε : ε > 0
M : ℝ := C * (1 + 2 * π ^ 2) + ‖↑A‖ * (2 * π ^ 2)
⊢ ∀ᶠ (x : ℝ) in atTop, dist (S x ψ.toFun) 0 < ε

State before:
case intro
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
key : ∀ (R ε : ℝ), ε > 0 → ∀ᶠ (x : ℝ) in atTop, dist (S x (Ψ R).toFun) 0 < ε
key2 : ∀ ε > 0, ∀ᶠ (x : ℝ) in atTop, dist (W21.norm (ψ.toFun - (Ψ x).toFun)) 0 < ε
ε : ℝ
hε : ε > 0
M : ℝ := C * (1 + 2 * π ^ 2) + ‖↑A‖ * (2 * π ^ 2)
⊢ ∀ᶠ (x : ℝ) in atTop, dist (S x ψ.toFun) 0 < ε
Tactic:
obtain ⟨R, hRψ⟩ := (key2 ((ε / 2) / (1 + M)) (by positivity)).exists
State after:
case intro.intro
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
key : ∀ (R ε : ℝ), ε > 0 → ∀ᶠ (x : ℝ) in atTop, dist (S x (Ψ R).toFun) 0 < ε
key2 : ∀ ε > 0, ∀ᶠ (x : ℝ) in atTop, dist (W21.norm (ψ.toFun - (Ψ x).toFun)) 0 < ε
ε : ℝ
hε : ε > 0
M : ℝ := C * (1 + 2 * π ^ 2) + ‖↑A‖ * (2 * π ^ 2)
R : ℝ
hRψ : dist (W21.norm (ψ.toFun - (Ψ R).toFun)) 0 < ε / 2 / (1 + M)
⊢ ∀ᶠ (x : ℝ) in atTop, dist (S x ψ.toFun) 0 < ε

State before:
case intro.intro
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
key : ∀ (R ε : ℝ), ε > 0 → ∀ᶠ (x : ℝ) in atTop, dist (S x (Ψ R).toFun) 0 < ε
key2 : ∀ ε > 0, ∀ᶠ (x : ℝ) in atTop, dist (W21.norm (ψ.toFun - (Ψ x).toFun)) 0 < ε
ε : ℝ
hε : ε > 0
M : ℝ := C * (1 + 2 * π ^ 2) + ‖↑A‖ * (2 * π ^ 2)
R : ℝ
hRψ : dist (W21.norm (ψ.toFun - (Ψ R).toFun)) 0 < ε / 2 / (1 + M)
⊢ ∀ᶠ (x : ℝ) in atTop, dist (S x ψ.toFun) 0 < ε
Tactic:
simp only [dist_zero_right, Real.norm_eq_abs, abs_eq_self.mpr W21.norm_nonneg] at hRψ key
State after:
case intro.intro
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 : ℝ) in atTop, dist (S x ψ.toFun) 0 < ε

State before:
case intro.intro
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 : ℝ) in atTop, dist (S x ψ.toFun) 0 < ε
Tactic:
filter_upwards [eventually_ge_atTop 1, key R (ε / 2) (by positivity)] with x hx key
State after:
case h
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
⊢ dist (S x ψ.toFun) 0 < ε

State before:
case h
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
⊢ dist (S x ψ.toFun) 0 < ε
Tactic:
have key3 : ‖S x (ψ - Ψ R)‖ < ε / 2 := by
  have : ‖S x _‖ ≤ _ * M := @bound_main f C A x hx (ψ - Ψ R) hcheby
  apply this.trans_lt
  apply (mul_le_mul (d := 1 + M) le_rfl (by simp) (by positivity) W21.norm_nonneg).trans_lt
  have : 0 < 1 + M := by positivity
  convert (mul_lt_mul_right this).mpr hRψ using 1 ; field_simp ; ring
State after:
case h
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
⊢ dist (S x ψ.toFun) 0 < ε

State before:
case h
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
S2_sub : S2 x (ψ.toFun - (Ψ R).toFun) = S2 x ψ.toFun - S2 x (Ψ R).toFun
⊢ dist (S x ψ.toFun) 0 < ε
Tactic:
have S_sub : S x (ψ - Ψ R) = S x ψ - S x (Ψ R) := by simp [S, S1_sub, S2_sub] ; ring
State after:
case h
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
S2_sub : S2 x (ψ.toFun - (Ψ R).toFun) = S2 x ψ.toFun - S2 x (Ψ R).toFun
S_sub : S x (ψ.toFun - (Ψ R).toFun) = S x ψ.toFun - S x (Ψ R).toFun
⊢ dist (S x ψ.toFun) 0 < ε

State before:
case h
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
S2_sub : S2 x (ψ.toFun - (Ψ R).toFun) = S2 x ψ.toFun - S2 x (Ψ R).toFun
S_sub : S x (ψ.toFun - (Ψ R).toFun) = S x ψ.toFun - S x (Ψ R).toFun
⊢ dist (S x ψ.toFun) 0 < ε
Tactic:
simpa [S_sub, Ψ] using norm_add_le _ _ |>.trans_lt (_root_.add_lt_add key3 key)
State after:
no goals

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 * ψ
key : ∀ (R : ℝ), Tendsto (fun x => S x (Ψ R).toFun) atTop (𝓝 0)
C : ℝ
hcheby : chebyWith C f
⊢ 0 ≤ C
Tactic:
have : ‖f 0‖ ≤ C := by simpa [cumsum] using hcheby 1
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 * ψ
key : ∀ (R : ℝ), Tendsto (fun x => S x (Ψ R).toFun) atTop (𝓝 0)
C : ℝ
hcheby : chebyWith C f
this : ‖f 0‖ ≤ C
⊢ 0 ≤ C

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 * ψ
key : ∀ (R : ℝ), Tendsto (fun x => S x (Ψ R).toFun) atTop (𝓝 0)
C : ℝ
hcheby : chebyWith C f
this : ‖f 0‖ ≤ C
⊢ 0 ≤ C
Tactic:
have : 0 ≤ ‖f 0‖ := by positivity
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 * ψ
key : ∀ (R : ℝ), Tendsto (fun x => S x (Ψ R).toFun) atTop (𝓝 0)
C : ℝ
hcheby : chebyWith C f
this✝ : ‖f 0‖ ≤ C
this : 0 ≤ ‖f 0‖
⊢ 0 ≤ C

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 * ψ
key : ∀ (R : ℝ), Tendsto (fun x => S x (Ψ R).toFun) atTop (𝓝 0)
C : ℝ
hcheby : chebyWith C f
this✝ : ‖f 0‖ ≤ C
this : 0 ≤ ‖f 0‖
⊢ 0 ≤ C
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 𝕜
ψ : 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 * ψ
key : ∀ (R : ℝ), Tendsto (fun x => S x (Ψ R).toFun) atTop (𝓝 0)
C : ℝ
hcheby : chebyWith C f
⊢ ‖f 0‖ ≤ C
Tactic:
simpa [cumsum] using hcheby 1
State after:
no goals

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 * ψ
key : ∀ (R : ℝ), Tendsto (fun x => S x (Ψ R).toFun) atTop (𝓝 0)
C : ℝ
hcheby : chebyWith C f
this : ‖f 0‖ ≤ C
⊢ 0 ≤ ‖f 0‖
Tactic:
positivity
State after:
no goals

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
key : ∀ (R ε : ℝ), ε > 0 → ∀ᶠ (x : ℝ) in atTop, dist (S x (Ψ R).toFun) 0 < ε
key2 : ∀ ε > 0, ∀ᶠ (x : ℝ) in atTop, dist (W21.norm (ψ.toFun - (Ψ x).toFun)) 0 < ε
ε : ℝ
hε : ε > 0
M : ℝ := C * (1 + 2 * π ^ 2) + ‖↑A‖ * (2 * π ^ 2)
⊢ ε / 2 / (1 + M) > 0
Tactic:
positivity
State after:
no goals

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‖ < ε
⊢ ε / 2 > 0
Tactic:
positivity
State after:
no goals

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
⊢ ‖S x (ψ.toFun - (Ψ R).toFun)‖ < ε / 2
Tactic:
have : ‖S x _‖ ≤ _ * M := @bound_main f C A x hx (ψ - Ψ R) hcheby
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
this : ‖S x (ψ - W21.ofCS2 (Ψ R)).toFun‖ ≤ W21.norm (ψ - W21.ofCS2 (Ψ R)).toFun * M
⊢ ‖S x (ψ.toFun - (Ψ R).toFun)‖ < ε / 2

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
this : ‖S x (ψ - W21.ofCS2 (Ψ R)).toFun‖ ≤ W21.norm (ψ - W21.ofCS2 (Ψ R)).toFun * M
⊢ ‖S x (ψ.toFun - (Ψ R).toFun)‖ < ε / 2
Tactic:
apply this.trans_lt
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
this : ‖S x (ψ - W21.ofCS2 (Ψ R)).toFun‖ ≤ W21.norm (ψ - W21.ofCS2 (Ψ R)).toFun * M
⊢ W21.norm (ψ - W21.ofCS2 (Ψ R)).toFun * M < ε / 2

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
this : ‖S x (ψ - W21.ofCS2 (Ψ R)).toFun‖ ≤ W21.norm (ψ - W21.ofCS2 (Ψ R)).toFun * M
⊢ W21.norm (ψ - W21.ofCS2 (Ψ R)).toFun * M < ε / 2
Tactic:
apply (mul_le_mul (d := 1 + M) le_rfl (by simp) (by positivity) W21.norm_nonneg).trans_lt
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
this : ‖S x (ψ - W21.ofCS2 (Ψ R)).toFun‖ ≤ W21.norm (ψ - W21.ofCS2 (Ψ R)).toFun * M
⊢ W21.norm (ψ - W21.ofCS2 (Ψ R)).toFun * (1 + M) < ε / 2

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
this : ‖S x (ψ - W21.ofCS2 (Ψ R)).toFun‖ ≤ W21.norm (ψ - W21.ofCS2 (Ψ R)).toFun * M
⊢ W21.norm (ψ - W21.ofCS2 (Ψ R)).toFun * (1 + M) < ε / 2
Tactic:
have : 0 < 1 + M := by positivity
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
this✝ : ‖S x (ψ - W21.ofCS2 (Ψ R)).toFun‖ ≤ W21.norm (ψ - W21.ofCS2 (Ψ R)).toFun * M
this : 0 < 1 + M
⊢ W21.norm (ψ - W21.ofCS2 (Ψ R)).toFun * (1 + M) < ε / 2

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
this✝ : ‖S x (ψ - W21.ofCS2 (Ψ R)).toFun‖ ≤ W21.norm (ψ - W21.ofCS2 (Ψ R)).toFun * M
this : 0 < 1 + M
⊢ W21.norm (ψ - W21.ofCS2 (Ψ R)).toFun * (1 + M) < ε / 2
Tactic:
convert (mul_lt_mul_right this).mpr hRψ using 1
State after:
case h.e'_4
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
this✝ : ‖S x (ψ - W21.ofCS2 (Ψ R)).toFun‖ ≤ W21.norm (ψ - W21.ofCS2 (Ψ R)).toFun * M
this : 0 < 1 + M
⊢ ε / 2 = ε / 2 / (1 + M) * (1 + M)

State before:
case h.e'_4
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
this✝ : ‖S x (ψ - W21.ofCS2 (Ψ R)).toFun‖ ≤ W21.norm (ψ - W21.ofCS2 (Ψ R)).toFun * M
this : 0 < 1 + M
⊢ ε / 2 = ε / 2 / (1 + M) * (1 + M)
Tactic:
field_simp
State after:
case h.e'_4
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
this✝ : ‖S x (ψ - W21.ofCS2 (Ψ R)).toFun‖ ≤ W21.norm (ψ - W21.ofCS2 (Ψ R)).toFun * M
this : 0 < 1 + M
⊢ ε * (2 * (1 + M)) = ε * (1 + M) * 2

State before:
case h.e'_4
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
this✝ : ‖S x (ψ - W21.ofCS2 (Ψ R)).toFun‖ ≤ W21.norm (ψ - W21.ofCS2 (Ψ R)).toFun * M
this : 0 < 1 + M
⊢ ε * (2 * (1 + M)) = ε * (1 + M) * 2
Tactic:
ring
State after:
no goals

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
this : ‖S x (ψ - W21.ofCS2 (Ψ R)).toFun‖ ≤ W21.norm (ψ - W21.ofCS2 (Ψ R)).toFun * M
⊢ M ≤ 1 + M
Tactic:
simp
State after:
no goals

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
this : ‖S x (ψ - W21.ofCS2 (Ψ R)).toFun‖ ≤ W21.norm (ψ - W21.ofCS2 (Ψ R)).toFun * M
⊢ 0 ≤ M
Tactic:
positivity
State after:
no goals

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
this : ‖S x (ψ - W21.ofCS2 (Ψ R)).toFun‖ ≤ W21.norm (ψ - W21.ofCS2 (Ψ R)).toFun * M
⊢ 0 < 1 + M
Tactic:
positivity
State after:
no goals

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
x : ℝ
⊢ 𝓕 (ψ.toFun - (Ψ R).toFun) x = 𝓕 ψ.toFun x - 𝓕 (Ψ R).toFun x
Tactic:
have l1 : AEStronglyMeasurable (fun x_1 : ℝ ↦ cexp (-(2 * ↑π * (↑x_1 * ↑x) * I))) volume := by
  refine (Continuous.mul ?_ continuous_const).neg.cexp.aestronglyMeasurable
  apply continuous_const.mul <| contDiff_ofReal.continuous.mul continuous_const
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
x : ℝ
l1 : AEStronglyMeasurable (fun x_1 => cexp (-(2 * ↑π * (↑x_1 * ↑x) * I))) volume
⊢ 𝓕 (ψ.toFun - (Ψ R).toFun) x = 𝓕 ψ.toFun x - 𝓕 (Ψ R).toFun x

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
x : ℝ
l1 : AEStronglyMeasurable (fun x_1 => cexp (-(2 * ↑π * (↑x_1 * ↑x) * I))) volume
⊢ 𝓕 (ψ.toFun - (Ψ R).toFun) x = 𝓕 ψ.toFun x - 𝓕 (Ψ R).toFun x
Tactic:
simp [Real.fourierIntegral_eq', mul_sub]
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
x : ℝ
l1 : AEStronglyMeasurable (fun x_1 => cexp (-(2 * ↑π * (↑x_1 * ↑x) * I))) volume
⊢ ∫ (v : ℝ), cexp (-(2 * ↑π * (↑v * ↑x) * I)) * ψ.toFun v - cexp (-(2 * ↑π * (↑v * ↑x) * I)) * (Ψ R).toFun v =
    (∫ (v : ℝ), cexp (-(2 * ↑π * (↑v * ↑x) * I)) * ψ.toFun v) -
      ∫ (v : ℝ), cexp (-(2 * ↑π * (↑v * ↑x) * I)) * (Ψ R).toFun v

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
x : ℝ
l1 : AEStronglyMeasurable (fun x_1 => cexp (-(2 * ↑π * (↑x_1 * ↑x) * I))) volume
⊢ ∫ (v : ℝ), cexp (-(2 * ↑π * (↑v * ↑x) * I)) * ψ.toFun v - cexp (-(2 * ↑π * (↑v * ↑x) * I)) * (Ψ R).toFun v =
    (∫ (v : ℝ), cexp (-(2 * ↑π * (↑v * ↑x) * I)) * ψ.toFun v) -
      ∫ (v : ℝ), cexp (-(2 * ↑π * (↑v * ↑x) * I)) * (Ψ R).toFun v
Tactic:
apply integral_sub
State after:
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
x : ℝ
l1 : AEStronglyMeasurable (fun x_1 => cexp (-(2 * ↑π * (↑x_1 * ↑x) * I))) volume
⊢ Integrable (fun a => cexp (-(2 * ↑π * (↑a * ↑x) * I)) * ψ.toFun a) volume

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
x : ℝ
l1 : AEStronglyMeasurable (fun x_1 => cexp (-(2 * ↑π * (↑x_1 * ↑x) * I))) volume
⊢ Integrable (fun a => cexp (-(2 * ↑π * (↑a * ↑x) * I)) * (Ψ R).toFun a) volume

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
x : ℝ
⊢ AEStronglyMeasurable (fun x_1 => cexp (-(2 * ↑π * (↑x_1 * ↑x) * I))) volume
Tactic:
refine (Continuous.mul ?_ continuous_const).neg.cexp.aestronglyMeasurable
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
x : ℝ
⊢ Continuous fun x_1 => 2 * ↑π * (↑x_1 * ↑x)

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
x : ℝ
⊢ Continuous fun x_1 => 2 * ↑π * (↑x_1 * ↑x)
Tactic:
apply continuous_const.mul <| contDiff_ofReal.continuous.mul continuous_const
State after:
no goals

State before:
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
x : ℝ
l1 : AEStronglyMeasurable (fun x_1 => cexp (-(2 * ↑π * (↑x_1 * ↑x) * I))) volume
⊢ Integrable (fun a => cexp (-(2 * ↑π * (↑a * ↑x) * I)) * ψ.toFun a) volume
Tactic:
apply ψ.hf.bdd_mul l1
State after:
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
x : ℝ
l1 : AEStronglyMeasurable (fun x_1 => cexp (-(2 * ↑π * (↑x_1 * ↑x) * I))) volume
⊢ ∃ C, ∀ (x_1 : ℝ), ‖cexp (-(2 * ↑π * (↑x_1 * ↑x) * I))‖ ≤ C

State before:
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
x : ℝ
l1 : AEStronglyMeasurable (fun x_1 => cexp (-(2 * ↑π * (↑x_1 * ↑x) * I))) volume
⊢ ∃ C, ∀ (x_1 : ℝ), ‖cexp (-(2 * ↑π * (↑x_1 * ↑x) * I))‖ ≤ C
Tactic:
use 1
State after:
case h
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
x : ℝ
l1 : AEStronglyMeasurable (fun x_1 => cexp (-(2 * ↑π * (↑x_1 * ↑x) * I))) volume
⊢ ∀ (x_1 : ℝ), ‖cexp (-(2 * ↑π * (↑x_1 * ↑x) * I))‖ ≤ 1

State before:
case h
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
x : ℝ
l1 : AEStronglyMeasurable (fun x_1 => cexp (-(2 * ↑π * (↑x_1 * ↑x) * I))) volume
⊢ ∀ (x_1 : ℝ), ‖cexp (-(2 * ↑π * (↑x_1 * ↑x) * I))‖ ≤ 1
Tactic:
simp [Complex.norm_eq_abs, Complex.abs_exp]
State after:
no goals

State before:
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
x : ℝ
l1 : AEStronglyMeasurable (fun x_1 => cexp (-(2 * ↑π * (↑x_1 * ↑x) * I))) volume
⊢ Integrable (fun a => cexp (-(2 * ↑π * (↑a * ↑x) * I)) * (Ψ R).toFun a) volume
Tactic:
apply (Ψ R : W21) |>.hf |>.bdd_mul l1
State after:
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
x : ℝ
l1 : AEStronglyMeasurable (fun x_1 => cexp (-(2 * ↑π * (↑x_1 * ↑x) * I))) volume
⊢ ∃ C, ∀ (x_1 : ℝ), ‖cexp (-(2 * ↑π * (↑x_1 * ↑x) * I))‖ ≤ C

State before:
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
x : ℝ
l1 : AEStronglyMeasurable (fun x_1 => cexp (-(2 * ↑π * (↑x_1 * ↑x) * I))) volume
⊢ ∃ C, ∀ (x_1 : ℝ), ‖cexp (-(2 * ↑π * (↑x_1 * ↑x) * I))‖ ≤ C
Tactic:
use 1
State after:
case h
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
x : ℝ
l1 : AEStronglyMeasurable (fun x_1 => cexp (-(2 * ↑π * (↑x_1 * ↑x) * I))) volume
⊢ ∀ (x_1 : ℝ), ‖cexp (-(2 * ↑π * (↑x_1 * ↑x) * I))‖ ≤ 1

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 x (ψ.toFun - (Ψ R).toFun) = S1 x ψ.toFun - S1 x (Ψ R).toFun
Tactic:
simp [S1, S1_sub_1, mul_sub]
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
⊢ ∑' (n : ℕ), (f n / ↑n * 𝓕 ψ.toFun (π⁻¹ * 2⁻¹ * (↑n / x).log) - f n / ↑n * 𝓕 (Ψ R).toFun (π⁻¹ * 2⁻¹ * (↑n / x).log)) =
    ∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (π⁻¹ * 2⁻¹ * (↑n / x).log) -
      ∑' (n : ℕ), f n / ↑n * 𝓕 (Ψ R).toFun (π⁻¹ * 2⁻¹ * (↑n / x).log)

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
⊢ ∑' (n : ℕ), (f n / ↑n * 𝓕 ψ.toFun (π⁻¹ * 2⁻¹ * (↑n / x).log) - f n / ↑n * 𝓕 (Ψ R).toFun (π⁻¹ * 2⁻¹ * (↑n / x).log)) =
    ∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (π⁻¹ * 2⁻¹ * (↑n / x).log) -
      ∑' (n : ℕ), f n / ↑n * 𝓕 (Ψ R).toFun (π⁻¹ * 2⁻¹ * (↑n / x).log)
Tactic:
apply tsum_sub
State after:
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
⊢ Summable fun b => f b / ↑b * 𝓕 ψ.toFun (π⁻¹ * 2⁻¹ * (↑b / 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
⊢ Summable fun b => f b / ↑b * 𝓕 (Ψ R).toFun (π⁻¹ * 2⁻¹ * (↑b / x).log)

State before:
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
⊢ Summable fun b => f b / ↑b * 𝓕 ψ.toFun (π⁻¹ * 2⁻¹ * (↑b / x).log)
Tactic:
have := summable_fourier x (by positivity) ψ ⟨_, hcheby⟩
State after:
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
this : Summable fun i => ‖f i / ↑i * 𝓕 ψ.toFun (1 / (2 * π) * (↑i / x).log)‖
⊢ Summable fun b => f b / ↑b * 𝓕 ψ.toFun (π⁻¹ * 2⁻¹ * (↑b / x).log)

State before:
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
this : Summable fun i => ‖f i / ↑i * 𝓕 ψ.toFun (1 / (2 * π) * (↑i / x).log)‖
⊢ Summable fun b => f b / ↑b * 𝓕 ψ.toFun (π⁻¹ * 2⁻¹ * (↑b / x).log)
Tactic:
rw [summable_norm_iff] at this
State after:
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
this : Summable fun i => f i / ↑i * 𝓕 ψ.toFun (1 / (2 * π) * (↑i / x).log)
⊢ Summable fun b => f b / ↑b * 𝓕 ψ.toFun (π⁻¹ * 2⁻¹ * (↑b / x).log)

State before:
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
this : Summable fun i => f i / ↑i * 𝓕 ψ.toFun (1 / (2 * π) * (↑i / x).log)
⊢ Summable fun b => f b / ↑b * 𝓕 ψ.toFun (π⁻¹ * 2⁻¹ * (↑b / x).log)
Tactic:
simpa using this
State after:
no goals

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
⊢ 0 < x
Tactic:
positivity
State after:
no goals

State before:
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
⊢ Summable fun b => f b / ↑b * 𝓕 (Ψ R).toFun (π⁻¹ * 2⁻¹ * (↑b / x).log)
Tactic:
have := summable_fourier x (by positivity) (Ψ R) ⟨_, hcheby⟩
State after:
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
this : Summable fun i => ‖f i / ↑i * 𝓕 (W21.ofCS2 (Ψ R)).toFun (1 / (2 * π) * (↑i / x).log)‖
⊢ Summable fun b => f b / ↑b * 𝓕 (Ψ R).toFun (π⁻¹ * 2⁻¹ * (↑b / x).log)

State before:
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
this : Summable fun i => ‖f i / ↑i * 𝓕 (W21.ofCS2 (Ψ R)).toFun (1 / (2 * π) * (↑i / x).log)‖
⊢ Summable fun b => f b / ↑b * 𝓕 (Ψ R).toFun (π⁻¹ * 2⁻¹ * (↑b / x).log)
Tactic:
rw [summable_norm_iff] at this
State after:
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
this : Summable fun i => f i / ↑i * 𝓕 (W21.ofCS2 (Ψ R)).toFun (1 / (2 * π) * (↑i / x).log)
⊢ Summable fun b => f b / ↑b * 𝓕 (Ψ R).toFun (π⁻¹ * 2⁻¹ * (↑b / x).log)

State before:
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
this : Summable fun i => f i / ↑i * 𝓕 (W21.ofCS2 (Ψ R)).toFun (1 / (2 * π) * (↑i / x).log)
⊢ Summable fun b => f b / ↑b * 𝓕 (Ψ R).toFun (π⁻¹ * 2⁻¹ * (↑b / x).log)
Tactic:
simpa using this
State after:
no goals

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
⊢ S2 x (ψ.toFun - (Ψ R).toFun) = S2 x ψ.toFun - S2 x (Ψ R).toFun
Tactic:
simp [S2, S1_sub_1]
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 * ∫ (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 * π))

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]
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)))

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 * ((∫ (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)))
Tactic:
ring
State after:
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)))

State before:
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)))
Tactic:
exact ψ.integrable_fourier (by positivity) |>.restrict
State after:
no goals

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
⊢ 2 * π ≠ 0
Tactic:
positivity
State after:
no goals

State before:
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)))
Tactic:
exact (Ψ R : W21).integrable_fourier (by positivity) |>.restrict
State after:
no goals

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
S2_sub : S2 x (ψ.toFun - (Ψ R).toFun) = S2 x ψ.toFun - S2 x (Ψ R).toFun
⊢ S x (ψ.toFun - (Ψ R).toFun) = S x ψ.toFun - S x (Ψ R).toFun
Tactic:
simp [S, S1_sub, S2_sub]
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
S2_sub : S2 x (ψ.toFun - (Ψ R).toFun) = S2 x ψ.toFun - S2 x (Ψ R).toFun
⊢ S1 x ψ.toFun - S1 x (Ψ R).toFun - (S2 x ψ.toFun - S2 x (Ψ R).toFun) =
    S1 x ψ.toFun - S2 x ψ.toFun - (S1 x (Ψ R).toFun - S2 x (Ψ R).toFun)

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
S2_sub : S2 x (ψ.toFun - (Ψ R).toFun) = S2 x ψ.toFun - S2 x (Ψ R).toFun
⊢ S1 x ψ.toFun - S1 x (Ψ R).toFun - (S2 x ψ.toFun - S2 x (Ψ R).toFun) =
    S1 x ψ.toFun - S2 x ψ.toFun - (S1 x (Ψ R).toFun - S2 x (Ψ R).toFun)
Tactic:
ring
State after:
no goals