Theorems · Definition · real analysis

IsSymmSndFDerivAt

(𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      {F : Type u_3} →
        [inst_1 : NormedAddCommGroup E] →
          [NormedSpace 𝕜 E] → [inst_3 : NormedAddCommGroup F] → [NormedSpace 𝕜 F] → (E → F) → E → Prop

Definition recording that a function has a symmetric second derivative at a point. This is automatic in most cases of interest (open sets over real or complex vector fields, or general case for analytic functions), but we can express theorems of calculus using this as a general assumption, and then specialize to these situations.

Defined in

Mathlib.Analysis.Calculus.FDeriv.Symmetric

Cited by

10 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace