theorem lemma_3_3_1 {a b : ℝ} (hle : a ≤ b) {f : ℝ → ℝ} (hf : ContinuousOn f (Set.Icc a b)) : ∃ (M : ℝ), ∀ x ∈ Set.Icc a b, |f x| ≤ M

Lemma 3.3.1. A continuous function f : [a, b] → ℝ is bounded.

theorem theorem_3_3_2_min_helper {a b : ℝ} (hle : a ≤ b) {f : ℝ → ℝ} (hf : ContinuousOn f (Set.Icc a b)) : ∃ c ∈ Set.Icc a b, ∀ x ∈ Set.Icc a b, f c ≤ f x

Helper lemma for Theorem 3.3.2: a continuous function reaches its minimum on [a, b].

theorem theorem_3_3_2_max_helper {a b : ℝ} (hle : a ≤ b) {f : ℝ → ℝ} (hf : ContinuousOn f (Set.Icc a b)) : ∃ d ∈ Set.Icc a b, ∀ x ∈ Set.Icc a b, f x ≤ f d

Helper lemma for Theorem 3.3.2: a continuous function reaches its maximum on [a, b].

theorem theorem_3_3_2 {a b : ℝ} (hle : a ≤ b) {f : ℝ → ℝ} (hf : ContinuousOn f (Set.Icc a b)) : (∃ c ∈ Set.Icc a b, ∀ x ∈ Set.Icc a b, f c ≤ f x) ∧ ∃ d ∈ Set.Icc a b, ∀ x ∈ Set.Icc a b, f x ≤ f d

Theorem 3.3.2 (Minimum-maximum theorem / Extreme value theorem). A continuous function f : [a, b] → ℝ attains an absolute minimum and an absolute maximum on [a, b].

theorem example_3_3_3_min_bound (x : ℝ) : (fun (x : ℝ) => x ^ 2 + 1) 0 ≤ (fun (x : ℝ) => x ^ 2 + 1) x

theorem example_3_3_3_sq_le_4 {x : ℝ} (hx : x ∈ Set.Icc (-1) 2) : x ^ 2 ≤ 4

theorem example_3_3_3_sq_le_100 {x : ℝ} (hx : x ∈ Set.Icc (-10) 10) : x ^ 2 ≤ 100

theorem example_3_3_3 : (∀ x ∈ Set.Icc (-1) 2, (fun (x : ℝ) => x ^ 2 + 1) 0 ≤ (fun (x : ℝ) => x ^ 2 + 1) x) ∧ (fun (x : ℝ) => x ^ 2 + 1) 0 = 1 ∧ (∀ x ∈ Set.Icc (-1) 2, (fun (x : ℝ) => x ^ 2 + 1) x ≤ (fun (x : ℝ) => x ^ 2 + 1) 2) ∧ (fun (x : ℝ) => x ^ 2 + 1) 2 = 5 ∧ (∀ x ∈ Set.Icc (-10) 10, (fun (x : ℝ) => x ^ 2 + 1) x ≤ (fun (x : ℝ) => x ^ 2 + 1) 10) ∧ ∀ x ∈ Set.Icc (-10) 10, (fun (x : ℝ) => x ^ 2 + 1) x ≤ (fun (x : ℝ) => x ^ 2 + 1) (-10)

Example 3.3.3. For f x = x ^ 2 + 1 on [-1, 2], the minimum is achieved at x = 0 with value f 0 = 1 and the maximum at x = 2 with value f 2 = 5. On the larger interval [-10, 10], the maximum occurs at the endpoints x = 10 or x = -10.

theorem example_3_3_4 : (¬∃ (c : ℝ), ∀ (x : ℝ), (fun (x : ℝ) => x) c ≤ (fun (x : ℝ) => x) x) ∧ ¬∃ (d : ℝ), ∀ (x : ℝ), (fun (x : ℝ) => x) x ≤ (fun (x : ℝ) => x) d

Example 3.3.4. The identity function f : ℝ → ℝ, given by f x = x, achieves neither a minimum nor a maximum on ℝ, illustrating that bounded intervals are required to guarantee extrema.

theorem example_3_3_5 : ContinuousOn (fun (x : ℝ) => 1 / x) (Set.Ioo 0 1) ∧ (¬∃ c ∈ Set.Ioo 0 1, ∀ x ∈ Set.Ioo 0 1, (fun (x : ℝ) => 1 / x) c ≤ (fun (x : ℝ) => 1 / x) x) ∧ (¬∃ d ∈ Set.Ioo 0 1, ∀ x ∈ Set.Ioo 0 1, (fun (x : ℝ) => 1 / x) x ≤ (fun (x : ℝ) => 1 / x) d) ∧ (∀ (M : ℝ), ∃ x ∈ Set.Ioo 0 1, M ≤ (fun (x : ℝ) => 1 / x) x) ∧ (∀ x ∈ Set.Ioo 0 1, 1 < (fun (x : ℝ) => 1 / x) x) ∧ ∀ ε > 0, ∃ x ∈ Set.Ioo 0 1, |(fun (x : ℝ) => 1 / x) x - 1| < ε

Example 3.3.5. The function f : (0, 1) → ℝ given by f x = 1 / x is continuous on the open interval but achieves neither a minimum nor a maximum. The values are unbounded as x approaches 0, while as x → 1 the values tend to 1 with f x > 1 for all x ∈ (0, 1), so no point of the domain yields the value 1. This shows the need for a closed interval in the extreme value theorem.

noncomputable def example_3_3_6_function (x : ℝ) : ℝ

Example 3.3.6. On the closed, bounded interval [0, 1], consider f : [0, 1] → ℝ given by f x = 1 / x for x > 0 and f 0 = 0. The function is not continuous at 0, and because the values blow up near 0, it fails to attain a maximum on [0, 1] despite the domain being compact.

Equations

• example_3_3_6_function x = if x = 0 then 0 else 1 / x

theorem example_3_3_6_function_pos {x : ℝ} (hx : 0 < x) : example_3_3_6_function x = 1 / x

theorem example_3_3_6_not_cont : ¬ContinuousAt example_3_3_6_function 0

theorem example_3_3_6_no_max_point {d : ℝ} : d ∈ Set.Icc 0 1 → ∃ x ∈ Set.Icc 0 1, example_3_3_6_function d < example_3_3_6_function x

theorem example_3_3_6_unbounded (M : ℝ) : ∃ x ∈ Set.Icc 0 1, M ≤ example_3_3_6_function x

theorem example_3_3_6 : ¬ContinuousAt example_3_3_6_function 0 ∧ (¬∃ d ∈ Set.Icc 0 1, ∀ x ∈ Set.Icc 0 1, example_3_3_6_function x ≤ example_3_3_6_function d) ∧ ∀ (M : ℝ), ∃ x ∈ Set.Icc 0 1, M ≤ example_3_3_6_function x

theorem lemma_3_3_7 {a b : ℝ} (hab : a < b) {f : ℝ → ℝ} (hf : ContinuousOn f (Set.Icc a b)) (ha : f a < 0) (hb : 0 < f b) : ∃ c ∈ Set.Ioo a b, f c = 0

Lemma 3.3.7 (Bolzano's intermediate value theorem). For a continuous function f : [a, b] → ℝ with f a < 0 and 0 < f b, there exists a point c strictly between a and b such that f c = 0.

theorem theorem_3_3_8 {a b y : ℝ} (hab : a < b) {f : ℝ → ℝ} (hf : ContinuousOn f (Set.Icc a b)) (hy : f a < y ∧ y < f b ∨ f a > y ∧ y > f b) : ∃ c ∈ Set.Ioo a b, f c = y

Theorem 3.3.8 (Bolzano's intermediate value theorem). Let f : [a, b] → ℝ be continuous. If a real number y satisfies f a < y < f b or f a > y > f b, then there is some c strictly between a and b such that f c = y.

theorem example_3_3_9 : (fun (x : ℝ) => x ^ 3 - 2 * x ^ 2 + x - 1) 1 = -1 ∧ (fun (x : ℝ) => x ^ 3 - 2 * x ^ 2 + x - 1) 2 = 1 ∧ (fun (x : ℝ) => x ^ 3 - 2 * x ^ 2 + x - 1) (3 / 2) < 0 ∧ (fun (x : ℝ) => x ^ 3 - 2 * x ^ 2 + x - 1) (7 / 4) < 0 ∧ 0 < (fun (x : ℝ) => x ^ 3 - 2 * x ^ 2 + x - 1) (15 / 8) ∧ ContinuousOn (fun (x : ℝ) => x ^ 3 - 2 * x ^ 2 + x - 1) (Set.Icc 1 2) ∧ ∃ c ∈ Set.Ioo 1 2, (fun (x : ℝ) => x ^ 3 - 2 * x ^ 2 + x - 1) c = 0

Example 3.3.9 (Bisection method). For f x = x ^ 3 - 2 x ^ 2 + x - 1, we have f 1 = -1 and f 2 = 1, so by the intermediate value theorem there is a root c ∈ (1, 2). Evaluating at midpoints shows sign changes on nested intervals: f (3/2) < 0, f (7/4) < 0, and 0 < f (15/8), so the root lies in (7/4, 15/8), numerically near 1.7549.

theorem proposition_3_3_10 {p : Polynomial ℝ} (hodd : Odd p.natDegree) (h₀ : p.leadingCoeff ≠ 0) : ∃ (x : ℝ), Polynomial.eval x p = 0

Proposition 3.3.10. A real polynomial of odd degree has a real root.

theorem example_3_3_11_pow_pos {k : ℕ} (hk : 1 < k) {y : ℝ} (hy : 1 < y) : 0 < y ^ k - y

theorem example_3_3_11 {k : ℕ} (hk : 0 < k) {y : ℝ} (hy : 0 < y) : ∃ (x : ℝ), 0 < x ∧ x ^ k = y

Example 3.3.11. For any natural number k > 0 and any y > 0, there exists x > 0 such that x ^ k = y, which follows from Bolzano's intermediate value theorem applied to x ↦ x ^ k - y.

noncomputable def example_3_3_12_function (x : ℝ) : ℝ

Example 3.3.12. The function f x = sin (1 / x) for x ≠ 0 and f 0 = 0 is discontinuous at 0, yet it still has the intermediate value property: whenever a < b and y lies strictly between f a and f b (in either order), there exists some c ∈ (a, b) with f c = y.

Equations

• example_3_3_12_function x = if x = 0 then 0 else Real.sin (1 / x)

theorem example_3_3_12_function_of_ne {x : ℝ} (hx : x ≠ 0) : example_3_3_12_function x = Real.sin (1 / x)

theorem example_3_3_12_function_neg (x : ℝ) : example_3_3_12_function (-x) = -example_3_3_12_function x

theorem example_3_3_12_abs_le_one (x : ℝ) : |example_3_3_12_function x| ≤ 1

theorem example_3_3_12_continuous_on_nonzero {a b : ℝ} (hzero : 0 ∉ Set.Icc a b) : ContinuousOn example_3_3_12_function (Set.Icc a b)

theorem example_3_3_12_hits_pm_one (ε : ℝ) : ε > 0 → ∃ (t₁ : ℝ) (t₂ : ℝ), 0 < t₁ ∧ t₁ < t₂ ∧ t₂ < ε ∧ example_3_3_12_function t₁ = -1 ∧ example_3_3_12_function t₂ = 1

theorem example_3_3_12_between_bounds {a b y : ℝ} (hy : example_3_3_12_function a < y ∧ y < example_3_3_12_function b ∨ example_3_3_12_function a > y ∧ y > example_3_3_12_function b) : -1 < y ∧ y < 1

theorem example_3_3_12_not_cont : ¬ContinuousAt example_3_3_12_function 0

theorem example_3_3_12_IVT_cross_zero {a b y : ℝ} (ha : a < 0) (hb : 0 < b) (hy : example_3_3_12_function a < y ∧ y < example_3_3_12_function b ∨ example_3_3_12_function a > y ∧ y > example_3_3_12_function b) : ∃ c ∈ Set.Ioo a b, example_3_3_12_function c = y

theorem example_3_3_12 : ¬ContinuousAt example_3_3_12_function 0 ∧ ∀ {a b y : ℝ}, a < b → example_3_3_12_function a < y ∧ y < example_3_3_12_function b ∨ example_3_3_12_function a > y ∧ y > example_3_3_12_function b → ∃ c ∈ Set.Ioo a b, example_3_3_12_function c = y

theorem corollary_3_3_13_image_subset {a b : ℝ} {f : ℝ → ℝ} {xmin xmax : ℝ} (_hxmin : xmin ∈ Set.Icc a b) (_hxmax : xmax ∈ Set.Icc a b) (hmin : ∀ x ∈ Set.Icc a b, f xmin ≤ f x) (hmax : ∀ x ∈ Set.Icc a b, f x ≤ f xmax) : f '' Set.Icc a b ⊆ Set.Icc (f xmin) (f xmax)

If f has a minimum at xmin and a maximum at xmax on [a, b], then the image lies between the endpoint values.

theorem corollary_3_3_13_Icc_subset_image {a b : ℝ} {f : ℝ → ℝ} {xmin xmax : ℝ} (hxmin : xmin ∈ Set.Icc a b) (hxmax : xmax ∈ Set.Icc a b) (hf : ContinuousOn f (Set.Icc a b)) (_hmin : ∀ x ∈ Set.Icc a b, f xmin ≤ f x) (_hmax : ∀ x ∈ Set.Icc a b, f x ≤ f xmax) (hcd : f xmin < f xmax) : Set.Icc (f xmin) (f xmax) ⊆ f '' Set.Icc a b

If the minimum and maximum values are distinct, then every value between them is achieved on [a, b].

theorem corollary_3_3_13 {a b : ℝ} (hle : a ≤ b) {f : ℝ → ℝ} (hf : ContinuousOn f (Set.Icc a b)) : (∃ (c : ℝ) (d : ℝ), c ≤ d ∧ f '' Set.Icc a b = Set.Icc c d) ∨ ∃ (c : ℝ), f '' Set.Icc a b = {c}

Corollary 3.3.13. If f : [a, b] → ℝ is continuous, then the image f '' [a, b] is either a closed and bounded interval or a single point.