Zulip Chat Archive

Stream: general

Topic: representing "objects" in n-dimensional space

Twain Byrnes (Nov 21 2022 at 13:30):

hi! I was trying to do a formalization of the ham sandwich theorem and I couldn't figure out how to talk about having "n n-dimensional objects" in my theorem statement (or how to talk about slicing all of them in half with whatever volume means...)
i was thinking i would start with the pancake theorem (2-D version), in which case I would need to know how to tell Lean that I want a theorem statement saying "If I have two two-dimensional objects (on a plane), I can draw one line that bisects the area of both objects".
pretty much all I've got right now is euclidean_space ℝ (fin 2) and I have no idea how to write the rest. Any help would be greatly appreciated!
thanks :)

Riccardo Brasca (Nov 21 2022 at 13:42):

Forgetting Lean for a moment, what mathematical object have you in mind? A n-dimensional topological manifold?

Riccardo Brasca (Nov 21 2022 at 13:42):

In any case before formalizing anything, you should have a very precise mathematical statement.

Yaël Dillies (Nov 21 2022 at 13:44):

I suspect the correct generality is measurable sets

Twain Byrnes (Nov 21 2022 at 14:10):

i think i don't want a manifold. maybe a measurable set? but i'm not really sure what measureable means
not really sure what the precise words i'm looking for are
but like in two dimensions, i would want any closed loop, like a circle or a rectangle
three dimensions i would want something like a sphere or a platonic solid

Riccardo Brasca (Nov 21 2022 at 14:15):

First of all find a precise mathematical statement, that's completely unrelated to Lean. Don't worry about having the most general version at the beginning, but you need a theorem to formalize.

Twain Byrnes (Nov 21 2022 at 15:03):

the wiki article states the theorem as
"for every positive integer n the ham sandwich theorem states that given n measurable "objects" in n-dimensional Euclidean space, it is possible to divide each one of them in half (with respect to their measure, e.g. volume) with a single (n − 1)-dimensional hyperplane"

Adam Topaz (Nov 21 2022 at 15:11):

What does "object" mean in this theorem?

Vincent Beffara (Nov 21 2022 at 15:22):

"object" here sounds like "measurable set of finite measure"

Julian Berman (Nov 21 2022 at 16:29):

@Twain Byrnes it may help to share what your background is and/or whether you saw this theorem in a particular book, or just in the Wikipedia article

Twain Byrnes (Nov 21 2022 at 17:16):

okay i was able to find a paper referencing it that described it like so

i'm presently a junior in college studying electrical engineering; i've taken a lot of discrete courses for an EE, but not a lot relative to a lot of maths majors

Riccardo Brasca (Nov 21 2022 at 17:19):

Do you know a proof of this theorem?

Riccardo Brasca (Nov 21 2022 at 17:20):

It is very difficult to learn some mathematics while formalizing it. If you want to practice Lean, it's better to take a theorem you understand well, and formalize it.

Eric Wieser (Nov 21 2022 at 17:22):

What's the canonical way in mathilb to talk about an affine halfplane like the one described there? (cutting with a hyperplane is intersecting with a halfplane)

Eric Wieser (Nov 21 2022 at 17:23):

(sure, you could say there exists a point and a normal vector, but it seems like a useful primitive to have somewhere)

Jireh Loreaux (Nov 21 2022 at 17:27):

How about the sub-level sets of a linear functional?

Riccardo Brasca (Nov 21 2022 at 17:28):

Maybe an docs#affine_subspace such that docs#affine_subspace.direction has the required dimension?

Jireh Loreaux (Nov 21 2022 at 17:29):

I would be surprised if we didn't have this somewhere in all the convexity theory. @Yaël Dillies would probably know. It's surely required for Hahn-Banach separation.

Riccardo Brasca (Nov 21 2022 at 17:29):

Hahn-Banach separation is spelled out using functionals.

Eric Wieser (Nov 21 2022 at 17:35):

Unless I'm mistake, an affine subspace can do the hyperplane but not the halfplane

Eric Wieser (Nov 21 2022 at 17:35):

(if k were a semiring but not a ring then things might be different)

Eric Wieser (Nov 21 2022 at 17:36):

Ah, so an affine map from V to R should probably suffice?

Riccardo Brasca (Nov 21 2022 at 17:37):

Why do you want the halfplane?

Riccardo Brasca (Nov 21 2022 at 17:38):

The theorem in ℝ² is that if you have two slice of bread you can, with only one cut, cut both slices in half. The cut is a line, an hyperplane.

Jireh Loreaux (Nov 21 2022 at 17:43):

Eric, if f : V →ₗ[ℝ] ℝ is a linear functional and a : ℝ, then {x : V | f x ≤ a} is a half-space whose boundary is an affine subspace. Is this clear? Maybe I'm misunderstanding your confusion.

Twain Byrnes (Nov 21 2022 at 17:47):

Riccardo Brasca said:

Do you know a proof of this theorem?

so in 2d it's pretty easy with IVT and the n-dimensional generalization apparently follows pretty directly from borsuk ulam (not quite sure how that works, but i think it shouldn't be too bad to understand)
this is probably the best proof i've seen for 2d: https://prove-me-wrong.com/2022/07/01/the-pancake-theorem/

Eric Wieser (Nov 21 2022 at 17:58):

Why do you want the halfplane?

Because then the theorem can be stated as "there exists a halfplane such that h intersected with each of the sets has measure equal to half the measure of the object"

Eric Wieser (Nov 21 2022 at 17:59):

@Jireh Loreaux: I thought you were claiming that {x : V | f x ≤ a} was itself an affine space. I fully mostly agree with your last message (P →ᵃ[ℝ] ℝ not V →ₗ[ℝ] ℝ if it's affine, right).

Jireh Loreaux (Nov 21 2022 at 18:01):

No, it's a linear functional. The affine part is the a.

Junyan Xu (Nov 21 2022 at 18:22):

I think a halfspace can be defined either as the sub-zero set of an affine map to ℝ, or as the sub-level set of a linear functional. A halfplane is meant to be a 2-dimensional halfspace, right?

Yaël Dillies (Nov 21 2022 at 19:17):

Yes, everything was said already. Halfspaces in mathlib are modelled as sub/superlevels of functionals.

Joseph Myers (Nov 21 2022 at 19:40):

Given the affine subspace (of the right dimension), you could also consider equivalence classes with respect to the s_same_side relation in analysis.convex.side. Or connected components of the complement.

I suspect the way to assert that the affine subspace has the right dimension is is_coatom (though we don't have any lemmas at all about is_coatom for affine subspaces).

Last updated: Aug 03 2023 at 10:10 UTC