Аналіз I, Розділ 9.4: Неперервні функції

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

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

• Неперервність функцій із використанням понять Mathlib

theorem Chapter9.ContinuousWithinAt.iff (X : Set ℝ) (f : ℝ → ℝ) (x₀ : ℝ) : ContinuousWithinAt f X x₀ ↔ Convergesto X f (f x₀) x₀

Визначення 9.4.1. Тут ми використовуємо визначення неперервності з Mathlib. Гіпотеза x ∈ X не потрібна!

@[reducible, inline]

noncomputable abbrev Chapter9.f_9_4_6 (x : ℝ) : ℝ

Приклад 9.4.6 -

Equations

• Chapter9.f_9_4_6 x = if x ≥ 0 then 1 else 0

theorem Chapter9.ContinuousWithinAt.tfae (X : Set ℝ) (f : ℝ → ℝ) {x₀ : ℝ} (h : x₀ ∈ X) : [ContinuousWithinAt f X x₀, ∀ (a : ℕ → ℝ), (∀ (n : ℕ), a n ∈ X) → Filter.Tendsto a Filter.atTop (nhds x₀) → Filter.Tendsto (fun (n : ℕ) => f (a n)) Filter.atTop (nhds (f x₀)), ∀ ε > 0, ∃ δ > 0, ∀ x ∈ X, |x - x₀| < δ → |f x - f x₀| < ε].TFAE

Твердження 9.4.7 / Вправа 9.4.1. Можливо, гіпотеза x₀ ∈ X не є необхідною.

theorem Filter.Tendsto.comp_of_continuous {X : Set ℝ} {f : ℝ → ℝ} {x₀ : ℝ} (h : x₀ ∈ X) (h_cont : ContinuousWithinAt f X x₀) {a : ℕ → ℝ} (ha : ∀ (n : ℕ), a n ∈ X) (hconv : Tendsto a atTop (nhds x₀)) : Tendsto (fun (n : ℕ) => f (a n)) atTop (nhds (f x₀))

Зауваження 9.4.8 -

theorem Chapter9.ContinuousWithinAt.add {X : Set ℝ} (f g : ℝ → ℝ) {x₀ : ℝ} (h : x₀ ∈ X) (hf : ContinuousWithinAt f X x₀) (hg : ContinuousWithinAt g X x₀) : ContinuousWithinAt (f + g) X x₀

theorem Chapter9.ContinuousWithinAt.sub {X : Set ℝ} (f g : ℝ → ℝ) {x₀ : ℝ} (h : x₀ ∈ X) (hf : ContinuousWithinAt f X x₀) (hg : ContinuousWithinAt g X x₀) : ContinuousWithinAt (f - g) X x₀

theorem Chapter9.ContinuousWithinAt.max {X : Set ℝ} (f g : ℝ → ℝ) {x₀ : ℝ} (h : x₀ ∈ X) (hf : ContinuousWithinAt f X x₀) (hg : ContinuousWithinAt g X x₀) : ContinuousWithinAt (f ⊔ g) X x₀

theorem Chapter9.ContinuousWithinAt.min {X : Set ℝ} (f g : ℝ → ℝ) {x₀ : ℝ} (h : x₀ ∈ X) (hf : ContinuousWithinAt f X x₀) (hg : ContinuousWithinAt g X x₀) : ContinuousWithinAt (f ⊓ g) X x₀

theorem Chapter9.ContinuousWithinAt.mul' {X : Set ℝ} (f g : ℝ → ℝ) {x₀ : ℝ} (h : x₀ ∈ X) (hf : ContinuousWithinAt f X x₀) (hg : ContinuousWithinAt g X x₀) : ContinuousWithinAt (f * g) X x₀

theorem Chapter9.ContinuousWithinAt.div' {X : Set ℝ} (f g : ℝ → ℝ) {x₀ : ℝ} (h : x₀ ∈ X) (hM : g x₀ ≠ 0) (hf : ContinuousWithinAt f X x₀) (hg : ContinuousWithinAt g X x₀) : ContinuousWithinAt (f / g) X x₀

theorem Chapter9.Continuous.exp {a : ℝ} (ha : a > 0) : Continuous fun (x : ℝ) => a ^ x

Твердження 9.4.10 / Вправа 9.4.3

theorem Chapter9.Continuous.exp' (p : ℝ) : ContinuousOn (fun (x : ℝ) => x ^ p) (Set.Ioi 0)

Твердження 9.4.11 / Вправа 9.4.4

theorem Chapter9.Continuous.abs : Continuous fun (x : ℝ) => |x|

Твердження 9.4.12

theorem Chapter9.ContinuousWithinAt.comp {x : ℝ} {X Y : Set ℝ} {f g : ℝ → ℝ} (hf : ∀ x ∈ X, f x ∈ Y) {x₀ : ℝ} (hx₀ : x ∈ X) (hf_cont : ContinuousWithinAt f X x₀) (hg_cont : ContinuousWithinAt g Y (f x₀)) : ContinuousWithinAt (g ∘ f) X x₀

Твердження 9.4.13 / Вправа 9.4.5

theorem Chapter9.ContinuousOn.restrict {X Y : Set ℝ} {f : ℝ → ℝ} (hY : Y ⊆ X) (hf : ContinuousOn f X) : ContinuousOn f Y

Вправа 9.4.6

theorem Chapter9.Continuous.polynomial {n : ℕ} (c : Fin n → ℝ) : Continuous fun (x : ℝ) => ∑ i : Fin n, c i * x ^ ↑i

Вправа 9.4.7