interval integral: do we need `α ≠ real`?

Stream: maths

[Yury G. Kudryashov]

Currently ∫ x in a..b, f x ∂μ works for x : α with [linear_order α]. Do we ever need α ≠ real?

[Patrick Massot]

We could need a subtype of reals I guess (but I never did)

[Yury G. Kudryashov]

I tried to use subtype once and decided to extend the function to all reals instead

[Yury G. Kudryashov]

Lots of important theorems (at least FTC and its reverse dependencies) only work for reals.

[Kevin Buzzard]

I know plenty of exotic integrals on profinite spaces but none of the base objects ever have a total order

[Yury G. Kudryashov]

/poll Should we restrict the definition of interval integral to functions from reals?
Yes
No

[Yury G. Kudryashov]

My reasons: (a) I never used interval integrals over other types; (b) it's easier to assume the domain to be real than to add appropriate typeclass assumptions here and there.

[Jireh Loreaux]

Personally, I would be hesitant to restrict it because then it wouldn't apply to nnreal. But my opinion probably shouldn't matter that much; I don't have tons of experience.

[Johan Commelin]

Do you suggest to simply use manifolds for all other use cases? Jireh just mentioned nnreal. I could also imagine putting a linear order on { (x,c) | x ∈ ℝ} or {(x,x) | x ∈ ℝ}. Things like that. But in the end, whatever is said about these integrals must probably be converted to an honest integral on honest ℝ. So that conversion could also be done upfront.

[Yury G. Kudryashov]

I suggest to use ∫ x in Ioc a b, f x ∂μ in other cases.

[Reid Barton]

So basically the question is about when you need $\int_b^a = - \int_a^b$?

[Yury G. Kudryashov]

Yes

[Yury G. Kudryashov]

It would be nice to have more votes here.

[Yury G. Kudryashov]

@Johan Commelin Do I understand correctly that you abstain? If yes, could you please do it explicitly? Thanks!

[Yury G. Kudryashov]

I have two reasons to migrate to α = ℝ: the first one is written above (we can stop worrying about typeclass assumptions on α); the second is that now Lean can't correctly parse ∫ x in 0..π, complex.exp x

[Yury G. Kudryashov]

And it's even worse with ∫ x in 0..1, x because if we introduce a volume on ℕ, then it will parse as ∫ n : ℕ in 0..1, n.

[Johan Commelin]

Done. Although you just listed some good reasons why to specialize to ℝ.

[Floris van Doorn]

I'm a little worried about restricting the definition and realizing later that the interval integral would be nice on some other type. But changing it does make it more convenient to use, so I vote a tentative "yes".