∀ {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 →
                    (fun h =>
                        f (x + h • (2 • v + 2 • w)) + f (x + h • (v + w)) - f (x + h • (2 • v + w)) -
                            f (x + h • (v + 2 • w)) -
                          h ^ 2 • (f'' v) w) =o[nhdsWithin 0 (Set.Ioi 0)]
                      fun h => h ^ 2