Poincaré lemma for 1-forms

In this file we prove Poincaré lemma for 1-forms for convex sets. Namely, we show that a closed 1-form on a convex subset of a normed space is exact.

We also prove that the integrals of a closed 1-form along 2 curves that are joined by a C²-smooth homotopy are equal. In the future, this will allow us to prove Poincaré lemma for simply connected open sets and, more generally, for simply connected locally convex sets.

Implementation notes

In this file, we represent a 1-form as ω : E → E →L[𝕜] F, where 𝕜 is ℝ or ℂ, not as ω : E → E [⋀^Fin 1]→L[𝕜] F. A 1-form represented this way is closed iff its Fréchet derivative dω : E → E →L[𝕜] E →L[𝕜] F is symmetric, dω a x y = dω a y x.

theorem ContinuousMap.Homotopy.curveIntegral_add_curveIntegral_eq_of_hasFDerivWithinAt_off_countable {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace ℝ E] [NormedSpace ℝ F] {a b c d : E} {γ₁ : Path a b} {γ₂ : Path c d} {s : Set (↑unitInterval × ↑unitInterval)} {t : Set E} {ω : E → E →L[𝕜] F} {dω : E → E →L[ℝ] E →L[𝕜] F} (φ : (↑γ₁).Homotopy ↑γ₂) (hs : s.Countable) (hφt : ∀ a_1 ∈ Set.Ioo 0 1, ∀ b_1 ∈ Set.Ioo 0 1, φ (a_1, b_1) ∈ t) (hω : ∀ a_1 ∈ Set.Ioo 0 1, ∀ b_1 ∈ Set.Ioo 0 1, (a_1, b_1) ∉ s → HasFDerivWithinAt ω (dω (φ (a_1, b_1))) t (φ (a_1, b_1))) (hωc : ContinuousOn ω (closure t)) (hdω_symm : ∀ a_1 ∈ Set.Ioo 0 1, ∀ b_1 ∈ Set.Ioo 0 1, (a_1, b_1) ∉ s → ∀ u ∈ tangentConeAt ℝ t (φ (a_1, b_1)), ∀ v ∈ tangentConeAt ℝ t (φ (a_1, b_1)), ((dω (φ (a_1, b_1))) u) v = ((dω (φ (a_1, b_1))) v) u) (hcontdiff : ContDiffOn ℝ 2 (fun (xy : ℝ × ℝ) => Set.IccExtend ⋯ (⇑(φ.extend xy.1)) xy.2) (Set.Icc 0 1)) : ∫ᶜ (x : E) in γ₁, ω x + ∫ᶜ (x : E) in φ.evalAt 1, ω x = ∫ᶜ (x : E) in γ₂, ω x + ∫ᶜ (x : E) in φ.evalAt 0, ω x

The curve integral of a closed 1-form along the boundary of the image of a unit square under a smooth map is zero. We may ignore the behavior on a countable set.

This theorem is stated in terms of a $$C^2$$ homotopy between two paths.

theorem ContinuousMap.Homotopy.curveIntegral_add_curveIntegral_eq_of_hasFDerivWithinAt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace ℝ E] [NormedSpace ℝ F] {a b c d : E} {γ₁ : Path a b} {γ₂ : Path c d} {t : Set E} {ω : E → E →L[𝕜] F} {dω : E → E →L[ℝ] E →L[𝕜] F} (φ : (↑γ₁).Homotopy ↑γ₂) (hφt : ∀ a_1 ∈ Set.Ioo 0 1, ∀ b_1 ∈ Set.Ioo 0 1, φ (a_1, b_1) ∈ t) (hω : ∀ x ∈ t, HasFDerivWithinAt ω (dω x) t x) (hωc : ContinuousOn ω (closure t)) (hdω_symm : ∀ x ∈ t, ∀ u ∈ tangentConeAt ℝ t x, ∀ v ∈ tangentConeAt ℝ t x, ((dω x) u) v = ((dω x) v) u) (hcontdiff : ContDiffOn ℝ 2 (fun (xy : ℝ × ℝ) => Set.IccExtend ⋯ (⇑(φ.extend xy.1)) xy.2) (Set.Icc 0 1)) : ∫ᶜ (x : E) in γ₁, ω x + ∫ᶜ (x : E) in φ.evalAt 1, ω x = ∫ᶜ (x : E) in γ₂, ω x + ∫ᶜ (x : E) in φ.evalAt 0, ω x

The curve integral of a closed 1-form along the boundary of the image of a unit square under a smooth map is zero.

This theorem is stated in terms of a $$C^2$$ homotopy between two paths.

theorem ContinuousMap.Homotopy.curveIntegral_add_curveIntegral_eq_of_diffContOnCl {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace ℝ E] [NormedSpace ℝ F] {a b c d : E} {γ₁ : Path a b} {γ₂ : Path c d} {t : Set E} {ω : E → E →L[𝕜] F} (φ : (↑γ₁).Homotopy ↑γ₂) (hφt : ∀ a_1 ∈ Set.Ioo 0 1, ∀ b_1 ∈ Set.Ioo 0 1, φ (a_1, b_1) ∈ t) (hω : DiffContOnCl ℝ ω t) (hdω_symm : ∀ x ∈ t, ∀ u ∈ tangentConeAt ℝ t x, ∀ v ∈ tangentConeAt ℝ t x, ((fderivWithin ℝ ω t x) u) v = ((fderivWithin ℝ ω t x) v) u) (hcontdiff : ContDiffOn ℝ 2 (fun (xy : ℝ × ℝ) => Set.IccExtend ⋯ (⇑(φ.extend xy.1)) xy.2) (Set.Icc 0 1)) : ∫ᶜ (x : E) in γ₁, ω x + ∫ᶜ (x : E) in φ.evalAt 1, ω x = ∫ᶜ (x : E) in γ₂, ω x + ∫ᶜ (x : E) in φ.evalAt 0, ω x

The curve integral of a closed 1-form along the boundary of the image of a unit square under a smooth map is zero, a version stated in terms of DiffContOnC1.

This theorem is stated in terms of a $$C^2$$ homotopy between two paths.

theorem Convex.curveIntegral_segment_add_eq_of_hasFDerivWithinAt_symmetric {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace ℝ E] [NormedSpace ℝ F] {a b c : E} {s : Set E} {ω : E → E →L[𝕜] F} {dω : E → E →L[ℝ] E →L[𝕜] F} (hs : Convex ℝ s) (hω : ∀ x ∈ s, HasFDerivWithinAt ω (dω x) s x) (hdω : ∀ a ∈ s, ∀ x ∈ tangentConeAt ℝ s a, ∀ y ∈ tangentConeAt ℝ s a, ((dω a) x) y = ((dω a) y) x) (ha : a ∈ s) (hb : b ∈ s) (hc : c ∈ s) : ∫ᶜ (x : E) in Path.segment a b, ω x + ∫ᶜ (x : E) in Path.segment b c, ω x = ∫ᶜ (x : E) in Path.segment a c, ω x

If ω is a closed 1-form on a convex set, then ∫ᶜ x in Path.segment a b, ω x + ∫ᶜ x in Path.segment b c, ω x = ∫ᶜ x in Path.segment a c, ω x for all a b c ∈ s.

This is the key lemma used to establish that closed a 1-form on a convex set has a primitive.

theorem Convex.hasFDerivWithinAt_curveIntegral_segment_of_hasFDerivWithinAt_symmetric {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace ℝ E] [NormedSpace ℝ F] {a b : E} {s : Set E} {ω : E → E →L[𝕜] F} {dω : E → E →L[ℝ] E →L[𝕜] F} [CompleteSpace F] (hs : Convex ℝ s) (hω : ∀ x ∈ s, HasFDerivWithinAt ω (dω x) s x) (hdω : ∀ a ∈ s, ∀ x ∈ tangentConeAt ℝ s a, ∀ y ∈ tangentConeAt ℝ s a, ((dω a) x) y = ((dω a) y) x) (ha : a ∈ s) (hb : b ∈ s) : HasFDerivWithinAt (fun (x : E) => ∫ᶜ (x : E) in Path.segment a x, ω x) (ω b) s b

If ω is a closed 1-form on a convex set s, then the function given by F b = ∫ᶜ x in Path.segment a b, ω x is a primitive of ω on s, i.e., dF = ω.

theorem Convex.exists_forall_hasFDerivWithinAt_of_hasFDerivWithinAt_symmetric {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace ℝ E] [NormedSpace ℝ F] {s : Set E} {ω : E → E →L[𝕜] F} {dω : E → E →L[ℝ] E →L[𝕜] F} [CompleteSpace F] (hs : Convex ℝ s) (hω : ∀ x ∈ s, HasFDerivWithinAt ω (dω x) s x) (hdω : ∀ a ∈ s, ∀ x ∈ tangentConeAt ℝ s a, ∀ y ∈ tangentConeAt ℝ s a, ((dω a) x) y = ((dω a) y) x) : ∃ (f : E → 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.

theorem Convex.exists_forall_hasFDerivWithinAt_of_fderivWithin_symmetric {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace ℝ E] [NormedSpace ℝ F] {s : Set E} {ω : E → E →L[𝕜] F} [CompleteSpace F] (hs : Convex ℝ s) (hω : DifferentiableOn ℝ ω s) (hdω : ∀ a ∈ s, ∀ x ∈ tangentConeAt ℝ s a, ∀ y ∈ tangentConeAt ℝ s a, ((fderivWithin ℝ ω s a) x) y = ((fderivWithin ℝ ω s a) y) x) : ∃ (f : E → 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 fderivWithin.

theorem Convex.exists_forall_hasFDerivAt_of_fderiv_symmetric {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace ℝ E] [NormedSpace ℝ F] {s : Set E} {ω : E → E →L[𝕜] F} [CompleteSpace F] (hs : Convex ℝ s) (hso : IsOpen s) (hω : DifferentiableOn ℝ ω s) (hdω : ∀ a ∈ s, ∀ (x y : E), ((fderiv ℝ ω a) x) y = ((fderiv ℝ ω a) y) x) : ∃ (f : E → 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.

theorem Convex.exists_forall_hasDerivWithinAt {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {f : 𝕜 → E} {s : Set 𝕜} (hs : Convex ℝ s) (hf : DifferentiableOn 𝕜 f s) : ∃ (g : 𝕜 → E), ∀ a ∈ s, HasDerivWithinAt g (f a) s a

If f : 𝕜 → E, 𝕜 = ℝ or 𝕜 = ℂ, is differentiable on a convex set s, then it admits a primitive.