Аналіз I, Глава 9.5

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.right_limit_exists (X : Set ℝ) (f : ℝ → ℝ) (x₀ : ℝ) : Prop

Визначення 9.5.1. We give left and right limits the "junk" value of 0 if the limit does not exist.

Equations

• Chapter9.right_limit_exists X f x₀ = ∃ (L : ℝ), Filter.Tendsto f (nhds x₀ ⊓ Filter.principal (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.right_limit_exists X f x₀ then Exists.choose h else 0

@[reducible, inline]

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

Equations

• Chapter9.left_limit_exists X f x₀ = ∃ (L : ℝ), Filter.Tendsto f (nhds x₀ ⊓ Filter.principal (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.left_limit_exists 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 (nhds x₀ ⊓ Filter.principal (X ∩ Set.Ioi x₀)) (nhds L)) : 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 (nhds x₀ ⊓ Filter.principal (X ∩ Set.Iio x₀)) (nhds L)) : left_limit X f x₀ = L

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

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

theorem Chapter9.right_limit.conv {X : Set ℝ} {f : ℝ → ℝ} {x₀ L : ℝ} (had : AdherentPt x₀ (X ∩ Set.Ioi x₀)) (h : right_limit_exists 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₀ L : ℝ} (had : AdherentPt x₀ (X ∩ Set.Iio x₀)) (h : left_limit_exists 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₀ ↔ right_limit_exists X f x₀ ∧ left_limit_exists X f x₀ ∧ right_limit X f x₀ = f x₀ ∧ left_limit X f x₀ = f x₀

Твердження 9.5.3

@[reducible, inline]

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

Equations

• Chapter9.has_jump_discontinuity X f x₀ = (Chapter9.right_limit_exists X f x₀ ∧ Chapter9.left_limit_exists X f x₀ ∧ Chapter9.right_limit X f x₀ ≠ Chapter9.left_limit X f x₀)

@[reducible, inline]

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

Equations

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