Theorems · Theorem · global analysis

Convex.exists_forall_hasFDerivAt_of_fderiv_symmetric

∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [inst_5 : NormedSpace ℝ E]
  [inst_6 : NormedSpace ℝ F] {s : Set E} {ω : E → E →L[𝕜] F} [CompleteSpace F],
  Convex ℝ s →
    IsOpen s →
      DifferentiableOn ℝ ω s →
        (∀ a ∈ s, ∀ (x y : E), ((fderiv ℝ ω a) x) y = ((fderiv ℝ ω a) y) x) → ∃ f, ∀ a ∈ s, HasFDerivAt f (ω a) a

If ω is a closed 1-form on an open convex set s, then it admits a primitive, a version stated in terms of fderiv.

Defined in

Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare

Cited by

0 results in Mathlib

Foundations

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

Assumes

RCLikeNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceNormedSpaceNormedSpaceCompleteSpace