Poincaré lemma

Stream: maths

[Yury G. Kudryashov]

Hi,

I have a sorry-free proof of the following lemma, see #24019:

theorem Convex.exists_forall_hasFDerivAt_of_fderiv_symmetric {E F : Type*} [NormedAddCommGroup E]
  [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {s : Set E} (hs : Convex ℝ s)
  (hso : IsOpen s) {ω : E → E →L[ℝ] F} (hω : DifferentiableOn ℝ ω s)
  (hdω : ∀ a ∈ s, ∀ (x y : E), fderiv ℝ ω a x y = fderiv ℝ ω a y) x : ∃ f, ∀ a ∈ s, HasFDerivAt f (ω a) a

Note that this theorem doesn't assume continuity of fderiv ℝ ω. There are some versions for non-open convex sets and HasFDerivWithinAt too.

[Yury G. Kudryashov]

The code needs a lot of polishing before it will be ready for review.

[Yury G. Kudryashov]

Also, I want to generalize from convex sets to simply connected open sets.

[Yury G. Kudryashov]

CC: @Alex Kontorovich This is a more general version of #9598 I promised a long time ago.

[Yury G. Kudryashov]

(I need to generalize some derivatives to RCLike to make it strictly more general)

[Yury G. Kudryashov]

I've tried to prove a similar theorem (without assuming $C^1$) for k-forms, but I've hit the following roadblock: given a differentiable $\omega\in\Omega^{k+1}(E, F)$ with zero exterior derivative, I can show (not formalized yet) that there exists a $k$-form $\eta(a)=\int_0^1 i_a\omega(ta)\,dt$ such that ω and η satisfy the Stokes theorem (at least, for nice domains like cubes). However, I can't show differentiability of η without assuming $C^1$ smoothness of $\omega$.

[Yury G. Kudryashov]

Is this version (with Stokes theorem but no Fréchet differentiability of $\eta$) (a) interesting? (b) published?

[Dominic Steinitz]

How do one forms here relate to https://github.com/urkud/DeRhamCohomology?

[Sam Lindauer]

Dominic Steinitz said:

How do one forms here relate to https://github.com/urkud/DeRhamCohomology?

(Alternating) forms on normed spaces are defined as follows in https://github.com/urkud/DeRhamCohomology :

notation "Ω^" n "⟮" E ", " F "⟯" => E → E [⋀^Fin n]→L[ℝ] F

where E [⋀^Fin n]→L[ℝ] F is the notation for an n-alternating map over ℝ from E to F. In the repository, there exists an equivalence ofSubsingleton between this definition for n = 1 and the definition used by Yury above:

def ofSubsingleton :
    (E → E →L[ℝ] F) ≃ (Ω^1⟮E, F⟯) where
  toFun f := fun e ↦ ContinuousAlternatingMap.ofSubsingleton ℝ E F 0 (f e)
  invFun f := fun e ↦ (ContinuousAlternatingMap.ofSubsingleton ℝ E F 0).symm (f e)
  left_inv _ := rfl
  right_inv _ := by simp

[Yury G. Kudryashov]

I took the fastest route to the result in this branch. Before actually merging it, we need to decide:

• should we use E → E →L[ℝ] F or E → E [⋀^Fin 1]→L[ℝ] F? we can convert both ways, but the former may be more convenient in some cases;
• what should be the higher rank version of pathIntegral?
• should we use docs#Path or maps from ℝ with a specified start and end points?
• should we use symmetry of fderiv ℝ ω (makes sense with E → E →L[ℝ] F) or ederiv ℝ ω = 0 (ederiv is defined in https://github.com/urkud/DeRhamCohomology)?
• what parts need derivatives "within" sets?
• what about extension to the boundary for sets that are more complicated than convex sets?
• what parts should be generalized to RCLike? E.g., do we allow E → E →L[ℝ] F / E → E [⋀^Fin 1]→L[K] F in the definition of pathIntegral or force users to use restrictScalars if needed?

[Yury G. Kudryashov]

Suggestions are welcome!