Theorems · Theorem · global analysis

Convex.exists_forall_hasFDerivWithinAt_of_hasFDerivWithinAt_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} {dω : E → E →L[ℝ] E →L[𝕜] F} [CompleteSpace F],
  Convex ℝ s →
    (∀ x ∈ s, HasFDerivWithinAt ω (dω x) s x) →
      (∀ a ∈ s, ∀ x ∈ tangentConeAt ℝ s a, ∀ y ∈ tangentConeAt ℝ s a, ((dω a) x) y = ((dω a) y) x) →
        ∃ f, ∀ a ∈ s, HasFDerivWithinAt f (ω a) s a

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

Defined in

Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare

Cited by

2 results in Mathlib

Foundations

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

Assumes

RCLikeNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceNormedSpaceNormedSpaceCompleteSpace