representing "objects" in n-dimensional space

Stream: general

[Twain Byrnes]

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]

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

[Riccardo Brasca]

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

[Yaël Dillies]

I suspect the correct generality is measurable sets

[Twain Byrnes]

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]

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]

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]

What does "object" mean in this theorem?

[Vincent Beffara]

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

[Julian Berman]

@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]

image.png
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]

Do you know a proof of this theorem?

[Riccardo Brasca]

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]

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]

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

[Jireh Loreaux]

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

[Riccardo Brasca]

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

[Jireh Loreaux]

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]

Hahn-Banach separation is spelled out using functionals.

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Riccardo Brasca]

Why do you want the halfplane?

[Riccardo Brasca]

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]

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]

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]

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]

@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]

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

[Junyan Xu]

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]

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

[Joseph Myers]

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).