Theorems · Definition · real analysis

CurveIntegrable

{𝕜 : 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] → {a b : E} → (E → E →L[𝕜] F) → Path a b → Prop

A 1-form ω is curve integrable along a path γ, if the function curveIntegralFun ω γ t = ω (γ t) (γ' t) is integrable on [0, 1]. The actual definition uses Path.extend γ, because both interval integrals and derivatives expect globally defined functions.

Defined in

Mathlib.MeasureTheory.Integral.CurveIntegral.Basic

Cited by

26 results in Mathlib

Foundations

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

Assumes

RCLikeNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace