internlm/Lean-Github huggingface dataset:
Theorem: limiting_cor_W21
Proof 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
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
key3 : ‖S x (ψ.toFun - (Ψ R).toFun)‖ < ε / 2
⊢ dist (S x ψ.toFun) 0 < ε
Theorem: limiting_cor_W21
Proof 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
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
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 < ε
Theorem: limiting_cor_W21
Proof 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)
Proof state after:
no goals
Theorem: limiting_cor_W21
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
S1 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ∑' (n : ℕ), f n / ↑n * 𝓕 ψ (1 / (2 * π) * (↑n / x).log)
S2 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ (u / (2 * π))
S : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => S1 x ψ - S2 x ψ
g : trunc
Ψ : ℝ → CS 2 ℂ := fun R => g.scale R * ψ
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
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
S1 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ∑' (n : ℕ), f n / ↑n * 𝓕 ψ (1 / (2 * π) * (↑n / x).log)
S2 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ (u / (2 * π))
S : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => S1 x ψ - S2 x ψ
g : trunc
Ψ : ℝ → CS 2 ℂ := fun R => g.scale R * ψ
key : ∀ (R : ℝ), Tendsto (fun x => S x (Ψ R).toFun) atTop (𝓝 0)
C : ℝ
hcheby : chebyWith C f
this : ‖f 0‖ ≤ C
⊢ 0 ≤ C
Theorem: limiting_cor_W21
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
S1 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ∑' (n : ℕ), f n / ↑n * 𝓕 ψ (1 / (2 * π) * (↑n / x).log)
S2 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ (u / (2 * π))
S : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => S1 x ψ - S2 x ψ
g : trunc
Ψ : ℝ → CS 2 ℂ := fun R => g.scale R * ψ
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
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
S1 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ∑' (n : ℕ), f n / ↑n * 𝓕 ψ (1 / (2 * π) * (↑n / x).log)
S2 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ (u / (2 * π))
S : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => S1 x ψ - S2 x ψ
g : trunc
Ψ : ℝ → CS 2 ℂ := fun R => g.scale R * ψ
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
Theorem: limiting_cor_W21
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
S1 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ∑' (n : ℕ), f n / ↑n * 𝓕 ψ (1 / (2 * π) * (↑n / x).log)
S2 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ (u / (2 * π))
S : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => S1 x ψ - S2 x ψ
g : trunc
Ψ : ℝ → CS 2 ℂ := fun R => g.scale R * ψ
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
Proof state after:
no goals
Theorem: limiting_cor_W21
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
S1 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ∑' (n : ℕ), f n / ↑n * 𝓕 ψ (1 / (2 * π) * (↑n / x).log)
S2 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ (u / (2 * π))
S : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => S1 x ψ - S2 x ψ
g : trunc
Ψ : ℝ → CS 2 ℂ := fun R => g.scale R * ψ
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
Proof state after:
no goals
Theorem: limiting_cor_W21
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
S1 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ∑' (n : ℕ), f n / ↑n * 𝓕 ψ (1 / (2 * π) * (↑n / x).log)
S2 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ (u / (2 * π))
S : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => S1 x ψ - S2 x ψ
g : trunc
Ψ : ℝ → CS 2 ℂ := fun R => g.scale R * ψ
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
Proof state after:
no goals
Theorem: limiting_cor_W21
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
S1 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ∑' (n : ℕ), f n / ↑n * 𝓕 ψ (1 / (2 * π) * (↑n / x).log)
S2 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ (u / (2 * π))
S : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => S1 x ψ - S2 x ψ
g : trunc
Ψ : ℝ → CS 2 ℂ := fun R => g.scale R * ψ
C : ℝ
hcheby : chebyWith C f
hC : 0 ≤ C
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
Proof state after:
no goals
Theorem: limiting_cor_W21
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
S1 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ∑' (n : ℕ), f n / ↑n * 𝓕 ψ (1 / (2 * π) * (↑n / x).log)
S2 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ (u / (2 * π))
S : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => S1 x ψ - S2 x ψ
g : trunc
Ψ : ℝ → CS 2 ℂ := fun R => g.scale R * ψ
C : ℝ
hcheby : chebyWith C f
hC : 0 ≤ C
key2 : ∀ ε > 0, ∀ᶠ (x : ℝ) in atTop, dist (W21.norm (ψ.toFun - (Ψ x).toFun)) 0 < ε
ε : ℝ
hε : ε > 0
M : ℝ := C * (1 + 2 * π ^ 2) + ‖↑A‖ * (2 * π ^ 2)
R : ℝ
hRψ : W21.norm (ψ.toFun - (Ψ R).toFun) < ε / 2 / (1 + M)
key : ∀ (R ε : ℝ), ε > 0 → ∀ᶠ (x : ℝ) in atTop, ‖S x (Ψ R).toFun‖ < ε
⊢ ε / 2 > 0
Tactic:
positivity
Proof state after:
no goals
Theorem: limiting_cor_W21
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
S1 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ∑' (n : ℕ), f n / ↑n * 𝓕 ψ (1 / (2 * π) * (↑n / x).log)
S2 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ (u / (2 * π))
S : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => S1 x ψ - S2 x ψ
g : trunc
Ψ : ℝ → CS 2 ℂ := fun R => g.scale R * ψ
C : ℝ
hcheby : chebyWith C f
hC : 0 ≤ C
key2 : ∀ ε > 0, ∀ᶠ (x : ℝ) in atTop, dist (W21.norm (ψ.toFun - (Ψ x).toFun)) 0 < ε
ε : ℝ
hε : ε > 0
M : ℝ := C * (1 + 2 * π ^ 2) + ‖↑A‖ * (2 * π ^ 2)
R : ℝ
hRψ : W21.norm (ψ.toFun - (Ψ R).toFun) < ε / 2 / (1 + M)
key✝ : ∀ (R ε : ℝ), ε > 0 → ∀ᶠ (x : ℝ) in atTop, ‖S x (Ψ R).toFun‖ < ε
x : ℝ
hx : 1 ≤ x
key : ‖S x (Ψ R).toFun‖ < ε / 2
⊢ ‖S x (ψ.toFun - (Ψ R).toFun)‖ < ε / 2
Tactic:
have : ‖S x _‖ ≤ _ * M := @bound_main f C A x hx (ψ - Ψ R) hcheby
Proof state after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
S1 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ∑' (n : ℕ), f n / ↑n * 𝓕 ψ (1 / (2 * π) * (↑n / x).log)
S2 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ (u / (2 * π))
S : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => S1 x ψ - S2 x ψ
g : trunc
Ψ : ℝ → CS 2 ℂ := fun R => g.scale R * ψ
C : ℝ
hcheby : chebyWith C f
hC : 0 ≤ C
key2 : ∀ ε > 0, ∀ᶠ (x : ℝ) in atTop, dist (W21.norm (ψ.toFun - (Ψ x).toFun)) 0 < ε
ε : ℝ
hε : ε > 0
M : ℝ := C * (1 + 2 * π ^ 2) + ‖↑A‖ * (2 * π ^ 2)
R : ℝ
hRψ : W21.norm (ψ.toFun - (Ψ R).toFun) < ε / 2 / (1 + M)
key✝ : ∀ (R ε : ℝ), ε > 0 → ∀ᶠ (x : ℝ) in atTop, ‖S x (Ψ R).toFun‖ < ε
x : ℝ
hx : 1 ≤ x
key : ‖S x (Ψ R).toFun‖ < ε / 2
this : ‖S x (ψ - W21.ofCS2 (Ψ R)).toFun‖ ≤ W21.norm (ψ - W21.ofCS2 (Ψ R)).toFun * M
⊢ ‖S x (ψ.toFun - (Ψ R).toFun)‖ < ε / 2
Theorem: limiting_cor_W21
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
S1 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ∑' (n : ℕ), f n / ↑n * 𝓕 ψ (1 / (2 * π) * (↑n / x).log)
S2 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ (u / (2 * π))
S : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => S1 x ψ - S2 x ψ
g : trunc
Ψ : ℝ → CS 2 ℂ := fun R => g.scale R * ψ
C : ℝ
hcheby : chebyWith C f
hC : 0 ≤ C
key2 : ∀ ε > 0, ∀ᶠ (x : ℝ) in atTop, dist (W21.norm (ψ.toFun - (Ψ x).toFun)) 0 < ε
ε : ℝ
hε : ε > 0
M : ℝ := C * (1 + 2 * π ^ 2) + ‖↑A‖ * (2 * π ^ 2)
R : ℝ
hRψ : W21.norm (ψ.toFun - (Ψ R).toFun) < ε / 2 / (1 + M)
key✝ : ∀ (R ε : ℝ), ε > 0 → ∀ᶠ (x : ℝ) in atTop, ‖S x (Ψ R).toFun‖ < ε
x : ℝ
hx : 1 ≤ x
key : ‖S x (Ψ R).toFun‖ < ε / 2
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
Proof state after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
S1 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ∑' (n : ℕ), f n / ↑n * 𝓕 ψ (1 / (2 * π) * (↑n / x).log)
S2 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ (u / (2 * π))
S : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => S1 x ψ - S2 x ψ
g : trunc
Ψ : ℝ → CS 2 ℂ := fun R => g.scale R * ψ
C : ℝ
hcheby : chebyWith C f
hC : 0 ≤ C
key2 : ∀ ε > 0, ∀ᶠ (x : ℝ) in atTop, dist (W21.norm (ψ.toFun - (Ψ x).toFun)) 0 < ε
ε : ℝ
hε : ε > 0
M : ℝ := C * (1 + 2 * π ^ 2) + ‖↑A‖ * (2 * π ^ 2)
R : ℝ
hRψ : W21.norm (ψ.toFun - (Ψ R).toFun) < ε / 2 / (1 + M)
key✝ : ∀ (R ε : ℝ), ε > 0 → ∀ᶠ (x : ℝ) in atTop, ‖S x (Ψ R).toFun‖ < ε
x : ℝ
hx : 1 ≤ x
key : ‖S x (Ψ R).toFun‖ < ε / 2
this : ‖S x (ψ - W21.ofCS2 (Ψ R)).toFun‖ ≤ W21.norm (ψ - W21.ofCS2 (Ψ R)).toFun * M
⊢ W21.norm (ψ - W21.ofCS2 (Ψ R)).toFun * M < ε / 2
Theorem: limiting_cor_W21
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
S1 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ∑' (n : ℕ), f n / ↑n * 𝓕 ψ (1 / (2 * π) * (↑n / x).log)
S2 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ (u / (2 * π))
S : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => S1 x ψ - S2 x ψ
g : trunc
Ψ : ℝ → CS 2 ℂ := fun R => g.scale R * ψ
C : ℝ
hcheby : chebyWith C f
hC : 0 ≤ C
key2 : ∀ ε > 0, ∀ᶠ (x : ℝ) in atTop, dist (W21.norm (ψ.toFun - (Ψ x).toFun)) 0 < ε
ε : ℝ
hε : ε > 0
M : ℝ := C * (1 + 2 * π ^ 2) + ‖↑A‖ * (2 * π ^ 2)
R : ℝ
hRψ : W21.norm (ψ.toFun - (Ψ R).toFun) < ε / 2 / (1 + M)
key✝ : ∀ (R ε : ℝ), ε > 0 → ∀ᶠ (x : ℝ) in atTop, ‖S x (Ψ R).toFun‖ < ε
x : ℝ
hx : 1 ≤ x
key : ‖S x (Ψ R).toFun‖ < ε / 2
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
Proof state after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
S1 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ∑' (n : ℕ), f n / ↑n * 𝓕 ψ (1 / (2 * π) * (↑n / x).log)
S2 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ (u / (2 * π))
S : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => S1 x ψ - S2 x ψ
g : trunc
Ψ : ℝ → CS 2 ℂ := fun R => g.scale R * ψ
C : ℝ
hcheby : chebyWith C f
hC : 0 ≤ C
key2 : ∀ ε > 0, ∀ᶠ (x : ℝ) in atTop, dist (W21.norm (ψ.toFun - (Ψ x).toFun)) 0 < ε
ε : ℝ
hε : ε > 0
M : ℝ := C * (1 + 2 * π ^ 2) + ‖↑A‖ * (2 * π ^ 2)
R : ℝ
hRψ : W21.norm (ψ.toFun - (Ψ R).toFun) < ε / 2 / (1 + M)
key✝ : ∀ (R ε : ℝ), ε > 0 → ∀ᶠ (x : ℝ) in atTop, ‖S x (Ψ R).toFun‖ < ε
x : ℝ
hx : 1 ≤ x
key : ‖S x (Ψ R).toFun‖ < ε / 2
this : ‖S x (ψ - W21.ofCS2 (Ψ R)).toFun‖ ≤ W21.norm (ψ - W21.ofCS2 (Ψ R)).toFun * M
⊢ W21.norm (ψ - W21.ofCS2 (Ψ R)).toFun * (1 + M) < ε / 2
Theorem: limiting_cor_W21
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
S1 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ∑' (n : ℕ), f n / ↑n * 𝓕 ψ (1 / (2 * π) * (↑n / x).log)
S2 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ (u / (2 * π))
S : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => S1 x ψ - S2 x ψ
g : trunc
Ψ : ℝ → CS 2 ℂ := fun R => g.scale R * ψ
C : ℝ
hcheby : chebyWith C f
hC : 0 ≤ C
key2 : ∀ ε > 0, ∀ᶠ (x : ℝ) in atTop, dist (W21.norm (ψ.toFun - (Ψ x).toFun)) 0 < ε
ε : ℝ
hε : ε > 0
M : ℝ := C * (1 + 2 * π ^ 2) + ‖↑A‖ * (2 * π ^ 2)
R : ℝ
hRψ : W21.norm (ψ.toFun - (Ψ R).toFun) < ε / 2 / (1 + M)
key✝ : ∀ (R ε : ℝ), ε > 0 → ∀ᶠ (x : ℝ) in atTop, ‖S x (Ψ R).toFun‖ < ε
x : ℝ
hx : 1 ≤ x
key : ‖S x (Ψ R).toFun‖ < ε / 2
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
Proof state after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
S1 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ∑' (n : ℕ), f n / ↑n * 𝓕 ψ (1 / (2 * π) * (↑n / x).log)
S2 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ (u / (2 * π))
S : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => S1 x ψ - S2 x ψ
g : trunc
Ψ : ℝ → CS 2 ℂ := fun R => g.scale R * ψ
C : ℝ
hcheby : chebyWith C f
hC : 0 ≤ C
key2 : ∀ ε > 0, ∀ᶠ (x : ℝ) in atTop, dist (W21.norm (ψ.toFun - (Ψ x).toFun)) 0 < ε
ε : ℝ
hε : ε > 0
M : ℝ := C * (1 + 2 * π ^ 2) + ‖↑A‖ * (2 * π ^ 2)
R : ℝ
hRψ : W21.norm (ψ.toFun - (Ψ R).toFun) < ε / 2 / (1 + M)
key✝ : ∀ (R ε : ℝ), ε > 0 → ∀ᶠ (x : ℝ) in atTop, ‖S x (Ψ R).toFun‖ < ε
x : ℝ
hx : 1 ≤ x
key : ‖S x (Ψ R).toFun‖ < ε / 2
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
Theorem: limiting_cor_W21
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
S1 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ∑' (n : ℕ), f n / ↑n * 𝓕 ψ (1 / (2 * π) * (↑n / x).log)
S2 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ (u / (2 * π))
S : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => S1 x ψ - S2 x ψ
g : trunc
Ψ : ℝ → CS 2 ℂ := fun R => g.scale R * ψ
C : ℝ
hcheby : chebyWith C f
hC : 0 ≤ C
key2 : ∀ ε > 0, ∀ᶠ (x : ℝ) in atTop, dist (W21.norm (ψ.toFun - (Ψ x).toFun)) 0 < ε
ε : ℝ
hε : ε > 0
M : ℝ := C * (1 + 2 * π ^ 2) + ‖↑A‖ * (2 * π ^ 2)
R : ℝ
hRψ : W21.norm (ψ.toFun - (Ψ R).toFun) < ε / 2 / (1 + M)
key✝ : ∀ (R ε : ℝ), ε > 0 → ∀ᶠ (x : ℝ) in atTop, ‖S x (Ψ R).toFun‖ < ε
x : ℝ
hx : 1 ≤ x
key : ‖S x (Ψ R).toFun‖ < ε / 2
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
Proof 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)