Ulam's floating body problem

AbbreviationUnit sphere#✓fully proved

For a natural number \(d\), the unit sphere \(S^{d-1} = \{x \in \mathbb{R}^d : \|x\| = 1\}\) in \(\mathbb{R}^d\), centered at the origin.

abbrev S : Set ℝᵈ := Metric.sphere 0 1

Used by 5

Used byCutting hyperplane at a level · Floating in equilibrium in a direction · Floating in equilibrium in every orientation · Lower half-space · Direction of the line through the centers of mass

AbbreviationOrigin-symmetric set#✓fully proved

A set \(K \subseteq \mathbb{R}^d\) is origin-symmetric if \(K = -K\), where \(-K = \{-x : x \in K\}\).

abbrev IsOriginSymmetric (K : Set ℝᵈ) : Prop :=
  K = -K

Used by 1

Used byCentrally symmetric set

AbbreviationCentrally symmetric set#✓fully proved

A set \(K \subseteq \mathbb{R}^d\) is centrally symmetric if there is a point \(p \in \mathbb{R}^d\) such that the translate \(K - p = \{x - p : x \in K\}\) is origin-symmetric, that is, \(K - p = -(K - p)\).

abbrev IsCentrallySymmetric (K : Set ℝᵈ) : Prop :=
  ∃ p, IsOriginSymmetric (K - {p})

Uses 1 · Used by 1

Statement usesOrigin-symmetric set

Used byRyabogin's negative answer to Ulam's floating body problem

AbbreviationCenter of mass#✓fully proved

The center of mass of a set \(K \subseteq \mathbb{R}^d\) is the average \(\frac{1}{\operatorname{vol}(K)} \int_K x \, dx\), where \(dx\) is Lebesgue measure on \(\mathbb{R}^d\). By convention it is \(0\) when \(\operatorname{vol}(K)\) is \(0\) or infinite, or when \(x \mapsto x\) is not integrable on \(K\). For a compact convex body this is the usual center of mass.

noncomputable abbrev centerOfMass (K : Set ℝᵈ) : ℝᵈ := ⨍ x in K, x

Used by 1

Used byDirection of the line through the centers of mass

DefinitionLower half-space#✓fully proved

For a unit vector \(\xi \in \mathbb{R}^d\) and \(t \in \mathbb{R}\), the closed lower half-space is \(H^-(\xi) = \{p \in \mathbb{R}^d : \xi \cdot p \le t\}\).

def H_minus (ξ : S d) (t : ℝ) : Set ℝᵈ := { x | ⟪x, ξ⟫ ≤ t }

Sources

• D. Ryabogin, A negative answer to Ulam's Problem 19 from the Scottish Book, Annals of Math. 195 (3) 2022, Equation (1).

Uses 1 · Used by 2

Statement usesUnit sphere

Used byCutting hyperplane at a level · Direction of the line through the centers of mass

StructureCutting hyperplane at a level#✓fully proved

Let \(K \subseteq \mathbb{R}^d\), let \(\xi \in \mathbb{R}^d\) be a unit vector and let \(\delta \in \mathbb{R}\). A cutting hyperplane of \(K\) in direction \(\xi\) at level \(\delta\) is a real number \(t\), standing for the hyperplane \(\{p \in \mathbb{R}^d : \xi \cdot p = t\}\), such that the volume of \(K \cap \{p \in \mathbb{R}^d : \xi \cdot p \le t\}\) equals \(\delta\). Here a set of infinite volume is assigned volume \(0\).

structure CuttingHyperplaneAtLevel (K : Set ℝᵈ) (ξ : S d) (δ : ℝ) where
  /-- The translation of the hyperplane. -/
  t : ℝ
  vol : volume.real (K ∩ H_minus ξ t) = δ

Uses 2 · Used by 2

Statement usesLower half-space · Unit sphere

Used byFloating in equilibrium in a direction · Direction of the line through the centers of mass

DefinitionDirection of the line through the centers of mass#✓fully proved

Let \(d\) be a natural number, let \(K \subseteq \mathbb{R}^d\), let \(\xi\) be a unit vector in \(\mathbb{R}^d\), let \(\delta \in \mathbb{R}\), and let \(H\) be a cutting hyperplane of \(K\) in direction \(\xi\) at level \(\delta\), with translation \(t\), so that \(H^-(\xi) = \{x \in \mathbb{R}^d : \langle x, \xi \rangle \le t\}\). Writing \(c(A)\) for the center of mass of a set \(A \subseteq \mathbb{R}^d\), the direction vector of the line \(l(\xi)\) through the center of mass of \(K\) and the center of mass of the submerged part \(K \cap H^-(\xi)\) is the vector \(c(K) - c(K \cap H^-(\xi))\).

noncomputable def CuttingHyperplaneAtLevel.lineThroughCentersOfMass {K : Set ℝᵈ} {ξ : S d} {δ : ℝ}
    (H : CuttingHyperplaneAtLevel K ξ δ) : ℝᵈ :=
  centerOfMass K - centerOfMass (K ∩ H_minus ξ H.t)

Uses 4 · Used by 1

Statement usesCutting hyperplane at a level · Lower half-space · Unit sphere · Center of mass

Used byFloating in equilibrium in a direction

DefinitionFloating in equilibrium in a direction#✓fully proved

Let \(K \subseteq \mathbb{R}^d\), let \(\xi \in \mathbb{R}^d\) be a unit vector and let \(\delta \in \mathbb{R}\). We say that \(K\) floats in equilibrium in direction \(\xi\) at level \(\delta\) if, for every cutting hyperplane \(\{p : \xi \cdot p = t\}\) of \(K\) in direction \(\xi\) at level \(\delta\), the center of mass of \(K\) minus the center of mass of \(K \cap \{p : \xi \cdot p \le t\}\) is a real multiple of \(\xi\) (possibly zero); that is, the line through the two centers of mass is parallel to \(\xi\) when they differ.

def FloatsInEquilibriumInDirectionAtLevel (K : Set ℝᵈ) (ξ : S d) (δ : ℝ) : Prop :=
  ∀ H : CuttingHyperplaneAtLevel K ξ δ, H.lineThroughCentersOfMass ∈ ℝ ∙ ξ.val

Uses 3 · Used by 1

Statement usesCutting hyperplane at a level · Direction of the line through the centers of mass · Unit sphere

Used byFloating in equilibrium in every orientation

DefinitionFloating in equilibrium in every orientation#✓fully proved

A set \(K \subseteq \mathbb{R}^d\) floats in equilibrium in every orientation at level \(\delta \in \mathbb{R}\) if it floats in equilibrium in direction \(\xi\) at level \(\delta\) for every unit vector \(\xi \in \mathbb{R}^d\).

def FloatsInEquilibriumInEveryOrientationAtLevel (K : Set ℝᵈ) (δ : ℝ) : Prop :=
  ∀ ξ, FloatsInEquilibriumInDirectionAtLevel K ξ δ

Uses 2 · Used by 1

Statement usesFloating in equilibrium in a direction · Unit sphere

Used byRyabogin's negative answer to Ulam's floating body problem

StructureBody of revolution#✓fully proved

A body of revolution in \(\mathbb{R}^d\) is given by real numbers \(R_1, R_2\) and a function \(f : \mathbb{R} \to \mathbb{R}\) that vanishes outside the interval \([-R_1, R_2]\), is infinitely differentiable on the open interval \((-R_1, R_2)\) and is concave on \([-R_1, R_2]\). The dimension \(d\) is only a parameter; these data do not depend on it.

structure BodyOfRevolution (d : ℕ) where
  /-- The left half-length of the interval; `f` is supported on `[-R₁, R₂]`. -/
  R₁ : ℝ
  /-- The right half-length of the interval; `f` is supported on `[-R₁, R₂]`. -/
  R₂ : ℝ
  /-- The smooth concave function `f : ℝ → ℝ` defining the body of revolution. -/
  f : ℝ → ℝ
  support : f.support ⊆ Set.Icc (-R₁) R₂
  smooth : ContDiffOn ℝ ∞ f (Set.Ioo (-R₁) R₂)
  concave : ConcaveOn ℝ (Set.Icc (-R₁) R₂) f

Used by 2

Used bySolid of revolution · Ryabogin's negative answer to Ulam's floating body problem

DefinitionSolid of revolution#✓fully proved

Let \(d \ge 1\) and let a body of revolution in \(\mathbb{R}^d\) be given by \(R_1\), \(R_2\) and \(f\). Writing points of \(\mathbb{R}^d\) as \(x = (x_0, \dots, x_{d-1})\), its solid is the set of all \(x\) with \(x_0 \in [-R_1, R_2]\) and \(x_1^2 + \dots + x_{d-1}^2 \le f(x_0)^2\).

def BodyOfRevolution.body [NeZero d] (K : BodyOfRevolution d) : Set ℝᵈ :=
  { x | x 0 ∈ Set.Icc (-K.R₁) K.R₂ ∧ ∑ i > 0, (x i) ^ 2 ≤ K.f (x 0) ^ 2 }

Uses 1 · Used by 1

Statement usesBody of revolution

Used byRyabogin's negative answer to Ulam's floating body problem

DefinitionStrictly convex body#✓fully proved

A set \(K \subseteq \mathbb{R}^d\) is a strictly convex body if it is strictly convex (for distinct \(x, y \in K\), every point of the open segment between \(x\) and \(y\) lies in the interior of \(K\)), compact, and has nonempty interior.

def IsStrictlyConvexBody (K : Set ℝᵈ) : Prop :=
  StrictConvex ℝ K ∧ IsCompact K ∧ (interior K).Nonempty

Used by 1

Used byRyabogin's negative answer to Ulam's floating body problem

TheoremRyabogin's negative answer to Ulam's floating body problem#●ready to prove

Let \(d \ge 3\). There exists a body of revolution \(K \subset \mathbb{R}^d\) that is a strictly convex body, is not centrally symmetric, and floats in equilibrium in every orientation at the level \(\operatorname{vol}(K)/2\).

public theorem_wanted theorem_1 (hd : 3 ≤ d) : letI : NeZero d := ⟨by omega⟩
    ∃ K : BodyOfRevolution d, IsStrictlyConvexBody K.body ∧ ¬ IsCentrallySymmetric K.body ∧
      FloatsInEquilibriumInEveryOrientationAtLevel K.body (volume.real K.body / 2)

Sources

• D. Ryabogin, A negative answer to Ulam's Problem 19 from the Scottish Book, Annals of Math, 195 (3) 2022. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_ulam of the lean-eval benchmark.

Uses 5

Statement usesBody of revolution · Solid of revolution · Floating in equilibrium in every orientation · Centrally symmetric set · Strictly convex body

12 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.