Namespace for pathIntegral

Stream: mathlib4

[Yury G. Kudryashov]

In #24754, I define the integral of a 1-form (given as E → E →L[𝕜] F) along a (piecewise smooth) Path. @Sébastien Gouëzel asks me to move the whole thing to a namespace, e.g., ContinuousLinearMap, because we're going to have more notions of a "path integral" in the future, including

• integral of a function f : ℂ → E along a path;
• integral of a 1-form along a path on a manifold;
• path integral of a section of a vector bundle with a connection along a path in the base;
• Feynman path integral (one or more definitions).

IMHO, we should decide on names for these notions now, before merging #24754. WDYT?

[Scott Carnahan]

My informal training usually used contour integral for integrating f : ℂ → E along a path, and line integral for the integral of a 1-form along a path on a manifold.

[Robert Maxton]

As a physicist, I'm obligated to advocate reserving 'path integral' for, if not the Feynman path integral specifically, at least the general notion of "integrating a functional over a space of functions" :p

[Robert Maxton]

Whiiiich I think might be your third case, actually?

[Robert Maxton]

Hmmm, maybe PathIntegral for the general notion in terms of topologies, abstract spaces and vector bundles, and FunctionalIntegral or even FeynmanIntegral for the more concrete case where everything's in ℝ or ℂ or similar?

[Yury G. Kudryashov]

One more notion: integral of a scalar function w.r.t. arclength/variation.

[Yury G. Kudryashov]

WDYT about this?

• lineIntegral for #24754 (should notation still say ^p or should I switch to ^l?) Wikipedia says that it's more common, though "path integral" and "curve integral" are listed as alternative names
• contourIntegral for functions on Complex
• mlineIntegral for the integral of a 1-form on a manifold
• for sections of vector bundles, is there a notion of an integral, or only parallel transport/holonomy? If yes, what's the codomain?
• reserve variations of pathIntegral for Feynman-like integrals.

[Sébastien Gouëzel]

I don't like lineIntegral for #24754 because there is no line here. Although it may be a language issue -- we definitely don't use the corresponding "intégrale de ligne" in French, but if it's completely standard in English then we should probably go for it.

[Patrick Massot]

I would never naturally associate the terminology path integral to anything but Feynman stuff. And I’ve never seen “line integral”. But, like Sébastien, my dialect of English is Frenglish.

[Yury G. Kudryashov]

My English is Runglish, so I've tried to base the names on English Wikipedia which uses https://en.wikipedia.org/wiki/Line_integral as the main name.

In mathematics, a line integral is an integral where the function to be integrated is evaluated along a curve.[1] The terms path integral, curve integral, and curvilinear integral are also used; contour integral is used as well, although that is typically reserved for line integrals in the complex plane.

[Yury G. Kudryashov]

It would be nice to get more opinions of native speakers.

[Matthew Ballard]

Pedantic: ParamCurveIntegralor some permutation. Line integral would be the most common literature term for me.

[Robert Maxton]

Line integral is indeed the name I was taught in the US. It may not be 'straight' but it's topologically a line!

[Jireh Loreaux]

The Wikipedia entry I believe is representative of English usage. Surely "line integral" appears throughout calculus texts. However, I agree that such terminology is a bit strange.

Personally, I would advocate for pathIntegral in the current PR. For physics, FeynmanIntegral or FeynmanPathIntegral` I think are reasonable.

[Yury G. Kudryashov]

/poll Name for the integral of a 1-form along a path in a normed space (may be generalized to TVS soon)
pathIntegral, may need to be renamed when we come to Feynman integrals
lineIntegral, non-native speakers may assume that it's about straight lines
curveIntegral
curvelinearIntegral

[Yury G. Kudryashov]

I've created a poll. For me, going forward with pushing Poincaré theorem for 1-forms into Mathlib is more important than choosing the best name, so I voted for all 4 names from Wikipedia.

[Antoine Chambert-Loir]

(arcIntegral, by analogy with “arcwise connectedness”, but this may not be a good idea at all because that notion often implies “injective paths” — which, topologically; would then be lines, as noted by @Robert Maxton)

[Yury G. Kudryashov]

I want to reserve something like arclenIntegral for the integral w.r.t. the measure defined by docs#eVariationOn

[Yury G. Kudryashov]

So far, the first 3 options are tied. Let's wait for 2 more days.

[Yury G. Kudryashov]

curveIntegral has 2 more voices than the first 2 options, so I'll go with it. How should we tell a curve integral from a contour integral in the notation? Both naturally abbreviate to ∫ᶜ.

[Yury G. Kudryashov]

A potential "pro" of the lineIntegral name is that we can use ˡ or ᴸ for line/curve integrals and ᶜ for contour integrals.

[Yury G. Kudryashov]

While we can use lowercase and uppercase superscript C for curve/contour, it's harder to distinguish them.

[Jireh Loreaux]

Can't we use a different unicode character? Maybe ∮ for contour integral?

[Yury G. Kudryashov]

This notation suggests cyclic paths, but it makes sense to integrate complex functions along other paths too.

[Jireh Loreaux]

Sure, it suggests cyclic paths, but when I teach complex analysis I use it for either one, especially because the cyclic case is the most common one (or, at least along paths which together constitute a cyclic path).

[Yury G. Kudryashov]

I think I'll migrate the current pr to curveIntegral and notation with superscript c. We can decide about notation for contour integrals when we add them.

[Robert Maxton]

I was under the impression that ∮ was standard, yes. (And at least in my field, most of the time when we take 'open' contour integrals we're actually 'closing them at infinity' so we can keep using the residue theorem, so they're still cyclic.)

[Yury G. Kudryashov]

E.g., you need integrals over non closed contours to prove existence of an antiderivative