Theorem: WienerIkeharaInterval (PrimeNumberTheoremAnd/Wiener.lean)

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}
ha : 0 < a
hb : a ≤ b
⊢ Tendsto (fun x => (∑' (n : ℕ), f n * (Ico a b).indicator 1 (↑n / x)) / x) atTop (𝓝 (A * (b - a)))
Tactic:
by_cases hab : a = b
State after:
case pos
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}
ha : 0 < a
hb : a ≤ b
hab : a = b
⊢ Tendsto (fun x => (∑' (n : ℕ), f n * (Ico a b).indicator 1 (↑n / x)) / x) atTop (𝓝 (A * (b - a)))

case neg
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}
ha : 0 < a
hb : a ≤ b
hab : ¬a = b
⊢ Tendsto (fun x => (∑' (n : ℕ), f n * (Ico a b).indicator 1 (↑n / x)) / x) atTop (𝓝 (A * (b - a)))

State before:
case pos
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}
ha : 0 < a
hb : a ≤ b
hab : a = b
⊢ Tendsto (fun x => (∑' (n : ℕ), f n * (Ico a b).indicator 1 (↑n / x)) / x) atTop (𝓝 (A * (b - a)))

case neg
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}
ha : 0 < a
hb : a ≤ b
hab : ¬a = b
⊢ Tendsto (fun x => (∑' (n : ℕ), f n * (Ico a b).indicator 1 (↑n / x)) / x) atTop (𝓝 (A * (b - a)))
Tactic:
simp [hab]
State after:
case neg
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}
ha : 0 < a
hb : a ≤ b
hab : ¬a = b
⊢ Tendsto (fun x => (∑' (n : ℕ), f n * (Ico a b).indicator 1 (↑n / x)) / x) atTop (𝓝 (A * (b - a)))

State before:
case neg
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}
ha : 0 < a
hb : a ≤ b
hab : ¬a = b
⊢ Tendsto (fun x => (∑' (n : ℕ), f n * (Ico a b).indicator 1 (↑n / x)) / x) atTop (𝓝 (A * (b - a)))
Tactic:
replace hb : a < b := lt_of_le_of_ne hb hab
State after:
case neg
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}
ha : 0 < a
hab : ¬a = b
hb : a < b
⊢ Tendsto (fun x => (∑' (n : ℕ), f n * (Ico a b).indicator 1 (↑n / x)) / x) atTop (𝓝 (A * (b - a)))

State before:
case neg
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}
ha : 0 < a
hab : ¬a = b
hb : a < b
⊢ Tendsto (fun x => (∑' (n : ℕ), f n * (Ico a b).indicator 1 (↑n / x)) / x) atTop (𝓝 (A * (b - a)))
Tactic:
clear hab
State after:
case neg
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}
ha : 0 < a
hb : a < b
⊢ Tendsto (fun x => (∑' (n : ℕ), f n * (Ico a b).indicator 1 (↑n / x)) / x) atTop (𝓝 (A * (b - a)))

State before:
case neg
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}
ha : 0 < a
hb : a < b
⊢ Tendsto (fun x => (∑' (n : ℕ), f n * (Ico a b).indicator 1 (↑n / x)) / x) atTop (𝓝 (A * (b - a)))
Tactic:
let S (g : ℝ → ℝ) (x : ℝ) :=  (∑' n, f n * g (n / x)) / x
State after:
case neg
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
⊢ Tendsto (fun x => (∑' (n : ℕ), f n * (Ico a b).indicator 1 (↑n / x)) / x) atTop (𝓝 (A * (b - a)))

State before:
case neg
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
⊢ Tendsto (fun x => (∑' (n : ℕ), f n * (Ico a b).indicator 1 (↑n / x)) / x) atTop (𝓝 (A * (b - a)))
Tactic:
have hSnonneg {g : ℝ → ℝ} (hg : 0 ≤ g) : ∀ᶠ x : ℝ in atTop, 0 ≤ S g x := by
  filter_upwards [eventually_ge_atTop 0] with x hx
  refine div_nonneg ?_ hx
  refine tsum_nonneg (fun i => mul_nonneg (hpos _) (hg _))
State after:
case neg
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
⊢ Tendsto (fun x => (∑' (n : ℕ), f n * (Ico a b).indicator 1 (↑n / x)) / x) atTop (𝓝 (A * (b - a)))

State before:
case neg
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
⊢ Tendsto (fun x => (∑' (n : ℕ), f n * (Ico a b).indicator 1 (↑n / x)) / x) atTop (𝓝 (A * (b - a)))
Tactic:
have hA : 0 ≤ A := residue_nonneg hpos hf hcheby hG hG'
State after:
case neg
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
⊢ Tendsto (fun x => (∑' (n : ℕ), f n * (Ico a b).indicator 1 (↑n / x)) / x) atTop (𝓝 (A * (b - a)))

State before:
case neg
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
⊢ Tendsto (fun x => (∑' (n : ℕ), f n * (Ico a b).indicator 1 (↑n / x)) / x) atTop (𝓝 (A * (b - a)))
Tactic:
let Iab : ℝ → ℝ := indicator (Ico a b) 1
State after:
case neg
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
⊢ Tendsto (fun x => (∑' (n : ℕ), f n * (Ico a b).indicator 1 (↑n / x)) / x) atTop (𝓝 (A * (b - a)))

State before:
case neg
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
⊢ Tendsto (fun x => (∑' (n : ℕ), f n * (Ico a b).indicator 1 (↑n / x)) / x) atTop (𝓝 (A * (b - a)))
Tactic:
change Tendsto (S Iab) atTop (𝓝 (A * (b - a)))
State after:
case neg
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
⊢ Tendsto (S Iab) atTop (𝓝 (A * (b - a)))

State before:
case neg
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
⊢ Tendsto (S Iab) atTop (𝓝 (A * (b - a)))
Tactic:
have hIab : HasCompactSupport Iab := by simpa [Iab, HasCompactSupport, tsupport, hb.ne] using isCompact_Icc
State after:
case neg
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
⊢ Tendsto (S Iab) atTop (𝓝 (A * (b - a)))

State before:
case neg
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
⊢ Tendsto (S Iab) atTop (𝓝 (A * (b - a)))
Tactic:
have Iab_nonneg : ∀ᶠ x : ℝ in atTop, 0 ≤ S Iab x := hSnonneg (indicator_nonneg (by simp))
State after:
case neg
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
⊢ Tendsto (S Iab) atTop (𝓝 (A * (b - a)))

State before:
case neg
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
sup_le : limsup (S Iab) atTop ≤ A * (b - a)
le_inf : A * (b - a) ≤ liminf (S Iab) atTop
⊢ Tendsto (S Iab) atTop (𝓝 (A * (b - a)))
Tactic:
have : liminf (S Iab) atTop ≤ limsup (S Iab) atTop := liminf_le_limsup Iab2 Iab3
State after:
case neg
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
sup_le : limsup (S Iab) atTop ≤ A * (b - a)
le_inf : A * (b - a) ≤ liminf (S Iab) atTop
this : liminf (S Iab) atTop ≤ limsup (S Iab) atTop
⊢ Tendsto (S Iab) atTop (𝓝 (A * (b - a)))

State before:
case neg
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
sup_le : limsup (S Iab) atTop ≤ A * (b - a)
le_inf : A * (b - a) ≤ liminf (S Iab) atTop
this : liminf (S Iab) atTop ≤ limsup (S Iab) atTop
⊢ Tendsto (S Iab) atTop (𝓝 (A * (b - a)))
Tactic:
refine tendsto_of_liminf_eq_limsup ?_ ?_ Iab2 Iab3 <;> linarith
State after:
no goals

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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
g : ℝ → ℝ
hg : 0 ≤ g
⊢ ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
Tactic:
filter_upwards [eventually_ge_atTop 0] with x hx
State after:
case h
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
g : ℝ → ℝ
hg : 0 ≤ g
x : ℝ
hx : 0 ≤ x
⊢ 0 ≤ S g x

State before:
case h
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
g : ℝ → ℝ
hg : 0 ≤ g
x : ℝ
hx : 0 ≤ x
⊢ 0 ≤ S g x
Tactic:
refine div_nonneg ?_ hx
State after:
case h
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
g : ℝ → ℝ
hg : 0 ≤ g
x : ℝ
hx : 0 ≤ x
⊢ 0 ≤ ∑' (n : ℕ), f n * g (↑n / x)

State before:
case h
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
g : ℝ → ℝ
hg : 0 ≤ g
x : ℝ
hx : 0 ≤ x
⊢ 0 ≤ ∑' (n : ℕ), f n * g (↑n / x)
Tactic:
refine tsum_nonneg (fun i => mul_nonneg (hpos _) (hg _))
State after:
no goals

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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
⊢ HasCompactSupport Iab
Tactic:
simpa [Iab, HasCompactSupport, tsupport, hb.ne] using isCompact_Icc
State after:
no goals

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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
⊢ ∀ a_1 ∈ Ico a b, 0 ≤ 1 a_1
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 𝕜
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Tactic:
obtain ⟨C, hC⟩ := hcheby
State after:
case intro
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)) σ')
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
C : ℝ
hC : chebyWith C fun n => ↑(f n)
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)

State before:
case intro
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)) σ')
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
C : ℝ
hC : chebyWith C fun n => ↑(f n)
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Tactic:
exact ⟨C * 2 * b, WI_sum_Iab_le' hpos hC (by linarith)⟩
State after:
no goals

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)) σ')
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
C : ℝ
hC : chebyWith C fun n => ↑(f n)
⊢ 0 < b
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 𝕜
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
l_sup : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, limsup (S Iab) atTop ≤ A * (b - a + ε)
⊢ limsup (S Iab) atTop ≤ A * (b - a)
Tactic:
cases' (eq_or_ne A 0) with h h
State after:
case inl
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
l_sup : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, limsup (S Iab) atTop ≤ A * (b - a + ε)
h : A = 0
⊢ limsup (S Iab) atTop ≤ A * (b - a)

case inr
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
l_sup : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, limsup (S Iab) atTop ≤ A * (b - a + ε)
h : A ≠ 0
⊢ limsup (S Iab) atTop ≤ A * (b - a)

State before:
case inl
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
l_sup : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, limsup (S Iab) atTop ≤ A * (b - a + ε)
h : A = 0
⊢ limsup (S Iab) atTop ≤ A * (b - a)

case inr
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
l_sup : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, limsup (S Iab) atTop ≤ A * (b - a + ε)
h : A ≠ 0
⊢ limsup (S Iab) atTop ≤ A * (b - a)
Tactic:
simpa [h] using l_sup
State after:
case inr
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
l_sup : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, limsup (S Iab) atTop ≤ A * (b - a + ε)
h : A ≠ 0
⊢ limsup (S Iab) atTop ≤ A * (b - a)

State before:
case inr
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
l_sup : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, limsup (S Iab) atTop ≤ A * (b - a + ε)
h : A ≠ 0
⊢ limsup (S Iab) atTop ≤ A * (b - a)
Tactic:
apply le_of_eventually_nhdsWithin
State after:
case inr.h
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
l_sup : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, limsup (S Iab) atTop ≤ A * (b - a + ε)
h : A ≠ 0
⊢ ∀ᶠ (c : ℝ) in 𝓝[>] (A * (b - a)), limsup (S Iab) atTop ≤ c

State before:
case inr.h
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
l_sup : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, limsup (S Iab) atTop ≤ A * (b - a + ε)
h : A ≠ 0
⊢ ∀ᶠ (c : ℝ) in 𝓝[>] (A * (b - a)), limsup (S Iab) atTop ≤ c
Tactic:
have key : 0 < A := lt_of_le_of_ne hA h.symm
State after:
case inr.h
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
l_sup : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, limsup (S Iab) atTop ≤ A * (b - a + ε)
h : A ≠ 0
key : 0 < A
⊢ ∀ᶠ (c : ℝ) in 𝓝[>] (A * (b - a)), limsup (S Iab) atTop ≤ c

State before:
case inr.h
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
l_sup : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, limsup (S Iab) atTop ≤ A * (b - a + ε)
h : A ≠ 0
key : 0 < A
⊢ ∀ᶠ (c : ℝ) in 𝓝[>] (A * (b - a)), limsup (S Iab) atTop ≤ c
Tactic:
filter_upwards [WI_tendsto_aux a b key l_sup] with x hx
State after:
case h
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
l_sup : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, limsup (S Iab) atTop ≤ A * (b - a + ε)
h : A ≠ 0
key : 0 < A
x : ℝ
hx : x ∈ (fun c => c / A - (b - a)) ⁻¹' {x | limsup (S Iab) atTop ≤ A * (b - a + x)}
⊢ limsup (S Iab) atTop ≤ x

State before:
case h
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
l_sup : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, limsup (S Iab) atTop ≤ A * (b - a + ε)
h : A ≠ 0
key : 0 < A
x : ℝ
hx : x ∈ (fun c => c / A - (b - a)) ⁻¹' {x | limsup (S Iab) atTop ≤ A * (b - a + x)}
⊢ limsup (S Iab) atTop ≤ x
Tactic:
simp at hx
State after:
case h
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
l_sup : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, limsup (S Iab) atTop ≤ A * (b - a + ε)
h : A ≠ 0
key : 0 < A
x : ℝ
hx : limsup (S Iab) atTop ≤ A * (x / A)
⊢ limsup (S Iab) atTop ≤ x

State before:
case h
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
l_sup : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, limsup (S Iab) atTop ≤ A * (b - a + ε)
h : A ≠ 0
key : 0 < A
x : ℝ
hx : limsup (S Iab) atTop ≤ A * (x / A)
⊢ limsup (S Iab) atTop ≤ x
Tactic:
convert hx
State after:
case h.e'_4
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
l_sup : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, limsup (S Iab) atTop ≤ A * (b - a + ε)
h : A ≠ 0
key : 0 < A
x : ℝ
hx : limsup (S Iab) atTop ≤ A * (x / A)
⊢ x = A * (x / A)

State before:
case h.e'_4
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
l_sup : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, limsup (S Iab) atTop ≤ A * (b - a + ε)
h : A ≠ 0
key : 0 < A
x : ℝ
hx : limsup (S Iab) atTop ≤ A * (x / A)
⊢ x = A * (x / A)
Tactic:
field_simp
State after:
no goals

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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
⊢ ∀ᶠ (ε : ℝ) in 𝓝[>] 0, limsup (S Iab) atTop ≤ A * (b - a + ε)
Tactic:
filter_upwards [interval_approx_sup ha hb] with ε ⟨ψ, h1, h2, h3, h4, h6⟩
State after:
case h
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico a b).indicator 1 ≤ ψ
h6 : ∫ (y : ℝ) in Ioi 0, ψ y ≤ b - a + ε
⊢ limsup (S Iab) atTop ≤ A * (b - a + ε)

State before:
case h
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico a b).indicator 1 ≤ ψ
h6 : ∫ (y : ℝ) in Ioi 0, ψ y ≤ b - a + ε
⊢ limsup (S Iab) atTop ≤ A * (b - a + ε)
Tactic:
have l1 : Tendsto (S ψ) atTop _ := wiener_ikehara_smooth_real hf hcheby hG hG' h1 h2 h3
State after:
case h
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico a b).indicator 1 ≤ ψ
h6 : ∫ (y : ℝ) in Ioi 0, ψ y ≤ b - a + ε
l1 : Tendsto (S ψ) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
⊢ limsup (S Iab) atTop ≤ A * (b - a + ε)

State before:
case h
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico a b).indicator 1 ≤ ψ
h6 : ∫ (y : ℝ) in Ioi 0, ψ y ≤ b - a + ε
l1 : Tendsto (S ψ) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
⊢ limsup (S Iab) atTop ≤ A * (b - a + ε)
Tactic:
have l6 : S Iab ≤ᶠ[atTop] S ψ := by
  filter_upwards [eventually_gt_atTop 0] with x hx using WI_sum_le hpos h4 hx hIab h2
State after:
case h
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico a b).indicator 1 ≤ ψ
h6 : ∫ (y : ℝ) in Ioi 0, ψ y ≤ b - a + ε
l1 : Tendsto (S ψ) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l6 : S Iab ≤ᶠ[atTop] S ψ
⊢ limsup (S Iab) atTop ≤ A * (b - a + ε)

State before:
case h
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico a b).indicator 1 ≤ ψ
h6 : ∫ (y : ℝ) in Ioi 0, ψ y ≤ b - a + ε
l1 : Tendsto (S ψ) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l6 : S Iab ≤ᶠ[atTop] S ψ
l5 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S ψ)
⊢ limsup (S Iab) atTop ≤ A * (b - a + ε)
Tactic:
have l3 : limsup (S Iab) atTop ≤ limsup (S ψ) atTop := limsup_le_limsup l6 Iab1 l5
State after:
case h
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico a b).indicator 1 ≤ ψ
h6 : ∫ (y : ℝ) in Ioi 0, ψ y ≤ b - a + ε
l1 : Tendsto (S ψ) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l6 : S Iab ≤ᶠ[atTop] S ψ
l5 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S ψ)
l3 : limsup (S Iab) atTop ≤ limsup (S ψ) atTop
⊢ limsup (S Iab) atTop ≤ A * (b - a + ε)

State before:
case h
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico a b).indicator 1 ≤ ψ
h6 : ∫ (y : ℝ) in Ioi 0, ψ y ≤ b - a + ε
l1 : Tendsto (S ψ) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l6 : S Iab ≤ᶠ[atTop] S ψ
l5 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S ψ)
l3 : limsup (S Iab) atTop ≤ limsup (S ψ) atTop
⊢ limsup (S Iab) atTop ≤ A * (b - a + ε)
Tactic:
apply l3.trans
State after:
case h
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico a b).indicator 1 ≤ ψ
h6 : ∫ (y : ℝ) in Ioi 0, ψ y ≤ b - a + ε
l1 : Tendsto (S ψ) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l6 : S Iab ≤ᶠ[atTop] S ψ
l5 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S ψ)
l3 : limsup (S Iab) atTop ≤ limsup (S ψ) atTop
⊢ limsup (S ψ) atTop ≤ A * (b - a + ε)

State before:
case h
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico a b).indicator 1 ≤ ψ
h6 : ∫ (y : ℝ) in Ioi 0, ψ y ≤ b - a + ε
l1 : Tendsto (S ψ) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l6 : S Iab ≤ᶠ[atTop] S ψ
l5 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S ψ)
l3 : limsup (S Iab) atTop ≤ limsup (S ψ) atTop
⊢ limsup (S ψ) atTop ≤ A * (b - a + ε)
Tactic:
rw [l1.limsup_eq]
State after:
case h
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico a b).indicator 1 ≤ ψ
h6 : ∫ (y : ℝ) in Ioi 0, ψ y ≤ b - a + ε
l1 : Tendsto (S ψ) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l6 : S Iab ≤ᶠ[atTop] S ψ
l5 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S ψ)
l3 : limsup (S Iab) atTop ≤ limsup (S ψ) atTop
⊢ A * ∫ (y : ℝ) in Ioi 0, ψ y ≤ A * (b - a + ε)

State before:
case h
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico a b).indicator 1 ≤ ψ
h6 : ∫ (y : ℝ) in Ioi 0, ψ y ≤ b - a + ε
l1 : Tendsto (S ψ) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l6 : S Iab ≤ᶠ[atTop] S ψ
l5 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S ψ)
l3 : limsup (S Iab) atTop ≤ limsup (S ψ) atTop
⊢ A * ∫ (y : ℝ) in Ioi 0, ψ y ≤ A * (b - a + ε)
Tactic:
gcongr
State after:
no goals

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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico a b).indicator 1 ≤ ψ
h6 : ∫ (y : ℝ) in Ioi 0, ψ y ≤ b - a + ε
l1 : Tendsto (S ψ) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
⊢ S Iab ≤ᶠ[atTop] S ψ
Tactic:
filter_upwards [eventually_gt_atTop 0] with x hx using WI_sum_le hpos h4 hx hIab h2
State after:
no goals

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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
sup_le : limsup (S Iab) atTop ≤ A * (b - a)
l_inf : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, A * (b - a - ε) ≤ liminf (S Iab) atTop
⊢ A * (b - a) ≤ liminf (S Iab) atTop
Tactic:
cases' (eq_or_ne A 0) with h h
State after:
case inl
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
sup_le : limsup (S Iab) atTop ≤ A * (b - a)
l_inf : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, A * (b - a - ε) ≤ liminf (S Iab) atTop
h : A = 0
⊢ A * (b - a) ≤ liminf (S Iab) atTop

case inr
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
sup_le : limsup (S Iab) atTop ≤ A * (b - a)
l_inf : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, A * (b - a - ε) ≤ liminf (S Iab) atTop
h : A ≠ 0
⊢ A * (b - a) ≤ liminf (S Iab) atTop

State before:
case inl
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
sup_le : limsup (S Iab) atTop ≤ A * (b - a)
l_inf : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, A * (b - a - ε) ≤ liminf (S Iab) atTop
h : A = 0
⊢ A * (b - a) ≤ liminf (S Iab) atTop

case inr
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
sup_le : limsup (S Iab) atTop ≤ A * (b - a)
l_inf : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, A * (b - a - ε) ≤ liminf (S Iab) atTop
h : A ≠ 0
⊢ A * (b - a) ≤ liminf (S Iab) atTop
Tactic:
simpa [h] using l_inf
State after:
case inr
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
sup_le : limsup (S Iab) atTop ≤ A * (b - a)
l_inf : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, A * (b - a - ε) ≤ liminf (S Iab) atTop
h : A ≠ 0
⊢ A * (b - a) ≤ liminf (S Iab) atTop

State before:
case inr
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
sup_le : limsup (S Iab) atTop ≤ A * (b - a)
l_inf : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, A * (b - a - ε) ≤ liminf (S Iab) atTop
h : A ≠ 0
⊢ A * (b - a) ≤ liminf (S Iab) atTop
Tactic:
apply ge_of_eventually_nhdsWithin
State after:
case inr.h
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
sup_le : limsup (S Iab) atTop ≤ A * (b - a)
l_inf : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, A * (b - a - ε) ≤ liminf (S Iab) atTop
h : A ≠ 0
⊢ ∀ᶠ (c : ℝ) in 𝓝[<] (A * (b - a)), c ≤ liminf (S Iab) atTop

State before:
case inr.h
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
sup_le : limsup (S Iab) atTop ≤ A * (b - a)
l_inf : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, A * (b - a - ε) ≤ liminf (S Iab) atTop
h : A ≠ 0
⊢ ∀ᶠ (c : ℝ) in 𝓝[<] (A * (b - a)), c ≤ liminf (S Iab) atTop
Tactic:
have key : 0 < A := lt_of_le_of_ne hA h.symm
State after:
case inr.h
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
sup_le : limsup (S Iab) atTop ≤ A * (b - a)
l_inf : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, A * (b - a - ε) ≤ liminf (S Iab) atTop
h : A ≠ 0
key : 0 < A
⊢ ∀ᶠ (c : ℝ) in 𝓝[<] (A * (b - a)), c ≤ liminf (S Iab) atTop

State before:
case inr.h
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
sup_le : limsup (S Iab) atTop ≤ A * (b - a)
l_inf : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, A * (b - a - ε) ≤ liminf (S Iab) atTop
h : A ≠ 0
key : 0 < A
⊢ ∀ᶠ (c : ℝ) in 𝓝[<] (A * (b - a)), c ≤ liminf (S Iab) atTop
Tactic:
filter_upwards [WI_tendsto_aux' a b key l_inf] with x hx
State after:
case h
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
sup_le : limsup (S Iab) atTop ≤ A * (b - a)
l_inf : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, A * (b - a - ε) ≤ liminf (S Iab) atTop
h : A ≠ 0
key : 0 < A
x : ℝ
hx : x ∈ (fun c => b - a - c / A) ⁻¹' {x | A * (b - a - x) ≤ liminf (S Iab) atTop}
⊢ x ≤ liminf (S Iab) atTop

State before:
case h
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
sup_le : limsup (S Iab) atTop ≤ A * (b - a)
l_inf : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, A * (b - a - ε) ≤ liminf (S Iab) atTop
h : A ≠ 0
key : 0 < A
x : ℝ
hx : x ∈ (fun c => b - a - c / A) ⁻¹' {x | A * (b - a - x) ≤ liminf (S Iab) atTop}
⊢ x ≤ liminf (S Iab) atTop
Tactic:
simp at hx
State after:
case h
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
sup_le : limsup (S Iab) atTop ≤ A * (b - a)
l_inf : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, A * (b - a - ε) ≤ liminf (S Iab) atTop
h : A ≠ 0
key : 0 < A
x : ℝ
hx : A * (x / A) ≤ liminf (S Iab) atTop
⊢ x ≤ liminf (S Iab) atTop

State before:
case h
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
sup_le : limsup (S Iab) atTop ≤ A * (b - a)
l_inf : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, A * (b - a - ε) ≤ liminf (S Iab) atTop
h : A ≠ 0
key : 0 < A
x : ℝ
hx : A * (x / A) ≤ liminf (S Iab) atTop
⊢ x ≤ liminf (S Iab) atTop
Tactic:
convert hx
State after:
case h.e'_3
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
sup_le : limsup (S Iab) atTop ≤ A * (b - a)
l_inf : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, A * (b - a - ε) ≤ liminf (S Iab) atTop
h : A ≠ 0
key : 0 < A
x : ℝ
hx : A * (x / A) ≤ liminf (S Iab) atTop
⊢ x = A * (x / A)

State before:
case h.e'_3
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
sup_le : limsup (S Iab) atTop ≤ A * (b - a)
l_inf : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, A * (b - a - ε) ≤ liminf (S Iab) atTop
h : A ≠ 0
key : 0 < A
x : ℝ
hx : A * (x / A) ≤ liminf (S Iab) atTop
⊢ x = A * (x / A)
Tactic:
field_simp
State after:
no goals

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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
sup_le : limsup (S Iab) atTop ≤ A * (b - a)
⊢ ∀ᶠ (ε : ℝ) in 𝓝[>] 0, A * (b - a - ε) ≤ liminf (S Iab) atTop
Tactic:
filter_upwards [interval_approx_inf ha hb] with ε ⟨ψ, h1, h2, h3, h5, h6⟩
State after:
case h
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
sup_le : limsup (S Iab) atTop ≤ A * (b - a)
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h5 : ψ ≤ (Ico a b).indicator 1
h6 : b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y
⊢ A * (b - a - ε) ≤ liminf (S Iab) atTop

State before:
case h
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
sup_le : limsup (S Iab) atTop ≤ A * (b - a)
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h5 : ψ ≤ (Ico a b).indicator 1
h6 : b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y
⊢ A * (b - a - ε) ≤ liminf (S Iab) atTop
Tactic:
have l1 : Tendsto (S ψ) atTop _ := wiener_ikehara_smooth_real hf hcheby hG hG' h1 h2 h3
State after:
case h
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
sup_le : limsup (S Iab) atTop ≤ A * (b - a)
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h5 : ψ ≤ (Ico a b).indicator 1
h6 : b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y
l1 : Tendsto (S ψ) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
⊢ A * (b - a - ε) ≤ liminf (S Iab) atTop

State before:
case h
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
sup_le : limsup (S Iab) atTop ≤ A * (b - a)
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h5 : ψ ≤ (Ico a b).indicator 1
h6 : b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y
l1 : Tendsto (S ψ) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
⊢ A * (b - a - ε) ≤ liminf (S Iab) atTop
Tactic:
have l2 : S ψ ≤ᶠ[atTop] S Iab := by
  filter_upwards [eventually_gt_atTop 0] with x hx using WI_sum_le hpos h5 hx h2 hIab
State after:
case h
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
sup_le : limsup (S Iab) atTop ≤ A * (b - a)
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h5 : ψ ≤ (Ico a b).indicator 1
h6 : b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y
l1 : Tendsto (S ψ) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l2 : S ψ ≤ᶠ[atTop] S Iab
⊢ A * (b - a - ε) ≤ liminf (S Iab) atTop

State before:
case h
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
sup_le : limsup (S Iab) atTop ≤ A * (b - a)
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h5 : ψ ≤ (Ico a b).indicator 1
h6 : b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y
l1 : Tendsto (S ψ) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l2 : S ψ ≤ᶠ[atTop] S Iab
l4 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S ψ)
⊢ A * (b - a - ε) ≤ liminf (S Iab) atTop
Tactic:
have l3 : liminf (S ψ) atTop ≤ liminf (S Iab) atTop := liminf_le_liminf l2 l4 Iab0
State after:
case h
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
sup_le : limsup (S Iab) atTop ≤ A * (b - a)
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h5 : ψ ≤ (Ico a b).indicator 1
h6 : b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y
l1 : Tendsto (S ψ) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l2 : S ψ ≤ᶠ[atTop] S Iab
l4 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S ψ)
l3 : liminf (S ψ) atTop ≤ liminf (S Iab) atTop
⊢ A * (b - a - ε) ≤ liminf (S Iab) atTop

State before:
case h
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
sup_le : limsup (S Iab) atTop ≤ A * (b - a)
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h5 : ψ ≤ (Ico a b).indicator 1
h6 : b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y
l1 : Tendsto (S ψ) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l2 : S ψ ≤ᶠ[atTop] S Iab
l4 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S ψ)
l3 : liminf (S ψ) atTop ≤ liminf (S Iab) atTop
⊢ A * (b - a - ε) ≤ liminf (S Iab) atTop
Tactic:
apply le_trans ?_ l3
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
sup_le : limsup (S Iab) atTop ≤ A * (b - a)
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h5 : ψ ≤ (Ico a b).indicator 1
h6 : b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y
l1 : Tendsto (S ψ) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l2 : S ψ ≤ᶠ[atTop] S Iab
l4 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S ψ)
l3 : liminf (S ψ) atTop ≤ liminf (S Iab) atTop
⊢ A * (b - a - ε) ≤ liminf (S ψ) atTop

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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
sup_le : limsup (S Iab) atTop ≤ A * (b - a)
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h5 : ψ ≤ (Ico a b).indicator 1
h6 : b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y
l1 : Tendsto (S ψ) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l2 : S ψ ≤ᶠ[atTop] S Iab
l4 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S ψ)
l3 : liminf (S ψ) atTop ≤ liminf (S Iab) atTop
⊢ A * (b - a - ε) ≤ liminf (S ψ) atTop
Tactic:
rw [l1.liminf_eq]
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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
sup_le : limsup (S Iab) atTop ≤ A * (b - a)
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h5 : ψ ≤ (Ico a b).indicator 1
h6 : b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y
l1 : Tendsto (S ψ) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l2 : S ψ ≤ᶠ[atTop] S Iab
l4 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S ψ)
l3 : liminf (S ψ) atTop ≤ liminf (S Iab) atTop
⊢ A * (b - a - ε) ≤ A * ∫ (y : ℝ) in Ioi 0, ψ y

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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
sup_le : limsup (S Iab) atTop ≤ A * (b - a)
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h5 : ψ ≤ (Ico a b).indicator 1
h6 : b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y
l1 : Tendsto (S ψ) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l2 : S ψ ≤ᶠ[atTop] S Iab
l4 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S ψ)
l3 : liminf (S ψ) atTop ≤ liminf (S Iab) atTop
⊢ A * (b - a - ε) ≤ A * ∫ (y : ℝ) in Ioi 0, ψ y
Tactic:
gcongr
State after:
no goals

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}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
sup_le : limsup (S Iab) atTop ≤ A * (b - a)
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h5 : ψ ≤ (Ico a b).indicator 1
h6 : b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y
l1 : Tendsto (S ψ) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
⊢ S ψ ≤ᶠ[atTop] S Iab
Tactic:
filter_upwards [eventually_gt_atTop 0] with x hx using WI_sum_le hpos h5 hx h2 hIab
State after:
no goals