Аналіз I, Розділ 9.6: Принцип максимуму

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

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

• Неперервні функції на замкнутих і обмежених відрізках є обмеженими.
• Неперервні функції на замкнутих і обмежених відрізках досягають своїх максимуму та мінімуму.

@[reducible, inline]

abbrev Chapter9.BddAboveOn (f : ℝ → ℝ) (X : Set ℝ) : Prop

Визначення 9.6.1

Equations

• Chapter9.BddAboveOn f X = ∃ (M : ℝ), ∀ x ∈ X, f x ≤ M

@[reducible, inline]

abbrev Chapter9.BddBelowOn (f : ℝ → ℝ) (X : Set ℝ) : Prop

Equations

• Chapter9.BddBelowOn f X = ∃ (M : ℝ), ∀ x ∈ X, -M ≤ f x

@[reducible, inline]

abbrev Chapter9.BddOn (f : ℝ → ℝ) (X : Set ℝ) : Prop

Equations

• Chapter9.BddOn f X = ∃ (M : ℝ), ∀ x ∈ X, |f x| ≤ M

theorem Chapter9.BddOn.iff (f : ℝ → ℝ) (X : Set ℝ) : BddOn f X ↔ BddAboveOn f X ∧ BddBelowOn f X

Зауваження 9.6.2

theorem Chapter9.BddOn.iff' (f : ℝ → ℝ) (X : Set ℝ) : BddOn f X ↔ Bornology.IsBounded (f '' X)

theorem Chapter9.BddOn.of_bounded {f : ℝ → ℝ} {X : Set ℝ} {M : ℝ} (h : ∀ x ∈ X, |f x| ≤ M) : BddOn f X

theorem Chapter9.why_7_6_3 {n : ℕ → ℕ} (hn : StrictMono n) (j : ℕ) : n j ≥ j

theorem Chapter9.BddOn.of_continuous_on_compact {a b : ℝ} (h : a < b) {f : ℝ → ℝ} (hf : ContinuousOn f (Set.Icc a b)) : BddOn f (Set.Icc a b)

Лема 9.6.3

theorem Chapter9.BddAboveOn.isMaxOn {f : ℝ → ℝ} {X : Set ℝ} {x₀ : ℝ} (h : IsMaxOn f X x₀) : BddAboveOn f X

Зауваження 9.6.6

theorem Chapter9.BddBelowOn.isMinOn {f : ℝ → ℝ} {X : Set ℝ} {x₀ : ℝ} (h : IsMinOn f X x₀) : BddBelowOn f X

theorem Chapter9.IsMaxOn.of_continuous_on_compact {a b : ℝ} (h : a < b) {f : ℝ → ℝ} (hf : ContinuousOn f (Set.Icc a b)) : ∃ xmax ∈ Set.Icc a b, IsMaxOn f (Set.Icc a b) xmax

Твердження 9.6.7 (Принцип максимуму)

theorem Chapter9.IsMinOn.of_continuous_on_compact {a b : ℝ} (h : a < b) {f : ℝ → ℝ} (hf : ContinuousOn f (Set.Icc a b)) : ∃ xmin ∈ Set.Icc a b, IsMinOn f (Set.Icc a b) xmin

theorem Chapter9.sSup.of_isMaxOn {f : ℝ → ℝ} {X : Set ℝ} {x₀ : ℝ} (hx₀ : x₀ ∈ X) (h : IsMaxOn f X x₀) : sSup (f '' X) = f x₀

theorem Chapter9.sInf.of_isMinOn {f : ℝ → ℝ} {X : Set ℝ} {x₀ : ℝ} (hx₀ : x₀ ∈ X) (h : IsMinOn f X x₀) : sInf (f '' X) = f x₀

theorem Chapter9.sSup.of_continuous_on_compact {a b : ℝ} (h : a < b) (f : ℝ → ℝ) (hf : ContinuousOn f (Set.Icc a b)) : ∃ xmax ∈ Set.Icc a b, sSup (f '' Set.Icc a b) = f xmax

theorem Chapter9.sInf.of_continuous_on_compact {a b : ℝ} (h : a < b) (f : ℝ → ℝ) (hf : ContinuousOn f (Set.Icc a b)) : ∃ xmin ∈ Set.Icc a b, sInf (f '' Set.Icc a b) = f xmin