Refinement of two dissections

Stream: new members

[Mantas Baksys]

Hi all! I've been working on formalizing the definition of the Riemann integral for educational purposes and ran into the following issue. I have defined a dissection as follows :

import data.real.basic

structure dissection (a b : ℝ):=
(N: ℕ)
(x: fin (N+1) → ℝ)
(to_right: a ≤ b)
(x_zero: x (0: fin(N+1)) = a)
(x_last: x (N: fin(N+1)) = b)
(mono : ∀ i : fin N, x (i.cast_succ) ≤ x i.succ)

Now, I would like to be able to take two partitions D1 and D2 and take the union (or the so- called minimal common refinement of these dissections). I realise that this could be done by somehow taking union of the images of D1.x and D2.x and then constructing a monotone sequence out of this set, however this is something I have no idea how to do. Does anybody have any suggestions? :smiley:

[Eric Rodriguez]

Maybe something like docs#list.merge_sort and use a list instead of x, N and list.sorted instead of mono? I have a feeling that's probably hard to work with though, someone with more experience than me will know that. The image of a function is easy though, the notation for the image of a function f x in mathlib is f '' X

[Kevin Buzzard]

Your data is equivalent to just giving a finite subset of (a,b), and if you worked with this as the definition then you'd just be able to take the union. You could write API to extract all the other disection stuff from this subset rather than making it part of the definition.

[Kevin Buzzard]

Actually it is not quite equivalent because you seem to allow $x_i=x_{i+1}$, so the way you have it it's equivalent to a multiset in [a,b] (modulo the degenerate case N=0 and a=b)

[Mantas Baksys]

Thanks Kevin and Eric. I'm now starting to realise that often times the solution actually is to just 'redefine the structures in a suitable way' rather than look for some workaround :smiley:.

[Kevin Buzzard]

Definitions are the hard part (at least if you're a mathematician). If you get them wrong then theorems can become hard to prove.

[Bryan Gin-ge Chen]

There's a (long!) thread where @Patrick Thomas was working on related matters here; some parts might be helpful.

[Mantas Baksys]

Just a quick follow-up question. I was trying to sort the following finset but got an error:

import data.real.basic data.set.intervals.unordered_interval data.finset.sort

open set

def sorted_set {a b: ℝ} (S: finset (Ioo a b)) : list (Ioo a b) := finset.sort (≤) S

As far as I looked, I haven't found a specific statement that defines ≤ on Ioo a b so that it would be easily accessible. Am I missing something?

[Alex J. Best]

Ioo coerced to a type is a subtype, so you can do:

import data.real.basic data.set.intervals.unordered_interval data.finset.sort

open set
open_locale classical
noncomputable theory
instance {a b: ℝ} : preorder (Ioo a b) := subtype.preorder _

def sorted_set {a b: ℝ} (S: finset (Ioo a b)) : list (Ioo a b) := finset.sort (≤) S

but you might be better off just sorting a list of reals, and separately tracking the hypothesis that they are all in that interval

[Eric Wieser]

Should that instance be automatic?

[Eric Wieser]

Do we have it already as docs#set_coe.preorder?

[Mantas Baksys]

I think the instance is automatic, however the problem was decidability (at least that's my guess). The code @Alex J. Best posted outputs an error if we do no include open_locale classical, so I guess I'll just just use that every time to avoid the decidability hell.