Theorems · Theorem · real analysis

Convex.second_derivative_within_at_symmetric_of_mem_interior

∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {s : Set E},
  Convex ℝ s →
    ∀ {f : E → F} {f' : E → E →L[ℝ] F} {f'' : E →L[ℝ] E →L[ℝ] F},
      (∀ x ∈ interior s, HasFDerivAt f (f' x) x) →
        ∀ {x : E},
          x ∈ s →
            HasFDerivWithinAt f' f'' (interior s) x →
              ∀ {v w : E}, x + 4 • v ∈ interior s → x + 4 • w ∈ interior s → (f'' w) v = (f'' v) w

Assume that f is differentiable inside a convex set s, and that its derivative f' is differentiable at a point x. Then, given two vectors v and w pointing inside s, one has f'' v w = f'' w v. Superseded by Convex.second_derivative_within_at_symmetric, which removes the assumption that v and w point inside s.

Defined in

Mathlib.Analysis.Calculus.FDeriv.Symmetric

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace