Theorem: tendsto_S_S_zero (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
hcheby : cheby fun n => ↑(f n)
⊢ TendstoUniformlyOnFilter (S f) (S f 0) (𝓝[>] 0) atTop
Tactic:
rw [Metric.tendstoUniformlyOnFilter_iff]
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
hcheby : cheby fun n => ↑(f n)
⊢ ∀ ε > 0, ∀ᶠ (n : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, dist (S f 0 n.2) (S f n.1 n.2) < ε

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
hcheby : cheby fun n => ↑(f n)
⊢ ∀ ε > 0, ∀ᶠ (n : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, dist (S f 0 n.2) (S f n.1 n.2) < ε
Tactic:
intro δ hδ
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
hcheby : cheby fun n => ↑(f n)
δ : ℝ
hδ : δ > 0
⊢ ∀ᶠ (n : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, dist (S f 0 n.2) (S f n.1 n.2) < δ

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
hcheby : cheby fun n => ↑(f n)
δ : ℝ
hδ : δ > 0
⊢ ∀ᶠ (n : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, dist (S f 0 n.2) (S f n.1 n.2) < δ
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
δ : ℝ
hδ : δ > 0
C : ℝ
hC : chebyWith C fun n => ↑(f n)
⊢ ∀ᶠ (n : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, dist (S f 0 n.2) (S f n.1 n.2) < δ

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
δ : ℝ
hδ : δ > 0
C : ℝ
hC : chebyWith C fun n => ↑(f n)
⊢ ∀ᶠ (n : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, dist (S f 0 n.2) (S f n.1 n.2) < δ
Tactic:
have l1 : ∀ᶠ (p : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, C * ⌈p.1 * p.2⌉₊ / p.2 < δ := by
  have r1 := tendsto_mul_ceil_div.const_mul C
  simp [mul_div_assoc'] at r1 ; exact r1 (Iio_mem_nhds hδ)
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
δ : ℝ
hδ : δ > 0
C : ℝ
hC : chebyWith C fun n => ↑(f n)
l1 : ∀ᶠ (p : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, C * ↑⌈p.1 * ↑p.2⌉₊ / ↑p.2 < δ
⊢ ∀ᶠ (n : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, dist (S f 0 n.2) (S f n.1 n.2) < δ

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
δ : ℝ
hδ : δ > 0
C : ℝ
hC : chebyWith C fun n => ↑(f n)
l1 : ∀ᶠ (p : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, C * ↑⌈p.1 * ↑p.2⌉₊ / ↑p.2 < δ
⊢ ∀ᶠ (n : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, dist (S f 0 n.2) (S f n.1 n.2) < δ
Tactic:
have : Ioc 0 1 ∈ 𝓝[>] (0 : ℝ) := inter_mem_nhdsWithin _ (Iic_mem_nhds zero_lt_one)
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
δ : ℝ
hδ : δ > 0
C : ℝ
hC : chebyWith C fun n => ↑(f n)
l1 : ∀ᶠ (p : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, C * ↑⌈p.1 * ↑p.2⌉₊ / ↑p.2 < δ
this : Ioc 0 1 ∈ 𝓝[>] 0
⊢ ∀ᶠ (n : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, dist (S f 0 n.2) (S f n.1 n.2) < δ

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
δ : ℝ
hδ : δ > 0
C : ℝ
hC : chebyWith C fun n => ↑(f n)
l1 : ∀ᶠ (p : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, C * ↑⌈p.1 * ↑p.2⌉₊ / ↑p.2 < δ
this : Ioc 0 1 ∈ 𝓝[>] 0
⊢ ∀ᶠ (n : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, dist (S f 0 n.2) (S f n.1 n.2) < δ
Tactic:
filter_upwards [l1, Eventually.prod_inl this _] with (ε, N) h1 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
δ : ℝ
hδ : δ > 0
C : ℝ
hC : chebyWith C fun n => ↑(f n)
l1 : ∀ᶠ (p : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, C * ↑⌈p.1 * ↑p.2⌉₊ / ↑p.2 < δ
this : Ioc 0 1 ∈ 𝓝[>] 0
ε : ℝ
N : ℕ
h1 : C * ↑⌈(ε, N).1 * ↑(ε, N).2⌉₊ / ↑(ε, N).2 < δ
h2 : 0 < (ε, N).1 ∧ (ε, N).1 ≤ 1
⊢ dist (S f 0 (ε, N).2) (S f (ε, N).1 (ε, N).2) < δ

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
δ : ℝ
hδ : δ > 0
C : ℝ
hC : chebyWith C fun n => ↑(f n)
l1 : ∀ᶠ (p : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, C * ↑⌈p.1 * ↑p.2⌉₊ / ↑p.2 < δ
this : Ioc 0 1 ∈ 𝓝[>] 0
ε : ℝ
N : ℕ
h1 : C * ↑⌈(ε, N).1 * ↑(ε, N).2⌉₊ / ↑(ε, N).2 < δ
h2 : 0 < (ε, N).1 ∧ (ε, N).1 ≤ 1
⊢ dist (S f 0 (ε, N).2) (S f (ε, N).1 (ε, N).2) < δ
Tactic:
have l2 : |cumsum f ⌈ε * ↑N⌉₊ / ↑N| ≤ C * ⌈ε * N⌉₊ / N := by
  have r1 := hC ⌈ε * N⌉₊
  have r2 : 0 ≤ cumsum f ⌈ε * N⌉₊ := by apply cumsum_nonneg hpos
  simp only [Complex.norm_eq_abs, abs_ofReal, abs_eq_self.mpr (hpos _), abs_div,
    abs_eq_self.mpr r2, Nat.abs_cast, ge_iff_le] at r1 ⊢
  apply div_le_div_of_nonneg_right r1 (by positivity)
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
δ : ℝ
hδ : δ > 0
C : ℝ
hC : chebyWith C fun n => ↑(f n)
l1 : ∀ᶠ (p : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, C * ↑⌈p.1 * ↑p.2⌉₊ / ↑p.2 < δ
this : Ioc 0 1 ∈ 𝓝[>] 0
ε : ℝ
N : ℕ
h1 : C * ↑⌈(ε, N).1 * ↑(ε, N).2⌉₊ / ↑(ε, N).2 < δ
h2 : 0 < (ε, N).1 ∧ (ε, N).1 ≤ 1
l2 : |cumsum f ⌈ε * ↑N⌉₊ / ↑N| ≤ C * ↑⌈ε * ↑N⌉₊ / ↑N
⊢ dist (S f 0 (ε, N).2) (S f (ε, N).1 (ε, N).2) < δ

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
δ : ℝ
hδ : δ > 0
C : ℝ
hC : chebyWith C fun n => ↑(f n)
l1 : ∀ᶠ (p : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, C * ↑⌈p.1 * ↑p.2⌉₊ / ↑p.2 < δ
this : Ioc 0 1 ∈ 𝓝[>] 0
ε : ℝ
N : ℕ
h1 : C * ↑⌈(ε, N).1 * ↑(ε, N).2⌉₊ / ↑(ε, N).2 < δ
h2 : 0 < (ε, N).1 ∧ (ε, N).1 ≤ 1
l2 : |cumsum f ⌈ε * ↑N⌉₊ / ↑N| ≤ C * ↑⌈ε * ↑N⌉₊ / ↑N
⊢ dist (S f 0 (ε, N).2) (S f (ε, N).1 (ε, N).2) < δ
Tactic:
simpa [← S_sub_S h2.2] using l2.trans_lt h1
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
δ : ℝ
hδ : δ > 0
C : ℝ
hC : chebyWith C fun n => ↑(f n)
⊢ ∀ᶠ (p : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, C * ↑⌈p.1 * ↑p.2⌉₊ / ↑p.2 < δ
Tactic:
have r1 := tendsto_mul_ceil_div.const_mul C
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
δ : ℝ
hδ : δ > 0
C : ℝ
hC : chebyWith C fun n => ↑(f n)
r1 : Tendsto (fun k => C * (↑⌈k.1 * ↑k.2⌉₊ / ↑k.2)) (𝓝[>] 0 ×ˢ atTop) (𝓝 (C * 0))
⊢ ∀ᶠ (p : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, C * ↑⌈p.1 * ↑p.2⌉₊ / ↑p.2 < δ

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
δ : ℝ
hδ : δ > 0
C : ℝ
hC : chebyWith C fun n => ↑(f n)
r1 : Tendsto (fun k => C * (↑⌈k.1 * ↑k.2⌉₊ / ↑k.2)) (𝓝[>] 0 ×ˢ atTop) (𝓝 (C * 0))
⊢ ∀ᶠ (p : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, C * ↑⌈p.1 * ↑p.2⌉₊ / ↑p.2 < δ
Tactic:
simp [mul_div_assoc'] at r1
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
δ : ℝ
hδ : δ > 0
C : ℝ
hC : chebyWith C fun n => ↑(f n)
r1 : Tendsto (fun k => C * ↑⌈k.1 * ↑k.2⌉₊ / ↑k.2) (𝓝[>] 0 ×ˢ atTop) (𝓝 0)
⊢ ∀ᶠ (p : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, C * ↑⌈p.1 * ↑p.2⌉₊ / ↑p.2 < δ

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
δ : ℝ
hδ : δ > 0
C : ℝ
hC : chebyWith C fun n => ↑(f n)
r1 : Tendsto (fun k => C * ↑⌈k.1 * ↑k.2⌉₊ / ↑k.2) (𝓝[>] 0 ×ˢ atTop) (𝓝 0)
⊢ ∀ᶠ (p : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, C * ↑⌈p.1 * ↑p.2⌉₊ / ↑p.2 < δ
Tactic:
exact r1 (Iio_mem_nhds hδ)
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
δ : ℝ
hδ : δ > 0
C : ℝ
hC : chebyWith C fun n => ↑(f n)
l1 : ∀ᶠ (p : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, C * ↑⌈p.1 * ↑p.2⌉₊ / ↑p.2 < δ
this : Ioc 0 1 ∈ 𝓝[>] 0
ε : ℝ
N : ℕ
h1 : C * ↑⌈(ε, N).1 * ↑(ε, N).2⌉₊ / ↑(ε, N).2 < δ
h2 : 0 < (ε, N).1 ∧ (ε, N).1 ≤ 1
⊢ |cumsum f ⌈ε * ↑N⌉₊ / ↑N| ≤ C * ↑⌈ε * ↑N⌉₊ / ↑N
Tactic:
have r1 := hC ⌈ε * N⌉₊
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
δ : ℝ
hδ : δ > 0
C : ℝ
hC : chebyWith C fun n => ↑(f n)
l1 : ∀ᶠ (p : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, C * ↑⌈p.1 * ↑p.2⌉₊ / ↑p.2 < δ
this : Ioc 0 1 ∈ 𝓝[>] 0
ε : ℝ
N : ℕ
h1 : C * ↑⌈(ε, N).1 * ↑(ε, N).2⌉₊ / ↑(ε, N).2 < δ
h2 : 0 < (ε, N).1 ∧ (ε, N).1 ≤ 1
r1 : cumsum (fun x => ‖(fun n => ↑(f n)) x‖) ⌈ε * ↑N⌉₊ ≤ C * ↑⌈ε * ↑N⌉₊
⊢ |cumsum f ⌈ε * ↑N⌉₊ / ↑N| ≤ C * ↑⌈ε * ↑N⌉₊ / ↑N

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
δ : ℝ
hδ : δ > 0
C : ℝ
hC : chebyWith C fun n => ↑(f n)
l1 : ∀ᶠ (p : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, C * ↑⌈p.1 * ↑p.2⌉₊ / ↑p.2 < δ
this : Ioc 0 1 ∈ 𝓝[>] 0
ε : ℝ
N : ℕ
h1 : C * ↑⌈(ε, N).1 * ↑(ε, N).2⌉₊ / ↑(ε, N).2 < δ
h2 : 0 < (ε, N).1 ∧ (ε, N).1 ≤ 1
r1 : cumsum (fun x => ‖(fun n => ↑(f n)) x‖) ⌈ε * ↑N⌉₊ ≤ C * ↑⌈ε * ↑N⌉₊
⊢ |cumsum f ⌈ε * ↑N⌉₊ / ↑N| ≤ C * ↑⌈ε * ↑N⌉₊ / ↑N
Tactic:
have r2 : 0 ≤ cumsum f ⌈ε * N⌉₊ := by apply cumsum_nonneg hpos
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
δ : ℝ
hδ : δ > 0
C : ℝ
hC : chebyWith C fun n => ↑(f n)
l1 : ∀ᶠ (p : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, C * ↑⌈p.1 * ↑p.2⌉₊ / ↑p.2 < δ
this : Ioc 0 1 ∈ 𝓝[>] 0
ε : ℝ
N : ℕ
h1 : C * ↑⌈(ε, N).1 * ↑(ε, N).2⌉₊ / ↑(ε, N).2 < δ
h2 : 0 < (ε, N).1 ∧ (ε, N).1 ≤ 1
r1 : cumsum (fun x => ‖(fun n => ↑(f n)) x‖) ⌈ε * ↑N⌉₊ ≤ C * ↑⌈ε * ↑N⌉₊
r2 : 0 ≤ cumsum f ⌈ε * ↑N⌉₊
⊢ |cumsum f ⌈ε * ↑N⌉₊ / ↑N| ≤ C * ↑⌈ε * ↑N⌉₊ / ↑N

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
δ : ℝ
hδ : δ > 0
C : ℝ
hC : chebyWith C fun n => ↑(f n)
l1 : ∀ᶠ (p : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, C * ↑⌈p.1 * ↑p.2⌉₊ / ↑p.2 < δ
this : Ioc 0 1 ∈ 𝓝[>] 0
ε : ℝ
N : ℕ
h1 : C * ↑⌈(ε, N).1 * ↑(ε, N).2⌉₊ / ↑(ε, N).2 < δ
h2 : 0 < (ε, N).1 ∧ (ε, N).1 ≤ 1
r1 : cumsum (fun x => ‖(fun n => ↑(f n)) x‖) ⌈ε * ↑N⌉₊ ≤ C * ↑⌈ε * ↑N⌉₊
r2 : 0 ≤ cumsum f ⌈ε * ↑N⌉₊
⊢ |cumsum f ⌈ε * ↑N⌉₊ / ↑N| ≤ C * ↑⌈ε * ↑N⌉₊ / ↑N
Tactic:
simp only [Complex.norm_eq_abs, abs_ofReal, abs_eq_self.mpr (hpos _), abs_div,
  abs_eq_self.mpr r2, Nat.abs_cast, ge_iff_le] at r1 ⊢
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
δ : ℝ
hδ : δ > 0
C : ℝ
hC : chebyWith C fun n => ↑(f n)
l1 : ∀ᶠ (p : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, C * ↑⌈p.1 * ↑p.2⌉₊ / ↑p.2 < δ
this : Ioc 0 1 ∈ 𝓝[>] 0
ε : ℝ
N : ℕ
h1 : C * ↑⌈(ε, N).1 * ↑(ε, N).2⌉₊ / ↑(ε, N).2 < δ
h2 : 0 < (ε, N).1 ∧ (ε, N).1 ≤ 1
r2 : 0 ≤ cumsum f ⌈ε * ↑N⌉₊
r1 : cumsum (fun x => f x) ⌈ε * ↑N⌉₊ ≤ C * ↑⌈ε * ↑N⌉₊
⊢ cumsum f ⌈ε * ↑N⌉₊ / ↑N ≤ C * ↑⌈ε * ↑N⌉₊ / ↑N

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
δ : ℝ
hδ : δ > 0
C : ℝ
hC : chebyWith C fun n => ↑(f n)
l1 : ∀ᶠ (p : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, C * ↑⌈p.1 * ↑p.2⌉₊ / ↑p.2 < δ
this : Ioc 0 1 ∈ 𝓝[>] 0
ε : ℝ
N : ℕ
h1 : C * ↑⌈(ε, N).1 * ↑(ε, N).2⌉₊ / ↑(ε, N).2 < δ
h2 : 0 < (ε, N).1 ∧ (ε, N).1 ≤ 1
r2 : 0 ≤ cumsum f ⌈ε * ↑N⌉₊
r1 : cumsum (fun x => f x) ⌈ε * ↑N⌉₊ ≤ C * ↑⌈ε * ↑N⌉₊
⊢ cumsum f ⌈ε * ↑N⌉₊ / ↑N ≤ C * ↑⌈ε * ↑N⌉₊ / ↑N
Tactic:
apply div_le_div_of_nonneg_right r1 (by positivity)
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
δ : ℝ
hδ : δ > 0
C : ℝ
hC : chebyWith C fun n => ↑(f n)
l1 : ∀ᶠ (p : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, C * ↑⌈p.1 * ↑p.2⌉₊ / ↑p.2 < δ
this : Ioc 0 1 ∈ 𝓝[>] 0
ε : ℝ
N : ℕ
h1 : C * ↑⌈(ε, N).1 * ↑(ε, N).2⌉₊ / ↑(ε, N).2 < δ
h2 : 0 < (ε, N).1 ∧ (ε, N).1 ≤ 1
r1 : cumsum (fun x => ‖(fun n => ↑(f n)) x‖) ⌈ε * ↑N⌉₊ ≤ C * ↑⌈ε * ↑N⌉₊
⊢ 0 ≤ cumsum f ⌈ε * ↑N⌉₊
Tactic:
apply cumsum_nonneg hpos
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
δ : ℝ
hδ : δ > 0
C : ℝ
hC : chebyWith C fun n => ↑(f n)
l1 : ∀ᶠ (p : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, C * ↑⌈p.1 * ↑p.2⌉₊ / ↑p.2 < δ
this : Ioc 0 1 ∈ 𝓝[>] 0
ε : ℝ
N : ℕ
h1 : C * ↑⌈(ε, N).1 * ↑(ε, N).2⌉₊ / ↑(ε, N).2 < δ
h2 : 0 < (ε, N).1 ∧ (ε, N).1 ≤ 1
r2 : 0 ≤ cumsum f ⌈ε * ↑N⌉₊
r1 : cumsum (fun x => f x) ⌈ε * ↑N⌉₊ ≤ C * ↑⌈ε * ↑N⌉₊
⊢ 0 ≤ ↑N
Tactic:
positivity
State after:
no goals