Аналіз I, Розділ 9.5: Ліві та праві границі

Я (прим. перекл. Терренс Тао) намагався зробити переклад якомога точнішим перефразуванням оригінального тексту. Коли є вибір між більш ідіоматичним підходом Lean та більш точним перекладом, я зазвичай обирав останній. Зокрема, будуть місця, де код Lean можна було б "підправити", щоб зробити його більш елегантним та ідіоматичним, але я свідомо уникав цього вибору.

Основні конструкції та результати цього розділу:

• Ліві та праві односторонні границі.

@[reducible, inline]

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

Визначення 9.5.1. Ми надаємо лівим і правим границям «сміттеве» значення 0, якщо границя не існує.

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₀

Твердження 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.