def RealAnalysis.tendsTo (a : ℕ → ℝ) (L : ℝ) : Prop

Equations

• RealAnalysis.tendsTo a L = ∀ (ε : ℝ), 0 < ε → eventually fun (x : ℕ) => |a x - L| < ε

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

Equations

• RealAnalysis.converges a = ∃ (L : ℝ), RealAnalysis.tendsTo a L

noncomputable def RealAnalysis.limit (a : ℕ → ℝ) : ℝ

Equations

• RealAnalysis.limit a = Classical.epsilon fun (L : ℝ) => RealAnalysis.tendsTo a L

noncomputable def RealAnalysis.someLt (x : ℝ) : ℝ

Equations

• RealAnalysis.someLt x = Classical.epsilon fun (y : ℝ) => y < x

noncomputable def RealAnalysis.someGt (x : ℝ) : ℝ

Equations

• RealAnalysis.someGt x = Classical.epsilon fun (y : ℝ) => x < y

noncomputable def RealAnalysis.glb (a : ℕ → ℝ) : ℝ

Equations

• RealAnalysis.glb a = ⨅ (i : ℕ), a i

noncomputable def RealAnalysis.lub (a : ℕ → ℝ) : ℝ

Equations

• RealAnalysis.lub a = ⨆ (i : ℕ), a i

noncomputable def RealAnalysis.lb (a : ℕ → ℝ) : ℝ

Equations

• RealAnalysis.lb a = RealAnalysis.someLt (RealAnalysis.glb a)

noncomputable def RealAnalysis.ub (a : ℕ → ℝ) : ℝ

Equations

• RealAnalysis.ub a = RealAnalysis.someGt (RealAnalysis.lub a)

theorem RealAnalysis.tendsTo_unique {a : ℕ → ℝ} {L₁ L₂ : ℝ} (h₁ : tendsTo a L₁) (h₂ : tendsTo a L₂) : L₁ = L₂

theorem RealAnalysis.tendsTo_const {L : ℝ} : tendsTo (fun (x : ℕ) => L) L

@[simp]

theorem RealAnalysis.tendsTo_const_iff {L M : ℝ} : tendsTo (fun (x : ℕ) => L) M ↔ L = M

@[simp]

theorem RealAnalysis.tendsTo_const_nat_iff {n : ℕ} {L : ℝ} : tendsTo (OfNat.ofNat n) L ↔ OfNat.ofNat n = L

theorem RealAnalysis.tendsTo_drop_iff' {a : ℕ → ℝ} {L : ℝ} {k : ℕ} : tendsTo (fun (x : ℕ) => a (x + k)) L ↔ tendsTo a L

theorem RealAnalysis.converges_drop_iff {a : ℕ → ℝ} {k : ℕ} : (converges fun (x : ℕ) => a (x + k)) ↔ converges a

theorem RealAnalysis.tendsTo_one_div : tendsTo (fun (x : ℕ) => 1 / ↑x) 0

theorem RealAnalysis.tendsTo_one_div_succ : tendsTo (fun (n : ℕ) => 1 / (↑n + 1)) 0

theorem RealAnalysis.not_converges_alternating {x y : ℝ} (h : x ≠ y) : ¬converges fun (x_1 : ℕ) => if Even x_1 then x else y

theorem RealAnalysis.not_converges_minus_one_pow : ¬converges fun (x : ℕ) => (-1) ^ x

theorem RealAnalysis.ofNat_seq_eq {n : ℕ} : OfNat.ofNat n = fun (x : ℕ) => ↑n

theorem RealAnalysis.cast_seq_eq {n : ℕ} : ↑n = fun (x : ℕ) => ↑n

theorem RealAnalysis.tendsTo_neg {a : ℕ → ℝ} {L : ℝ} (h : tendsTo a L) : tendsTo (-a) (-L)

theorem RealAnalysis.tendsTo_add {a₁ a₂ : ℕ → ℝ} {L₁ L₂ : ℝ} (h₁ : tendsTo a₁ L₁) (h₂ : tendsTo a₂ L₂) : tendsTo (a₁ + a₂) (L₁ + L₂)

theorem RealAnalysis.tendsTo_sub {a₁ a₂ : ℕ → ℝ} {L₁ L₂ : ℝ} (h₁ : tendsTo a₁ L₁) (h₂ : tendsTo a₂ L₂) : tendsTo (a₁ - a₂) (L₁ - L₂)

theorem RealAnalysis.tendsTo_iff_eps_lt_one {a : ℕ → ℝ} {L : ℝ} : tendsTo a L ↔ ∀ (ε : ℝ), 0 < ε → ε < 1 → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → |a n - L| < ε

theorem RealAnalysis.eventually_ne_of_ne_limit {a : ℕ → ℝ} {L M : ℝ} (h₁ : tendsTo a L) (h₂ : M ≠ L) : eventually fun (x : ℕ) => a x ≠ M

theorem RealAnalysis.drop_ne_of_ne_limit {a : ℕ → ℝ} {L M : ℝ} (h₁ : tendsTo a L) (h₂ : M ≠ L) : ∃ (k : ℕ), tendsTo (fun (x : ℕ) => a (x + k)) L ∧ ∀ (n : ℕ), a (n + k) ≠ M

theorem RealAnalysis.tendsTo_inv_aux₁ {x y : ℝ} (h : |x - y| < |y| / 2) : |y| / 2 < |x|

theorem RealAnalysis.tendsTo_inv_aux₂ {a : ℕ → ℝ} {L : ℝ} (h₁ : ∀ (n : ℕ), a n ≠ 0) (h₂ : L ≠ 0) (h₃ : tendsTo a L) : ∃ (x : ℝ), 0 < x ∧ ∀ (n : ℕ), x ≤ |a n|

theorem RealAnalysis.tendsTo_inv_aux₃ {a : ℕ → ℝ} {L : ℝ} (h₁ : ∀ (n : ℕ), a n ≠ 0) (h₂ : L ≠ 0) (h₃ : tendsTo a L) : tendsTo a⁻¹ L⁻¹

theorem RealAnalysis.tendsTo_inv {a : ℕ → ℝ} {L : ℝ} (h₁ : L ≠ 0) (h₂ : tendsTo a L) : tendsTo a⁻¹ L⁻¹

@[simp]

theorem RealAnalysis.someLt_lt {x : ℝ} : someLt x < x

@[simp]

theorem RealAnalysis.lt_someGt {x : ℝ} : x < someGt x

theorem RealAnalysis.converges_of_tendsTo {a : ℕ → ℝ} {L : ℝ} (h : tendsTo a L) : converges a

theorem RealAnalysis.bddBelow_of_converges {a : ℕ → ℝ} (h : converges a) : BddBelow (Set.range a)

@[simp]

theorem RealAnalysis.converges_neg {a : ℕ → ℝ} : converges (-a) ↔ converges a

theorem RealAnalysis.bddAbove_of_converges {a : ℕ → ℝ} (h : converges a) : BddAbove (Set.range a)

theorem RealAnalysis.glb_le_of_tendsTo {a : ℕ → ℝ} {L : ℝ} (h : tendsTo a L) : (∀ (i : ℕ), glb a ≤ a i) ∧ glb a ≤ L

theorem RealAnalysis.le_lub_of_tendsTo {a : ℕ → ℝ} {L : ℝ} (h : tendsTo a L) : (∀ (i : ℕ), a i ≤ lub a) ∧ L ≤ lub a

theorem RealAnalysis.le_glb_of_le {a : ℕ → ℝ} {m : ℝ} (h : ∀ (i : ℕ), m ≤ a i) : m ≤ glb a

theorem RealAnalysis.lub_le_of_le {a : ℕ → ℝ} {m : ℝ} (h : ∀ (i : ℕ), a i ≤ m) : lub a ≤ m

theorem RealAnalysis.glb_neg {a : ℕ → ℝ} (h : converges a) : glb (-a) = -lub a

theorem RealAnalysis.lub_neg {a : ℕ → ℝ} (h : converges a) : lub (-a) = -glb a

@[simp]

theorem RealAnalysis.lb_lt_glb {a : ℕ → ℝ} : lb a < glb a

@[simp]

theorem RealAnalysis.lub_lt_ub {a : ℕ → ℝ} : lub a < ub a

theorem RealAnalysis.lb_lt_of_tendsTo {a : ℕ → ℝ} {L : ℝ} (h : tendsTo a L) : (∀ (i : ℕ), lb a < a i) ∧ lb a < L

theorem RealAnalysis.lt_ub_of_tendsTo {a : ℕ → ℝ} {L : ℝ} (h : tendsTo a L) : (∀ (i : ℕ), a i < ub a) ∧ L < ub a

theorem RealAnalysis.tendsTo_mul_aux₁ {a₁ a₂ : ℕ → ℝ} {L₁ L₂ : ℝ} (h₁ : tendsTo a₁ L₁) (h₂ : tendsTo a₂ L₂) (h₄' : ∀ (i : ℕ), 1 < a₂ i) (h₅' : 1 < L₁) (h₆' : 1 < L₂) : tendsTo (a₁ * a₂) (L₁ * L₂)

theorem RealAnalysis.tendsTo_mul {a₁ a₂ : ℕ → ℝ} {L₁ L₂ : ℝ} (h₁ : tendsTo a₁ L₁) (h₂ : tendsTo a₂ L₂) : tendsTo (a₁ * a₂) (L₁ * L₂)

theorem RealAnalysis.tendsTo_div {a₁ a₂ : ℕ → ℝ} {L₁ L₂ : ℝ} (h₁ : L₂ ≠ 0) (h₂ : tendsTo a₁ L₁) (h₃ : tendsTo a₂ L₂) : tendsTo (a₁ / a₂) (L₁ / L₂)

theorem RealAnalysis.squeeze {a b c : ℕ → ℝ} {L : ℝ} (h₁ : ∀ (n : ℕ), a n ≤ b n) (h₂ : ∀ (n : ℕ), b n ≤ c n) (h₃ : tendsTo a L) (h₄ : tendsTo c L) : tendsTo b L

theorem RealAnalysis.eventually_pos_of_limit_pos {a : ℕ → ℝ} {L : ℝ} (h₁ : 0 < L) (h₂ : tendsTo a L) : eventually fun (x : ℕ) => 0 < a x

theorem RealAnalysis.eventually_neg_of_limit_neg {a : ℕ → ℝ} {L : ℝ} (h₁ : L < 0) (h₂ : tendsTo a L) : eventually fun (x : ℕ) => a x < 0

theorem RealAnalysis.eventually_abs_limit_div_two_lt_aux₁ {a : ℕ → ℝ} {L : ℝ} (h₁ : 0 < L) (h₂ : ∀ (n : ℕ), 0 < a n) (h₃ : tendsTo a L) : eventually fun (x : ℕ) => |L| / 2 < |a x|

theorem RealAnalysis.eventually_abs_limit_div_two_lt_aux₂ {a : ℕ → ℝ} {L : ℝ} (h₁ : 0 < L) (h₂ : tendsTo a L) : eventually fun (x : ℕ) => |L| / 2 < |a x|

theorem RealAnalysis.eventually_abs_limit_div_two_lt {a : ℕ → ℝ} {L : ℝ} (h₁ : L ≠ 0) (h₂ : tendsTo a L) : eventually fun (x : ℕ) => |L| / 2 < |a x|

theorem RealAnalysis.eventually_abs_limit_div_two_le {a : ℕ → ℝ} {L : ℝ} (h : tendsTo a L) : eventually fun (x : ℕ) => |L| / 2 ≤ |a x|

theorem RealAnalysis.tendsTo_abs {a : ℕ → ℝ} {L : ℝ} (h : tendsTo a L) : tendsTo (fun (x : ℕ) => |a x|) |L|

theorem RealAnalysis.lt_ub_of_converges {a : ℕ → ℝ} {n : ℕ} (h : converges a) : a n < ub a

theorem RealAnalysis.lb_lt_of_converges {a : ℕ → ℝ} {n : ℕ} (h : converges a) : lb a < a n

def RealAnalysis.boundedBy (a : ℕ → ℝ) (m : ℝ) : Prop

Equations

• RealAnalysis.boundedBy a m = ∀ (n : ℕ), |a n| ≤ m

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

Equations

• RealAnalysis.bounded a = ∃ (m : ℝ), RealAnalysis.boundedBy a m

def RealAnalysis.bounded' (a : ℕ → ℝ) : Prop

Equations

• RealAnalysis.bounded' a = ∃ (m : ℝ), 0 < m ∧ RealAnalysis.boundedBy a m

theorem RealAnalysis.bounded'_iff_bounded {a : ℕ → ℝ} : bounded' a ↔ bounded a

theorem RealAnalysis.bounded_of_converges {a : ℕ → ℝ} (h : converges a) : bounded a

theorem RealAnalysis.not_converges_of_not_bounded {a : ℕ → ℝ} (h : ¬bounded a) : ¬converges a

theorem RealAnalysis.not_bounded_id : ¬bounded fun (x : ℕ) => ↑x

theorem RealAnalysis.boundedBy_zero_iff_const_zero {a : ℕ → ℝ} : boundedBy a 0 ↔ a = 0

theorem RealAnalysis.limit_eq_of_tendsTo {a : ℕ → ℝ} {L : ℝ} (h : tendsTo a L) : limit a = L

theorem RealAnalysis.tendsTo_limit_of_tendsTo {a : ℕ → ℝ} {L : ℝ} (h : tendsTo a L) : tendsTo a (limit a)

theorem RealAnalysis.tendsTo_limit_of_converges {a : ℕ → ℝ} (h : converges a) : tendsTo a (limit a)

theorem RealAnalysis.converges_add {a b : ℕ → ℝ} (ha : converges a) (hb : converges b) : converges (a + b)

theorem RealAnalysis.converges_sub {a b : ℕ → ℝ} (ha : converges a) (hb : converges b) : converges (a - b)

theorem RealAnalysis.converges_mul {a b : ℕ → ℝ} (ha : converges a) (hb : converges b) : converges (a * b)

theorem RealAnalysis.converges_div {a b : ℕ → ℝ} (ha : converges a) (hb : converges b) (h : limit b ≠ 0) : converges (a / b)

theorem RealAnalysis.converges_inv {a : ℕ → ℝ} (ha : converges a) (h : limit a ≠ 0) : converges a⁻¹

theorem RealAnalysis.tendsTo_pow {a : ℕ → ℝ} {L : ℝ} {k : ℕ} (h : tendsTo a L) : tendsTo (a ^ k) (L ^ k)

theorem RealAnalysis.converges_pow {a : ℕ → ℝ} {k : ℕ} (ha : converges a) : converges (a ^ k)

theorem RealAnalysis.seq_ofNat_eq {n : ℕ} : OfNat.ofNat n = ↑n

theorem RealAnalysis.limit_le_of_forall_le {a : ℕ → ℝ} {L K : ℝ} (h₁ : tendsTo a L) (h₂ : ∀ (n : ℕ), a n ≤ K) : L ≤ K

theorem RealAnalysis.le_limit_of_forall_le {a : ℕ → ℝ} {L K : ℝ} (h₁ : tendsTo a L) (h₂ : ∀ (n : ℕ), K ≤ a n) : K ≤ L

def RealAnalysis.Subseq (σ : ℕ → ℕ) : Prop

Equations

• RealAnalysis.Subseq σ = ∀ (i j : ℕ), i < j → σ i < σ j

theorem RealAnalysis.nat_le_of_forall_lt_apply_succ {σ : ℕ → ℕ} {n : ℕ} (h : ∀ (n : ℕ), σ n < σ (n + 1)) : n ≤ σ n

theorem RealAnalysis.nat_le_of_subseq {σ : ℕ → ℕ} {n : ℕ} (h : Subseq σ) : n ≤ σ n

theorem RealAnalysis.tendsTo_subseq {a : ℕ → ℝ} {σ : ℕ → ℕ} {L : ℝ} (h₁ : tendsTo a L) (h₂ : Subseq σ) : tendsTo (a ∘ σ) L

theorem RealAnalysis.exi_subseq_tendsTo_of_neg_one_pow : ∃ (σ : ℕ → ℕ) (L : ℝ), Subseq σ ∧ tendsTo ((fun (x : ℕ) => (-1) ^ x) ∘ σ) L

theorem RealAnalysis.bounded_drop_iff {a : ℕ → ℝ} {k : ℕ} : (bounded fun (x : ℕ) => a (x + k)) ↔ bounded a

theorem RealAnalysis.le_lub_of_bounded_top {a : ℕ → ℝ} {n : ℕ} (ha : ∃ (m : ℝ), ∀ (n : ℕ), a n ≤ m) : a n ≤ lub a

theorem RealAnalysis.glb_le_of_bounded_bottom {a : ℕ → ℝ} {n : ℕ} (ha : ∃ (m : ℝ), ∀ (n : ℕ), m ≤ a n) : glb a ≤ a n

theorem RealAnalysis.exi_lub_sub_lt_of_bounded_top {a : ℕ → ℝ} {ε : ℝ} (ha : ∃ (m : ℝ), ∀ (n : ℕ), a n ≤ m) (he : 0 < ε) : ∃ (n : ℕ), lub a - a n < ε

theorem RealAnalysis.exi_sub_glb_lt_of_bounded_bottom {a : ℕ → ℝ} {ε : ℝ} (ha : ∃ (m : ℝ), ∀ (n : ℕ), m ≤ a n) (he : 0 < ε) : ∃ (n : ℕ), a n - glb a < ε

theorem RealAnalysis.tendsTo_drop_iff {a : ℕ → ℝ} {L : ℝ} {k : ℕ} : tendsTo (fun (x : ℕ) => a (k + x)) L ↔ tendsTo a L

theorem RealAnalysis.tendsTo_drop_of {a : ℕ → ℝ} {L : ℝ} {k : ℕ} (h : tendsTo a L) : tendsTo (fun (x : ℕ) => a (k + x)) L

@[simp]

theorem RealAnalysis.tendsTo_limit_iff_converges {a : ℕ → ℝ} : tendsTo a (limit a) ↔ converges a

@[simp]

theorem RealAnalysis.converges_const {x : ℝ} : converges fun (x_1 : ℕ) => x

@[simp]

theorem RealAnalysis.converges_const_nat {n : ℕ} : converges (OfNat.ofNat n)