def RealAnalysis.unBddCnd' (p : ℕ → Prop) : Prop

Equations

• RealAnalysis.unBddCnd' p = ∀ (N : ℕ), ∃ (n : ℕ), N ≤ n ∧ p n

def RealAnalysis.unBddCnd (p : ℝ → Prop) (a : ℕ → ℝ) : Prop

Equations

• RealAnalysis.unBddCnd p a = RealAnalysis.unBddCnd' fun (x : ℕ) => p (a x)

noncomputable def RealAnalysis.filter (p : ℝ → Prop) (a : ℕ → ℝ) (n : ℕ) : ℝ

Equations

• RealAnalysis.filter p a 0 = a (Nat.find! fun (x : ℕ) => p (a x))
• RealAnalysis.filter p a n_2.succ = RealAnalysis.filter p (fun (x : ℕ) => a ((Nat.find! fun (x : ℕ) => p (a x)) + 1 + x)) n_2

noncomputable def RealAnalysis.filterSubseq (p : ℝ → Prop) (a : ℕ → ℝ) (n : ℕ) : ℕ

Equations

• RealAnalysis.filterSubseq p a 0 = Nat.find! fun (x : ℕ) => p (a x)
• RealAnalysis.filterSubseq p a n_2.succ = (Nat.find! fun (x : ℕ) => p (a x)) + 1 + RealAnalysis.filterSubseq p (fun (x : ℕ) => a ((Nat.find! fun (x : ℕ) => p (a x)) + 1 + x)) n_2

noncomputable def RealAnalysis.monoLtSubseq (a : ℕ → ℝ) (n : ℕ) : ℕ

Equations

• RealAnalysis.monoLtSubseq a 0 = 0
• RealAnalysis.monoLtSubseq a n_2.succ = RealAnalysis.monoLtSubseq a n_2 + Nat.find! fun (k : ℕ) => a (RealAnalysis.monoLtSubseq a n_2) < a (RealAnalysis.monoLtSubseq a n_2 + k)

def RealAnalysis.isPeak (a : ℕ → ℝ) (k : ℕ) : Prop

Equations

• RealAnalysis.isPeak a k = ∀ (n : ℕ), k ≤ n → a n ≤ a k

def RealAnalysis.unBddPeaks (a : ℕ → ℝ) : Prop

Equations

• RealAnalysis.unBddPeaks a = RealAnalysis.unBddCnd' (RealAnalysis.isPeak a)

def RealAnalysis.convAndNotMono (a : ℕ → ℝ) : Prop

Equations

• RealAnalysis.convAndNotMono a = (RealAnalysis.converges a ∧ ¬RealAnalysis.monoLe a ∧ ¬RealAnalysis.monoGe a)

theorem RealAnalysis.unBddCnd'_iff_alt₁ {p : ℕ → Prop} : unBddCnd' p ↔ ∀ (N : ℕ), ∃ (n : ℕ), N < n ∧ p n

theorem RealAnalysis.unBddCnd_iff_alt₁ {a : ℕ → ℝ} {p : ℝ → Prop} : unBddCnd p a ↔ ∀ (N : ℕ), ∃ (n : ℕ), N < n ∧ p (a n)

theorem RealAnalysis.unBddCnd'_iff_alt₂ {p : ℕ → Prop} : unBddCnd' p ↔ {n : ℕ | p n}.Infinite

theorem RealAnalysis.unBddCnd_iff_alt₂ {a : ℕ → ℝ} {p : ℝ → Prop} : unBddCnd p a ↔ {n : ℕ | p (a n)}.Infinite

theorem RealAnalysis.unBddCnd_drop_of {a : ℕ → ℝ} {p : ℝ → Prop} {k : ℕ} (h : unBddCnd p a) : unBddCnd p fun (x : ℕ) => a (k + x)

theorem RealAnalysis.unBddCnd_drop_iff {a : ℕ → ℝ} {p : ℝ → Prop} {k : ℕ} : (unBddCnd p fun (x : ℕ) => a (k + x)) ↔ unBddCnd p a

theorem RealAnalysis.subseq_filterSubseq {a : ℕ → ℝ} {p : ℝ → Prop} (h : unBddCnd p a) : Subseq (filterSubseq p a)

theorem RealAnalysis.filter_eq_filterSubseq {a : ℕ → ℝ} {p : ℝ → Prop} (h : unBddCnd p a) : filter p a = a ∘ filterSubseq p a

theorem RealAnalysis.tendsTo_filter {a : ℕ → ℝ} {L : ℝ} {p : ℝ → Prop} (h₁ : tendsTo a L) (h₂ : unBddCnd p a) : tendsTo (filter p a) L

theorem RealAnalysis.unBddCnd_or_of_or {a : ℕ → ℝ} {p₁ p₂ : ℝ → Prop} (h : ∀ (n : ℕ), p₁ (a n) ∨ p₂ (a n)) : unBddCnd p₁ a ∨ unBddCnd p₂ a

theorem RealAnalysis.unBddCnd_le_or_ge {a : ℕ → ℝ} {M : ℝ} : unBddCnd (fun (x : ℝ) => x ≤ M) a ∨ unBddCnd (fun (x : ℝ) => M ≤ x) a

theorem RealAnalysis.apply_nat_find!_of_unBddCnd {a : ℕ → ℝ} {p : ℝ → Prop} (h : unBddCnd p a) : p (a (Nat.find! fun (x : ℕ) => p (a x)))

theorem RealAnalysis.apply_filterSubseq {a : ℕ → ℝ} {p : ℝ → Prop} {n : ℕ} (h : unBddCnd p a) : p (a (filterSubseq p a n))

theorem RealAnalysis.apply_filter {a : ℕ → ℝ} {p : ℝ → Prop} {n : ℕ} (h : unBddCnd p a) : p (filter p a n)

theorem RealAnalysis.unBddCnd_filter {a : ℕ → ℝ} {p : ℝ → Prop} (h : unBddCnd p a) : unBddCnd p (filter p a)

theorem RealAnalysis.exi_cnd_add_of_lt_limit {a : ℕ → ℝ} {L : ℝ} {n m : ℕ} (h₁ : tendsTo a L) (h₂ : ∀ (n : ℕ), a n < L) : ∃ (k : ℕ), a n < a (m + k)

theorem RealAnalysis.exi_cnd_of_lt_limit {a : ℕ → ℝ} {L : ℝ} {n : ℕ} (h₁ : tendsTo a L) (h₂ : ∀ (n : ℕ), a n < L) : ∃ (k : ℕ), a n < a k

theorem RealAnalysis.apply_natfind!_of_lt_limit {a : ℕ → ℝ} {L : ℝ} {n : ℕ} (h₁ : tendsTo a L) (h₂ : ∀ (n : ℕ), a n < L) : a n < a (Nat.find! fun (x : ℕ) => a n < a x)

theorem RealAnalysis.apply_natfind!_add_of_lt_limit {a : ℕ → ℝ} {L : ℝ} {n m : ℕ} (h₁ : tendsTo a L) (h₂ : ∀ (n : ℕ), a n < L) : a n < a (m + Nat.find! fun (k : ℕ) => a n < a (m + k))

theorem RealAnalysis.pos_natfind!_add_of_lt_limit {a : ℕ → ℝ} {L : ℝ} {n : ℕ} (h₁ : tendsTo a L) (h₂ : ∀ (n : ℕ), a n < L) : 0 < Nat.find! fun (k : ℕ) => a n < a (n + k)

theorem RealAnalysis.subseq_monoLtSubseq {a : ℕ → ℝ} {L : ℝ} (h₁ : tendsTo a L) (h₂ : ∀ (n : ℕ), a n < L) : Subseq (monoLtSubseq a)

theorem RealAnalysis.monoLt_monoLtSubseq {a : ℕ → ℝ} {L : ℝ} (h₁ : tendsTo a L) (h₂ : ∀ (n : ℕ), a n < L) : monoLt (a ∘ monoLtSubseq a)

theorem RealAnalysis.exi_monoLt_subseq_of_forall_lt_limit {a : ℕ → ℝ} {L : ℝ} (h₁ : tendsTo a L) (h₂ : ∀ (n : ℕ), a n < L) : ∃ (σ : ℕ → ℕ), Subseq σ ∧ monoLt (a ∘ σ)

theorem RealAnalysis.exi_monoLe_subseq_of_forall_le_limit {a : ℕ → ℝ} {L : ℝ} (h₁ : tendsTo a L) (h₂ : ∀ (n : ℕ), a n ≤ L) : ∃ (σ : ℕ → ℕ), Subseq σ ∧ monoLe (a ∘ σ)

theorem RealAnalysis.exi_monoLe_subseq_of_unBddCnd_le_limit {a : ℕ → ℝ} {L : ℝ} (h₁ : tendsTo a L) (h₂ : unBddCnd (fun (x : ℝ) => x ≤ L) a) : ∃ (σ : ℕ → ℕ), Subseq σ ∧ monoLe (a ∘ σ)

theorem RealAnalysis.exi_monoLt_subseq_of_unBddCnd_lt_limit {a : ℕ → ℝ} {L : ℝ} (h₁ : tendsTo a L) (h₂ : unBddCnd (fun (x : ℝ) => x < L) a) : ∃ (σ : ℕ → ℕ), Subseq σ ∧ monoLt (a ∘ σ)

theorem RealAnalysis.exi_monoGe_subseq_of_unBddCnd_limit_le {a : ℕ → ℝ} {L : ℝ} (h₁ : tendsTo a L) (h₂ : unBddCnd (fun (x : ℝ) => L ≤ x) a) : ∃ (σ : ℕ → ℕ), Subseq σ ∧ monoGe (a ∘ σ)

theorem RealAnalysis.exi_monoGt_subseq_of_unBddCnd_limit_lt {a : ℕ → ℝ} {L : ℝ} (h₁ : tendsTo a L) (h₂ : unBddCnd (fun (x : ℝ) => L < x) a) : ∃ (σ : ℕ → ℕ), Subseq σ ∧ monoGt (a ∘ σ)

theorem RealAnalysis.isPeak_iff_alt₁ {a : ℕ → ℝ} {k : ℕ} : isPeak a k ↔ ∀ (n : ℕ), k < n → a n ≤ a k

theorem RealAnalysis.exi_drop_eq_subseq {a : ℕ → ℝ} {k : ℕ} : ∃ (σ : ℕ → ℕ), Subseq σ ∧ (fun (x : ℕ) => a (k + x)) = a ∘ σ

theorem RealAnalysis.exi_monoLe_subseq_of_not_unBddPeaks {a : ℕ → ℝ} (h : ¬unBddPeaks a) : ∃ (σ : ℕ → ℕ), Subseq σ ∧ monoLe (a ∘ σ)

theorem RealAnalysis.exi_monoGe_subseq_of_unBddPeaks {a : ℕ → ℝ} (h : unBddPeaks a) : ∃ (σ : ℕ → ℕ), Subseq σ ∧ monoGe (a ∘ σ)

theorem RealAnalysis.exi_monoLe_or_monoGe_subseq {a : ℕ → ℝ} : ∃ (σ : ℕ → ℕ), Subseq σ ∧ (monoLe (a ∘ σ) ∨ monoGe (a ∘ σ))

theorem RealAnalysis.convAndNotMono_neg_one_pow_div_add_one : convAndNotMono fun (n : ℕ) => (-1) ^ n / (↑n + 1)

theorem RealAnalysis.convAndNotMono_ite_div : convAndNotMono fun (n : ℕ) => if n = 0 then 0 else 1 / ↑n

theorem RealAnalysis.tendsTo_zero_iff_of_int {a : ℕ → ℤ} : tendsTo (fun (x : ℕ) => ↑(a x)) 0 ↔ ∀ (ε : ℤ), 0 < ε → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → |a n| < ε