strictAntiOn_deriv — Mathlib

English

If f is StrictConcaveOn on S and differentiableOn on S, then deriv f is StrictAntiOn on S.

Русский

Если fStrictConcaveOn на S и дифференцируема на S, то производная deriv f строго антимонотонна на S.

LaTeX

$$$\text{StrictConcaveOn}(\mathbb{R}, S, f)\land \text{DifferentiableOn}(\mathbb{R}, f, S)\Rightarrow \text{StrictAntiOn}(\operatorname{deriv} f)\ S.$$$

Lean4

theorem strictAntiOn_deriv (hfc : StrictConcaveOn ℝ S f) (hfd : ∀ x ∈ S, DifferentiableAt ℝ f x) :
    StrictAntiOn (deriv f) S := by simpa using (hfc.neg.strictMonoOn_deriv (fun x hx ↦ (hfd x hx).neg)).neg

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