internlm/Lean-Github huggingface dataset:
Theorem: Finset.sum_shift_front'
Proof state before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝¹ : _root_.RCLike 𝕜
E : Type u_1
inst✝ : Ring E
u : ℕ → E
⊢ shift (cumsum u) = (fun x => u 0) + cumsum (shift u)
Tactic:
ext n
Proof state after:
case h
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝¹ : _root_.RCLike 𝕜
E : Type u_1
inst✝ : Ring E
u : ℕ → E
n : ℕ
⊢ shift (cumsum u) n = ((fun x => u 0) + cumsum (shift u)) n
Theorem: Finset.sum_shift_front'
Proof state before:
case h
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝¹ : _root_.RCLike 𝕜
E : Type u_1
inst✝ : Ring E
u : ℕ → E
n : ℕ
⊢ shift (cumsum u) n = ((fun x => u 0) + cumsum (shift u)) n
Tactic:
apply Finset.sum_shift_front
Proof state after:
no goals
Theorem: Finset.sum_shift_back
Proof state before:
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝¹ : _root_.RCLike 𝕜
E : Type u_1
inst✝ : Ring E
u : ℕ → E
n : ℕ
⊢ cumsum u (n + 1) = cumsum u n + u n
Tactic:
simp [cumsum, Finset.range_succ, add_comm]
Proof state after:
no goals
Theorem: Finset.sum_shift_back'
Proof state before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝¹ : _root_.RCLike 𝕜
E : Type u_1
inst✝ : Ring E
u : ℕ → E
⊢ shift (cumsum u) = cumsum u + u
Tactic:
ext n
Proof state after:
case h
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝¹ : _root_.RCLike 𝕜
E : Type u_1
inst✝ : Ring E
u : ℕ → E
n : ℕ
⊢ shift (cumsum u) n = (cumsum u + u) n
Theorem: Finset.sum_shift_back'
Proof state before:
case h
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝¹ : _root_.RCLike 𝕜
E : Type u_1
inst✝ : Ring E
u : ℕ → E
n : ℕ
⊢ shift (cumsum u) n = (cumsum u + u) n
Tactic:
apply Finset.sum_shift_back
Proof state after:
no goals
Theorem: summation_by_parts
Proof state before:
n✝ : ℕ
A✝ a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝¹ : _root_.RCLike 𝕜
E : Type u_1
inst✝ : Ring E
a A b : ℕ → E
ha : a = nabla A
n : ℕ
⊢ cumsum (a * b) (n + 1) = A (n + 1) * b n - A 0 * b 0 - cumsum (shift A * fun i => b (i + 1) - b i) n
Tactic:
have l1 : ∑ x in Finset.range (n + 1), A (x + 1) * b x = ∑ x in Finset.range n, A (x + 1) * b x + A (n + 1) * b n :=
  Finset.sum_shift_back
Proof state after:
n✝ : ℕ
A✝ a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝¹ : _root_.RCLike 𝕜
E : Type u_1
inst✝ : Ring E
a A b : ℕ → E
ha : a = nabla A
n : ℕ
l1 : ∑ x ∈ Finset.range (n + 1), A (x + 1) * b x = ∑ x ∈ Finset.range n, A (x + 1) * b x + A (n + 1) * b n
⊢ cumsum (a * b) (n + 1) = A (n + 1) * b n - A 0 * b 0 - cumsum (shift A * fun i => b (i + 1) - b i) n
Theorem: summation_by_parts
Proof state before:
n✝ : ℕ
A✝ a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝¹ : _root_.RCLike 𝕜
E : Type u_1
inst✝ : Ring E
a A b : ℕ → E
ha : a = nabla A
n : ℕ
l1 : ∑ x ∈ Finset.range (n + 1), A (x + 1) * b x = ∑ x ∈ Finset.range n, A (x + 1) * b x + A (n + 1) * b n
⊢ cumsum (a * b) (n + 1) = A (n + 1) * b n - A 0 * b 0 - cumsum (shift A * fun i => b (i + 1) - b i) n
Tactic:
have l2 : ∑ x in Finset.range (n + 1), A x * b x = A 0 * b 0 + ∑ x in Finset.range n, A (x + 1) * b (x + 1) :=
  Finset.sum_shift_front
Proof state after:
n✝ : ℕ
A✝ a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝¹ : _root_.RCLike 𝕜
E : Type u_1
inst✝ : Ring E
a A b : ℕ → E
ha : a = nabla A
n : ℕ
l1 : ∑ x ∈ Finset.range (n + 1), A (x + 1) * b x = ∑ x ∈ Finset.range n, A (x + 1) * b x + A (n + 1) * b n
l2 : ∑ x ∈ Finset.range (n + 1), A x * b x = A 0 * b 0 + ∑ x ∈ Finset.range n, A (x + 1) * b (x + 1)
⊢ cumsum (a * b) (n + 1) = A (n + 1) * b n - A 0 * b 0 - cumsum (shift A * fun i => b (i + 1) - b i) n
Theorem: summation_by_parts
Proof state before:
n✝ : ℕ
A✝ a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝¹ : _root_.RCLike 𝕜
E : Type u_1
inst✝ : Ring E
a A b : ℕ → E
ha : a = nabla A
n : ℕ
l1 : ∑ x ∈ Finset.range (n + 1), A (x + 1) * b x = ∑ x ∈ Finset.range n, A (x + 1) * b x + A (n + 1) * b n
l2 : ∑ x ∈ Finset.range (n + 1), A x * b x = A 0 * b 0 + ∑ x ∈ Finset.range n, A (x + 1) * b (x + 1)
⊢ cumsum (a * b) (n + 1) = A (n + 1) * b n - A 0 * b 0 - cumsum (shift A * fun i => b (i + 1) - b i) n
Tactic:
simp [cumsum, shift, ha, nabla, sub_mul, mul_sub, l1, l2]
Proof state after:
n✝ : ℕ
A✝ a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝¹ : _root_.RCLike 𝕜
E : Type u_1
inst✝ : Ring E
a A b : ℕ → E
ha : a = nabla A
n : ℕ
l1 : ∑ x ∈ Finset.range (n + 1), A (x + 1) * b x = ∑ x ∈ Finset.range n, A (x + 1) * b x + A (n + 1) * b n
l2 : ∑ x ∈ Finset.range (n + 1), A x * b x = A 0 * b 0 + ∑ x ∈ Finset.range n, A (x + 1) * b (x + 1)
⊢ ∑ x ∈ Finset.range n, A (x + 1) * b x + A (n + 1) * b n - (A 0 * b 0 + ∑ x ∈ Finset.range n, A (x + 1) * b (x + 1)) =
    A (n + 1) * b n - A 0 * b 0 - (∑ x ∈ Finset.range n, A (x + 1) * b (x + 1) - ∑ x ∈ Finset.range n, A (x + 1) * b x)
Theorem: summation_by_parts
Proof state before:
n✝ : ℕ
A✝ a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝¹ : _root_.RCLike 𝕜
E : Type u_1
inst✝ : Ring E
a A b : ℕ → E
ha : a = nabla A
n : ℕ
l1 : ∑ x ∈ Finset.range (n + 1), A (x + 1) * b x = ∑ x ∈ Finset.range n, A (x + 1) * b x + A (n + 1) * b n
l2 : ∑ x ∈ Finset.range (n + 1), A x * b x = A 0 * b 0 + ∑ x ∈ Finset.range n, A (x + 1) * b (x + 1)
⊢ ∑ x ∈ Finset.range n, A (x + 1) * b x + A (n + 1) * b n - (A 0 * b 0 + ∑ x ∈ Finset.range n, A (x + 1) * b (x + 1)) =
    A (n + 1) * b n - A 0 * b 0 - (∑ x ∈ Finset.range n, A (x + 1) * b (x + 1) - ∑ x ∈ Finset.range n, A (x + 1) * b x)
Tactic:
abel
Proof state after:
no goals
Theorem: summation_by_parts'
Proof state before:
n✝ : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝¹ : _root_.RCLike 𝕜
E : Type u_1
inst✝ : Ring E
a b : ℕ → E
n : ℕ
⊢ cumsum (a * b) (n + 1) = cumsum a (n + 1) * b n - cumsum (shift (cumsum a) * nabla b) n
Tactic:
simpa using summation_by_parts (a := a) (b := b) (A := cumsum a) (by simp [Finset.sum_shift_back])
Proof state after:
no goals
Theorem: summation_by_parts'
Proof state before:
n✝ : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝¹ : _root_.RCLike 𝕜
E : Type u_1
inst✝ : Ring E
a b : ℕ → E
n : ℕ
⊢ a = nabla (cumsum a)
Tactic:
simp [Finset.sum_shift_back]
Proof state after:
no goals
Theorem: summation_by_parts''
Proof state before:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝¹ : _root_.RCLike 𝕜
E : Type u_1
inst✝ : Ring E
a b : ℕ → E
⊢ shift (cumsum (a * b)) = shift (cumsum a) * b - cumsum (shift (cumsum a) * nabla b)
Tactic:
ext n
Proof state after:
case h
n✝ : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝¹ : _root_.RCLike 𝕜
E : Type u_1
inst✝ : Ring E
a b : ℕ → E
n : ℕ
⊢ shift (cumsum (a * b)) n = (shift (cumsum a) * b - cumsum (shift (cumsum a) * nabla b)) n
Theorem: summation_by_parts''
Proof state before:
case h
n✝ : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝¹ : _root_.RCLike 𝕜
E : Type u_1
inst✝ : Ring E
a b : ℕ → E
n : ℕ
⊢ shift (cumsum (a * b)) n = (shift (cumsum a) * b - cumsum (shift (cumsum a) * nabla b)) n
Tactic:
apply summation_by_parts'
Proof state after:
no goals
Theorem: summable_iff_bounded
Proof state before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : 0 ≤ u
⊢ Summable u ↔ atTop.BoundedAtFilter (cumsum u)
Tactic:
have l1 : (cumsum u =O[atTop] 1) ↔ _ := isBigO_one_nat_atTop_iff
Proof state after:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : 0 ≤ u
l1 : cumsum u =O[atTop] 1 ↔ ∃ C, ∀ (n : ℕ), ‖cumsum u n‖ ≤ C
⊢ Summable u ↔ atTop.BoundedAtFilter (cumsum u)
Theorem: summable_iff_bounded
Proof state before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : 0 ≤ u
l1 : cumsum u =O[atTop] 1 ↔ ∃ C, ∀ (n : ℕ), ‖cumsum u n‖ ≤ C
⊢ Summable u ↔ atTop.BoundedAtFilter (cumsum u)
Tactic:
have l2 n : ‖cumsum u n‖ = cumsum u n := by simpa using cumsum_nonneg hu n
Proof state after:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : 0 ≤ u
l1 : cumsum u =O[atTop] 1 ↔ ∃ C, ∀ (n : ℕ), ‖cumsum u n‖ ≤ C
l2 : ∀ (n : ℕ), ‖cumsum u n‖ = cumsum u n
⊢ Summable u ↔ atTop.BoundedAtFilter (cumsum u)
Theorem: summable_iff_bounded
Proof state before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : 0 ≤ u
l1 : cumsum u =O[atTop] 1 ↔ ∃ C, ∀ (n : ℕ), ‖cumsum u n‖ ≤ C
l2 : ∀ (n : ℕ), ‖cumsum u n‖ = cumsum u n
⊢ Summable u ↔ atTop.BoundedAtFilter (cumsum u)
Tactic:
simp only [BoundedAtFilter, l1, l2]
Proof state after:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : 0 ≤ u
l1 : cumsum u =O[atTop] 1 ↔ ∃ C, ∀ (n : ℕ), ‖cumsum u n‖ ≤ C
l2 : ∀ (n : ℕ), ‖cumsum u n‖ = cumsum u n
⊢ Summable u ↔ ∃ C, ∀ (n : ℕ), cumsum u n ≤ C
Theorem: summable_iff_bounded
Proof state before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : 0 ≤ u
l1 : cumsum u =O[atTop] 1 ↔ ∃ C, ∀ (n : ℕ), ‖cumsum u n‖ ≤ C
l2 : ∀ (n : ℕ), ‖cumsum u n‖ = cumsum u n
⊢ Summable u ↔ ∃ C, ∀ (n : ℕ), cumsum u n ≤ C
Tactic:
constructor <;> intro ⟨C, h1⟩
Proof state after:
case mp
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : 0 ≤ u
l1 : cumsum u =O[atTop] 1 ↔ ∃ C, ∀ (n : ℕ), ‖cumsum u n‖ ≤ C
l2 : ∀ (n : ℕ), ‖cumsum u n‖ = cumsum u n
C : ℝ
h1 : HasSum u C
⊢ ∃ C, ∀ (n : ℕ), cumsum u n ≤ C

case mpr
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : 0 ≤ u
l1 : cumsum u =O[atTop] 1 ↔ ∃ C, ∀ (n : ℕ), ‖cumsum u n‖ ≤ C
l2 : ∀ (n : ℕ), ‖cumsum u n‖ = cumsum u n
C : ℝ
h1 : ∀ (n : ℕ), cumsum u n ≤ C
⊢ Summable u
Theorem: summable_iff_bounded
Proof state before:
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : 0 ≤ u
l1 : cumsum u =O[atTop] 1 ↔ ∃ C, ∀ (n : ℕ), ‖cumsum u n‖ ≤ C
n : ℕ
⊢ ‖cumsum u n‖ = cumsum u n
Tactic:
simpa using cumsum_nonneg hu n
Proof state after:
no goals
Theorem: summable_iff_bounded
Proof state before:
case mp
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : 0 ≤ u
l1 : cumsum u =O[atTop] 1 ↔ ∃ C, ∀ (n : ℕ), ‖cumsum u n‖ ≤ C
l2 : ∀ (n : ℕ), ‖cumsum u n‖ = cumsum u n
C : ℝ
h1 : HasSum u C
⊢ ∃ C, ∀ (n : ℕ), cumsum u n ≤ C
Tactic:
exact ⟨C, fun n => sum_le_hasSum _ (fun i _ => hu i) h1⟩
Proof state after:
no goals
Theorem: summable_iff_bounded
Proof state before:
case mpr
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : 0 ≤ u
l1 : cumsum u =O[atTop] 1 ↔ ∃ C, ∀ (n : ℕ), ‖cumsum u n‖ ≤ C
l2 : ∀ (n : ℕ), ‖cumsum u n‖ = cumsum u n
C : ℝ
h1 : ∀ (n : ℕ), cumsum u n ≤ C
⊢ Summable u
Tactic:
exact summable_of_sum_range_le hu h1
Proof state after:
no goals
Theorem: summable_congr_ae
Proof state before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u v : ℕ → ℝ
huv : u =ᶠ[atTop] v
⊢ Summable u ↔ Summable v
Tactic:
constructor <;> intro h <;> simp [huv.summable, huv.symm.summable, h]
Proof state after:
no goals
Theorem: BoundedAtFilter.add_const
Proof state before:
n : ℕ
A a b c✝ d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
c : ℝ
⊢ (atTop.BoundedAtFilter fun n => u n + c) ↔ atTop.BoundedAtFilter u
Tactic:
have : u = fun n => (u n + c) + (-c) := by ext n ; ring
Proof state after:
n : ℕ
A a b c✝ d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
c : ℝ
this : u = fun n => u n + c + -c
⊢ (atTop.BoundedAtFilter fun n => u n + c) ↔ atTop.BoundedAtFilter u
Theorem: BoundedAtFilter.add_const
Proof state before:
n : ℕ
A a b c✝ d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
c : ℝ
this : u = fun n => u n + c + -c
⊢ (atTop.BoundedAtFilter fun n => u n + c) ↔ atTop.BoundedAtFilter u
Tactic:
simp [BoundedAtFilter]
Proof state after:
n : ℕ
A a b c✝ d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
c : ℝ
this : u = fun n => u n + c + -c
⊢ (fun n => u n + c) =O[atTop] 1 ↔ u =O[atTop] 1
Theorem: BoundedAtFilter.add_const
Proof state before:
n : ℕ
A a b c✝ d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
c : ℝ
this : u = fun n => u n + c + -c
⊢ (fun n => u n + c) =O[atTop] 1 ↔ u =O[atTop] 1
Tactic:
constructor <;> intro h
Proof state after:
case mp
n : ℕ
A a b c✝ d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
c : ℝ
this : u = fun n => u n + c + -c
h : (fun n => u n + c) =O[atTop] 1
⊢ u =O[atTop] 1

case mpr
n : ℕ
A a b c✝ d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
c : ℝ
this : u = fun n => u n + c + -c
h : u =O[atTop] 1
⊢ (fun n => u n + c) =O[atTop] 1
Theorem: BoundedAtFilter.add_const
Proof state before:
case mp
n : ℕ
A a b c✝ d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
c : ℝ
this : u = fun n => u n + c + -c
h : (fun n => u n + c) =O[atTop] 1
⊢ u =O[atTop] 1

case mpr
n : ℕ
A a b c✝ d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
c : ℝ
this : u = fun n => u n + c + -c
h : u =O[atTop] 1
⊢ (fun n => u n + c) =O[atTop] 1
Tactic:
rw [this]
Proof state after:
case mp
n : ℕ
A a b c✝ d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
c : ℝ
this : u = fun n => u n + c + -c
h : (fun n => u n + c) =O[atTop] 1
⊢ (fun n => u n + c + -c) =O[atTop] 1

case mpr
n : ℕ
A a b c✝ d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
c : ℝ
this : u = fun n => u n + c + -c
h : u =O[atTop] 1
⊢ (fun n => u n + c) =O[atTop] 1
Theorem: BoundedAtFilter.add_const
Proof state before:
case mp
n : ℕ
A a b c✝ d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
c : ℝ
this : u = fun n => u n + c + -c
h : (fun n => u n + c) =O[atTop] 1
⊢ (fun n => u n + c + -c) =O[atTop] 1

case mpr
n : ℕ
A a b c✝ d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
c : ℝ
this : u = fun n => u n + c + -c
h : u =O[atTop] 1
⊢ (fun n => u n + c) =O[atTop] 1
Tactic:
all_goals { exact h.add (const_boundedAtFilter _ _) }
Proof state after:
no goals
Theorem: BoundedAtFilter.add_const
Proof state before:
n : ℕ
A a b c✝ d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
c : ℝ
⊢ u = fun n => u n + c + -c
Tactic:
ext n
Proof state after:
case h
n✝ : ℕ
A a b c✝ d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
c : ℝ
n : ℕ
⊢ u n = u n + c + -c
Theorem: BoundedAtFilter.add_const
Proof state before:
case h
n✝ : ℕ
A a b c✝ d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
c : ℝ
n : ℕ
⊢ u n = u n + c + -c
Tactic:
ring
Proof state after:
no goals
Theorem: BoundedAtFilter.add_const
Proof state before:
case mpr
n : ℕ
A a b c✝ d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
c : ℝ
this : u = fun n => u n + c + -c
h : u =O[atTop] 1
⊢ (fun n => u n + c) =O[atTop] 1
Tactic:
exact h.add (const_boundedAtFilter _ _)
Proof state after:
no goals
Theorem: BoundedAtFilter.comp_add
Proof state before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
N : ℕ
⊢ (atTop.BoundedAtFilter fun n => u (n + N)) ↔ atTop.BoundedAtFilter u
Tactic:
simp [BoundedAtFilter, isBigO_iff]
Proof state after:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
N : ℕ
⊢ (∃ c a, ∀ (b : ℕ), a ≤ b → |u (b + N)| ≤ c) ↔ ∃ c a, ∀ (b : ℕ), a ≤ b → |u b| ≤ c
Theorem: BoundedAtFilter.comp_add
Proof state before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
N : ℕ
⊢ (∃ c a, ∀ (b : ℕ), a ≤ b → |u (b + N)| ≤ c) ↔ ∃ c a, ∀ (b : ℕ), a ≤ b → |u b| ≤ c
Tactic:
constructor <;> intro ⟨C, n₀, h⟩ <;> use C
Proof state after:
case h
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
N : ℕ
C : ℝ
n₀ : ℕ
h : ∀ (b : ℕ), n₀ ≤ b → |u (b + N)| ≤ C
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → |u b| ≤ C

case h
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
N : ℕ
C : ℝ
n₀ : ℕ
h : ∀ (b : ℕ), n₀ ≤ b → |u b| ≤ C
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → |u (b + N)| ≤ C
Theorem: BoundedAtFilter.comp_add
Proof state before:
case h
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
N : ℕ
C : ℝ
n₀ : ℕ
h : ∀ (b : ℕ), n₀ ≤ b → |u (b + N)| ≤ C
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → |u b| ≤ C
Tactic:
refine ⟨n₀ + N, fun n hn => ?_⟩
Proof state after:
case h
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
N : ℕ
C : ℝ
n₀ : ℕ
h : ∀ (b : ℕ), n₀ ≤ b → |u (b + N)| ≤ C
n : ℕ
hn : n₀ + N ≤ n
⊢ |u n| ≤ C
Theorem: BoundedAtFilter.comp_add
Proof state before:
case h
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
N : ℕ
C : ℝ
n₀ : ℕ
h : ∀ (b : ℕ), n₀ ≤ b → |u (b + N)| ≤ C
n : ℕ
hn : n₀ + N ≤ n
⊢ |u n| ≤ C
Tactic:
obtain ⟨k, hk⟩ := Nat.exists_eq_add_of_le' (m := N) (by linarith)
Proof state after:
case h.intro
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
N : ℕ
C : ℝ
n₀ : ℕ
h : ∀ (b : ℕ), n₀ ≤ b → |u (b + N)| ≤ C
n : ℕ
hn : n₀ + N ≤ n
k : ℕ
hk : n = k + N
⊢ |u n| ≤ C
Theorem: BoundedAtFilter.comp_add
Proof state before:
case h.intro
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
N : ℕ
C : ℝ
n₀ : ℕ
h : ∀ (b : ℕ), n₀ ≤ b → |u (b + N)| ≤ C
n : ℕ
hn : n₀ + N ≤ n
k : ℕ
hk : n = k + N
⊢ |u n| ≤ C
Tactic:
subst n
Proof state after:
case h.intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
N : ℕ
C : ℝ
n₀ : ℕ
h : ∀ (b : ℕ), n₀ ≤ b → |u (b + N)| ≤ C
k : ℕ
hn : n₀ + N ≤ k + N
⊢ |u (k + N)| ≤ C
Theorem: BoundedAtFilter.comp_add
Proof state before:
case h.intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
N : ℕ
C : ℝ
n₀ : ℕ
h : ∀ (b : ℕ), n₀ ≤ b → |u (b + N)| ≤ C
k : ℕ
hn : n₀ + N ≤ k + N
⊢ |u (k + N)| ≤ C
Tactic:
exact h _ <| Nat.add_le_add_iff_right.mp hn
Proof state after:
no goals
Theorem: BoundedAtFilter.comp_add
Proof state before:
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
N : ℕ
C : ℝ
n₀ : ℕ
h : ∀ (b : ℕ), n₀ ≤ b → |u (b + N)| ≤ C
n : ℕ
hn : n₀ + N ≤ n
⊢ N ≤ ?m.960186
Tactic:
linarith
Proof state after:
no goals
Theorem: BoundedAtFilter.comp_add
Proof state before:
case h
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
N : ℕ
C : ℝ
n₀ : ℕ
h : ∀ (b : ℕ), n₀ ≤ b → |u b| ≤ C
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → |u (b + N)| ≤ C
Tactic:
exact ⟨n₀, fun n hn => h _ (by linarith)⟩
Proof state after:
no goals
Theorem: BoundedAtFilter.comp_add
Proof state before:
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
N : ℕ
C : ℝ
n₀ : ℕ
h : ∀ (b : ℕ), n₀ ≤ b → |u b| ≤ C
n : ℕ
hn : n₀ ≤ n
⊢ n₀ ≤ n + N
Tactic:
linarith
Proof state after:
no goals
Theorem: summable_iff_bounded'
Proof state before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, 0 ≤ u n
⊢ Summable u ↔ atTop.BoundedAtFilter (cumsum u)
Tactic:
obtain ⟨N, hu⟩ := eventually_atTop.mp hu
Proof state after:
case intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu✝ : ∀ᶠ (n : ℕ) in atTop, 0 ≤ u n
N : ℕ
hu : ∀ b ≥ N, 0 ≤ u b
⊢ Summable u ↔ atTop.BoundedAtFilter (cumsum u)
Theorem: summable_iff_bounded'
Proof state before:
case intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu✝ : ∀ᶠ (n : ℕ) in atTop, 0 ≤ u n
N : ℕ
hu : ∀ b ≥ N, 0 ≤ u b
⊢ Summable u ↔ atTop.BoundedAtFilter (cumsum u)
Tactic:
have e2 : cumsum (fun i ↦ u (i + N)) = fun n => cumsum u (n + N) - cumsum u N := by
  ext n ; simp_rw [cumsum, add_comm _ N, Finset.sum_range_add] ; ring
Proof state after:
case intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu✝ : ∀ᶠ (n : ℕ) in atTop, 0 ≤ u n
N : ℕ
hu : ∀ b ≥ N, 0 ≤ u b
e2 : (cumsum fun i => u (i + N)) = fun n => cumsum u (n + N) - cumsum u N
⊢ Summable u ↔ atTop.BoundedAtFilter (cumsum u)
Theorem: summable_iff_bounded'
Proof state before:
case intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu✝ : ∀ᶠ (n : ℕ) in atTop, 0 ≤ u n
N : ℕ
hu : ∀ b ≥ N, 0 ≤ u b
e2 : (cumsum fun i => u (i + N)) = fun n => cumsum u (n + N) - cumsum u N
⊢ Summable u ↔ atTop.BoundedAtFilter (cumsum u)
Tactic:
rw [← summable_nat_add_iff N, summable_iff_bounded (fun n => hu _ <| Nat.le_add_left N n), e2]
Proof state after:
case intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu✝ : ∀ᶠ (n : ℕ) in atTop, 0 ≤ u n
N : ℕ
hu : ∀ b ≥ N, 0 ≤ u b
e2 : (cumsum fun i => u (i + N)) = fun n => cumsum u (n + N) - cumsum u N
⊢ (atTop.BoundedAtFilter fun n => cumsum u (n + N) - cumsum u N) ↔ atTop.BoundedAtFilter (cumsum u)
Theorem: summable_iff_bounded'
Proof state before:
case intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu✝ : ∀ᶠ (n : ℕ) in atTop, 0 ≤ u n
N : ℕ
hu : ∀ b ≥ N, 0 ≤ u b
e2 : (cumsum fun i => u (i + N)) = fun n => cumsum u (n + N) - cumsum u N
⊢ (atTop.BoundedAtFilter fun n => cumsum u (n + N) - cumsum u N) ↔ atTop.BoundedAtFilter (cumsum u)
Tactic:
simp_rw [sub_eq_add_neg, BoundedAtFilter.add_const, BoundedAtFilter.comp_add]
Proof state after:
no goals
Theorem: summable_iff_bounded'
Proof state before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu✝ : ∀ᶠ (n : ℕ) in atTop, 0 ≤ u n
N : ℕ
hu : ∀ b ≥ N, 0 ≤ u b
⊢ (cumsum fun i => u (i + N)) = fun n => cumsum u (n + N) - cumsum u N
Tactic:
ext n
Proof state after:
case h
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu✝ : ∀ᶠ (n : ℕ) in atTop, 0 ≤ u n
N : ℕ
hu : ∀ b ≥ N, 0 ≤ u b
n : ℕ
⊢ cumsum (fun i => u (i + N)) n = cumsum u (n + N) - cumsum u N
Theorem: summable_iff_bounded'
Proof state before:
case h
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu✝ : ∀ᶠ (n : ℕ) in atTop, 0 ≤ u n
N : ℕ
hu : ∀ b ≥ N, 0 ≤ u b
n : ℕ
⊢ cumsum (fun i => u (i + N)) n = cumsum u (n + N) - cumsum u N
Tactic:
simp_rw [cumsum, add_comm _ N, Finset.sum_range_add]
Proof state after:
case h
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu✝ : ∀ᶠ (n : ℕ) in atTop, 0 ≤ u n
N : ℕ
hu : ∀ b ≥ N, 0 ≤ u b
n : ℕ
⊢ ∑ x ∈ Finset.range n, u (N + x) =
    ∑ x ∈ Finset.range N, u x + ∑ x ∈ Finset.range n, u (N + x) - ∑ x ∈ Finset.range N, u x