Stream: new members

Topic: Refinement of two dissections

Mantas Baksys (Apr 04 2021 at 15:44):

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 (Apr 04 2021 at 15:56):

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 (Apr 04 2021 at 16:06):

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 (Apr 04 2021 at 16:07):

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 (Apr 04 2021 at 17:53):

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 (Apr 04 2021 at 18:49):

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 (Apr 04 2021 at 19:08):

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

Mantas Baksys (Apr 04 2021 at 22:09):

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 (Apr 04 2021 at 22:37):

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 (Apr 04 2021 at 22:38):

Should that instance be automatic?

Eric Wieser (Apr 04 2021 at 22:38):

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

Mantas Baksys (Apr 05 2021 at 09:24):

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.

Last updated: Dec 20 2023 at 11:08 UTC