Theorems · Theorem · real analysis

isMinOn_Ioc_of_deriv

∀ {f : ℝ → ℝ} {a b c : ℝ},
  ContinuousAt f b →
    ContinuousAt f c →
      DifferentiableOn ℝ f (Set.Ioo a b) →
        DifferentiableOn ℝ f (Set.Ioo b c) →
          (∀ x ∈ Set.Ioo a b, deriv f x ≤ 0) → (∀ x ∈ Set.Ioo b c, 0 ≤ deriv f x) → IsMinOn f (Set.Ioc a c) b

Suppose f : ℝ → ℝ is continuous at b and c, the derivative f' is nonpositive on Ioo a b and nonnegative on Ioo b c. Then f attains its minimum on Ioc a c at b.

Defined in

Mathlib.Analysis.Calculus.DerivativeTest

Cited by

0 results in Mathlib

Foundations

Depth 192 from the axioms · uses propext, Classical.choice, Quot.sound