internlm/Lean-Github huggingface dataset:
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 : ℕ
⊢ ∑ 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
Tactic:
ring
Proof state after:
no goals
Theorem: bounded_of_shift
Proof state before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
h : atTop.BoundedAtFilter (shift u)
⊢ atTop.BoundedAtFilter u
Tactic:
simp only [BoundedAtFilter, isBigO_iff, eventually_atTop] at h ⊢
Proof state after:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
h : ∃ c a, ∀ b ≥ a, ‖shift u b‖ ≤ c * ‖OfNat.ofNat 1 b‖
⊢ ∃ c a, ∀ b ≥ a, ‖u b‖ ≤ c * ‖OfNat.ofNat 1 b‖
Theorem: bounded_of_shift
Proof state before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
h : ∃ c a, ∀ b ≥ a, ‖shift u b‖ ≤ c * ‖OfNat.ofNat 1 b‖
⊢ ∃ c a, ∀ b ≥ a, ‖u b‖ ≤ c * ‖OfNat.ofNat 1 b‖
Tactic:
obtain ⟨C, N, hC⟩ := h
Proof state after:
case intro.intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
C : ℝ
N : ℕ
hC : ∀ b ≥ N, ‖shift u b‖ ≤ C * ‖OfNat.ofNat 1 b‖
⊢ ∃ c a, ∀ b ≥ a, ‖u b‖ ≤ c * ‖OfNat.ofNat 1 b‖
Theorem: bounded_of_shift
Proof state before:
case intro.intro
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
C : ℝ
N : ℕ
hC : ∀ b ≥ N, ‖shift u b‖ ≤ C * ‖OfNat.ofNat 1 b‖
⊢ ∃ c a, ∀ b ≥ a, ‖u b‖ ≤ c * ‖OfNat.ofNat 1 b‖
Tactic:
refine ⟨C, N + 1, fun n hn => ?_⟩
Proof state after:
case intro.intro
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
C : ℝ
N : ℕ
hC : ∀ b ≥ N, ‖shift u b‖ ≤ C * ‖OfNat.ofNat 1 b‖
n : ℕ
hn : n ≥ N + 1
⊢ ‖u n‖ ≤ C * ‖OfNat.ofNat 1 n‖
Theorem: bounded_of_shift
Proof state before:
case intro.intro
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
C : ℝ
N : ℕ
hC : ∀ b ≥ N, ‖shift u b‖ ≤ C * ‖OfNat.ofNat 1 b‖
n : ℕ
hn : n ≥ N + 1
⊢ ‖u n‖ ≤ C * ‖OfNat.ofNat 1 n‖
Tactic:
simp only [shift] at hC
Proof state after:
case intro.intro
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
C : ℝ
N : ℕ
hC : ∀ b ≥ N, ‖u (b + 1)‖ ≤ C * ‖OfNat.ofNat 1 b‖
n : ℕ
hn : n ≥ N + 1
⊢ ‖u n‖ ≤ C * ‖OfNat.ofNat 1 n‖
Theorem: bounded_of_shift
Proof state before:
case intro.intro
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
C : ℝ
N : ℕ
hC : ∀ b ≥ N, ‖u (b + 1)‖ ≤ C * ‖OfNat.ofNat 1 b‖
n : ℕ
hn : n ≥ N + 1
⊢ ‖u n‖ ≤ C * ‖OfNat.ofNat 1 n‖
Tactic:
have r1 : n - 1 ≥ N := Nat.le_sub_one_of_lt hn
Proof state after:
case intro.intro
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
C : ℝ
N : ℕ
hC : ∀ b ≥ N, ‖u (b + 1)‖ ≤ C * ‖OfNat.ofNat 1 b‖
n : ℕ
hn : n ≥ N + 1
r1 : n - 1 ≥ N
⊢ ‖u n‖ ≤ C * ‖OfNat.ofNat 1 n‖
Theorem: bounded_of_shift
Proof state before:
case intro.intro
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
C : ℝ
N : ℕ
hC : ∀ b ≥ N, ‖u (b + 1)‖ ≤ C * ‖OfNat.ofNat 1 b‖
n : ℕ
hn : n ≥ N + 1
r1 : n - 1 ≥ N
⊢ ‖u n‖ ≤ C * ‖OfNat.ofNat 1 n‖
Tactic:
have r2 : n - 1 + 1 = n := Nat.sub_add_cancel <| NeZero.one_le.trans hn.le
Proof state after:
case intro.intro
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
C : ℝ
N : ℕ
hC : ∀ b ≥ N, ‖u (b + 1)‖ ≤ C * ‖OfNat.ofNat 1 b‖
n : ℕ
hn : n ≥ N + 1
r1 : n - 1 ≥ N
r2 : n - 1 + 1 = n
⊢ ‖u n‖ ≤ C * ‖OfNat.ofNat 1 n‖
Theorem: bounded_of_shift
Proof state before:
case intro.intro
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
C : ℝ
N : ℕ
hC : ∀ b ≥ N, ‖u (b + 1)‖ ≤ C * ‖OfNat.ofNat 1 b‖
n : ℕ
hn : n ≥ N + 1
r1 : n - 1 ≥ N
r2 : n - 1 + 1 = n
⊢ ‖u n‖ ≤ C * ‖OfNat.ofNat 1 n‖
Tactic:
simpa [r2] using hC (n - 1) r1
Proof state after:
no goals
Theorem: dirichlet_test'
Proof state before:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℕ → ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hAb : atTop.BoundedAtFilter (shift (cumsum a) * b)
hbb : ∀ᶠ (n : ℕ) in atTop, b (n + 1) ≤ b n
h : Summable (shift (cumsum a) * nnabla b)
⊢ Summable (a * b)
Tactic:
have l1 : ∀ᶠ n in atTop, 0 ≤ (shift (cumsum a) * nnabla b) n := by
  filter_upwards [hbb] with n hb
  exact mul_nonneg (by simpa [shift] using Finset.sum_nonneg' ha) (sub_nonneg.mpr hb)
Proof state after:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℕ → ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hAb : atTop.BoundedAtFilter (shift (cumsum a) * b)
hbb : ∀ᶠ (n : ℕ) in atTop, b (n + 1) ≤ b n
h : Summable (shift (cumsum a) * nnabla b)
l1 : ∀ᶠ (n : ℕ) in atTop, 0 ≤ (shift (cumsum a) * nnabla b) n
⊢ Summable (a * b)
Theorem: dirichlet_test'
Proof state before:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℕ → ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hAb : atTop.BoundedAtFilter (shift (cumsum a) * b)
hbb : ∀ᶠ (n : ℕ) in atTop, b (n + 1) ≤ b n
h : Summable (shift (cumsum a) * nnabla b)
l1 : ∀ᶠ (n : ℕ) in atTop, 0 ≤ (shift (cumsum a) * nnabla b) n
⊢ Summable (a * b)
Tactic:
rw [summable_iff_bounded (mul_nonneg ha hb)]
Proof state after:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℕ → ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hAb : atTop.BoundedAtFilter (shift (cumsum a) * b)
hbb : ∀ᶠ (n : ℕ) in atTop, b (n + 1) ≤ b n
h : Summable (shift (cumsum a) * nnabla b)
l1 : ∀ᶠ (n : ℕ) in atTop, 0 ≤ (shift (cumsum a) * nnabla b) n
⊢ atTop.BoundedAtFilter (cumsum (a * b))
Theorem: dirichlet_test'
Proof state before:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℕ → ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hAb : atTop.BoundedAtFilter (shift (cumsum a) * b)
hbb : ∀ᶠ (n : ℕ) in atTop, b (n + 1) ≤ b n
h : Summable (shift (cumsum a) * nnabla b)
l1 : ∀ᶠ (n : ℕ) in atTop, 0 ≤ (shift (cumsum a) * nnabla b) n
⊢ atTop.BoundedAtFilter (cumsum (a * b))
Tactic:
rw [summable_iff_bounded' l1] at h
Proof state after:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℕ → ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hAb : atTop.BoundedAtFilter (shift (cumsum a) * b)
hbb : ∀ᶠ (n : ℕ) in atTop, b (n + 1) ≤ b n
h : atTop.BoundedAtFilter (cumsum fun n => (shift (cumsum a) * nnabla b) n)
l1 : ∀ᶠ (n : ℕ) in atTop, 0 ≤ (shift (cumsum a) * nnabla b) n
⊢ atTop.BoundedAtFilter (cumsum (a * b))
Theorem: dirichlet_test'
Proof state before:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℕ → ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hAb : atTop.BoundedAtFilter (shift (cumsum a) * b)
hbb : ∀ᶠ (n : ℕ) in atTop, b (n + 1) ≤ b n
h : atTop.BoundedAtFilter (cumsum fun n => (shift (cumsum a) * nnabla b) n)
l1 : ∀ᶠ (n : ℕ) in atTop, 0 ≤ (shift (cumsum a) * nnabla b) n
⊢ atTop.BoundedAtFilter (cumsum (a * b))
Tactic:
apply bounded_of_shift
Proof state after:
case h
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℕ → ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hAb : atTop.BoundedAtFilter (shift (cumsum a) * b)
hbb : ∀ᶠ (n : ℕ) in atTop, b (n + 1) ≤ b n
h : atTop.BoundedAtFilter (cumsum fun n => (shift (cumsum a) * nnabla b) n)
l1 : ∀ᶠ (n : ℕ) in atTop, 0 ≤ (shift (cumsum a) * nnabla b) n
⊢ atTop.BoundedAtFilter (shift (cumsum (a * b)))
Theorem: dirichlet_test'
Proof state before:
case h
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℕ → ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hAb : atTop.BoundedAtFilter (shift (cumsum a) * b)
hbb : ∀ᶠ (n : ℕ) in atTop, b (n + 1) ≤ b n
h : atTop.BoundedAtFilter (cumsum fun n => (shift (cumsum a) * nnabla b) n)
l1 : ∀ᶠ (n : ℕ) in atTop, 0 ≤ (shift (cumsum a) * nnabla b) n
⊢ atTop.BoundedAtFilter (shift (cumsum (a * b)))
Tactic:
simpa only [summation_by_parts'', sub_eq_add_neg, neg_cumsum, ← mul_neg, neg_nabla] using hAb.add h
Proof state after:
no goals
Theorem: dirichlet_test'
Proof state before:
n : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℕ → ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hAb : atTop.BoundedAtFilter (shift (cumsum a) * b)
hbb : ∀ᶠ (n : ℕ) in atTop, b (n + 1) ≤ b n
h : Summable (shift (cumsum a) * nnabla b)
⊢ ∀ᶠ (n : ℕ) in atTop, 0 ≤ (shift (cumsum a) * nnabla b) n
Tactic:
filter_upwards [hbb] with n hb
Proof state after:
case h
n✝ : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℕ → ℝ
ha : 0 ≤ a
hb✝ : 0 ≤ b
hAb : atTop.BoundedAtFilter (shift (cumsum a) * b)
hbb : ∀ᶠ (n : ℕ) in atTop, b (n + 1) ≤ b n
h : Summable (shift (cumsum a) * nnabla b)
n : ℕ
hb : b (n + 1) ≤ b n
⊢ 0 ≤ (shift (cumsum a) * nnabla b) n
Theorem: dirichlet_test'
Proof state before:
case h
n✝ : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℕ → ℝ
ha : 0 ≤ a
hb✝ : 0 ≤ b
hAb : atTop.BoundedAtFilter (shift (cumsum a) * b)
hbb : ∀ᶠ (n : ℕ) in atTop, b (n + 1) ≤ b n
h : Summable (shift (cumsum a) * nnabla b)
n : ℕ
hb : b (n + 1) ≤ b n
⊢ 0 ≤ (shift (cumsum a) * nnabla b) n
Tactic:
exact mul_nonneg (by simpa [shift] using Finset.sum_nonneg' ha) (sub_nonneg.mpr hb)
Proof state after:
no goals
Theorem: dirichlet_test'
Proof state before:
n✝ : ℕ
A a✝ b✝ c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b : ℕ → ℝ
ha : 0 ≤ a
hb✝ : 0 ≤ b
hAb : atTop.BoundedAtFilter (shift (cumsum a) * b)
hbb : ∀ᶠ (n : ℕ) in atTop, b (n + 1) ≤ b n
h : Summable (shift (cumsum a) * nnabla b)
n : ℕ
hb : b (n + 1) ≤ b n
⊢ 0 ≤ shift (cumsum a) n
Tactic:
simpa [shift] using Finset.sum_nonneg' ha
Proof state after:
no goals
Theorem: exists_antitone_of_eventually
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, u (n + 1) ≤ u n
⊢ ∃ v, range v ⊆ range u ∧ Antitone v ∧ v =ᶠ[atTop] u
Tactic:
obtain ⟨N, hN⟩ := 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, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
⊢ ∃ v, range v ⊆ range u ∧ Antitone v ∧ v =ᶠ[atTop] u
Theorem: exists_antitone_of_eventually
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, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
⊢ ∃ v, range v ⊆ range u ∧ Antitone v ∧ v =ᶠ[atTop] u
Tactic:
let v (n : ℕ) := u (if n < N then N else n)
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, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
⊢ ∃ v, range v ⊆ range u ∧ Antitone v ∧ v =ᶠ[atTop] u
Theorem: exists_antitone_of_eventually
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, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
⊢ ∃ v, range v ⊆ range u ∧ Antitone v ∧ v =ᶠ[atTop] u
Tactic:
refine ⟨v, ?_, ?_, ?_⟩
Proof state after:
case intro.refine_1
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
⊢ range v ⊆ range u

case intro.refine_2
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
⊢ Antitone v

case intro.refine_3
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
⊢ v =ᶠ[atTop] u
Theorem: exists_antitone_of_eventually
Proof state before:
case intro.refine_1
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
⊢ range v ⊆ range u
Tactic:
exact fun x ⟨n, hn⟩ => ⟨if n < N then N else n, hn⟩
Proof state after:
no goals
Theorem: exists_antitone_of_eventually
Proof state before:
case intro.refine_2
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
⊢ Antitone v
Tactic:
refine antitone_nat_of_succ_le (fun n => ?_)
Proof state after:
case intro.refine_2
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
n : ℕ
⊢ v (n + 1) ≤ v n
Theorem: exists_antitone_of_eventually
Proof state before:
case intro.refine_2
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
n : ℕ
⊢ v (n + 1) ≤ v n
Tactic:
by_cases h : n < N
Proof state after:
case pos
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
n : ℕ
h : n < N
⊢ v (n + 1) ≤ v n

case neg
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
n : ℕ
h : ¬n < N
⊢ v (n + 1) ≤ v n
Theorem: exists_antitone_of_eventually
Proof state before:
case pos
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
n : ℕ
h : n < N
⊢ v (n + 1) ≤ v n
Tactic:
by_cases h' : n + 1 < N <;> simp [v, h, h']
Proof state after:
case neg
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
n : ℕ
h : n < N
h' : ¬n + 1 < N
⊢ u (n + 1) ≤ u N
Theorem: exists_antitone_of_eventually
Proof state before:
case neg
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
n : ℕ
h : n < N
h' : ¬n + 1 < N
⊢ u (n + 1) ≤ u N
Tactic:
have : n + 1 = N := by linarith
Proof state after:
case neg
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
n : ℕ
h : n < N
h' : ¬n + 1 < N
this : n + 1 = N
⊢ u (n + 1) ≤ u N
Theorem: exists_antitone_of_eventually
Proof state before:
case neg
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
n : ℕ
h : n < N
h' : ¬n + 1 < N
this : n + 1 = N
⊢ u (n + 1) ≤ u N
Tactic:
simp [this]
Proof state after:
no goals
Theorem: exists_antitone_of_eventually
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, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
n : ℕ
h : n < N
h' : ¬n + 1 < N
⊢ n + 1 = N
Tactic:
linarith
Proof state after:
no goals
Theorem: exists_antitone_of_eventually
Proof state before:
case neg
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
n : ℕ
h : ¬n < N
⊢ v (n + 1) ≤ v n
Tactic:
have : ¬(n + 1 < N) := by linarith
Proof state after:
case neg
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
n : ℕ
h : ¬n < N
this : ¬n + 1 < N
⊢ v (n + 1) ≤ v n
Theorem: exists_antitone_of_eventually
Proof state before:
case neg
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
n : ℕ
h : ¬n < N
this : ¬n + 1 < N
⊢ v (n + 1) ≤ v n
Tactic:
simp [v, h, this]
Proof state after:
case neg
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
n : ℕ
h : ¬n < N
this : ¬n + 1 < N
⊢ u (n + 1) ≤ u n
Theorem: exists_antitone_of_eventually
Proof state before:
case neg
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
n : ℕ
h : ¬n < N
this : ¬n + 1 < N
⊢ u (n + 1) ≤ u n
Tactic:
apply hN
Proof state after:
case neg.a
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
n : ℕ
h : ¬n < N
this : ¬n + 1 < N
⊢ n ≥ N
Theorem: exists_antitone_of_eventually
Proof state before:
case neg.a
n✝ : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
n : ℕ
h : ¬n < N
this : ¬n + 1 < N
⊢ n ≥ N
Tactic:
linarith
Proof state after:
no goals
Theorem: exists_antitone_of_eventually
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, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
n : ℕ
h : ¬n < N
⊢ ¬n + 1 < N
Tactic:
linarith
Proof state after:
no goals
Theorem: exists_antitone_of_eventually
Proof state before:
case intro.refine_3
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
⊢ v =ᶠ[atTop] u
Tactic:
have : ∀ᶠ n in atTop, ¬(n < N) := by simpa using ⟨N, fun b hb => by linarith⟩
Proof state after:
case intro.refine_3
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
this : ∀ᶠ (n : ℕ) in atTop, ¬n < N
⊢ v =ᶠ[atTop] u
Theorem: exists_antitone_of_eventually
Proof state before:
case intro.refine_3
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
this : ∀ᶠ (n : ℕ) in atTop, ¬n < N
⊢ v =ᶠ[atTop] u
Tactic:
filter_upwards [this] with 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 : ℕ → ℝ
hu : ∀ᶠ (n : ℕ) in atTop, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
this : ∀ᶠ (n : ℕ) in atTop, ¬n < N
n : ℕ
hn : ¬n < N
⊢ v n = u n
Theorem: exists_antitone_of_eventually
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, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
this : ∀ᶠ (n : ℕ) in atTop, ¬n < N
n : ℕ
hn : ¬n < N
⊢ v n = u n
Tactic:
simp [v, hn]
Proof state after:
no goals
Theorem: exists_antitone_of_eventually
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, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
⊢ ∀ᶠ (n : ℕ) in atTop, ¬n < N
Tactic:
simpa using ⟨N, fun b hb => by linarith⟩
Proof state after:
no goals
Theorem: exists_antitone_of_eventually
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, u (n + 1) ≤ u n
N : ℕ
hN : ∀ b ≥ N, u (b + 1) ≤ u b
v : ℕ → ℝ := fun n => u (if n < N then N else n)
b : ℕ
hb : N ≤ b
⊢ N ≤ b
Tactic:
linarith
Proof state after:
no goals
Theorem: summable_inv_mul_log_sq
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ Summable fun n => (↑n * (↑n).log ^ 2)⁻¹
Tactic:
let u (n : ℕ) := (n * (Real.log n) ^ 2)⁻¹
Proof state after:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ := fun n => (↑n * (↑n).log ^ 2)⁻¹
⊢ Summable fun n => (↑n * (↑n).log ^ 2)⁻¹
Theorem: summable_inv_mul_log_sq
Proof state before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ := fun n => (↑n * (↑n).log ^ 2)⁻¹
⊢ Summable fun n => (↑n * (↑n).log ^ 2)⁻¹
Tactic:
have l7 : ∀ᶠ n : ℕ in atTop, 1 ≤ Real.log n := tendsto_atTop.mp (tendsto_log_atTop.comp tendsto_natCast_atTop_atTop) 1
Proof state after:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ := fun n => (↑n * (↑n).log ^ 2)⁻¹
l7 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ (↑n).log
⊢ Summable fun n => (↑n * (↑n).log ^ 2)⁻¹
Theorem: summable_inv_mul_log_sq
Proof state before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ := fun n => (↑n * (↑n).log ^ 2)⁻¹
l7 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ (↑n).log
⊢ Summable fun n => (↑n * (↑n).log ^ 2)⁻¹
Tactic:
have l8 : ∀ᶠ n : ℕ in atTop, 1 ≤ n := eventually_ge_atTop 1
Proof state after:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
u : ℕ → ℝ := fun n => (↑n * (↑n).log ^ 2)⁻¹
l7 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ (↑n).log
l8 : ∀ᶠ (n : ℕ) in atTop, 1 ≤ n
⊢ Summable fun n => (↑n * (↑n).log ^ 2)⁻¹