Analysis I, Section 9.5: Left and right limits

I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.

Main constructions and results of this section:

• Left and right limits.

@[reducible, inline]

abbrev Chapter9.RightLimitExists (X : Set ℝ) (f : ℝ → ℝ) (x₀ : ℝ) : Prop

Definition 9.5.1. We give left and right limits the "junk" value of 0 if the limit does not exist.

Equations

• Chapter9.RightLimitExists X f x₀ = ∃ (L : ℝ), Filter.Tendsto f (nhdsWithin x₀ (X ∩ Set.Ioi x₀)) (nhds L)

@[reducible, inline]

noncomputable abbrev Chapter9.right_limit (X : Set ℝ) (f : ℝ → ℝ) (x₀ : ℝ) : ℝ

Equations

• Chapter9.right_limit X f x₀ = if h : Chapter9.RightLimitExists X f x₀ then Exists.choose h else 0

@[reducible, inline]

abbrev Chapter9.LeftLimitExists (X : Set ℝ) (f : ℝ → ℝ) (x₀ : ℝ) : Prop

Equations

• Chapter9.LeftLimitExists X f x₀ = ∃ (L : ℝ), Filter.Tendsto f (nhdsWithin x₀ (X ∩ Set.Iio x₀)) (nhds L)

@[reducible, inline]

noncomputable abbrev Chapter9.left_limit (X : Set ℝ) (f : ℝ → ℝ) (x₀ : ℝ) : ℝ

Equations

• Chapter9.left_limit X f x₀ = if h : Chapter9.LeftLimitExists X f x₀ then Exists.choose h else 0

theorem Chapter9.right_limit.eq {X : Set ℝ} {f : ℝ → ℝ} {x₀ L : ℝ} (had : AdherentPt x₀ (X ∩ Set.Ioi x₀)) (h : Filter.Tendsto f (nhdsWithin x₀ (X ∩ Set.Ioi x₀)) (nhds L)) : RightLimitExists X f x₀ ∧ right_limit X f x₀ = L

theorem Chapter9.left_limit.eq {X : Set ℝ} {f : ℝ → ℝ} {x₀ L : ℝ} (had : AdherentPt x₀ (X ∩ Set.Iio x₀)) (h : Filter.Tendsto f (nhdsWithin x₀ (X ∩ Set.Iio x₀)) (nhds L)) : LeftLimitExists X f x₀ ∧ left_limit X f x₀ = L

theorem Chapter9.right_limit.eq' {X : Set ℝ} {f : ℝ → ℝ} {x₀ : ℝ} (h : RightLimitExists X f x₀) : Filter.Tendsto f (nhdsWithin x₀ (X ∩ Set.Ioi x₀)) (nhds (right_limit X f x₀))

theorem Chapter9.left_limit.eq' {X : Set ℝ} {f : ℝ → ℝ} {x₀ : ℝ} (h : LeftLimitExists X f x₀) : Filter.Tendsto f (nhdsWithin x₀ (X ∩ Set.Iio x₀)) (nhds (left_limit X f x₀))

theorem Chapter9.right_limit.conv {X : Set ℝ} {f : ℝ → ℝ} {x₀ : ℝ} (had : AdherentPt x₀ (X ∩ Set.Ioi x₀)) (h : RightLimitExists X f x₀) (a : ℕ → ℝ) (ha : ∀ (n : ℕ), a n ∈ X ∩ Set.Ioi x₀) (hconv : Filter.Tendsto a Filter.atTop (nhds x₀)) : Filter.Tendsto (fun (n : ℕ) => f (a n)) Filter.atTop (nhds (right_limit X f x₀))

theorem Chapter9.left_limit.conv {X : Set ℝ} {f : ℝ → ℝ} {x₀ : ℝ} (had : AdherentPt x₀ (X ∩ Set.Iio x₀)) (h : LeftLimitExists X f x₀) (a : ℕ → ℝ) (ha : ∀ (n : ℕ), a n ∈ X ∩ Set.Iio x₀) (hconv : Filter.Tendsto a Filter.atTop (nhds x₀)) : Filter.Tendsto (fun (n : ℕ) => f (a n)) Filter.atTop (nhds (left_limit X f x₀))

theorem Chapter9.ContinuousAt.iff_eq_left_right_limit {X : Set ℝ} {f : ℝ → ℝ} {x₀ : ℝ} (h : x₀ ∈ X) (had_left : AdherentPt x₀ (X ∩ Set.Iio x₀)) (had_right : AdherentPt x₀ (X ∩ Set.Ioi x₀)) : ContinuousWithinAt f X x₀ ↔ (RightLimitExists X f x₀ ∧ right_limit X f x₀ = f x₀) ∧ LeftLimitExists X f x₀ ∧ left_limit X f x₀ = f x₀

Proposition 9.5.3

@[reducible, inline]

abbrev Chapter9.HasJumpDiscontinuity (X : Set ℝ) (f : ℝ → ℝ) (x₀ : ℝ) : Prop

Equations

• Chapter9.HasJumpDiscontinuity X f x₀ = (Chapter9.RightLimitExists X f x₀ ∧ Chapter9.LeftLimitExists X f x₀ ∧ Chapter9.right_limit X f x₀ ≠ Chapter9.left_limit X f x₀)

@[reducible, inline]

abbrev Chapter9.HasRemovableDiscontinuity (X : Set ℝ) (f : ℝ → ℝ) (x₀ : ℝ) : Prop

Equations

• One or more equations did not get rendered due to their size.