def PolynomialHamSandwich.Bisects (d : ℕ) (P : MvPolynomial (Fin d) ℝ) (U : Set (Fin d → ℝ)) : Prop

A polynomial P : ℝ[x₁, …, x_d] bisects a measurable set U ⊆ ℝ^d if the parts of U where P > 0 and where P < 0 have equal Lebesgue volume.

noncomputable def PolynomialHamSandwich.signedVol (d : ℕ) (P : MvPolynomial (Fin d) ℝ) (U : Set (Fin d → ℝ)) : ℝ

The signed volume vol{P > 0 in U} − vol{P < 0 in U} as a real number; this function is zero exactly when P bisects U (assuming U is bounded).

theorem PolynomialHamSandwich.signedVol_neg (d : ℕ) (P : MvPolynomial (Fin d) ℝ) (U : Set (Fin d → ℝ)) : signedVol d (-P) U = -signedVol d P U

Negating the polynomial flips the sign of the signed volume: signedVol(−P, U) = −signedVol(P, U).

theorem PolynomialHamSandwich.bisects_of_signedVol_zero (d : ℕ) (P : MvPolynomial (Fin d) ℝ) (U : Set (Fin d → ℝ)) (hU_bounded : Bornology.IsBounded U) (h : signedVol d P U = 0) : Bisects d P U

For a bounded set U, vanishing of the signed volume signedVol d P U implies that P bisects U.

theorem PolynomialHamSandwich.combo_ne_zero {d m : ℕ} (basis : Fin m → MvPolynomial (Fin d) ℝ) (hbasis : LinearIndependent ℝ basis) (v : Fin m → ℝ) (hv : v ≠ 0) : ∑ i : Fin m, v i • basis i ≠ 0

A nontrivial linear combination of linearly independent polynomials is nonzero.

theorem PolynomialHamSandwich.combo_totalDegree_le {d D m : ℕ} (basis : Fin m → MvPolynomial (Fin d) ℝ) (hbasis_deg : ∀ (i : Fin m), (basis i).totalDegree ≤ D) (v : Fin m → ℝ) : (∑ i : Fin m, v i • basis i).totalDegree ≤ D

Any real-linear combination of polynomials of total degree at most D itself has total degree at most D.

theorem PolynomialHamSandwich.sphere_vec_ne_zero {n : ℕ} (x : ↑(BorsukUlam.Sphere n)) : (fun (i : Fin (n + 1)) => (↑x).ofLp i) ≠ 0

A point on the unit sphere S^n ⊆ ℝ^{n+1} has, in particular, a nonzero coordinate vector.

theorem PolynomialHamSandwich.exists_linearIndependent_polynomials (d D : ℕ) : ∃ (basis : Fin ((D + d).choose d) → MvPolynomial (Fin d) ℝ), LinearIndependent ℝ basis ∧ ∀ (i : Fin ((D + d).choose d)), (basis i).totalDegree ≤ D

The space of polynomials in d variables of total degree at most D has dimension binom(D + d, d); in particular it admits a linearly independent family of that size all of whose elements have total degree ≤ D.

theorem PolynomialHamSandwich.signedVol_map_continuous (d n : ℕ) (basis : Fin (n + 1) → MvPolynomial (Fin d) ℝ) (U : Fin n → Set (Fin d → ℝ)) (hU_open : ∀ (i : Fin n), IsOpen (U i)) (hU_bounded : ∀ (i : Fin n), Bornology.IsBounded (U i)) : Continuous fun (x : ↑(BorsukUlam.Sphere n)) => (EuclideanSpace.equiv (Fin n) ℝ).symm fun (i : Fin n) => signedVol d (∑ j : Fin (n + 1), (↑x).ofLp j • basis j) (U i)

Continuity of the signed-volume map. For a fixed basis of polynomials of bounded degree and bounded open sets U_i, the map sending a coefficient vector x on the sphere to the tuple of signed volumes (signedVol d (∑ x_j basis_j) U_i)_i is continuous as a map S^n → ℝ^n.

theorem PolynomialHamSandwich.polynomial_ham_sandwich (d D n : ℕ) (U : Fin n → Set (Fin d → ℝ)) (hU_open : ∀ (i : Fin n), IsOpen (U i)) (hU_bounded : ∀ (i : Fin n), Bornology.IsBounded (U i)) (hn : n ≤ (D + d).choose d - 1) : ∃ (P : MvPolynomial (Fin d) ℝ), P ≠ 0 ∧ P.totalDegree ≤ D ∧ ∀ (i : Fin n), Bisects d P (U i)

Polynomial Ham Sandwich Theorem. Given n bounded open sets U_1, …, U_n in ℝ^d and a degree bound D with n ≤ binom(D + d, d) − 1, there exists a nonzero polynomial P of total degree ≤ D whose zero set bisects every U_i. This is the polynomial generalization of the classical Ham Sandwich theorem, proved via Borsuk–Ulam applied to signed volumes.