Integral notation

Stream: mathlib4

[Yury G. Kudryashov]

In Lean 4, ∫ x, f x ∂μ = 5 has to be written as (∫ x, f x ∂μ) = 5.

[Yury G. Kudryashov]

This was not the case in Lean 3.

[Mario Carneiro]

is this the same issue as the one about sum precedence?

[Yury G. Kudryashov]

This is about Lean 4 notation, not about mathport output.

[Mario Carneiro]

maybe it's just missing a precedence then

[Yury G. Kudryashov]

It's

@[inherit_doc MeasureTheory.integral]
notation3"∫ "(...)", "r:(scoped f => f)" ∂"μ => integral μ r

[Mario Carneiro]

there are no precedences there...

[Mario Carneiro]

this is probably a post-mathport issue

[Yury G. Kudryashov]

What is the right precedence for the measure?

[Mario Carneiro]

mathport is fixed but bugfixes in mathport don't propagate to all the files that are already ported

[Mario Carneiro]

so go find that line in current mathport output and apply it

[Mario Carneiro]

https://github.com/leanprover-community/mathlib3port/commit/3fdc57bc6b5ce9c256c25248e07a1971dafe7620

[Mario Carneiro]

-- mathport name: «expr∫ , ∂ »
notation3"∫ "(...)", "r:60:(scoped f => f)" ∂"μ:70 => integral μ r

-- mathport name: «expr∫ , »
notation3"∫ "(...)", "r:60:(scoped f => integral volume f) => r

-- mathport name: «expr∫ in , ∂ »
notation3"∫ "(...)" in "s", "r:60:(scoped f => f)" ∂"μ:70 => integral (Measure.restrict μ s) r

-- mathport name: «expr∫ in , »
notation3"∫ "(...)" in "s", "r:60:(scoped f => integral Measure.restrict volume s f) => r

[Yury G. Kudryashov]

Thank you!

[Yury G. Kudryashov]

I'll test it.

[Eric Wieser]

Mario Carneiro said:

mathport is fixed but bugfixes in mathport don't propagate to all the files that are already ported

Perhaps we should have been putting the mathport version in the header comment too so that it was easier to track these down

[Eric Wieser]

Another obvious one is open vs open scoped

[Jireh Loreaux]

It should be possible to get an estimated mathport version from the mathlib3 SHA in the header. This may not pick up on things that have had forward ports, but it could be helpful as a first approximation.

[Eric Wieser]

!4#4960 cleans up the majority of the open scoped/open mismatches

[Eric Wieser]

Annoyingly it's hard to fix this kind of thing because we did random cleanup when porting files (such as merging together open commands), and now it's hard to apply the diffs from mathport...

[Yury G. Kudryashov]

I have a branch with precedences for integral notation, I'll fix compile and open a PR tonight.

[Yury G. Kudryashov]

While copying integral notation from mathlib3port, I noticed that mathport often omits parentheses around restrict _ _.

[Yury G. Kudryashov]

See any of its "set integral" notation commands.

[Yury G. Kudryashov]

(e.g., in MeasureTheory.Integral.Bochner)

[Mario Carneiro]

Do you mean like here:

notation3"∫ "(...)" in "s", "r:60:(scoped f => integral Measure.restrict volume s f) => r

[Mario Carneiro]

which I guess should be

notation3"∫ "(...)" in "s", "r:60:(scoped f => integral (Measure.restrict volume s) f) => r

[Mario Carneiro]

I would guess that the parenthesizer doesn't work inside notations for some reason

[Yury G. Kudryashov]

Yes, here.

[Yury G. Kudryashov]

A more important question: ∫ x in 0..2 * π, f x doesn't work, ∫ x in (0)..2 * π, f x works

[Mario Carneiro]

presumably another precedence issue

[Mario Carneiro]

what's the notation?

[Yury G. Kudryashov]

It's in IntervalIntegral

[Yury G. Kudryashov]

The error message says "invalid projection, structure has only 1 field(s)"

[Mario Carneiro]

hm, maybe another parser is triggering on it

[Yury G. Kudryashov]

https://github.com/leanprover-community/mathlib4/pull/4963/files#diff-896f2f3c71fb2f7eaa4fcfab2a525c0d02b0879311e75727ef42dfea851f55bc

[Yury G. Kudryashov]

It tries to interpret 0. as a dot-notation on 0

[Mario Carneiro]

does it work if you replace ".." by "." "."?

[Yury G. Kudryashov]

I'll try.

[Mario Carneiro]

also try adding a space like 0 .. 2 pi

[Yury G. Kudryashov]

Adding a space breaks notation too, with 0 or without.

[Mario Carneiro]

Actually I think it's not a dot notation on 0, it's a float literal

[Mario Carneiro]

0. is a float literal apparently

[Mario Carneiro]

Right, .. is not a good token because it's legal after an expression

[Mario Carneiro]

f .. means f _ _ _ for however many _ are needed

[Yury G. Kudryashov]

We can change notation for interval integral.

[Yury G. Kudryashov]

(or we can postpone this decision)

[Mario Carneiro]

how about ∫ _ in [a, b], r ∂μ

[Yury G. Kudryashov]

Note that we have ∫ _ in s, r ∂μ, where s is a set.

[Mario Carneiro]

true, but sets starting with [ are rare, no?

[Mario Carneiro]

and you can use a ( to disambiguate

[Yury G. Kudryashov]

And here comes localized notation for docs4#Set.uIcc (was [a, b] in mathlib3).

[Mario Carneiro]

well, those should be equal so it's fine :grinning:

[Yury G. Kudryashov]

No, they are not equal because of the sign.

[Yury G. Kudryashov]

∫ _ in 1..0, 1 = -1

[Yury G. Kudryashov]

The sign is the only reason why intervalIntegral exists as a separate definition.

[Mario Carneiro]

∫ₐᵇ x, f x ∂μ :see_no_evil:

[Yury G. Kudryashov]

We don't have a superscript pi.

[Mario Carneiro]

I think in practice we will want to use a composite version of the superscript parser and one that takes an explicit ^(expr) for when you can't do it with unicode

[Yury G. Kudryashov]

I mean, ∫_{a}^{b} x, f x ∂μ is closest to LaTeX...

[Yury G. Kudryashov]

Is it a problem that _{}^ are used elsewhere too?

[Mario Carneiro]

no, although this is more than notation3 will handle

[Mario Carneiro]

the fact that there is an initial (relatively) unique token helps a lot here

[Yury G. Kudryashov]

Parses:

notation3"∫_{"a"}^{"b"}"(...)", "r:60:(scoped f => intervalIntegral f a b volume) => r

example : ∫_{0}^{1} _, (0 : ℝ) = 0 := sorry

[Mario Carneiro]

oh I meant if you have multiple options for how to write the bounds

[Yury G. Kudryashov]

What other options do you want to have?

[Mario Carneiro]

maybe leaving off the braces, or using the superscript parser

[Mario Carneiro]

also you probably want to split the initial token or else it will break the other integral parsers

[Yury G. Kudryashov]

As a person who often writes 2^{3} in LaTeX, I don't care.

[Yury G. Kudryashov]

It doesn't: I added it after

notation3"∫ "(...)" in "a".."b", "r:60:(scoped f => intervalIntegral f a b volume) => r

and the file compiles.

[Yury G. Kudryashov]

I'll make a PR after !4#4963 gets merged.

[Yury G. Kudryashov]

What else should I edit to tell mathport to change old notation to the new one?

[Yury G. Kudryashov]

Or should I leave both options for now?

[Yury G. Kudryashov]

BTW, should we add notation for integrals over Iio a and Ioi a? Something like

notation3"∫_-∞^{"b"}"(...)", "r:60:(scoped f => integral f (restrict volume (Iio b))) => r

[Mario Carneiro]

you can't, right now, unless mathport hardcodes the new notation or you backport it to lean 3

[Mario Carneiro]

and I guess backporting doesn't actually do the rewriting for you

[Mario Carneiro]

how about skipping the braces for those?

[Mario Carneiro]

I'm still worried about the long tokens though, I'm pretty sure lean uses a longest match parse for the tokens and this might make some cases not apply

[Yury G. Kudryashov]

It's hard for me to skip braces around -∞: then the infinity symbol won't be a subscript!

[Mario Carneiro]

is using ⊥ too weird?

[Yury G. Kudryashov]

I tried adding new nothation both before and after the existing one, in each case file compiles.

[Yury G. Kudryashov]

Yes, it is too weird.

[Yury G. Kudryashov]

OK, I'm going to bed soon. I'll think about it again tomorrow.

[Mario Carneiro]

too bad there is no unicode subscript infinity

[Yury G. Kudryashov]

!3#19225 changes notation in Mathlib 3

[Sebastien Gouezel]

Are you sure it's more readable? Comparing in one of the first instances in the diff ∫ x in (-r:ℝ)..r to ∫_{(-r:ℝ)}^{r} x, I am not convinced (but maybe it's just because it takes some time to get used to it).

[Yury G. Kudryashov]

You can drop the type annotation.

[Yury G. Kudryashov]

I did a search&replace, so I didn't drop them.

[Yury G. Kudryashov]

The main issue with the current notation is that ∫ x in 0..r, x doesn't work in Lean 4 (see above).

[Yury G. Kudryashov]

We have a workaround ∫ x in (0)..r, x but it looks strange.

[Kyle Miller]

Would ∫ x in [0 : r], f x be too weird? Lean 4 already has [0:r] for a kind of interval notation (for natural number ranges), so it's at least parseable, and it even sort of looks like a closed interval.

[Yury G. Kudryashov]

For me, the main argument pro ∫_{a}^{b} is that it's what we write in LaTeX

[Yury G. Kudryashov]

In fact, I see no problem with ∫_{a}^{b} fun x => f x so that ∫_{a}^{b} (f - g) is a thing.

[Yury G. Kudryashov]

(but I'm ready to use any other notation that works)

[Kyle Miller]

Yeah, I figured it was LaTeX-inspired, though the way x works in ∫_{0}^{r} x, f x isn't very familiar

[Kyle Miller]

Here's another thought: if we defined I[a, b] to be I a b (this special notation is to help eliminate some parentheses and to look like a closed interval) then ∫ x in I[0, r], f x could rely on the ∫ x in s, f x notation

[Yury G. Kudryashov]

No, the main point of the interval integral notation is that it works for b < a: (∫ x in 1..0, 1) = -1

[Kyle Miller]

Oops, I was accidentally looking at the average integral in the PR

[Kyle Miller]

For the ∫ x in s, f x ambiguity, Mario and I discussed some ideas for extending the notation3 command to be able to give special interpretations of extended binders, so it's possible that we could have ∫ x ∈ s, f x with the same meaning (and similarly for Finset.prod/Finset.sum notation). That could open up in for interval integrals.

[Kyle Miller]

Yet another suggestion: ∫ x in 0 to r, x (viable if we're ok with to becoming a keyword, and it should be Lean 4 parseable)

[Yury G. Kudryashov]

I'm happy with any of these notations.

[Yury G. Kudryashov]

(and can write a regexp to migrate)

[Yury G. Kudryashov]

Should we start a poll?

[Yury G. Kudryashov]

Let me do it. tl;dr: ∫ x in 0..1, x doesn't work in Lean 4. Which notation should we use instead?

[Sebastien Gouezel]

Is there really no way to fix the notation ∫ x in 0..1, x?

[Yury G. Kudryashov]

/poll Notation for interval integral
∫_{a}^{b} x, f x ∂μ
∫ x in [a:b], f x ∂μ
∫_{a}^{b} fun x ↦ f x ∂μ
∫ x in a to b, f x ∂μ
∫ x from a to b, f x ∂μ (will it conflict with from?)

[Yury G. Kudryashov]

As far as I understand, Lean parses 0..1 as dot notation on 0. (decimal fraction) and fails.

[Yury G. Kudryashov]

We can use a different symbol instead of ... E.g., [a:b] is very close. I don't know if a::b will work.

[Yury G. Kudryashov]

I droped most of the explicit type annotations from the PR.

[Yury G. Kudryashov]

It looks like option 2 is winning. I'll change the PR.

[Yury G. Kudryashov]

Will it conflict with set integral notation + docs#Std.Range notation?

[Yury G. Kudryashov]

Let me try in Mathlib 4

[Kyle Miller]

There's a chance you might need to give (priority := high) in the notation3 command if it can't resolve the ambiguity itself

[Yury G. Kudryashov]

Even with (priority := high), it fails to parse ∫ _ in [j:N], (1 : ℝ) ∂ρ without a type annotation.

[Yury G. Kudryashov]

(here j and N are natural numbers)

[Yury G. Kudryashov]

I pushed to branch#YK-interval-integral. Have a look at Probability.StrongLaw

[Yury G. Kudryashov]

Note that I messed up with search&replace and added extra commas after some ]s

[Yury G. Kudryashov]

It looks like I fixed these in that file.

[Yury G. Kudryashov]

UPD: and now I actually pushed to github.

[Patrick Massot]

Any news here? @Yury G. Kudryashov

[Yury G. Kudryashov]

No news. I failed to implement ∫ x in [a:b], f x ∂μ.

[Yury G. Kudryashov]

It would be nice if someone who better understands how Lean notation work will do it.

[Mario Carneiro]

what is the desired behavior?

[Yury G. Kudryashov]

∫ x in [1:10], f x ∂μ should parse as an interval integral, not as set integral over a non-existent coercion of a range to set.