exists_hasDerivWithinAt_eq_of_gt_of_lt

English

Darboux's theorem: if a ≤ b and for all x ∈ [a,b], HasDerivWithinAt f (f' x) on [a,b] x, and f'(a) < m < f'(b), then m lies in the image f' of the open interval (a,b).

Русский

Дарбок: если a ≤ b и на отрезке [a,b] производная имеет значения f'(x) и f'(a) < m < f'(b), то m достигается как значение производной на некоторой точке (a,b).

LaTeX

$$$\text{existsHasDerivWithinAtEqGtLt}$: \text{Darboux: } a \le b, \forall x \in [a,b], HasDerivWithinAt f (f'(x)) [a,b] x, \; f'(a) < m < f'(b) \Rightarrow m \in f' '' (Ioo a b)$$

Lean4

/-- **Darboux's theorem**: if `a ≤ b` and `f' a < m < f' b`, then `f' c = m` for some
`c ∈ (a, b)`. -/
theorem exists_hasDerivWithinAt_eq_of_gt_of_lt (hab : a ≤ b) (hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x)
    {m : ℝ} (hma : f' a < m) (hmb : m < f' b) : m ∈ f' '' Ioo a b :=
  by
  rcases hab.eq_or_lt with (rfl | hab')
  · exact (lt_asymm hma hmb).elim
  set g : ℝ → ℝ := fun x => f x - m * x
  have hg : ∀ x ∈ Icc a b, HasDerivWithinAt g (f' x - m) (Icc a b) x :=
    by
    intro x hx
    simpa using (hf x hx).sub ((hasDerivWithinAt_id x _).const_mul m)
  obtain ⟨c, cmem, hc⟩ : ∃ c ∈ Icc a b, IsMinOn g (Icc a b) c :=
    isCompact_Icc.exists_isMinOn (nonempty_Icc.2 <| hab) fun x hx => (hg x hx).continuousWithinAt
  have cmem' : c ∈ Ioo a b :=
    by
    rcases cmem.1.eq_or_lt with
      (rfl | hac)
        -- Show that `c` can't be equal to `a`

    · refine absurd (sub_nonneg.1 <| nonneg_of_mul_nonneg_right ?_ (sub_pos.2 hab')) (not_le_of_gt hma)
      have : b - a ∈ posTangentConeAt (Icc a b) a :=
        sub_mem_posTangentConeAt_of_segment_subset (segment_eq_Icc hab ▸ Subset.rfl)
      simpa only [ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply] using
        hc.localize.hasFDerivWithinAt_nonneg (hg a (left_mem_Icc.2 hab)) this
    rcases cmem.2.eq_or_lt' with
      (rfl | hcb)
        -- Show that `c` can't be equal to `b`

    · refine absurd (sub_nonpos.1 <| nonpos_of_mul_nonneg_right ?_ (sub_lt_zero.2 hab')) (not_le_of_gt hmb)
      have : a - b ∈ posTangentConeAt (Icc a b) b :=
        sub_mem_posTangentConeAt_of_segment_subset (by rw [segment_symm, segment_eq_Icc hab])
      simpa only [ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply] using
        hc.localize.hasFDerivWithinAt_nonneg (hg b (right_mem_Icc.2 hab)) this
    exact ⟨hac, hcb⟩
  use c, cmem'
  rw [← sub_eq_zero]
  have : Icc a b ∈ 𝓝 c := by rwa [← mem_interior_iff_mem_nhds, interior_Icc]
  exact (hc.isLocalMin this).hasDerivAt_eq_zero ((hg c cmem).hasDerivAt this)

Похожие утверждения