Theorems · Definition · real analysis

curveIntegral

{𝕜 : Type u_4} →
  {E : Type u_5} →
    {F : Type u_6} →
      [inst : RCLike 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup F] → [inst_4 : NormedSpace 𝕜 F] → {a b : E} → (E → E →L[𝕜] F) → Path a b → F

Integral of a 1-form ω : E → E →L[𝕜] F along a path γ, defined as $\int_0^1 \omega(\gamma(t))(\gamma'(t))$. The actual definition uses curveIntegralFun which uses Path.extend γ and derivWithin (Path.extend γ) (Set.Icc 0 1) t, because calculus-related definitions in Mathlib expect globally defined functions as arguments.

Defined in

Mathlib.MeasureTheory.Integral.CurveIntegral.Basic

Cited by

32 results in Mathlib

Foundations

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

Assumes

RCLikeNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace