def RelativeMaxOn (S : Set ℝ) (f : ℝ → ℝ) (c : ℝ) : Prop

Definition 4.2.1: A function f : S → ℝ has a relative maximum at c ∈ S if some δ > 0 satisfies f x ≤ f c whenever x ∈ S and |x - c| < δ. The notion of relative minimum reverses the inequality.

Equations

• RelativeMaxOn S f c = ∃ δ > 0, ∀ {x : ℝ}, x ∈ S → |x - c| < δ → f x ≤ f c

def RelativeMinOn (S : Set ℝ) (f : ℝ → ℝ) (c : ℝ) : Prop

Equations

• RelativeMinOn S f c = ∃ δ > 0, ∀ {x : ℝ}, x ∈ S → |x - c| < δ → f c ≤ f x

theorem relativeMaxOn_iff_isLocalMaxOn {S : Set ℝ} {f : ℝ → ℝ} {c : ℝ} : RelativeMaxOn S f c ↔ IsLocalMaxOn f S c

The relative maximum defined via punctured-δ neighborhoods matches IsLocalMaxOn from mathlib.

theorem relativeMinOn_iff_isLocalMinOn {S : Set ℝ} {f : ℝ → ℝ} {c : ℝ} : RelativeMinOn S f c ↔ IsLocalMinOn f S c

The relative minimum defined via punctured-δ neighborhoods matches IsLocalMinOn from mathlib.

theorem deriv_eq_zero_of_relative_extremum {f : ℝ → ℝ} {a b c : ℝ} (hc : c ∈ Set.Ioo a b) (hf : DifferentiableAt ℝ f c) (hExt : RelativeMaxOn (Set.Ioo a b) f c ∨ RelativeMinOn (Set.Ioo a b) f c) : deriv f c = 0

Lemma 4.2.2: If f : (a, b) → ℝ is differentiable at c ∈ (a, b) and has a relative minimum or maximum at c, then deriv f c = 0.

theorem rolle {f : ℝ → ℝ} {a b : ℝ} (h₁ : a < b) (hcont : ContinuousOn f (Set.Icc a b)) (hdiff : DifferentiableOn ℝ f (Set.Ioo a b)) (hend : f a = f b) : ∃ c ∈ Set.Ioo a b, deriv f c = 0

Theorem 4.2.3 (Rolle): If f : [a, b] → ℝ is continuous on the closed interval, differentiable on the open interval, and satisfies f a = f b, then there exists some c ∈ (a, b) with deriv f c = 0.

theorem mean_value_theorem {f : ℝ → ℝ} {a b : ℝ} (h₁ : a < b) (hcont : ContinuousOn f (Set.Icc a b)) (hdiff : DifferentiableOn ℝ f (Set.Ioo a b)) : ∃ c ∈ Set.Ioo a b, f b - f a = deriv f c * (b - a)

Theorem 4.2.4 (Mean value theorem): If f : [a, b] → ℝ is continuous on the closed interval and differentiable on the open interval, then some c ∈ (a, b) satisfies f b - f a = deriv f c * (b - a).

theorem cauchy_mean_value_theorem {f φ : ℝ → ℝ} {a b : ℝ} (hab : a < b) (hcont_f : ContinuousOn f (Set.Icc a b)) (hcont_φ : ContinuousOn φ (Set.Icc a b)) (hdiff_f : DifferentiableOn ℝ f (Set.Ioo a b)) (hdiff_φ : DifferentiableOn ℝ φ (Set.Ioo a b)) : ∃ c ∈ Set.Ioo a b, (f b - f a) * deriv φ c = deriv f c * (φ b - φ a)

Theorem 4.2.5 (Cauchy's mean value theorem): If f, φ : [a, b] → ℝ are continuous on the closed interval and differentiable on the open interval, then some c ∈ (a, b) satisfies (f b - f a) * deriv φ c = deriv f c * (φ b - φ a).

theorem deriv_zero_on_interval_const {I : Set ℝ} (hI : I.OrdConnected) {f : ℝ → ℝ} (hdiff : DifferentiableOn ℝ f I) (hderiv : ∀ x ∈ I, deriv f x = 0) {x y : ℝ} : x ∈ I → y ∈ I → f x = f y

Proposition 4.2.6: If I is an interval and f : I → ℝ is differentiable with deriv f x = 0 for every x ∈ I, then f is constant on I.

theorem increasingOn_iff_deriv_nonneg {I : Set ℝ} (hI : I.OrdConnected) (hInt : (interior I).Nonempty) {f : ℝ → ℝ} (hdiff : DifferentiableOn ℝ f I) : MonotoneOn f I ↔ ∀ x ∈ I, 0 ≤ deriv f x

Proposition 4.2.7: For a differentiable real function on a nondegenerate interval, the derivative is nonnegative everywhere exactly when the function is increasing, and nonpositive everywhere exactly when the function is decreasing.

theorem decreasingOn_iff_deriv_nonpos {I : Set ℝ} (hI : I.OrdConnected) (hInt : (interior I).Nonempty) {f : ℝ → ℝ} (hdiff : DifferentiableOn ℝ f I) : AntitoneOn f I ↔ ∀ x ∈ I, deriv f x ≤ 0

theorem strictMonoOn_of_deriv_pos' {I : Set ℝ} (hI : I.OrdConnected) {f : ℝ → ℝ} (hdiff : DifferentiableOn ℝ f I) (hpos : ∀ x ∈ I, 0 < deriv f x) : StrictMonoOn f I

Proposition 4.2.8:

• (i) If I is an interval and f : I → ℝ is differentiable with deriv f x > 0 for every x ∈ I, then f is strictly increasing.
• (ii) If I is an interval and f : I → ℝ is differentiable with deriv f x < 0 for every x ∈ I, then f is strictly decreasing.

theorem strictAntiOn_of_deriv_neg' {I : Set ℝ} (hI : I.OrdConnected) {f : ℝ → ℝ} (hdiff : DifferentiableOn ℝ f I) (hneg : ∀ x ∈ I, deriv f x < 0) : StrictAntiOn f I

theorem mvt_le_of_deriv_nonpos {f : ℝ → ℝ} {x y : ℝ} (hxy : x < y) (hcont : ContinuousOn f (Set.Icc x y)) (hdiff : DifferentiableOn ℝ f (Set.Ioo x y)) (hderiv : ∀ z ∈ Set.Ioo x y, deriv f z ≤ 0) : f y ≤ f x

theorem mvt_ge_of_deriv_nonneg {f : ℝ → ℝ} {x y : ℝ} (hxy : x < y) (hcont : ContinuousOn f (Set.Icc x y)) (hdiff : DifferentiableOn ℝ f (Set.Ioo x y)) (hderiv : ∀ z ∈ Set.Ioo x y, 0 ≤ deriv f z) : f x ≤ f y

theorem absMinOf_deriv_nonpos_left_nonneg_right {f : ℝ → ℝ} {a b c : ℝ} (hc : c ∈ Set.Ioo a b) (hcont : ContinuousOn f (Set.Ioo a b)) (hdiff₁ : DifferentiableOn ℝ f (Set.Ioo a c)) (hdiff₂ : DifferentiableOn ℝ f (Set.Ioo c b)) (hle : ∀ x ∈ Set.Ioo a c, deriv f x ≤ 0) (hge : ∀ x ∈ Set.Ioo c b, 0 ≤ deriv f x) : IsMinOn f (Set.Ioo a b) c

Proposition 4.2.9: Let f : (a, b) → ℝ be continuous, let c ∈ (a, b), and assume f is differentiable on (a, c) and (c, b).

• (i) If deriv f x ≤ 0 for x ∈ (a, c) and deriv f x ≥ 0 for x ∈ (c, b), then f has an absolute minimum at c.
• (ii) If deriv f x ≥ 0 for x ∈ (a, c) and deriv f x ≤ 0 for x ∈ (c, b), then f has an absolute maximum at c.

theorem absMaxOf_deriv_nonneg_left_nonpos_right {f : ℝ → ℝ} {a b c : ℝ} (hc : c ∈ Set.Ioo a b) (hcont : ContinuousOn f (Set.Ioo a b)) (hdiff₁ : DifferentiableOn ℝ f (Set.Ioo a c)) (hdiff₂ : DifferentiableOn ℝ f (Set.Ioo c b)) (hge : ∀ x ∈ Set.Ioo a c, 0 ≤ deriv f x) (hle : ∀ x ∈ Set.Ioo c b, deriv f x ≤ 0) : IsMaxOn f (Set.Ioo a b) c

theorem deriv_at_left_endpoint_of_tendsto {f : ℝ → ℝ} {a b L : ℝ} (hab : a < b) (hcont : ContinuousOn f (Set.Icc a b)) (hdiff : DifferentiableOn ℝ f (Set.Ioo a b)) (hlim : Filter.Tendsto (fun (x : ℝ) => deriv f x) (nhdsWithin a (Set.Ioi a)) (nhds L)) : DifferentiableWithinAt ℝ f (Set.Icc a b) a ∧ derivWithin f (Set.Icc a b) a = L

Proposition 4.2.10:

• (i) If f : [a, b) → ℝ is continuous, differentiable on (a, b), and lim_{x → a} f' x = L, then f is differentiable at a with deriv f a = L.
• (ii) If f : (a, b] → ℝ is continuous, differentiable on (a, b), and lim_{x → b} f' x = L, then f is differentiable at b with deriv f b = L.

theorem deriv_at_right_endpoint_of_tendsto {f : ℝ → ℝ} {a b L : ℝ} (hab : a < b) (hcont : ContinuousOn f (Set.Icc a b)) (hdiff : DifferentiableOn ℝ f (Set.Ioo a b)) (hlim : Filter.Tendsto (fun (x : ℝ) => deriv f x) (nhdsWithin b (Set.Iio b)) (nhds L)) : DifferentiableWithinAt ℝ f (Set.Icc a b) b ∧ derivWithin f (Set.Icc a b) b = L

theorem derivWithin_left_eq_deriv {f : ℝ → ℝ} {a b : ℝ} (hfa : DifferentiableAt ℝ f a) (h₁ : a < b) : derivWithin f (Set.Icc a b) a = deriv f a

The derivative within the closed interval at the left endpoint equals the usual derivative when f is differentiable there.

theorem derivWithin_right_eq_deriv {f : ℝ → ℝ} {a b : ℝ} (hfb : DifferentiableAt ℝ f b) (h₁ : a < b) : derivWithin f (Set.Icc a b) b = deriv f b

The derivative within the closed interval at the right endpoint equals the usual derivative when f is differentiable there.

theorem darboux_deriv {f : ℝ → ℝ} {a b y : ℝ} (h₁ : a < b) (hdiff : DifferentiableOn ℝ f (Set.Icc a b)) (ha : DifferentiableAt ℝ f a) (hb : DifferentiableAt ℝ f b) (hy : deriv f a < y ∧ y < deriv f b ∨ deriv f a > y ∧ y > deriv f b) : ∃ c ∈ Set.Ioo a b, deriv f c = y

Theorem 4.2.11 (Darboux): If f : [a, b] → ℝ is differentiable and y lies strictly between deriv f a and deriv f b, then some c ∈ (a, b) has deriv f c = y.

noncomputable def oscillatorySquared (x : ℝ) : ℝ

Example 4.2.12: the function x ↦ (x * sin (1/x))^2 is differentiable on ℝ, has derivative 0 at the origin, but its derivative is not continuous there.

Equations

• oscillatorySquared x = (x * Real.sin x⁻¹) ^ 2

theorem oscillatorySquared_abs_le_square (x : ℝ) : |oscillatorySquared x| ≤ x ^ 2

theorem hasDerivAt_oscillatorySquared_zero : HasDerivAt oscillatorySquared 0 0

theorem hasDerivAt_oscillatorySquared_of_ne_zero {x : ℝ} (hx : x ≠ 0) : HasDerivAt oscillatorySquared (2 * Real.sin x⁻¹ * (x * Real.sin x⁻¹ - Real.cos x⁻¹)) x

theorem differentiable_oscillatorySquared : Differentiable ℝ oscillatorySquared

theorem deriv_oscillatorySquared_of_ne_zero {x : ℝ} (hx : x ≠ 0) : deriv oscillatorySquared x = 2 * Real.sin x⁻¹ * (x * Real.sin x⁻¹ - Real.cos x⁻¹)

theorem deriv_oscillatorySquared_at_zero : deriv oscillatorySquared 0 = 0

theorem oscillatorySquared_isGlobalMin : IsMinOn oscillatorySquared Set.univ 0

noncomputable def oscSeq₁ (n : ℕ) : ℝ

Equations

• oscSeq₁ n = 1 / (Real.pi / 4 + ↑n * (2 * Real.pi))

noncomputable def oscSeq₂ (n : ℕ) : ℝ

Equations

• oscSeq₂ n = 1 / (3 * Real.pi / 4 + ↑n * (2 * Real.pi))

theorem oscSeq₁_pos (n : ℕ) : 0 < oscSeq₁ n

theorem oscSeq₂_pos (n : ℕ) : 0 < oscSeq₂ n

theorem tendsto_nat_mul_add_const_atTop {a b : ℝ} (ha : 0 < a) : Filter.Tendsto (fun (n : ℕ) => ↑n * a + b) Filter.atTop Filter.atTop

theorem oscSeq₁_tendsto_zero : Filter.Tendsto oscSeq₁ Filter.atTop (nhds 0)

theorem oscSeq₂_tendsto_zero : Filter.Tendsto oscSeq₂ Filter.atTop (nhds 0)

theorem sin_inv_oscSeq₁ (n : ℕ) : Real.sin (oscSeq₁ n)⁻¹ = √2 / 2

theorem cos_inv_oscSeq₁ (n : ℕ) : Real.cos (oscSeq₁ n)⁻¹ = √2 / 2

theorem sin_inv_oscSeq₂ (n : ℕ) : Real.sin (oscSeq₂ n)⁻¹ = √2 / 2

theorem cos_inv_oscSeq₂ (n : ℕ) : Real.cos (oscSeq₂ n)⁻¹ = -Real.sin (oscSeq₂ n)⁻¹

theorem deriv_oscillatorySquared_oscSeq₁ (n : ℕ) : deriv oscillatorySquared (oscSeq₁ n) = oscSeq₁ n - 1

theorem deriv_oscillatorySquared_oscSeq₂ (n : ℕ) : deriv oscillatorySquared (oscSeq₂ n) = oscSeq₂ n + 1

theorem deriv_oscillatorySquared_not_continuous_at_zero : ¬ContinuousAt (fun (x : ℝ) => deriv oscillatorySquared x) 0

theorem deriv_oscillatorySquared_sign_changes (ε : ℝ) : ε > 0 → ∃ (x₁ : ℝ) (x₂ : ℝ), x₁ ∈ Set.Ioo (-ε) ε ∧ x₂ ∈ Set.Ioo (-ε) ε ∧ deriv oscillatorySquared x₁ < 0 ∧ deriv oscillatorySquared x₂ > 0

theorem oscSeq₁_ne_zero (n : ℕ) : oscSeq₁ n ≠ 0

theorem oscSeq₂_ne_zero (n : ℕ) : oscSeq₂ n ≠ 0