First n natural numbers

Stream: general

[Vincent Beffara]

This topic has appeared before but what I found is pretty old, so: what is the preferred way to talk about the natural numbers from 0 to n? (My use case is to have a finite ordered set of real numbers to describe a subdivision of an interval, which I want to index.) I'm hesitating between too many options:

• Fin (n + 1)
• Nat.Iic n
• Finset.range (n + 1)
• { i : ℕ | i ≤ n }
• don't, use ℕ with a separate assumption and treat values above n as garbage values
• don't, use a List instead of indexing

[Ruben Van de Velde]

• all of the above

[Yaël Dillies]

In your case, I'd go for the garbage values version, since you can treat the maximum of the interval as a garbage value (assuming it's a closed interval?).

[Vincent Beffara]

Right now I have this,

structure Subdivision (a b : ℝ) where
  n : ℕ
  toFun : ℕ → ℝ
  first : toFun 0 = a
  last : toFun (n + 1) = b
  mono : MonotoneOn toFun (Set.Iic (n + 1))

[Sebastien Gouezel]

Data point: for docs#eVariationOn, I went for ℕ and garbage values. This is quite nice from some points of view, but in retrospect things would have probably been smoother using lists (especially when gluing subdivisions of consecutive intervals). If you want to have a look at something really bad, look at the proof of docs#eVariationOn.add_point (which is about adding one point to a subdivision and checking that this does not decrease the variation).

So my advice is to use lists.

[Eric Wieser]

n being bundled is probably good evidence that you want a list

[Vincent Beffara]

Sebastien Gouezel said:

Data point: for docs#eVariationOn, I went for ℕ and garbage values. This is quite nice from some points of view, but in retrospect things would have probably been smoother using lists (especially when gluing subdivisions of consecutive intervals). If you want to have a look at something really bad, look at the proof of docs#eVariationOn.add_point (which is about adding one point to a subdivision and checking that this does not decrease the variation).

So my advice is to use lists.

Indeed docs#eVariationOn.add_point is rather painful to look at... I was starting to state that given two subdivisions there is a third which is finer than both and for than in fact Finset ℝ felt more appealing, but then getting the pairs of consecutive elements is a nontrivial operation.

[Sebastien Gouezel]

Another option is to look at Analysis.BoxIntegral which implements subdivisions into boxes in finite product spaces (which contains in particular the one-dimensional case).

[Sebastien Gouezel]

With the Finset ℝ approach, you can easily take unions, and for consecutive elements you can sort your finset, so it is probably quite manageable also.

[Vincent Beffara]

With the Finset option IIRC the issue I had was that I wanted to say that the smallest element was a, but the smallest element of a Finset lives in with_top something and I kept casting into and out of with_top all the time

[Vincent Beffara]

Ah, thanks, docs#BoxIntegral.Prepartition seems to be exactly what I needed. I will try to coerce my current code into using it...

[Sebastien Gouezel]

(Box integral code is written for product spaces, of the form ι → ℝ, so it's not clear that it can be used in your situation :-(

[Sebastien Gouezel]

There is docs#Finset.min' to avoid the withTop issue.

[Vincent Beffara]

Sebastien Gouezel said:

(Box integral code is written for product spaces, of the form ι → ℝ, so it's not clear that it can be used in your situation :-(

With ι = Fin 1 I believe it can, but then I'm not sure if the plumbing won't be heavier than writing everything from scratch.

[Vincent Beffara]

Sebastien Gouezel said:

There is docs#Finset.min' to avoid the withTop issue.

Yep, and then one has to carry around a proof that the Finset is not empty :-(

[Sebastien Gouezel]

Yes, or with ι = Unit, but it looks like too much plumbing indeed. Having a good intrinsic implementation, that we could use to streamline the bounded variation file, looks like a worthy goal.

[Sebastien Gouezel]

Vincent Beffara said:

Sebastien Gouezel said:

There is docs#Finset.min' to avoid the withTop issue.

Yep, and then one has to carry around a proof that the Finset is not empty :-(

Yes, you can't have the butter and the butter money :-)

(Not sure non-French speakers can understand that)

[Sebastien Gouezel]

But assuming nonemptyness is quite natural for subdivisions, right?

[Jireh Loreaux]

The english version of that idiom is so much more confusing: you can't have your cake and eat it too! (Isn't that exactly what you do with cake?!)

[Yaël Dillies]

Vincent Beffara said:

With the Finset option IIRC the issue I had was that I wanted to say that the smallest element was a, but the smallest element of a Finset lives in with_top something and I kept casting into and out of with_top all the time

Well you can use docs#FInset.inf'

[Vincent Beffara]

In the end I converged on def Subdivision (a b : ℝ) := Finset (Ioo a b) with a bit of API.