Theorem: residue_nonneg (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}
⊢ 0 ≤ A
Tactic:
let S (g : ℝ → ℝ) (x : ℝ) := (∑' n, f n * g (n / x)) / x
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun n => ↑(f n)) σ')
hcheby : cheby fun n => ↑(f n)
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries (fun n => ↑(f n)) s - ↑A / (s - 1)) {s | 1 < s.re}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
⊢ 0 ≤ A

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}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
⊢ 0 ≤ 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
  exact div_nonneg (tsum_nonneg (fun i => mul_nonneg (hpos _) (hg _))) hx
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun n => ↑(f n)) σ')
hcheby : cheby fun n => ↑(f n)
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries (fun n => ↑(f n)) s - ↑A / (s - 1)) {s | 1 < s.re}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
⊢ 0 ≤ A

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}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
⊢ 0 ≤ A
Tactic:
obtain ⟨ε, ψ, h1, h2, h3, h4, -⟩ := (interval_approx_sup zero_lt_one one_lt_two).exists
State after:
case intro.intro.intro.intro.intro.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)) σ')
hcheby : cheby fun n => ↑(f n)
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries (fun n => ↑(f n)) s - ↑A / (s - 1)) {s | 1 < s.re}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico 1 2).indicator 1 ≤ ψ
⊢ 0 ≤ A

State before:
case intro.intro.intro.intro.intro.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)) σ')
hcheby : cheby fun n => ↑(f n)
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries (fun n => ↑(f n)) s - ↑A / (s - 1)) {s | 1 < s.re}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico 1 2).indicator 1 ≤ ψ
⊢ 0 ≤ A
Tactic:
have key := @wiener_ikehara_smooth_real A G f ψ hf hcheby hG hG' h1 h2 h3
State after:
case intro.intro.intro.intro.intro.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)) σ')
hcheby : cheby fun n => ↑(f n)
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries (fun n => ↑(f n)) s - ↑A / (s - 1)) {s | 1 < s.re}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico 1 2).indicator 1 ≤ ψ
key : Tendsto (fun x => (∑' (n : ℕ), f n * ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
⊢ 0 ≤ A

State before:
case intro.intro.intro.intro.intro.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)) σ')
hcheby : cheby fun n => ↑(f n)
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries (fun n => ↑(f n)) s - ↑A / (s - 1)) {s | 1 < s.re}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico 1 2).indicator 1 ≤ ψ
key : Tendsto (fun x => (∑' (n : ℕ), f n * ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
⊢ 0 ≤ A
Tactic:
have l2 : 0 ≤ ψ := by apply le_trans _ h4 ; apply indicator_nonneg ; simp
State after:
case intro.intro.intro.intro.intro.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)) σ')
hcheby : cheby fun n => ↑(f n)
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries (fun n => ↑(f n)) s - ↑A / (s - 1)) {s | 1 < s.re}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico 1 2).indicator 1 ≤ ψ
key : Tendsto (fun x => (∑' (n : ℕ), f n * ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l2 : 0 ≤ ψ
⊢ 0 ≤ A

State before:
case intro.intro.intro.intro.intro.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)) σ')
hcheby : cheby fun n => ↑(f n)
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries (fun n => ↑(f n)) s - ↑A / (s - 1)) {s | 1 < s.re}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico 1 2).indicator 1 ≤ ψ
key : Tendsto (fun x => (∑' (n : ℕ), f n * ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l2 : 0 ≤ ψ
⊢ 0 ≤ A
Tactic:
have l1 : ∀ᶠ x in atTop, 0 ≤ S ψ x := hSnonneg l2
State after:
case intro.intro.intro.intro.intro.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)) σ')
hcheby : cheby fun n => ↑(f n)
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries (fun n => ↑(f n)) s - ↑A / (s - 1)) {s | 1 < s.re}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico 1 2).indicator 1 ≤ ψ
key : Tendsto (fun x => (∑' (n : ℕ), f n * ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l2 : 0 ≤ ψ
l1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S ψ x
⊢ 0 ≤ A

State before:
case intro.intro.intro.intro.intro.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)) σ')
hcheby : cheby fun n => ↑(f n)
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries (fun n => ↑(f n)) s - ↑A / (s - 1)) {s | 1 < s.re}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico 1 2).indicator 1 ≤ ψ
key : Tendsto (fun x => (∑' (n : ℕ), f n * ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l2 : 0 ≤ ψ
l1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S ψ x
⊢ 0 ≤ A
Tactic:
have l3 : 0 ≤ A * ∫ (y : ℝ) in Ioi 0, ψ y := ge_of_tendsto key l1
State after:
case intro.intro.intro.intro.intro.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)) σ')
hcheby : cheby fun n => ↑(f n)
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries (fun n => ↑(f n)) s - ↑A / (s - 1)) {s | 1 < s.re}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico 1 2).indicator 1 ≤ ψ
key : Tendsto (fun x => (∑' (n : ℕ), f n * ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l2 : 0 ≤ ψ
l1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S ψ x
l3 : 0 ≤ A * ∫ (y : ℝ) in Ioi 0, ψ y
⊢ 0 ≤ A

State before:
case intro.intro.intro.intro.intro.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)) σ')
hcheby : cheby fun n => ↑(f n)
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries (fun n => ↑(f n)) s - ↑A / (s - 1)) {s | 1 < s.re}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico 1 2).indicator 1 ≤ ψ
key : Tendsto (fun x => (∑' (n : ℕ), f n * ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l2 : 0 ≤ ψ
l1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S ψ x
l3 : 0 ≤ A * ∫ (y : ℝ) in Ioi 0, ψ y
⊢ 0 ≤ A
Tactic:
have l4 : 0 < ∫ (y : ℝ) in Ioi 0, ψ y := by
  have r1 : 0 ≤ᵐ[Measure.restrict volume (Ioi 0)] ψ := eventually_of_forall l2
  have r2 : IntegrableOn (fun y ↦ ψ y) (Ioi 0) volume :=
    (h1.continuous.integrable_of_hasCompactSupport h2).integrableOn
  have r3 : Ico 1 2 ⊆ Function.support ψ := by intro x hx ; have := h4 x ; simp [hx] at this ⊢ ; linarith
  have r4 : Ico 1 2 ⊆ Function.support ψ ∩ Ioi 0 := by
    simp only [subset_inter_iff, r3, true_and] ; apply Ico_subset_Icc_self.trans ; rw [Icc_subset_Ioi_iff] <;> linarith
  have r5 : 1 ≤ volume ((Function.support fun y ↦ ψ y) ∩ Ioi 0) := by convert volume.mono r4 ; norm_num
  simpa [setIntegral_pos_iff_support_of_nonneg_ae r1 r2] using zero_lt_one.trans_le r5
State after:
case intro.intro.intro.intro.intro.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)) σ')
hcheby : cheby fun n => ↑(f n)
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries (fun n => ↑(f n)) s - ↑A / (s - 1)) {s | 1 < s.re}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico 1 2).indicator 1 ≤ ψ
key : Tendsto (fun x => (∑' (n : ℕ), f n * ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l2 : 0 ≤ ψ
l1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S ψ x
l3 : 0 ≤ A * ∫ (y : ℝ) in Ioi 0, ψ y
l4 : 0 < ∫ (y : ℝ) in Ioi 0, ψ y
⊢ 0 ≤ A

State before:
case intro.intro.intro.intro.intro.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)) σ')
hcheby : cheby fun n => ↑(f n)
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries (fun n => ↑(f n)) s - ↑A / (s - 1)) {s | 1 < s.re}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico 1 2).indicator 1 ≤ ψ
key : Tendsto (fun x => (∑' (n : ℕ), f n * ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l2 : 0 ≤ ψ
l1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S ψ x
l3 : 0 ≤ A * ∫ (y : ℝ) in Ioi 0, ψ y
l4 : 0 < ∫ (y : ℝ) in Ioi 0, ψ y
⊢ 0 ≤ A
Tactic:
have := div_nonneg l3 l4.le
State after:
case intro.intro.intro.intro.intro.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)) σ')
hcheby : cheby fun n => ↑(f n)
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries (fun n => ↑(f n)) s - ↑A / (s - 1)) {s | 1 < s.re}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico 1 2).indicator 1 ≤ ψ
key : Tendsto (fun x => (∑' (n : ℕ), f n * ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l2 : 0 ≤ ψ
l1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S ψ x
l3 : 0 ≤ A * ∫ (y : ℝ) in Ioi 0, ψ y
l4 : 0 < ∫ (y : ℝ) in Ioi 0, ψ y
this : 0 ≤ (A * ∫ (y : ℝ) in Ioi 0, ψ y) / ∫ (y : ℝ) in Ioi 0, ψ y
⊢ 0 ≤ A

State before:
case intro.intro.intro.intro.intro.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)) σ')
hcheby : cheby fun n => ↑(f n)
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries (fun n => ↑(f n)) s - ↑A / (s - 1)) {s | 1 < s.re}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico 1 2).indicator 1 ≤ ψ
key : Tendsto (fun x => (∑' (n : ℕ), f n * ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l2 : 0 ≤ ψ
l1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S ψ x
l3 : 0 ≤ A * ∫ (y : ℝ) in Ioi 0, ψ y
l4 : 0 < ∫ (y : ℝ) in Ioi 0, ψ y
this : 0 ≤ (A * ∫ (y : ℝ) in Ioi 0, ψ y) / ∫ (y : ℝ) in Ioi 0, ψ y
⊢ 0 ≤ A
Tactic:
field_simp at this
State after:
case intro.intro.intro.intro.intro.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)) σ')
hcheby : cheby fun n => ↑(f n)
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries (fun n => ↑(f n)) s - ↑A / (s - 1)) {s | 1 < s.re}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico 1 2).indicator 1 ≤ ψ
key : Tendsto (fun x => (∑' (n : ℕ), f n * ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l2 : 0 ≤ ψ
l1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S ψ x
l3 : 0 ≤ A * ∫ (y : ℝ) in Ioi 0, ψ y
l4 : 0 < ∫ (y : ℝ) in Ioi 0, ψ y
this : 0 ≤ A
⊢ 0 ≤ A

State before:
case intro.intro.intro.intro.intro.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)) σ')
hcheby : cheby fun n => ↑(f n)
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries (fun n => ↑(f n)) s - ↑A / (s - 1)) {s | 1 < s.re}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico 1 2).indicator 1 ≤ ψ
key : Tendsto (fun x => (∑' (n : ℕ), f n * ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l2 : 0 ≤ ψ
l1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S ψ x
l3 : 0 ≤ A * ∫ (y : ℝ) in Ioi 0, ψ y
l4 : 0 < ∫ (y : ℝ) in Ioi 0, ψ y
this : 0 ≤ A
⊢ 0 ≤ A
Tactic:
exact this
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}
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}
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}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
g : ℝ → ℝ
hg : 0 ≤ g
x : ℝ
hx : 0 ≤ x
⊢ 0 ≤ S g x
Tactic:
exact div_nonneg (tsum_nonneg (fun i => mul_nonneg (hpos _) (hg _))) hx
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}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico 1 2).indicator 1 ≤ ψ
key : Tendsto (fun x => (∑' (n : ℕ), f n * ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
⊢ 0 ≤ ψ
Tactic:
apply le_trans _ h4
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun n => ↑(f n)) σ')
hcheby : cheby fun n => ↑(f n)
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries (fun n => ↑(f n)) s - ↑A / (s - 1)) {s | 1 < s.re}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico 1 2).indicator 1 ≤ ψ
key : Tendsto (fun x => (∑' (n : ℕ), f n * ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
⊢ 0 ≤ (Ico 1 2).indicator 1

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}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico 1 2).indicator 1 ≤ ψ
key : Tendsto (fun x => (∑' (n : ℕ), f n * ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
⊢ 0 ≤ (Ico 1 2).indicator 1
Tactic:
apply indicator_nonneg
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}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico 1 2).indicator 1 ≤ ψ
key : Tendsto (fun x => (∑' (n : ℕ), f n * ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
⊢ ∀ a ∈ Ico 1 2, 0 ≤ 1 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}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico 1 2).indicator 1 ≤ ψ
key : Tendsto (fun x => (∑' (n : ℕ), f n * ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
⊢ ∀ a ∈ Ico 1 2, 0 ≤ 1 a
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}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico 1 2).indicator 1 ≤ ψ
key : Tendsto (fun x => (∑' (n : ℕ), f n * ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l2 : 0 ≤ ψ
l1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S ψ x
l3 : 0 ≤ A * ∫ (y : ℝ) in Ioi 0, ψ y
⊢ 0 < ∫ (y : ℝ) in Ioi 0, ψ y
Tactic:
have r1 : 0 ≤ᵐ[Measure.restrict volume (Ioi 0)] ψ := eventually_of_forall l2
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun n => ↑(f n)) σ')
hcheby : cheby fun n => ↑(f n)
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries (fun n => ↑(f n)) s - ↑A / (s - 1)) {s | 1 < s.re}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico 1 2).indicator 1 ≤ ψ
key : Tendsto (fun x => (∑' (n : ℕ), f n * ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l2 : 0 ≤ ψ
l1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S ψ x
l3 : 0 ≤ A * ∫ (y : ℝ) in Ioi 0, ψ y
r1 : 0 ≤ᶠ[ae (volume.restrict (Ioi 0))] ψ
⊢ 0 < ∫ (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}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico 1 2).indicator 1 ≤ ψ
key : Tendsto (fun x => (∑' (n : ℕ), f n * ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l2 : 0 ≤ ψ
l1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S ψ x
l3 : 0 ≤ A * ∫ (y : ℝ) in Ioi 0, ψ y
r1 : 0 ≤ᶠ[ae (volume.restrict (Ioi 0))] ψ
⊢ 0 < ∫ (y : ℝ) in Ioi 0, ψ y
Tactic:
have r2 : IntegrableOn (fun y ↦ ψ y) (Ioi 0) volume :=
  (h1.continuous.integrable_of_hasCompactSupport h2).integrableOn
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun n => ↑(f n)) σ')
hcheby : cheby fun n => ↑(f n)
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries (fun n => ↑(f n)) s - ↑A / (s - 1)) {s | 1 < s.re}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico 1 2).indicator 1 ≤ ψ
key : Tendsto (fun x => (∑' (n : ℕ), f n * ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l2 : 0 ≤ ψ
l1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S ψ x
l3 : 0 ≤ A * ∫ (y : ℝ) in Ioi 0, ψ y
r1 : 0 ≤ᶠ[ae (volume.restrict (Ioi 0))] ψ
r2 : IntegrableOn (fun y => ψ y) (Ioi 0) volume
⊢ 0 < ∫ (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}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico 1 2).indicator 1 ≤ ψ
key : Tendsto (fun x => (∑' (n : ℕ), f n * ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l2 : 0 ≤ ψ
l1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S ψ x
l3 : 0 ≤ A * ∫ (y : ℝ) in Ioi 0, ψ y
r1 : 0 ≤ᶠ[ae (volume.restrict (Ioi 0))] ψ
r2 : IntegrableOn (fun y => ψ y) (Ioi 0) volume
⊢ 0 < ∫ (y : ℝ) in Ioi 0, ψ y
Tactic:
have r3 : Ico 1 2 ⊆ Function.support ψ := by intro x hx ; have := h4 x ; simp [hx] at this ⊢ ; linarith
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun n => ↑(f n)) σ')
hcheby : cheby fun n => ↑(f n)
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries (fun n => ↑(f n)) s - ↑A / (s - 1)) {s | 1 < s.re}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico 1 2).indicator 1 ≤ ψ
key : Tendsto (fun x => (∑' (n : ℕ), f n * ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l2 : 0 ≤ ψ
l1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S ψ x
l3 : 0 ≤ A * ∫ (y : ℝ) in Ioi 0, ψ y
r1 : 0 ≤ᶠ[ae (volume.restrict (Ioi 0))] ψ
r2 : IntegrableOn (fun y => ψ y) (Ioi 0) volume
r3 : Ico 1 2 ⊆ Function.support ψ
⊢ 0 < ∫ (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}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico 1 2).indicator 1 ≤ ψ
key : Tendsto (fun x => (∑' (n : ℕ), f n * ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l2 : 0 ≤ ψ
l1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S ψ x
l3 : 0 ≤ A * ∫ (y : ℝ) in Ioi 0, ψ y
r1 : 0 ≤ᶠ[ae (volume.restrict (Ioi 0))] ψ
r2 : IntegrableOn (fun y => ψ y) (Ioi 0) volume
r3 : Ico 1 2 ⊆ Function.support ψ
⊢ 0 < ∫ (y : ℝ) in Ioi 0, ψ y
Tactic:
have r4 : Ico 1 2 ⊆ Function.support ψ ∩ Ioi 0 := by
  simp only [subset_inter_iff, r3, true_and] ; apply Ico_subset_Icc_self.trans ; rw [Icc_subset_Ioi_iff] <;> linarith
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun n => ↑(f n)) σ')
hcheby : cheby fun n => ↑(f n)
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries (fun n => ↑(f n)) s - ↑A / (s - 1)) {s | 1 < s.re}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico 1 2).indicator 1 ≤ ψ
key : Tendsto (fun x => (∑' (n : ℕ), f n * ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l2 : 0 ≤ ψ
l1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S ψ x
l3 : 0 ≤ A * ∫ (y : ℝ) in Ioi 0, ψ y
r1 : 0 ≤ᶠ[ae (volume.restrict (Ioi 0))] ψ
r2 : IntegrableOn (fun y => ψ y) (Ioi 0) volume
r3 : Ico 1 2 ⊆ Function.support ψ
r4 : Ico 1 2 ⊆ Function.support ψ ∩ Ioi 0
⊢ 0 < ∫ (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}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico 1 2).indicator 1 ≤ ψ
key : Tendsto (fun x => (∑' (n : ℕ), f n * ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l2 : 0 ≤ ψ
l1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S ψ x
l3 : 0 ≤ A * ∫ (y : ℝ) in Ioi 0, ψ y
r1 : 0 ≤ᶠ[ae (volume.restrict (Ioi 0))] ψ
r2 : IntegrableOn (fun y => ψ y) (Ioi 0) volume
r3 : Ico 1 2 ⊆ Function.support ψ
r4 : Ico 1 2 ⊆ Function.support ψ ∩ Ioi 0
⊢ 0 < ∫ (y : ℝ) in Ioi 0, ψ y
Tactic:
have r5 : 1 ≤ volume ((Function.support fun y ↦ ψ y) ∩ Ioi 0) := by convert volume.mono r4 ; norm_num
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun n => ↑(f n)) σ')
hcheby : cheby fun n => ↑(f n)
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries (fun n => ↑(f n)) s - ↑A / (s - 1)) {s | 1 < s.re}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico 1 2).indicator 1 ≤ ψ
key : Tendsto (fun x => (∑' (n : ℕ), f n * ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l2 : 0 ≤ ψ
l1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S ψ x
l3 : 0 ≤ A * ∫ (y : ℝ) in Ioi 0, ψ y
r1 : 0 ≤ᶠ[ae (volume.restrict (Ioi 0))] ψ
r2 : IntegrableOn (fun y => ψ y) (Ioi 0) volume
r3 : Ico 1 2 ⊆ Function.support ψ
r4 : Ico 1 2 ⊆ Function.support ψ ∩ Ioi 0
r5 : 1 ≤ volume ((Function.support fun y => ψ y) ∩ Ioi 0)
⊢ 0 < ∫ (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}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico 1 2).indicator 1 ≤ ψ
key : Tendsto (fun x => (∑' (n : ℕ), f n * ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l2 : 0 ≤ ψ
l1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S ψ x
l3 : 0 ≤ A * ∫ (y : ℝ) in Ioi 0, ψ y
r1 : 0 ≤ᶠ[ae (volume.restrict (Ioi 0))] ψ
r2 : IntegrableOn (fun y => ψ y) (Ioi 0) volume
r3 : Ico 1 2 ⊆ Function.support ψ
r4 : Ico 1 2 ⊆ Function.support ψ ∩ Ioi 0
r5 : 1 ≤ volume ((Function.support fun y => ψ y) ∩ Ioi 0)
⊢ 0 < ∫ (y : ℝ) in Ioi 0, ψ y
Tactic:
simpa [setIntegral_pos_iff_support_of_nonneg_ae r1 r2] using zero_lt_one.trans_le r5
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}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico 1 2).indicator 1 ≤ ψ
key : Tendsto (fun x => (∑' (n : ℕ), f n * ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l2 : 0 ≤ ψ
l1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S ψ x
l3 : 0 ≤ A * ∫ (y : ℝ) in Ioi 0, ψ y
r1 : 0 ≤ᶠ[ae (volume.restrict (Ioi 0))] ψ
r2 : IntegrableOn (fun y => ψ y) (Ioi 0) volume
⊢ Ico 1 2 ⊆ Function.support ψ
Tactic:
intro x hx
State after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun n => ↑(f n)) σ')
hcheby : cheby fun n => ↑(f n)
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries (fun n => ↑(f n)) s - ↑A / (s - 1)) {s | 1 < s.re}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico 1 2).indicator 1 ≤ ψ
key : Tendsto (fun x => (∑' (n : ℕ), f n * ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l2 : 0 ≤ ψ
l1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S ψ x
l3 : 0 ≤ A * ∫ (y : ℝ) in Ioi 0, ψ y
r1 : 0 ≤ᶠ[ae (volume.restrict (Ioi 0))] ψ
r2 : IntegrableOn (fun y => ψ y) (Ioi 0) volume
x : ℝ
hx : x ∈ Ico 1 2
⊢ x ∈ Function.support ψ

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}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico 1 2).indicator 1 ≤ ψ
key : Tendsto (fun x => (∑' (n : ℕ), f n * ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l2 : 0 ≤ ψ
l1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S ψ x
l3 : 0 ≤ A * ∫ (y : ℝ) in Ioi 0, ψ y
r1 : 0 ≤ᶠ[ae (volume.restrict (Ioi 0))] ψ
r2 : IntegrableOn (fun y => ψ y) (Ioi 0) volume
x : ℝ
hx : x ∈ Ico 1 2
⊢ x ∈ Function.support ψ
Tactic:
have := h4 x
State after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun n => ↑(f n)) σ')
hcheby : cheby fun n => ↑(f n)
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries (fun n => ↑(f n)) s - ↑A / (s - 1)) {s | 1 < s.re}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico 1 2).indicator 1 ≤ ψ
key : Tendsto (fun x => (∑' (n : ℕ), f n * ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l2 : 0 ≤ ψ
l1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S ψ x
l3 : 0 ≤ A * ∫ (y : ℝ) in Ioi 0, ψ y
r1 : 0 ≤ᶠ[ae (volume.restrict (Ioi 0))] ψ
r2 : IntegrableOn (fun y => ψ y) (Ioi 0) volume
x : ℝ
hx : x ∈ Ico 1 2
this : (Ico 1 2).indicator 1 x ≤ ψ x
⊢ x ∈ Function.support ψ

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}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico 1 2).indicator 1 ≤ ψ
key : Tendsto (fun x => (∑' (n : ℕ), f n * ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l2 : 0 ≤ ψ
l1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S ψ x
l3 : 0 ≤ A * ∫ (y : ℝ) in Ioi 0, ψ y
r1 : 0 ≤ᶠ[ae (volume.restrict (Ioi 0))] ψ
r2 : IntegrableOn (fun y => ψ y) (Ioi 0) volume
x : ℝ
hx : x ∈ Ico 1 2
this : (Ico 1 2).indicator 1 x ≤ ψ x
⊢ x ∈ Function.support ψ
Tactic:
simp [hx] at this ⊢
State after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun n => ↑(f n)) σ')
hcheby : cheby fun n => ↑(f n)
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries (fun n => ↑(f n)) s - ↑A / (s - 1)) {s | 1 < s.re}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico 1 2).indicator 1 ≤ ψ
key : Tendsto (fun x => (∑' (n : ℕ), f n * ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l2 : 0 ≤ ψ
l1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S ψ x
l3 : 0 ≤ A * ∫ (y : ℝ) in Ioi 0, ψ y
r1 : 0 ≤ᶠ[ae (volume.restrict (Ioi 0))] ψ
r2 : IntegrableOn (fun y => ψ y) (Ioi 0) volume
x : ℝ
hx : x ∈ Ico 1 2
this : 1 ≤ ψ x
⊢ ¬ψ x = 0

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}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico 1 2).indicator 1 ≤ ψ
key : Tendsto (fun x => (∑' (n : ℕ), f n * ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l2 : 0 ≤ ψ
l1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S ψ x
l3 : 0 ≤ A * ∫ (y : ℝ) in Ioi 0, ψ y
r1 : 0 ≤ᶠ[ae (volume.restrict (Ioi 0))] ψ
r2 : IntegrableOn (fun y => ψ y) (Ioi 0) volume
x : ℝ
hx : x ∈ Ico 1 2
this : 1 ≤ ψ x
⊢ ¬ψ x = 0
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}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico 1 2).indicator 1 ≤ ψ
key : Tendsto (fun x => (∑' (n : ℕ), f n * ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l2 : 0 ≤ ψ
l1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S ψ x
l3 : 0 ≤ A * ∫ (y : ℝ) in Ioi 0, ψ y
r1 : 0 ≤ᶠ[ae (volume.restrict (Ioi 0))] ψ
r2 : IntegrableOn (fun y => ψ y) (Ioi 0) volume
r3 : Ico 1 2 ⊆ Function.support ψ
⊢ Ico 1 2 ⊆ Function.support ψ ∩ Ioi 0
Tactic:
simp only [subset_inter_iff, r3, true_and]
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun n => ↑(f n)) σ')
hcheby : cheby fun n => ↑(f n)
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries (fun n => ↑(f n)) s - ↑A / (s - 1)) {s | 1 < s.re}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico 1 2).indicator 1 ≤ ψ
key : Tendsto (fun x => (∑' (n : ℕ), f n * ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l2 : 0 ≤ ψ
l1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S ψ x
l3 : 0 ≤ A * ∫ (y : ℝ) in Ioi 0, ψ y
r1 : 0 ≤ᶠ[ae (volume.restrict (Ioi 0))] ψ
r2 : IntegrableOn (fun y => ψ y) (Ioi 0) volume
r3 : Ico 1 2 ⊆ Function.support ψ
⊢ Ico 1 2 ⊆ Ioi 0

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}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico 1 2).indicator 1 ≤ ψ
key : Tendsto (fun x => (∑' (n : ℕ), f n * ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l2 : 0 ≤ ψ
l1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S ψ x
l3 : 0 ≤ A * ∫ (y : ℝ) in Ioi 0, ψ y
r1 : 0 ≤ᶠ[ae (volume.restrict (Ioi 0))] ψ
r2 : IntegrableOn (fun y => ψ y) (Ioi 0) volume
r3 : Ico 1 2 ⊆ Function.support ψ
⊢ Ico 1 2 ⊆ Ioi 0
Tactic:
apply Ico_subset_Icc_self.trans
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun n => ↑(f n)) σ')
hcheby : cheby fun n => ↑(f n)
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries (fun n => ↑(f n)) s - ↑A / (s - 1)) {s | 1 < s.re}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico 1 2).indicator 1 ≤ ψ
key : Tendsto (fun x => (∑' (n : ℕ), f n * ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l2 : 0 ≤ ψ
l1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S ψ x
l3 : 0 ≤ A * ∫ (y : ℝ) in Ioi 0, ψ y
r1 : 0 ≤ᶠ[ae (volume.restrict (Ioi 0))] ψ
r2 : IntegrableOn (fun y => ψ y) (Ioi 0) volume
r3 : Ico 1 2 ⊆ Function.support ψ
⊢ Icc 1 2 ⊆ Ioi 0

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}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico 1 2).indicator 1 ≤ ψ
key : Tendsto (fun x => (∑' (n : ℕ), f n * ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l2 : 0 ≤ ψ
l1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S ψ x
l3 : 0 ≤ A * ∫ (y : ℝ) in Ioi 0, ψ y
r1 : 0 ≤ᶠ[ae (volume.restrict (Ioi 0))] ψ
r2 : IntegrableOn (fun y => ψ y) (Ioi 0) volume
r3 : Ico 1 2 ⊆ Function.support ψ
⊢ Icc 1 2 ⊆ Ioi 0
Tactic:
rw [Icc_subset_Ioi_iff] <;> 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}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico 1 2).indicator 1 ≤ ψ
key : Tendsto (fun x => (∑' (n : ℕ), f n * ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l2 : 0 ≤ ψ
l1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S ψ x
l3 : 0 ≤ A * ∫ (y : ℝ) in Ioi 0, ψ y
r1 : 0 ≤ᶠ[ae (volume.restrict (Ioi 0))] ψ
r2 : IntegrableOn (fun y => ψ y) (Ioi 0) volume
r3 : Ico 1 2 ⊆ Function.support ψ
r4 : Ico 1 2 ⊆ Function.support ψ ∩ Ioi 0
⊢ 1 ≤ volume ((Function.support fun y => ψ y) ∩ Ioi 0)
Tactic:
convert volume.mono r4
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}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico 1 2).indicator 1 ≤ ψ
key : Tendsto (fun x => (∑' (n : ℕ), f n * ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l2 : 0 ≤ ψ
l1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S ψ x
l3 : 0 ≤ A * ∫ (y : ℝ) in Ioi 0, ψ y
r1 : 0 ≤ᶠ[ae (volume.restrict (Ioi 0))] ψ
r2 : IntegrableOn (fun y => ψ y) (Ioi 0) volume
r3 : Ico 1 2 ⊆ Function.support ψ
r4 : Ico 1 2 ⊆ Function.support ψ ∩ Ioi 0
⊢ 1 = volume.measureOf (Ico 1 2)

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}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico 1 2).indicator 1 ≤ ψ
key : Tendsto (fun x => (∑' (n : ℕ), f n * ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l2 : 0 ≤ ψ
l1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S ψ x
l3 : 0 ≤ A * ∫ (y : ℝ) in Ioi 0, ψ y
r1 : 0 ≤ᶠ[ae (volume.restrict (Ioi 0))] ψ
r2 : IntegrableOn (fun y => ψ y) (Ioi 0) volume
r3 : Ico 1 2 ⊆ Function.support ψ
r4 : Ico 1 2 ⊆ Function.support ψ ∩ Ioi 0
⊢ 1 = volume.measureOf (Ico 1 2)
Tactic:
norm_num
State after:
no goals