internlm/Lean-Github huggingface dataset:
Theorem: tendsto_mul_ceil_div
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
N : ℕ
hε : 0 < ε
h1 : ε < δ / 2
h2 : 1 ≤ δ / 2 * ↑N
⊢ 0 < ↑N
Tactic:
simp
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
N : ℕ
hε : 0 < ε
h1 : ε < δ / 2
h2 : 1 ≤ δ / 2 * ↑N
⊢ 0 < N
Theorem: tendsto_mul_ceil_div
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
N : ℕ
hε : 0 < ε
h1 : ε < δ / 2
h2 : 1 ≤ δ / 2 * ↑N
⊢ 0 < N
Tactic:
rw [Nat.pos_iff_ne_zero]
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
N : ℕ
hε : 0 < ε
h1 : ε < δ / 2
h2 : 1 ≤ δ / 2 * ↑N
⊢ N ≠ 0
Theorem: tendsto_mul_ceil_div
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
N : ℕ
hε : 0 < ε
h1 : ε < δ / 2
h2 : 1 ≤ δ / 2 * ↑N
⊢ N ≠ 0
Tactic:
rintro rfl
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
hε : 0 < ε
h1 : ε < δ / 2
h2 : 1 ≤ δ / 2 * ↑0
⊢ False
Theorem: tendsto_mul_ceil_div
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
hε : 0 < ε
h1 : ε < δ / 2
h2 : 1 ≤ δ / 2 * ↑0
⊢ False
Tactic:
simp at h2
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
hε : 0 < ε
h1 : ε < δ / 2
h2 : 1 ≤ 0
⊢ False
Theorem: tendsto_mul_ceil_div
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
hε : 0 < ε
h1 : ε < δ / 2
h2 : 1 ≤ 0
⊢ False
Tactic:
linarith
Proof state after:
no goals
Theorem: tendsto_mul_ceil_div
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
N : ℕ
hε : 0 < ε
h1 : ε < δ / 2
h2 : 1 ≤ δ / 2 * ↑N
l3 : 0 < ↑N
⊢ 0 ≤ ε * ↑N
Tactic:
positivity
Proof state after:
no goals
Theorem: tendsto_mul_ceil_div
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
N : ℕ
hε : 0 < ε
h1 : ε < δ / 2
h2 : 1 ≤ δ / 2 * ↑N
l3 : 0 < ↑N
l5 : 0 ≤ ε * ↑N
⊢ 0 ≤ ↑N
Tactic:
positivity
Proof state after:
no goals
Theorem: tendsto_mul_ceil_div
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
N : ℕ
hε : 0 < ε
h1 : ε < δ / 2
h2 : 1 ≤ δ / 2 * ↑N
l3 : 0 < ↑N
l5 : 0 ≤ ε * ↑N
⊢ 0 ≤ δ / 2
Tactic:
positivity
Proof state after:
no goals
Theorem: S_sub_S
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
⊢ S f 0 N - S f ε N = cumsum f ⌈ε * ↑N⌉₊ / ↑N
Tactic:
have r1 : Finset.range N = Finset.range ⌈ε * N⌉₊ ∪ Finset.Ico ⌈ε * N⌉₊ N := by
  rw [Finset.range_eq_Ico] ; symm ; apply Finset.Ico_union_Ico_eq_Ico (by simp)
  simp ; convert_to ε * ↑N ≤ 1 * ↑N ; ring ; gcongr
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
r1 : Finset.range N = Finset.range ⌈ε * ↑N⌉₊ ∪ Finset.Ico ⌈ε * ↑N⌉₊ N
⊢ S f 0 N - S f ε N = cumsum f ⌈ε * ↑N⌉₊ / ↑N
Theorem: S_sub_S
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
r1 : Finset.range N = Finset.range ⌈ε * ↑N⌉₊ ∪ Finset.Ico ⌈ε * ↑N⌉₊ N
⊢ S f 0 N - S f ε N = cumsum f ⌈ε * ↑N⌉₊ / ↑N
Tactic:
have r2 : Disjoint (Finset.range ⌈ε * N⌉₊) (Finset.Ico ⌈ε * N⌉₊ N) := by
  rw [Finset.range_eq_Ico] ; apply Finset.Ico_disjoint_Ico_consecutive
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
r1 : Finset.range N = Finset.range ⌈ε * ↑N⌉₊ ∪ Finset.Ico ⌈ε * ↑N⌉₊ N
r2 : Disjoint (Finset.range ⌈ε * ↑N⌉₊) (Finset.Ico ⌈ε * ↑N⌉₊ N)
⊢ S f 0 N - S f ε N = cumsum f ⌈ε * ↑N⌉₊ / ↑N
Theorem: S_sub_S
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
r1 : Finset.range N = Finset.range ⌈ε * ↑N⌉₊ ∪ Finset.Ico ⌈ε * ↑N⌉₊ N
r2 : Disjoint (Finset.range ⌈ε * ↑N⌉₊) (Finset.Ico ⌈ε * ↑N⌉₊ N)
⊢ S f 0 N - S f ε N = cumsum f ⌈ε * ↑N⌉₊ / ↑N
Tactic:
simp [S, r1, Finset.sum_union r2, cumsum, add_div, abs_div]
Proof state after:
no goals
Theorem: S_sub_S
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
⊢ Finset.range N = Finset.range ⌈ε * ↑N⌉₊ ∪ Finset.Ico ⌈ε * ↑N⌉₊ N
Tactic:
rw [Finset.range_eq_Ico]
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
⊢ Finset.Ico 0 N = Finset.Ico 0 ⌈ε * ↑N⌉₊ ∪ Finset.Ico ⌈ε * ↑N⌉₊ N
Theorem: S_sub_S
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
⊢ Finset.Ico 0 N = Finset.Ico 0 ⌈ε * ↑N⌉₊ ∪ Finset.Ico ⌈ε * ↑N⌉₊ N
Tactic:
symm
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
⊢ Finset.Ico 0 ⌈ε * ↑N⌉₊ ∪ Finset.Ico ⌈ε * ↑N⌉₊ N = Finset.Ico 0 N
Theorem: S_sub_S
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
⊢ Finset.Ico 0 ⌈ε * ↑N⌉₊ ∪ Finset.Ico ⌈ε * ↑N⌉₊ N = Finset.Ico 0 N
Tactic:
apply Finset.Ico_union_Ico_eq_Ico (by simp)
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
⊢ ⌈ε * ↑N⌉₊ ≤ N
Theorem: S_sub_S
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
⊢ ⌈ε * ↑N⌉₊ ≤ N
Tactic:
simp
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
⊢ ε * ↑N ≤ ↑N
Theorem: S_sub_S
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
⊢ ε * ↑N ≤ ↑N
Tactic:
convert_to ε * ↑N ≤ 1 * ↑N
Proof state after:
case h.e'_4
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
⊢ ↑N = 1 * ↑N

n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
⊢ ε * ↑N ≤ 1 * ↑N
Theorem: S_sub_S
Proof state before:
case h.e'_4
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
⊢ ↑N = 1 * ↑N

n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
⊢ ε * ↑N ≤ 1 * ↑N
Tactic:
ring
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
⊢ ε * ↑N ≤ 1 * ↑N
Theorem: S_sub_S
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
⊢ ε * ↑N ≤ 1 * ↑N
Tactic:
gcongr
Proof state after:
no goals
Theorem: S_sub_S
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
⊢ 0 ≤ ⌈ε * ↑N⌉₊
Tactic:
simp
Proof state after:
no goals
Theorem: S_sub_S
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
r1 : Finset.range N = Finset.range ⌈ε * ↑N⌉₊ ∪ Finset.Ico ⌈ε * ↑N⌉₊ N
⊢ Disjoint (Finset.range ⌈ε * ↑N⌉₊) (Finset.Ico ⌈ε * ↑N⌉₊ N)
Tactic:
rw [Finset.range_eq_Ico]
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
r1 : Finset.range N = Finset.range ⌈ε * ↑N⌉₊ ∪ Finset.Ico ⌈ε * ↑N⌉₊ N
⊢ Disjoint (Finset.Ico 0 ⌈ε * ↑N⌉₊) (Finset.Ico ⌈ε * ↑N⌉₊ N)
Theorem: S_sub_S
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
r1 : Finset.range N = Finset.range ⌈ε * ↑N⌉₊ ∪ Finset.Ico ⌈ε * ↑N⌉₊ N
⊢ Disjoint (Finset.Ico 0 ⌈ε * ↑N⌉₊) (Finset.Ico ⌈ε * ↑N⌉₊ N)
Tactic:
apply Finset.Ico_disjoint_Ico_consecutive
Proof state after:
no goals
Theorem: tendsto_S_S_zero
Proof 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]
Proof 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) < ε
Theorem: tendsto_S_S_zero
Proof 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δ
Proof 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) < δ
Theorem: tendsto_S_S_zero
Proof 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
Proof 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) < δ
Theorem: tendsto_S_S_zero
Proof 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δ)
Proof 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) < δ
Theorem: tendsto_S_S_zero
Proof 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)
Proof 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) < δ
Theorem: tendsto_S_S_zero
Proof 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
Proof 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) < δ
Theorem: tendsto_S_S_zero
Proof 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)
Proof 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) < δ
Theorem: tendsto_S_S_zero
Proof 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
Proof state after:
no goals
Theorem: tendsto_S_S_zero
Proof 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
Proof 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 < δ
Theorem: tendsto_S_S_zero
Proof 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
Proof 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 < δ
Theorem: tendsto_S_S_zero
Proof 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δ)
Proof state after:
no goals
Theorem: tendsto_S_S_zero
Proof 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⌉₊
Proof 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
Theorem: tendsto_S_S_zero
Proof 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
Proof 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
Theorem: tendsto_S_S_zero
Proof 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 ⊢
Proof 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
Theorem: tendsto_S_S_zero
Proof 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)
Proof state after:
no goals
Theorem: tendsto_S_S_zero
Proof 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
Proof state after:
no goals
Theorem: tendsto_S_S_zero
Proof 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
Proof state after:
no goals