def HamSandwich.halfSpaceBelow (n : ℕ) (v : EuclideanSpace ℝ (Fin n)) (c : ℝ) : Set (EuclideanSpace ℝ (Fin n))

The open half-space {x : ⟨v, x⟩ < c} ⊆ ℝⁿ.

def HamSandwich.halfSpaceAbove (n : ℕ) (v : EuclideanSpace ℝ (Fin n)) (c : ℝ) : Set (EuclideanSpace ℝ (Fin n))

The open half-space {x : ⟨v, x⟩ > c} ⊆ ℝⁿ.

def HamSandwich.Bisects (n : ℕ) (v : EuclideanSpace ℝ (Fin n)) (c : ℝ) (A : Set (EuclideanSpace ℝ (Fin n))) : Prop

A hyperplane with normal v and offset c bisects a set A ⊆ ℝⁿ if the two open half-spaces it defines have equal Lebesgue measure when intersected with A.

noncomputable def HamSandwich.extractNormal (n : ℕ) (θ : EuclideanSpace ℝ (Fin (n + 1))) : EuclideanSpace ℝ (Fin n)

Given θ ∈ ℝⁿ⁺¹ (a parameter on the unit sphere), extractNormal returns the first n coordinates regarded as the normal vector of a hyperplane in ℝⁿ.

def HamSandwich.extractOffset (n : ℕ) (θ : EuclideanSpace ℝ (Fin (n + 1))) : ℝ

Given θ ∈ ℝⁿ⁺¹, extractOffset returns its last coordinate, interpreted as the constant c of an affine hyperplane ⟨v, x⟩ = c.

noncomputable def HamSandwich.affineFunctional (n : ℕ) (θ : EuclideanSpace ℝ (Fin (n + 1))) (x : EuclideanSpace ℝ (Fin n)) : ℝ

The affine functional x ↦ ⟨extractNormal θ, x⟩ - extractOffset θ whose sign determines the two sides of the hyperplane parametrised by θ ∈ Sⁿ.

theorem HamSandwich.extractNormal_neg (n : ℕ) (θ : EuclideanSpace ℝ (Fin (n + 1))) : extractNormal n (-θ) = -extractNormal n θ

extractNormal is linear in θ, in particular it sends negation to negation.

theorem HamSandwich.extractOffset_neg (n : ℕ) (θ : EuclideanSpace ℝ (Fin (n + 1))) : extractOffset n (-θ) = -extractOffset n θ

extractOffset sends negation to negation.

theorem HamSandwich.affineFunctional_neg (n : ℕ) (θ : EuclideanSpace ℝ (Fin (n + 1))) (x : EuclideanSpace ℝ (Fin n)) : affineFunctional n (-θ) x = -affineFunctional n θ x

The affine functional is odd in the parameter θ: replacing θ by -θ flips the sign of affineFunctional n θ x. This antipodal symmetry is what allows Borsuk-Ulam to be applied.

theorem HamSandwich.continuous_extractNormal (n : ℕ) : Continuous (extractNormal n)

extractNormal is continuous in its argument.

theorem HamSandwich.continuous_extractOffset (n : ℕ) : Continuous (extractOffset n)

extractOffset is continuous (it is a coordinate projection).

theorem HamSandwich.continuousAt_affineFunctional (n : ℕ) (x : EuclideanSpace ℝ (Fin n)) (θ₀ : EuclideanSpace ℝ (Fin (n + 1))) : ContinuousAt (fun (θ : EuclideanSpace ℝ (Fin (n + 1))) => affineFunctional n θ x) θ₀

For fixed x ∈ ℝⁿ, the map θ ↦ affineFunctional n θ x is continuous at every θ₀.

theorem HamSandwich.continuous_affineFunctional_x (n : ℕ) (θ : EuclideanSpace ℝ (Fin (n + 1))) : Continuous (affineFunctional n θ)

For fixed θ, the affine functional affineFunctional n θ : ℝⁿ → ℝ is continuous.

theorem HamSandwich.isOpen_halfSpace_pos (n : ℕ) (θ : EuclideanSpace ℝ (Fin (n + 1))) : IsOpen {y : EuclideanSpace ℝ (Fin n) | affineFunctional n θ y > 0}

The positive half-space {y : affineFunctional n θ y > 0} is open in ℝⁿ.

theorem HamSandwich.indicator_halfspace_continuousAt (n : ℕ) (θ₀ : EuclideanSpace ℝ (Fin (n + 1))) (x : EuclideanSpace ℝ (Fin n)) (hx : affineFunctional n θ₀ x ≠ 0) : ContinuousAt (fun (θ : EuclideanSpace ℝ (Fin (n + 1))) => {y : EuclideanSpace ℝ (Fin n) | affineFunctional n θ y > 0}.indicator (fun (x : EuclideanSpace ℝ (Fin n)) => 1) x) θ₀

If affineFunctional n θ₀ x ≠ 0, then the indicator of the positive half-space evaluated at x is continuous in θ at θ₀ (since x is in the interior of one side).

theorem HamSandwich.hyperplane_measure_zero {n : ℕ} (v : EuclideanSpace ℝ (Fin n)) (c : ℝ) (hv : v ≠ 0) : MeasureTheory.volume {x : EuclideanSpace ℝ (Fin n) | inner ℝ v x = c} = 0

An affine hyperplane {x : ⟨v, x⟩ = c} in ℝⁿ (with v ≠ 0) has Lebesgue measure zero.

theorem HamSandwich.ae_affineFunctional_ne_zero (n : ℕ) (θ₀ : EuclideanSpace ℝ (Fin (n + 1))) (hθ : θ₀ ≠ 0) (A : Set (EuclideanSpace ℝ (Fin n))) : ∀ᵐ (x : EuclideanSpace ℝ (Fin n)) ∂MeasureTheory.volume.restrict A, affineFunctional n θ₀ x ≠ 0

For any nonzero parameter θ₀ ∈ ℝⁿ⁺¹ and any set A ⊆ ℝⁿ, the affine functional is almost everywhere nonzero on A (the zero set is the hyperplane, which has measure zero when the normal is nonzero, and is empty when the normal is zero but the offset is not).

theorem HamSandwich.continuousAt_volume_halfspace (n : ℕ) (A : Set (EuclideanSpace ℝ (Fin n))) (hBdd : Bornology.IsBounded A) (θ₀ : EuclideanSpace ℝ (Fin (n + 1))) (hθ : θ₀ ≠ 0) : ContinuousAt (fun (θ : EuclideanSpace ℝ (Fin (n + 1))) => ∫ (x : EuclideanSpace ℝ (Fin n)) in A, {y : EuclideanSpace ℝ (Fin n) | affineFunctional n θ y > 0}.indicator (fun (x : EuclideanSpace ℝ (Fin n)) => 1) x) θ₀

For a bounded set A and nonzero θ₀, the volume of A ∩ {affineFunctional n θ · > 0} (as an integral of the indicator) varies continuously in θ at θ₀.

theorem HamSandwich.continuousAt_volume_halfspace_neg (n : ℕ) (A : Set (EuclideanSpace ℝ (Fin n))) (hBdd : Bornology.IsBounded A) (θ₀ : EuclideanSpace ℝ (Fin (n + 1))) (hθ : θ₀ ≠ 0) : ContinuousAt (fun (θ : EuclideanSpace ℝ (Fin (n + 1))) => ∫ (x : EuclideanSpace ℝ (Fin n)) in A, {y : EuclideanSpace ℝ (Fin n) | affineFunctional n θ y < 0}.indicator (fun (x : EuclideanSpace ℝ (Fin n)) => 1) x) θ₀

Same continuity as continuousAt_volume_halfspace but for the negative half-space.

theorem HamSandwich.integral_indicator_eq_volume {n : ℕ} (A S : Set (EuclideanSpace ℝ (Fin n))) (hS : MeasurableSet S) : ∫ (x : EuclideanSpace ℝ (Fin n)) in A, S.indicator (fun (x : EuclideanSpace ℝ (Fin n)) => 1) x = (MeasureTheory.volume (A ∩ S)).toReal

The integral over A of the indicator of a measurable set S equals the real value of volume (A ∩ S).

theorem HamSandwich.ham_sandwich_theorem (n : ℕ) (A : Fin n → Set (EuclideanSpace ℝ (Fin n))) (hOpen : ∀ (i : Fin n), IsOpen (A i)) (hBdd : ∀ (i : Fin n), Bornology.IsBounded (A i)) (hNe : ∀ (i : Fin n), (A i).Nonempty) (hn : 0 < n) : ∃ (v : EuclideanSpace ℝ (Fin n)) (c : ℝ), v ≠ 0 ∧ ∀ (i : Fin n), Bisects n v c (A i)

Corollary (Ham Sandwich Theorem). Given n open, bounded, nonempty sets A₁, …, Aₙ ⊆ ℝⁿ, there exists an affine hyperplane {x : ⟨v, x⟩ = c} (with v ≠ 0) that simultaneously bisects each Aᵢ by Lebesgue measure. The proof applies the Borsuk-Ulam theorem to the odd map on Sⁿ sending a parameter θ to the vector of signed volume-differences.