internlm/Lean-Github huggingface dataset:
Theorem: WI_sum_Iab_le
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
hxb' : 2 < x * b
l1 : ∀ i ∉ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) = 0
l2 : ∀ i ∈ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) ≤ |f i|
this✝ : cumsum (fun x => |f x|) ⌈b * x⌉₊ ≤ C * ↑⌈b * x⌉₊
this : 0 ≤ C
⊢ 0 ≤ b * x
Tactic:
positivity
Proof state after:
no goals
Theorem: WI_sum_Iab_le'
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
⊢ ∀ᶠ (x : ℝ) in atTop, (∑' (n : ℕ), f n * (Ico a b).indicator 1 (↑n / x)) / x ≤ C * 2 * b
Tactic:
filter_upwards [eventually_gt_atTop (2 / b)] with x hx using WI_sum_Iab_le hpos hcheby hb hx
Proof state after:
no goals
Theorem: le_of_eventually_nhdsWithin
Proof state before:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
h : ∀ᶠ (c : ℝ) in 𝓝[>] b, a ≤ c
⊢ a ≤ b
Tactic:
apply le_of_forall_lt'
Proof state after:
case H
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
h : ∀ᶠ (c : ℝ) in 𝓝[>] b, a ≤ c
⊢ ∀ (c : ℝ), b < c → a < c
Theorem: le_of_eventually_nhdsWithin
Proof state before:
case H
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
h : ∀ᶠ (c : ℝ) in 𝓝[>] b, a ≤ c
⊢ ∀ (c : ℝ), b < c → a < c
Tactic:
intro d hd
Proof state after:
case H
n : ℕ
A a✝ b✝ c d✝ u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
h : ∀ᶠ (c : ℝ) in 𝓝[>] b, a ≤ c
d : ℝ
hd : b < d
⊢ a < d
Theorem: le_of_eventually_nhdsWithin
Proof state before:
case H
n : ℕ
A a✝ b✝ c d✝ u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
h : ∀ᶠ (c : ℝ) in 𝓝[>] b, a ≤ c
d : ℝ
hd : b < d
⊢ a < d
Tactic:
have key : ∀ᶠ c in 𝓝[>] b, c < d := by
  apply eventually_of_mem (U := Iio d) ?_ (fun x hx => hx)
  rw [mem_nhdsWithin]
  refine ⟨Iio d, isOpen_Iio, hd, inter_subset_left _ _⟩
Proof state after:
case H
n : ℕ
A a✝ b✝ c d✝ u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
h : ∀ᶠ (c : ℝ) in 𝓝[>] b, a ≤ c
d : ℝ
hd : b < d
key : ∀ᶠ (c : ℝ) in 𝓝[>] b, c < d
⊢ a < d
Theorem: le_of_eventually_nhdsWithin
Proof state before:
case H
n : ℕ
A a✝ b✝ c d✝ u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
h : ∀ᶠ (c : ℝ) in 𝓝[>] b, a ≤ c
d : ℝ
hd : b < d
key : ∀ᶠ (c : ℝ) in 𝓝[>] b, c < d
⊢ a < d
Tactic:
obtain ⟨x, h1, h2⟩ := (h.and key).exists
Proof state after:
case H.intro.intro
n : ℕ
A a✝ b✝ c d✝ u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
h : ∀ᶠ (c : ℝ) in 𝓝[>] b, a ≤ c
d : ℝ
hd : b < d
key : ∀ᶠ (c : ℝ) in 𝓝[>] b, c < d
x : ℝ
h1 : a ≤ x
h2 : x < d
⊢ a < d
Theorem: le_of_eventually_nhdsWithin
Proof state before:
case H.intro.intro
n : ℕ
A a✝ b✝ c d✝ u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
h : ∀ᶠ (c : ℝ) in 𝓝[>] b, a ≤ c
d : ℝ
hd : b < d
key : ∀ᶠ (c : ℝ) in 𝓝[>] b, c < d
x : ℝ
h1 : a ≤ x
h2 : x < d
⊢ a < d
Tactic:
linarith
Proof state after:
no goals
Theorem: le_of_eventually_nhdsWithin
Proof state before:
n : ℕ
A a✝ b✝ c d✝ u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
h : ∀ᶠ (c : ℝ) in 𝓝[>] b, a ≤ c
d : ℝ
hd : b < d
⊢ ∀ᶠ (c : ℝ) in 𝓝[>] b, c < d
Tactic:
apply eventually_of_mem (U := Iio d) ?_ (fun x hx => hx)
Proof state after:
n : ℕ
A a✝ b✝ c d✝ u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
h : ∀ᶠ (c : ℝ) in 𝓝[>] b, a ≤ c
d : ℝ
hd : b < d
⊢ Iio d ∈ 𝓝[>] b
Theorem: le_of_eventually_nhdsWithin
Proof state before:
n : ℕ
A a✝ b✝ c d✝ u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
h : ∀ᶠ (c : ℝ) in 𝓝[>] b, a ≤ c
d : ℝ
hd : b < d
⊢ Iio d ∈ 𝓝[>] b
Tactic:
rw [mem_nhdsWithin]
Proof state after:
n : ℕ
A a✝ b✝ c d✝ u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
h : ∀ᶠ (c : ℝ) in 𝓝[>] b, a ≤ c
d : ℝ
hd : b < d
⊢ ∃ u, IsOpen u ∧ b ∈ u ∧ u ∩ Ioi b ⊆ Iio d
Theorem: le_of_eventually_nhdsWithin
Proof state before:
n : ℕ
A a✝ b✝ c d✝ u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
h : ∀ᶠ (c : ℝ) in 𝓝[>] b, a ≤ c
d : ℝ
hd : b < d
⊢ ∃ u, IsOpen u ∧ b ∈ u ∧ u ∩ Ioi b ⊆ Iio d
Tactic:
refine ⟨Iio d, isOpen_Iio, hd, inter_subset_left _ _⟩
Proof state after:
no goals
Theorem: ge_of_eventually_nhdsWithin
Proof state before:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
h : ∀ᶠ (c : ℝ) in 𝓝[<] b, c ≤ a
⊢ b ≤ a
Tactic:
apply le_of_forall_lt
Proof state after:
case H
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
h : ∀ᶠ (c : ℝ) in 𝓝[<] b, c ≤ a
⊢ ∀ c < b, c < a
Theorem: ge_of_eventually_nhdsWithin
Proof state before:
case H
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
h : ∀ᶠ (c : ℝ) in 𝓝[<] b, c ≤ a
⊢ ∀ c < b, c < a
Tactic:
intro d hd
Proof state after:
case H
n : ℕ
A a✝ b✝ c d✝ u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
h : ∀ᶠ (c : ℝ) in 𝓝[<] b, c ≤ a
d : ℝ
hd : d < b
⊢ d < a
Theorem: ge_of_eventually_nhdsWithin
Proof state before:
case H
n : ℕ
A a✝ b✝ c d✝ u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
h : ∀ᶠ (c : ℝ) in 𝓝[<] b, c ≤ a
d : ℝ
hd : d < b
⊢ d < a
Tactic:
have key : ∀ᶠ c in 𝓝[<] b, c > d := by
  apply eventually_of_mem (U := Ioi d) ?_ (fun x hx => hx)
  rw [mem_nhdsWithin]
  refine ⟨Ioi d, isOpen_Ioi, hd, inter_subset_left _ _⟩
Proof state after:
case H
n : ℕ
A a✝ b✝ c d✝ u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
h : ∀ᶠ (c : ℝ) in 𝓝[<] b, c ≤ a
d : ℝ
hd : d < b
key : ∀ᶠ (c : ℝ) in 𝓝[<] b, c > d
⊢ d < a
Theorem: ge_of_eventually_nhdsWithin
Proof state before:
case H
n : ℕ
A a✝ b✝ c d✝ u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
h : ∀ᶠ (c : ℝ) in 𝓝[<] b, c ≤ a
d : ℝ
hd : d < b
key : ∀ᶠ (c : ℝ) in 𝓝[<] b, c > d
⊢ d < a
Tactic:
obtain ⟨x, h1, h2⟩ := (h.and key).exists
Proof state after:
case H.intro.intro
n : ℕ
A a✝ b✝ c d✝ u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
h : ∀ᶠ (c : ℝ) in 𝓝[<] b, c ≤ a
d : ℝ
hd : d < b
key : ∀ᶠ (c : ℝ) in 𝓝[<] b, c > d
x : ℝ
h1 : x ≤ a
h2 : x > d
⊢ d < a
Theorem: ge_of_eventually_nhdsWithin
Proof state before:
case H.intro.intro
n : ℕ
A a✝ b✝ c d✝ u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
h : ∀ᶠ (c : ℝ) in 𝓝[<] b, c ≤ a
d : ℝ
hd : d < b
key : ∀ᶠ (c : ℝ) in 𝓝[<] b, c > d
x : ℝ
h1 : x ≤ a
h2 : x > d
⊢ d < a
Tactic:
linarith
Proof state after:
no goals
Theorem: ge_of_eventually_nhdsWithin
Proof state before:
n : ℕ
A a✝ b✝ c d✝ u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
h : ∀ᶠ (c : ℝ) in 𝓝[<] b, c ≤ a
d : ℝ
hd : d < b
⊢ ∀ᶠ (c : ℝ) in 𝓝[<] b, c > d
Tactic:
apply eventually_of_mem (U := Ioi d) ?_ (fun x hx => hx)
Proof state after:
n : ℕ
A a✝ b✝ c d✝ u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
h : ∀ᶠ (c : ℝ) in 𝓝[<] b, c ≤ a
d : ℝ
hd : d < b
⊢ Ioi d ∈ 𝓝[<] b
Theorem: ge_of_eventually_nhdsWithin
Proof state before:
n : ℕ
A a✝ b✝ c d✝ u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
h : ∀ᶠ (c : ℝ) in 𝓝[<] b, c ≤ a
d : ℝ
hd : d < b
⊢ Ioi d ∈ 𝓝[<] b
Tactic:
rw [mem_nhdsWithin]
Proof state after:
n : ℕ
A a✝ b✝ c d✝ u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
h : ∀ᶠ (c : ℝ) in 𝓝[<] b, c ≤ a
d : ℝ
hd : d < b
⊢ ∃ u, IsOpen u ∧ b ∈ u ∧ u ∩ Iio b ⊆ Ioi d
Theorem: ge_of_eventually_nhdsWithin
Proof state before:
n : ℕ
A a✝ b✝ c d✝ u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℝ
h : ∀ᶠ (c : ℝ) in 𝓝[<] b, c ≤ a
d : ℝ
hd : d < b
⊢ ∃ u, IsOpen u ∧ b ∈ u ∧ u ∩ Iio b ⊆ Ioi d
Tactic:
refine ⟨Ioi d, isOpen_Ioi, hd, inter_subset_left _ _⟩
Proof state after:
no goals
Theorem: WI_tendsto_aux
Proof state before:
n : ℕ
A✝ a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
⊢ Tendsto (fun c => c / A - (b - a)) (𝓝[>] (A * (b - a))) (𝓝[>] 0)
Tactic:
rw [Metric.tendsto_nhdsWithin_nhdsWithin]
Proof state after:
n : ℕ
A✝ a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
⊢ ∀ ε > 0,
    ∃ δ > 0,
      ∀ {x : ℝ},
        x ∈ Ioi (A * (b - a)) → dist x (A * (b - a)) < δ → x / A - (b - a) ∈ Ioi 0 ∧ dist (x / A - (b - a)) 0 < ε
Theorem: WI_tendsto_aux
Proof state before:
n : ℕ
A✝ a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
⊢ ∀ ε > 0,
    ∃ δ > 0,
      ∀ {x : ℝ},
        x ∈ Ioi (A * (b - a)) → dist x (A * (b - a)) < δ → x / A - (b - a) ∈ Ioi 0 ∧ dist (x / A - (b - a)) 0 < ε
Tactic:
intro ε hε
Proof state after:
n : ℕ
A✝ a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
⊢ ∃ δ > 0,
    ∀ {x : ℝ}, x ∈ Ioi (A * (b - a)) → dist x (A * (b - a)) < δ → x / A - (b - a) ∈ Ioi 0 ∧ dist (x / A - (b - a)) 0 < ε
Theorem: WI_tendsto_aux
Proof state before:
n : ℕ
A✝ a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
⊢ ∃ δ > 0,
    ∀ {x : ℝ}, x ∈ Ioi (A * (b - a)) → dist x (A * (b - a)) < δ → x / A - (b - a) ∈ Ioi 0 ∧ dist (x / A - (b - a)) 0 < ε
Tactic:
refine ⟨A * ε, by positivity, ?_⟩
Proof state after:
n : ℕ
A✝ a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
⊢ ∀ {x : ℝ},
    x ∈ Ioi (A * (b - a)) → dist x (A * (b - a)) < A * ε → x / A - (b - a) ∈ Ioi 0 ∧ dist (x / A - (b - a)) 0 < ε
Theorem: WI_tendsto_aux
Proof state before:
n : ℕ
A✝ a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
⊢ ∀ {x : ℝ},
    x ∈ Ioi (A * (b - a)) → dist x (A * (b - a)) < A * ε → x / A - (b - a) ∈ Ioi 0 ∧ dist (x / A - (b - a)) 0 < ε
Tactic:
intro x hx1 hx2
Proof state after:
n : ℕ
A✝ a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
x : ℝ
hx1 : x ∈ Ioi (A * (b - a))
hx2 : dist x (A * (b - a)) < A * ε
⊢ x / A - (b - a) ∈ Ioi 0 ∧ dist (x / A - (b - a)) 0 < ε
Theorem: WI_tendsto_aux
Proof state before:
n : ℕ
A✝ a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
x : ℝ
hx1 : x ∈ Ioi (A * (b - a))
hx2 : dist x (A * (b - a)) < A * ε
⊢ x / A - (b - a) ∈ Ioi 0 ∧ dist (x / A - (b - a)) 0 < ε
Tactic:
constructor
Proof state after:
case left
n : ℕ
A✝ a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
x : ℝ
hx1 : x ∈ Ioi (A * (b - a))
hx2 : dist x (A * (b - a)) < A * ε
⊢ x / A - (b - a) ∈ Ioi 0

case right
n : ℕ
A✝ a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
x : ℝ
hx1 : x ∈ Ioi (A * (b - a))
hx2 : dist x (A * (b - a)) < A * ε
⊢ dist (x / A - (b - a)) 0 < ε
Theorem: WI_tendsto_aux
Proof state before:
n : ℕ
A✝ a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
⊢ A * ε > 0
Tactic:
positivity
Proof state after:
no goals
Theorem: WI_tendsto_aux
Proof state before:
case left
n : ℕ
A✝ a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
x : ℝ
hx1 : x ∈ Ioi (A * (b - a))
hx2 : dist x (A * (b - a)) < A * ε
⊢ x / A - (b - a) ∈ Ioi 0
Tactic:
simpa [lt_div_iff' hA]
Proof state after:
no goals
Theorem: WI_tendsto_aux
Proof state before:
case right
n : ℕ
A✝ a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
x : ℝ
hx1 : x ∈ Ioi (A * (b - a))
hx2 : dist x (A * (b - a)) < A * ε
⊢ dist (x / A - (b - a)) 0 < ε
Tactic:
simp only [Real.dist_eq, dist_zero_right, Real.norm_eq_abs] at hx2 ⊢
Proof state after:
case right
n : ℕ
A✝ a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
x : ℝ
hx1 : x ∈ Ioi (A * (b - a))
hx2 : |x - A * (b - a)| < A * ε
⊢ |x / A - (b - a)| < ε
Theorem: WI_tendsto_aux
Proof state before:
case right
n : ℕ
A✝ a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
x : ℝ
hx1 : x ∈ Ioi (A * (b - a))
hx2 : |x - A * (b - a)| < A * ε
⊢ |x / A - (b - a)| < ε
Tactic:
have : |x / A - (b - a)| = |x - A * (b - a)| / A := by
  rw [← abs_eq_self.mpr hA.le, ← abs_div, abs_eq_self.mpr hA.le] ; congr ; field_simp
Proof state after:
case right
n : ℕ
A✝ a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
x : ℝ
hx1 : x ∈ Ioi (A * (b - a))
hx2 : |x - A * (b - a)| < A * ε
this : |x / A - (b - a)| = |x - A * (b - a)| / A
⊢ |x / A - (b - a)| < ε
Theorem: WI_tendsto_aux
Proof state before:
case right
n : ℕ
A✝ a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
x : ℝ
hx1 : x ∈ Ioi (A * (b - a))
hx2 : |x - A * (b - a)| < A * ε
this : |x / A - (b - a)| = |x - A * (b - a)| / A
⊢ |x / A - (b - a)| < ε
Tactic:
rwa [this, div_lt_iff' hA]
Proof state after:
no goals
Theorem: WI_tendsto_aux
Proof state before:
n : ℕ
A✝ a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
x : ℝ
hx1 : x ∈ Ioi (A * (b - a))
hx2 : |x - A * (b - a)| < A * ε
⊢ |x / A - (b - a)| = |x - A * (b - a)| / A
Tactic:
rw [← abs_eq_self.mpr hA.le, ← abs_div, abs_eq_self.mpr hA.le]
Proof state after:
n : ℕ
A✝ a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
x : ℝ
hx1 : x ∈ Ioi (A * (b - a))
hx2 : |x - A * (b - a)| < A * ε
⊢ |x / A - (b - a)| = |(x - A * (b - a)) / A|
Theorem: WI_tendsto_aux
Proof state before:
n : ℕ
A✝ a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
x : ℝ
hx1 : x ∈ Ioi (A * (b - a))
hx2 : |x - A * (b - a)| < A * ε
⊢ |x / A - (b - a)| = |(x - A * (b - a)) / A|
Tactic:
congr
Proof state after:
case e_a
n : ℕ
A✝ a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
x : ℝ
hx1 : x ∈ Ioi (A * (b - a))
hx2 : |x - A * (b - a)| < A * ε
⊢ x / A - (b - a) = (x - A * (b - a)) / A
Theorem: WI_tendsto_aux
Proof state before:
case e_a
n : ℕ
A✝ a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
x : ℝ
hx1 : x ∈ Ioi (A * (b - a))
hx2 : |x - A * (b - a)| < A * ε
⊢ x / A - (b - a) = (x - A * (b - a)) / A
Tactic:
field_simp
Proof state after:
no goals
Theorem: WI_tendsto_aux'
Proof state before:
n : ℕ
A✝ a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
⊢ Tendsto (fun c => b - a - c / A) (𝓝[<] (A * (b - a))) (𝓝[>] 0)
Tactic:
rw [Metric.tendsto_nhdsWithin_nhdsWithin]
Proof state after:
n : ℕ
A✝ a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
⊢ ∀ ε > 0,
    ∃ δ > 0,
      ∀ {x : ℝ}, x ∈ Iio (A * (b - a)) → dist x (A * (b - a)) < δ → b - a - x / A ∈ Ioi 0 ∧ dist (b - a - x / A) 0 < ε
Theorem: WI_tendsto_aux'
Proof state before:
n : ℕ
A✝ a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
⊢ ∀ ε > 0,
    ∃ δ > 0,
      ∀ {x : ℝ}, x ∈ Iio (A * (b - a)) → dist x (A * (b - a)) < δ → b - a - x / A ∈ Ioi 0 ∧ dist (b - a - x / A) 0 < ε
Tactic:
intro ε hε
Proof state after:
n : ℕ
A✝ a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
⊢ ∃ δ > 0,
    ∀ {x : ℝ}, x ∈ Iio (A * (b - a)) → dist x (A * (b - a)) < δ → b - a - x / A ∈ Ioi 0 ∧ dist (b - a - x / A) 0 < ε
Theorem: WI_tendsto_aux'
Proof state before:
n : ℕ
A✝ a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
⊢ ∃ δ > 0,
    ∀ {x : ℝ}, x ∈ Iio (A * (b - a)) → dist x (A * (b - a)) < δ → b - a - x / A ∈ Ioi 0 ∧ dist (b - a - x / A) 0 < ε
Tactic:
refine ⟨A * ε, by positivity, ?_⟩
Proof state after:
n : ℕ
A✝ a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
⊢ ∀ {x : ℝ}, x ∈ Iio (A * (b - a)) → dist x (A * (b - a)) < A * ε → b - a - x / A ∈ Ioi 0 ∧ dist (b - a - x / A) 0 < ε
Theorem: WI_tendsto_aux'
Proof state before:
n : ℕ
A✝ a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
⊢ ∀ {x : ℝ}, x ∈ Iio (A * (b - a)) → dist x (A * (b - a)) < A * ε → b - a - x / A ∈ Ioi 0 ∧ dist (b - a - x / A) 0 < ε
Tactic:
intro x hx1 hx2
Proof state after:
n : ℕ
A✝ a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
x : ℝ
hx1 : x ∈ Iio (A * (b - a))
hx2 : dist x (A * (b - a)) < A * ε
⊢ b - a - x / A ∈ Ioi 0 ∧ dist (b - a - x / A) 0 < ε
Theorem: WI_tendsto_aux'
Proof state before:
n : ℕ
A✝ a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
x : ℝ
hx1 : x ∈ Iio (A * (b - a))
hx2 : dist x (A * (b - a)) < A * ε
⊢ b - a - x / A ∈ Ioi 0 ∧ dist (b - a - x / A) 0 < ε
Tactic:
constructor
Proof state after:
case left
n : ℕ
A✝ a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
x : ℝ
hx1 : x ∈ Iio (A * (b - a))
hx2 : dist x (A * (b - a)) < A * ε
⊢ b - a - x / A ∈ Ioi 0

case right
n : ℕ
A✝ a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
x : ℝ
hx1 : x ∈ Iio (A * (b - a))
hx2 : dist x (A * (b - a)) < A * ε
⊢ dist (b - a - x / A) 0 < ε
Theorem: WI_tendsto_aux'
Proof state before:
n : ℕ
A✝ a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
⊢ A * ε > 0
Tactic:
positivity
Proof state after:
no goals
Theorem: WI_tendsto_aux'
Proof state before:
case left
n : ℕ
A✝ a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
x : ℝ
hx1 : x ∈ Iio (A * (b - a))
hx2 : dist x (A * (b - a)) < A * ε
⊢ b - a - x / A ∈ Ioi 0
Tactic:
simpa [div_lt_iff' hA]
Proof state after:
no goals
Theorem: WI_tendsto_aux'
Proof state before:
case right
n : ℕ
A✝ a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
x : ℝ
hx1 : x ∈ Iio (A * (b - a))
hx2 : dist x (A * (b - a)) < A * ε
⊢ dist (b - a - x / A) 0 < ε
Tactic:
simp [Real.dist_eq] at hx2 ⊢
Proof state after:
case right
n : ℕ
A✝ a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
x : ℝ
hx1 : x ∈ Iio (A * (b - a))
hx2 : |x - A * (b - a)| < A * ε
⊢ |b - a - x / A| < ε
Theorem: WI_tendsto_aux'
Proof state before:
case right
n : ℕ
A✝ a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
x : ℝ
hx1 : x ∈ Iio (A * (b - a))
hx2 : |x - A * (b - a)| < A * ε
⊢ |b - a - x / A| < ε
Tactic:
have : |(b - a) - x / A| = |A * (b - a) - x| / A := by
  rw [← abs_eq_self.mpr hA.le, ← abs_div, abs_eq_self.mpr hA.le] ; congr ; field_simp ; ring
Proof state after:
case right
n : ℕ
A✝ a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
x : ℝ
hx1 : x ∈ Iio (A * (b - a))
hx2 : |x - A * (b - a)| < A * ε
this : |b - a - x / A| = |A * (b - a) - x| / A
⊢ |b - a - x / A| < ε
Theorem: WI_tendsto_aux'
Proof state before:
case right
n : ℕ
A✝ a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
x : ℝ
hx1 : x ∈ Iio (A * (b - a))
hx2 : |x - A * (b - a)| < A * ε
this : |b - a - x / A| = |A * (b - a) - x| / A
⊢ |b - a - x / A| < ε
Tactic:
rwa [this, div_lt_iff' hA, ← neg_sub, abs_neg]
Proof state after:
no goals
Theorem: WI_tendsto_aux'
Proof state before:
n : ℕ
A✝ a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
x : ℝ
hx1 : x ∈ Iio (A * (b - a))
hx2 : |x - A * (b - a)| < A * ε
⊢ |b - a - x / A| = |A * (b - a) - x| / A
Tactic:
rw [← abs_eq_self.mpr hA.le, ← abs_div, abs_eq_self.mpr hA.le]
Proof state after:
n : ℕ
A✝ a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
x : ℝ
hx1 : x ∈ Iio (A * (b - a))
hx2 : |x - A * (b - a)| < A * ε
⊢ |b - a - x / A| = |(A * (b - a) - x) / A|
Theorem: WI_tendsto_aux'
Proof state before:
n : ℕ
A✝ a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
x : ℝ
hx1 : x ∈ Iio (A * (b - a))
hx2 : |x - A * (b - a)| < A * ε
⊢ |b - a - x / A| = |(A * (b - a) - x) / A|
Tactic:
congr
Proof state after:
case e_a
n : ℕ
A✝ a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
x : ℝ
hx1 : x ∈ Iio (A * (b - a))
hx2 : |x - A * (b - a)| < A * ε
⊢ b - a - x / A = (A * (b - a) - x) / A
Theorem: WI_tendsto_aux'
Proof state before:
case e_a
n : ℕ
A✝ a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
x : ℝ
hx1 : x ∈ Iio (A * (b - a))
hx2 : |x - A * (b - a)| < A * ε
⊢ b - a - x / A = (A * (b - a) - x) / A
Tactic:
field_simp
Proof state after:
case e_a
n : ℕ
A✝ a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
x : ℝ
hx1 : x ∈ Iio (A * (b - a))
hx2 : |x - A * (b - a)| < A * ε
⊢ (b - a) * A = A * (b - a)
Theorem: WI_tendsto_aux'
Proof state before:
case e_a
n : ℕ
A✝ a✝ b✝ c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b A : ℝ
hA : 0 < A
ε : ℝ
hε : ε > 0
x : ℝ
hx1 : x ∈ Iio (A * (b - a))
hx2 : |x - A * (b - a)| < A * ε
⊢ (b - a) * A = A * (b - a)
Tactic:
ring
Proof state after:
no goals
Theorem: residue_nonneg
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun n => ↑(f n)) σ')
hcheby : cheby fun n => ↑(f n)
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries (fun n => ↑(f n)) s - ↑A / (s - 1)) {s | 1 < s.re}
⊢ 0 ≤ A
Tactic:
let S (g : ℝ → ℝ) (x : ℝ) := (∑' n, f n * g (n / x)) / x
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun n => ↑(f n)) σ')
hcheby : cheby fun n => ↑(f n)
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries (fun n => ↑(f n)) s - ↑A / (s - 1)) {s | 1 < s.re}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
⊢ 0 ≤ A