Theorems · Theorem · global analysis

ContinuousMap.Homotopy.curveIntegral_add_curveIntegral_eq_of_hasFDerivWithinAt

∀ {𝕜 : 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] {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 ↑γ₂),
  (∀ a_1 ∈ Set.Ioo 0 1, ∀ b_1 ∈ Set.Ioo 0 1, φ (a_1, b_1) ∈ t) →
    (∀ x ∈ t, HasFDerivWithinAt ω (dω x) t x) →
      ContinuousOn ω (closure t) →
        (∀ x ∈ t, ∀ u ∈ tangentConeAt ℝ t x, ∀ v ∈ tangentConeAt ℝ t x, ((dω x) u) v = ((dω x) v) u) →
          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.

Defined in

Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare

Cited by

2 results in Mathlib

Foundations

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

Assumes

RCLikeNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceNormedSpaceNormedSpace