Analysis I, Section 9.6: The maximum principle

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:

• Continuous functions on closed and bounded intervals are bounded.

• Continuous functions on closed and bounded intervals attain their maximum and minimum.

namespace Chapter9 abbrev BddBelowOn (f:ℝ → ℝ) (X:Set ℝ) : Prop := ∃ M, ∀ x ∈ X, -M ≤ f xabbrev BddOn (f:ℝ → ℝ) (X:Set ℝ) : Prop := ∃ M, ∀ x ∈ X, |f x| ≤ M theorem declaration uses 'sorry'BddOn.iff' (f:ℝ → ℝ) (X:Set ℝ) : BddOn f X ↔ Bornology.IsBounded (f '' X) := byf:ℝ → ℝX:Set ℝ⊢ BddOn f X ↔ Bornology.IsBounded (f '' X) sorryAll goals completed! 🐙theorem BddOn.of_bounded {f :ℝ → ℝ} {X: Set ℝ} {M:ℝ} (h: ∀ x ∈ X, |f x| ≤ M) : BddOn f X := byf:ℝ → ℝX:Set ℝM:ℝh:∀ x ∈ X, |f x| ≤ M⊢ BddOn f X use MAll goals completed! 🐙declaration uses 'sorry'example : Continuous (fun x:ℝ ↦ x) := by⊢ Continuous fun x => x sorryAll goals completed! 🐙declaration uses 'sorry'example : ¬ BddOn (fun x:ℝ ↦ x) .univ := by⊢ ¬BddOn (fun x => x) Set.univ sorryAll goals completed! 🐙declaration uses 'sorry'example : BddOn (fun x:ℝ ↦ x) (.Icc 1 2) := by⊢ BddOn (fun x => x) (Set.Icc 1 2) sorryAll goals completed! 🐙declaration uses 'sorry'example : ContinuousOn (fun x:ℝ ↦ 1/x) (.Ioo 0 1) := by⊢ ContinuousOn (fun x => 1 / x) (Set.Ioo 0 1) sorryAll goals completed! 🐙declaration uses 'sorry'example : ¬ BddOn (fun x:ℝ ↦ 1/x) (.Ioo 0 1) := by⊢ ¬BddOn (fun x => 1 / x) (Set.Ioo 0 1) sorryAll goals completed! 🐙theorem declaration uses 'sorry'why_7_6_3 {n: ℕ → ℕ} (hn: StrictMono n) (j:ℕ) : n j ≥ j := byn:ℕ → ℕhn:StrictMono nj:ℕ⊢ n j ≥ j sorryAll goals completed! 🐙

isMaxOn_iff.{u, v} {α : Type u} {β : Type v} [Preorder β] {f : α → β} {s : Set α} {a : α} :
  IsMaxOn f s a ↔ ∀ x ∈ s, f x ≤ f a

isMinOn_iff.{u, v} {α : Type u} {β : Type v} [Preorder β] {f : α → β} {s : Set α} {a : α} :
  IsMinOn f s a ↔ ∀ x ∈ s, f a ≤ f x

theorem declaration uses 'sorry'BddBelowOn.isMinOn {f:ℝ → ℝ} {X:Set ℝ} {x₀:ℝ} (h: IsMinOn f X x₀): BddBelowOn f X := byf:ℝ → ℝX:Set ℝx₀:ℝh:IsMinOn f X x₀⊢ BddBelowOn f X sorryAll goals completed! 🐙 theorem declaration uses 'sorry'IsMinOn.of_continuous_on_compact {a b:ℝ} (h:a < b) {f:ℝ → ℝ} (hf: ContinuousOn f (.Icc a b)) : ∃ xmin ∈ Set.Icc a b, IsMinOn f (.Icc a b) xmin := bya:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)⊢ ∃ xmin ∈ Set.Icc a b, IsMinOn f (Set.Icc a b) xmin sorryAll goals completed! 🐙declaration uses 'sorry'example : IsMaxOn (fun x ↦ x^2) (.Icc (-2) 2) 2 := by⊢ IsMaxOn (fun x => x ^ 2) (Set.Icc (-2) 2) 2 sorryAll goals completed! 🐙declaration uses 'sorry'example : IsMaxOn (fun x ↦ x^2) (.Icc (-2) 2) (-2) := by⊢ IsMaxOn (fun x => x ^ 2) (Set.Icc (-2) 2) (-2) sorryAll goals completed! 🐙theorem sSup.of_isMaxOn {f:ℝ → ℝ} {X:Set ℝ} {x₀:ℝ} (hx₀: x₀ ∈ X) (h: IsMaxOn f X x₀) : sSup (f '' X) = f x₀ := byf:ℝ → ℝX:Set ℝx₀:ℝhx₀:x₀ ∈ Xh:IsMaxOn f X x₀⊢ sSup (f '' X) = f x₀ apply IsGreatest.csSup_eqHf:ℝ → ℝX:Set ℝx₀:ℝhx₀:x₀ ∈ Xh:IsMaxOn f X x₀⊢ IsGreatest (f '' X) (f x₀) simp [IsGreatest, mem_upperBounds]Hf:ℝ → ℝX:Set ℝx₀:ℝhx₀:x₀ ∈ Xh:IsMaxOn f X x₀⊢ (∃ x ∈ X, f x = f x₀) ∧ ∀ a ∈ X, f a ≤ f x₀ refine ⟨ ⟨x₀, hx₀, rfl ⟩, h ⟩All goals completed! 🐙theorem sInf.of_isMinOn {f:ℝ → ℝ} {X:Set ℝ} {x₀:ℝ} (hx₀: x₀ ∈ X) (h: IsMinOn f X x₀) : sInf (f '' X) = f x₀ := byf:ℝ → ℝX:Set ℝx₀:ℝhx₀:x₀ ∈ Xh:IsMinOn f X x₀⊢ sInf (f '' X) = f x₀ apply IsLeast.csInf_eqHf:ℝ → ℝX:Set ℝx₀:ℝhx₀:x₀ ∈ Xh:IsMinOn f X x₀⊢ IsLeast (f '' X) (f x₀) simp [IsLeast, mem_lowerBounds]Hf:ℝ → ℝX:Set ℝx₀:ℝhx₀:x₀ ∈ Xh:IsMinOn f X x₀⊢ (∃ x ∈ X, f x = f x₀) ∧ ∀ a ∈ X, f x₀ ≤ f a refine ⟨ ⟨x₀, hx₀, rfl ⟩, h ⟩All goals completed! 🐙theorem sSup.of_continuous_on_compact {a b:ℝ} (h:a < b) (f:ℝ → ℝ) (hf: ContinuousOn f (.Icc a b)) : ∃ xmax ∈ Set.Icc a b, sSup (f '' .Icc a b) = f xmax := bya:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)⊢ ∃ xmax ∈ Set.Icc a b, sSup (f '' Set.Icc a b) = f xmax choose x hx h' using IsMaxOn.of_continuous_on_compact h hfa:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)x:ℝhx:x ∈ Set.Icc a bh':IsMaxOn f (Set.Icc a b) x⊢ ∃ xmax ∈ Set.Icc a b, sSup (f '' Set.Icc a b) = f xmax grind [sSup.of_isMaxOn]All goals completed! 🐙theorem sInf.of_continuous_on_compact {a b:ℝ} (h:a < b) (f:ℝ → ℝ) (hf: ContinuousOn f (.Icc a b)) : ∃ xmin ∈ Set.Icc a b, sInf (f '' .Icc a b) = f xmin := bya:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)⊢ ∃ xmin ∈ Set.Icc a b, sInf (f '' Set.Icc a b) = f xmin choose x hx h' using IsMinOn.of_continuous_on_compact h hfa:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)x:ℝhx:x ∈ Set.Icc a bh':IsMinOn f (Set.Icc a b) x⊢ ∃ xmin ∈ Set.Icc a b, sInf (f '' Set.Icc a b) = f xmin grind [sInf.of_isMinOn]All goals completed! 🐙 end Chapter9