Stokes' theorem on singular…

TheoremStokes' theorem on singular `1`-chains #

The integral of dψ along a singular 1-chain is the evaluation of the 0-form ψ on its boundary.

TauCeti.chainsDesc_pathClassIntegral_mextDeriv.{u_1, u_2} {E : Type u_1} {H : Type u_2} {M F : Type}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H}
  [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F]
  [FiniteDimensional ℝ E] [T2Space M] [IsManifold I (↑⊤) M] [CompleteSpace F]
  {ψ : TauCeti.RoughForm I M F 0} (hψ : TauCeti.IsSmoothForm I 2 ψ) :
  (TauCeti.chainsDesc fun s =>
      TauCeti.pathClassIntegral (TauCeti.mextDeriv ψ)
        (Path.Homotopic.Quotient.mk (TauCeti.TopCat.path₁ s))) =
    (TauCeti.chainsDesc fun v => (ψ (TopCat.toSSetObj₀Equiv v)) 0) ∘ₗ
      ModuleCat.Hom.hom (((TauCeti.singularChains ℤ).obj ↧M).d 1 0)