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

Equations

• RealAnalysis.monoLe a = ∀ (i j : ℕ), i ≤ j → a i ≤ a j

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

Equations

• RealAnalysis.monoLt a = ∀ (i j : ℕ), i < j → a i < a j

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

Equations

• RealAnalysis.monoGe a = ∀ (i j : ℕ), i ≤ j → a j ≤ a i

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

Equations

• RealAnalysis.monoGt a = ∀ (i j : ℕ), i < j → a j < a i

theorem RealAnalysis.monoLe_iff_le_succ {a : ℕ → ℝ} : monoLe a ↔ ∀ (n : ℕ), a n ≤ a (n + 1)

theorem RealAnalysis.monoLt_iff_lt_succ {a : ℕ → ℝ} : monoLt a ↔ ∀ (n : ℕ), a n < a (n + 1)

theorem RealAnalysis.monoGe_iff_succ_le {a : ℕ → ℝ} : monoGe a ↔ ∀ (n : ℕ), a (n + 1) ≤ a n

theorem RealAnalysis.monoGt_iff_succ_lt {a : ℕ → ℝ} : monoGt a ↔ ∀ (n : ℕ), a (n + 1) < a n

theorem RealAnalysis.iterate_gap' {a : ℕ → ℝ} {t σ : ℕ → ℕ} {ε : ℝ} {i k : ℕ} (ha : monoLe a) (ht : ∀ (n : ℕ), n ≤ t n) (h : ∀ (n : ℕ), ε ≤ a (σ n) - a (t n)) : ↑k * ε ≤ a (σ^[k] i) - a i

theorem RealAnalysis.iterate_gap {a : ℕ → ℝ} {t σ : ℕ → ℕ} {ε : ℝ} {i k : ℕ} (ha : monoLe a) (ht : ∀ (n : ℕ), n ≤ t n) (hσ : ∀ (n : ℕ), t n ≤ σ n) (h : ∀ (n : ℕ), ε ≤ |a (σ n) - a (t n)|) : ↑k * ε ≤ a (σ^[k] i) - a i

theorem RealAnalysis.misc₁ {a : ℕ → ℝ} {t σ : ℕ → ℕ} {ε : ℝ} {k : ℕ} (hε : 0 < ε) (hσ : ∀ (n : ℕ), t n ≤ σ n) (h : ∀ (n : ℕ), ε ≤ |a (σ n) - a (t n)|) : t k < σ k

theorem RealAnalysis.monoLe_of_monoLt {a : ℕ → ℝ} (h : monoLt a) : monoLe a

theorem RealAnalysis.monoGe_of_monoGt {a : ℕ → ℝ} (h : monoGt a) : monoGe a

@[simp]

theorem RealAnalysis.monoLe_neg {a : ℕ → ℝ} : monoLe (-a) ↔ monoGe a

@[simp]

theorem RealAnalysis.monoLt_neg {a : ℕ → ℝ} : monoLt (-a) ↔ monoGt a

@[simp]

theorem RealAnalysis.monoGe_neg {a : ℕ → ℝ} : monoGe (-a) ↔ monoLe a

@[simp]

theorem RealAnalysis.monoGt_neg {a : ℕ → ℝ} : monoGt (-a) ↔ monoLt a

theorem RealAnalysis.misc₂ : ¬∀ {a : ℕ → ℝ} {t σ : ℕ → ℕ} {ε : ℝ}, monoLe a → (∀ (n : ℕ), n ≤ t n) → (∀ (n : ℕ), t n ≤ σ n) → (∀ (n : ℕ), ε ≤ |a (σ n) - a (t n)|) → Subseq t ∨ Subseq σ

theorem RealAnalysis.subseq_iff_lt_add_one {σ : ℕ → ℕ} : Subseq σ ↔ ∀ (n : ℕ), σ n < σ (n + 1)

theorem RealAnalysis.subseq_iterate_of_id_lt {σ : ℕ → ℕ} (h : ∀ (n : ℕ), n < σ n) {n : ℕ} : Subseq fun (x : ℕ) => σ^[x] n

theorem RealAnalysis.exi_Subseq_of_forall_exi_gt {p : ℕ → Prop} (h : ∀ (N : ℕ), ∃ (n : ℕ), N < n ∧ p n) : ∃ (σ : ℕ → ℕ), Subseq σ ∧ ∀ (n : ℕ), p (σ n)

theorem RealAnalysis.exi_Subseq_of_forall_exi_le {p : ℕ → Prop} (h : ∀ (N : ℕ), ∃ (n : ℕ), N ≤ n ∧ p n) : ∃ (σ : ℕ → ℕ), Subseq σ ∧ ∀ (n : ℕ), p (σ n)

theorem RealAnalysis.subseq_comp {σ₁ σ₂ : ℕ → ℕ} (h₁ : Subseq σ₁) (h₂ : Subseq σ₂) : Subseq (σ₁ ∘ σ₂)

theorem RealAnalysis.forall_exi_le_or_forall_exi_ge {a : ℕ → ℝ} {L : ℝ} : (∀ (N : ℕ), ∃ (n : ℕ), N ≤ n ∧ a n ≤ L) ∨ ∀ (N : ℕ), ∃ (n : ℕ), N ≤ n ∧ L ≤ a n

@[simp]

theorem RealAnalysis.monoLe_const {M : ℝ} : monoLe fun (x : ℕ) => M

@[simp]

theorem RealAnalysis.monoGe_const {M : ℝ} : monoGe fun (x : ℕ) => M

@[simp]

theorem RealAnalysis.not_monoLt_const {M : ℝ} : ¬monoLt fun (x : ℕ) => M

@[simp]

theorem RealAnalysis.not_monoGt_const {M : ℝ} : ¬monoGt fun (x : ℕ) => M

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

Equations

• RealAnalysis.DivergesToInf a = ∀ (M : ℝ), 0 < M → eventually fun (n : ℕ) => M < a n

theorem RealAnalysis.divergesToInf_mul_left {a b : ℕ → ℝ} {L : ℝ} (ha : DivergesToInf a) (hb : tendsTo b L) (hL : 0 < L) : DivergesToInf (a * b)