internlm/Lean-Github huggingface dataset:
Theorem: limiting_cor_W21
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
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 ψ
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
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)
Theorem: limiting_cor_W21
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
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)
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
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)
Theorem: limiting_cor_W21
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
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
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
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)
Theorem: limiting_cor_W21
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
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 * ψ
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
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)
Theorem: limiting_cor_W21
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
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'
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
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)
Theorem: limiting_cor_W21
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
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
Proof 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)
Theorem: limiting_cor_W21
Proof 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
Proof 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)
Theorem: limiting_cor_W21
Proof 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
Proof 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)
Theorem: limiting_cor_W21
Proof 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 ⊢
Proof 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 < ε
Theorem: limiting_cor_W21
Proof 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ε
Proof 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 < ε
Theorem: limiting_cor_W21
Proof 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)
Proof 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 < ε
Theorem: limiting_cor_W21
Proof 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
Proof 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 < ε
Theorem: limiting_cor_W21
Proof 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
Proof 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 < ε
Theorem: limiting_cor_W21
Proof 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
Proof 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 < ε