def book_clusterPoint_atTop (S : Set ℝ) : Prop

Definition 3.5.1. ∞ is a cluster point of S ⊆ ℝ if for every real M there exists x ∈ S with x ≥ M; similarly -∞ is a cluster point if for every M there is x ∈ S with x ≤ M. For a function f : S → ℝ with ∞ (resp. -∞) a cluster point of S, the limit lim_{x → ∞} f = L (resp. lim_{x → -∞} f = L) means that for every ε > 0 there exists M ∈ ℝ such that for all x ∈ S with x ≥ M (resp. x ≤ M) one has |f x - L| < ε.

Equations

• book_clusterPoint_atTop S = ∀ (M : ℝ), ∃ x ∈ S, M ≤ x

def book_clusterPoint_atBot (S : Set ℝ) : Prop

Definition 3.5.1. -∞ is a cluster point of S ⊆ ℝ if every real bound is exceeded below by some x ∈ S.

Equations

• book_clusterPoint_atBot S = ∀ (M : ℝ), ∃ x ∈ S, x ≤ M

theorem book_clusterPoint_atTop_iff_not_bddAbove {S : Set ℝ} : book_clusterPoint_atTop S ↔ ¬BddAbove S

The book notion that ∞ is a cluster point of a subset of ℝ is equivalent to the set being unbounded above.

theorem book_clusterPoint_atBot_iff_not_bddBelow {S : Set ℝ} : book_clusterPoint_atBot S ↔ ¬BddBelow S

The book notion that -∞ is a cluster point of a subset of ℝ is equivalent to the set being unbounded below.

def book_tendsto_atTop (S : Set ℝ) (f : ↑S → ℝ) (L : ℝ) : Prop

Definition 3.5.1. A function f : S → ℝ converges to L as x → ∞ if for every ε > 0 there exists M ∈ ℝ such that whenever x ∈ S satisfies x ≥ M, then |f x - L| < ε.

Equations

• book_tendsto_atTop S f L = ∀ ε > 0, ∃ (M : ℝ), ∀ (x : ↑S), M ≤ ↑x → |f x - L| < ε

def book_tendsto_atBot (S : Set ℝ) (f : ↑S → ℝ) (L : ℝ) : Prop

Definition 3.5.1. A function f : S → ℝ converges to L as x → -∞ if for every ε > 0 there exists M ∈ ℝ such that whenever x ∈ S satisfies x ≤ M, then |f x - L| < ε.

Equations

• book_tendsto_atBot S f L = ∀ ε > 0, ∃ (M : ℝ), ∀ (x : ↑S), ↑x ≤ M → |f x - L| < ε

theorem book_tendsto_atTop_iff_tendsto {S : Set ℝ} {f : ↑S → ℝ} {L : ℝ} (hS : book_clusterPoint_atTop S) : book_tendsto_atTop S f L ↔ Filter.Tendsto f Filter.atTop (nhds L)

Assuming ∞ is a cluster point of S, the book limit at ∞ coincides with the standard Tendsto formulation along Filter.atTop for functions on the subtype domain.

theorem book_tendsto_atBot_iff_tendsto {S : Set ℝ} {f : ↑S → ℝ} {L : ℝ} (hS : book_clusterPoint_atBot S) : book_tendsto_atBot S f L ↔ Filter.Tendsto f Filter.atBot (nhds L)

The book limit at -∞ coincides with the standard Tendsto formulation along Filter.atBot for functions on the subtype domain.

theorem limit_atTop_unique {S : Set ℝ} {f : ↑S → ℝ} {L₁ L₂ : ℝ} (hS : book_clusterPoint_atTop S) (h₁ : book_tendsto_atTop S f L₁) (h₂ : book_tendsto_atTop S f L₂) : L₁ = L₂

Proposition 3.5.2. If a function has a limit at ∞ (resp. -∞) in the sense above, that limit value is unique.

theorem limit_atBot_unique {S : Set ℝ} {f : ↑S → ℝ} {L₁ L₂ : ℝ} (hS : book_clusterPoint_atBot S) (h₁ : book_tendsto_atBot S f L₁) (h₂ : book_tendsto_atBot S f L₂) : L₁ = L₂

Proposition 3.5.2. If a function has a limit at -∞ in the sense above, that limit value is unique.

theorem example_3_5_3 : Filter.Tendsto (fun (x : ℝ) => 1 / (|x| + 1)) Filter.atTop (nhds 0) ∧ Filter.Tendsto (fun (x : ℝ) => 1 / (|x| + 1)) Filter.atBot (nhds 0)

Example 3.5.3. The function f x = 1 / (|x| + 1) satisfies lim_{x → ∞} f x = 0 and lim_{x → -∞} f x = 0.

theorem tendsto_linear_shift_atTop (c : ℝ) : Filter.Tendsto (fun (n : ℕ) => 2 * ↑n + c) Filter.atTop Filter.atTop

The affine sequence n ↦ 2n + c diverges to ∞.

theorem sin_pi_two_n_add_half (n : ℕ) : Real.sin (Real.pi * (2 * ↑n + 1 / 2)) = 1

Exact value of sin (π (2n + 1/2)).

theorem sin_pi_two_n_add_three_halves (n : ℕ) : Real.sin (Real.pi * (2 * ↑n + 3 / 2)) = -1

Exact value of sin (π (2n + 3/2)).

theorem example_3_5_4_limit_does_not_exist : ¬∃ (L : ℝ), Filter.Tendsto (fun (x : ℝ) => Real.sin (Real.pi * x)) Filter.atTop (nhds L)

Example 3.5.4. For f x = sin (π x), the limit lim_{x → ∞} f x does not exist, while the sequence limit lim_{n → ∞} sin (π n) equals 0; this illustrates the distinction between limits of continuous variables and limits of sequences.

theorem example_3_5_4_sequence_limit : Filter.Tendsto (fun (n : ℕ) => Real.sin (Real.pi * ↑n)) Filter.atTop (nhds 0)

Example 3.5.4. The sequence sin (π n) converges to 0 as n → ∞.

theorem lemma_3_5_5 {S : Set ℝ} {f : ↑S → ℝ} {L : ℝ} (_hS : book_clusterPoint_atTop S) : book_tendsto_atTop S f L ↔ ∀ (x : ℕ → ↑S), Filter.Tendsto (fun (n : ℕ) => ↑(x n)) Filter.atTop Filter.atTop → Filter.Tendsto (fun (n : ℕ) => f (x n)) Filter.atTop (nhds L)

Lemma 3.5.5. If f : S → ℝ, ∞ is a cluster point of S ⊆ ℝ, and L ∈ ℝ, then lim_{x → ∞} f x = L if and only if for every sequence xₙ ∈ S with xₙ → ∞ one has lim_{n → ∞} f (xₙ) = L.

def book_tendsto_atTop_top (S : Set ℝ) (f : ↑S → ℝ) : Prop

Definition 3.5.6. If S ⊆ ℝ has ∞ as a cluster point, a function f : S → ℝ is said to diverge to ∞ as x → ∞ provided that for every real bound N there is some M such that whenever x ∈ S with x ≥ M, we have f x > N; this is written as lim_{x → ∞} f x = ∞.

Equations

• book_tendsto_atTop_top S f = ∀ (N : ℝ), ∃ (M : ℝ), ∀ (x : ↑S), M ≤ ↑x → N < f x

theorem book_tendsto_atTop_top_iff_tendsto {S : Set ℝ} {f : ↑S → ℝ} (hS : book_clusterPoint_atTop S) : book_tendsto_atTop_top S f ↔ Filter.Tendsto f Filter.atTop Filter.atTop

The book notion that a function diverges to ∞ agrees with the standard Tendsto formulation to the filter atTop on ℝ.

theorem example_3_5_7_lower_bound {x : ℝ} (hx : 1 ≤ x) : (1 + x ^ 2) / (1 + x) ≥ x / 2

Helper for Example 3.5.7: for x ≥ 1, (1 + x^2) / (1 + x) dominates x / 2.

theorem example_3_5_7_half_eventually (N : ℝ) : ∀ᶠ (x : ℝ) in Filter.atTop, N < x / 2

Helper for Example 3.5.7: x / 2 diverges to ∞.

theorem example_3_5_7 : Filter.Tendsto (fun (x : ℝ) => (1 + x ^ 2) / (1 + x)) Filter.atTop Filter.atTop

Example 3.5.7. The limit of (1 + x^2) / (1 + x) as x → ∞ diverges to ∞.

theorem proposition_3_5_8 {A B : Set ℝ} {f : ℝ → ℝ} {g : ℝ → EReal} {a b : ℝ} {c : EReal} (_ha : ClusterPt a (Filter.principal A)) (_hb : ClusterPt b (Filter.principal B)) (hf_map : Set.MapsTo f A B) (hf : Filter.Tendsto f (nhdsWithin a A) (nhds b)) (hg : Filter.Tendsto g (nhdsWithin b B) (nhds c)) (_hbmem : b ∈ B → g b = c) : Filter.Tendsto (fun (x : ℝ) => g (f x)) (nhdsWithin a A) (nhds c)

Proposition 3.5.8. Let f : A → B and g : B → ℝ with A, B ⊆ ℝ, where a is a cluster point of A and b is a cluster point of B. Assume lim_{x → a} f x = b and lim_{y → b} g y = c for some c ∈ ℝ ∪ {±∞}; if moreover b ∈ B, suppose g b = c. Then lim_{x → a} g (f x) = c.

theorem neg_quad_eventually_le (M : ℝ) : ∀ᶠ (x : ℝ) in Filter.atTop, -x ^ 2 + x ≤ M

For any real bound M, the quadratic expression -x^2 + x is eventually below M along Filter.atTop.

theorem tendsto_neg_quad_atTop_atBot : Filter.Tendsto (fun (x : ℝ) => -x ^ 2 + x) Filter.atTop Filter.atBot

The quadratic polynomial -x^2 + x tends to -∞ along Filter.atTop.

theorem example_3_5_9 : Filter.Tendsto (fun (x : ℝ) => Real.exp (-x ^ 2 + x)) Filter.atTop (nhds 0)

Example 3.5.9. For h x = e ^ (-x^2 + x), we have lim_{x → ∞} h x = 0, using that -x^2 + x → -∞ and e^y → 0 as y → -∞.