Moving sofa: related mathematical developments

• Canonical.Foundations.Development001.
• Geometry.Foundations.Development003.
• Analysis.Foundations.Development003.
• Cap.Foundations.Development002.
• Analysis.Foundations.Development004.
• Convex.Foundations.Development002.
• Geometry.Foundations.Development004.
• Gerver.Foundations.Development002.
• Cap.Foundations.Development003.

Moving sofa: related mathematical developments

• Canonical.Definitions.
• Canonical.GerverDefinitions.

Definitions for the moving sofa problem

The definitions of MovingSofaSubmission/Challenge.lean, copied from FormalConjectures/Wikipedia/MovingSofa.lean in google-deepmind/formal-conjectures at commit ddfbaf90f4482030d88aae5233fe933874296a23. Here ABφθSpec.existsUnique is proved, from the certificate in GerverSofaLean, so that Gerver's constants are defined from a proved statement.

def EuclideanGeometry.«termℝ²» : Lean.ParserDescr

The standard two-dimensional Euclidean space over the reals.

Equations

• EuclideanGeometry.«termℝ²» = Lean.ParserDescr.node `EuclideanGeometry.«termℝ²» 1024 (Lean.ParserDescr.symbol "ℝ²")

@[instance_reducible]

noncomputable instance Module.orientedEuclideanSpaceFinTwo : Oriented ℝ (EuclideanSpace ℝ (Fin 2)) (Fin 2)

The plane ℝ² with the orientation of its standard basis, so that rotations are counterclockwise.

Equations

• Module.orientedEuclideanSpaceFinTwo = { positiveOrientation := (PiLp.basisFun 2 ℝ (Fin 2)).orientation }

instance fact_finrank_euclideanSpace_fin_two : Fact (Module.finrank ℝ (EuclideanSpace ℝ (Fin 2)) = 2)

The plane ℝ² has dimension two.

def MovingSofa.horizontalHallway : Set (EuclideanSpace ℝ (Fin 2))

The horizontal side of the hallway is $(-\infty, 1] \times [0, 1]$.

Equations

• MovingSofa.horizontalHallway = {x : EuclideanSpace ℝ (Fin 2) | ∃ (x_1 : ℝ) (y : ℝ) (_ : x_1 ≤ 1 ∧ 0 ≤ y ∧ y ≤ 1), !₂[x_1, y] = x}

def MovingSofa.verticalHallway : Set (EuclideanSpace ℝ (Fin 2))

The vertical side of the hallway is $[0, 1] \times (-\infty, 1]$.

Equations

• MovingSofa.verticalHallway = {x : EuclideanSpace ℝ (Fin 2) | ∃ (x_1 : ℝ) (y : ℝ) (_ : 0 ≤ x_1 ∧ x_1 ≤ 1 ∧ y ≤ 1), !₂[x_1, y] = x}

def MovingSofa.hallway : Set (EuclideanSpace ℝ (Fin 2))

The hallway is the union of its horizontal and vertical sides.

Equations

• MovingSofa.hallway = MovingSofa.horizontalHallway ∪ MovingSofa.verticalHallway

def MovingSofa.«termE(2)» : Lean.ParserDescr

The affine isometry group of the Euclidean plane.

Equations

• MovingSofa.«termE(2)» = Lean.ParserDescr.node `MovingSofa.«termE(2)» 1024 (Lean.ParserDescr.symbol "E(2)")

@[instance_reducible]

noncomputable instance MovingSofa.rigidMotionTopology : TopologicalSpace (EuclideanSpace ℝ (Fin 2) ≃ᵃⁱ[ℝ] EuclideanSpace ℝ (Fin 2))

The topology on the isometry group E(2), induced from the continuous affine maps of the plane.

Equations

• MovingSofa.rigidMotionTopology = TopologicalSpace.induced (fun (x : EuclideanSpace ℝ (Fin 2) ≃ᵃⁱ[ℝ] EuclideanSpace ℝ (Fin 2)) => x.toAffineIsometry.toContinuousAffineMap) inferInstance

structure MovingSofa.IsMovingSofa (s : Set (EuclideanSpace ℝ (Fin 2))) (m : ↑unitInterval → EuclideanSpace ℝ (Fin 2) ≃ᵃⁱ[ℝ] EuclideanSpace ℝ (Fin 2)) : Prop

A connected closed set $s$ is a moving sofa according to a rigid motion $m:I\to\mathrm{SE}(2)$, if the sofa is initially in the horizontal side of the hallway and ends up in the vertical side. Here, since $\mathrm{SE}(2)$ is not in Mathlib yet, we use $\mathrm{E}(2)$ and rely on continuity and $m(0) = \mathrm{id}$ to ensure $m$ is in $\mathrm{SE}(2)$.

• isConnected : IsConnected s
• isClosed : IsClosed s
• continuous : Continuous m
• zero : m 0 = AffineIsometryEquiv.refl ℝ (EuclideanSpace ℝ (Fin 2))
• initial : s ⊆ horizontalHallway
• subset_hallway (t : ↑unitInterval) : ⇑(m t) '' s ⊆ hallway
• final : ⇑(m 1) '' s ⊆ verticalHallway

noncomputable def MovingSofa.rotateTranslate (α : Real.Angle) (p : EuclideanSpace ℝ (Fin 2)) : EuclideanSpace ℝ (Fin 2) ≃ᵃⁱ[ℝ] EuclideanSpace ℝ (Fin 2)

The rigid motion that translates by $p$ and then rotates counterclockwise by $\alpha$. Note that [Ge92] used this definition while [Ro18] used rotation first and then translation.

Equations

• MovingSofa.rotateTranslate α p = (AffineIsometryEquiv.vaddConst ℝ p).trans (EuclideanGeometry.o.rotation α).toAffineIsometryEquiv

def MovingSofa.sofaOfRotateTranslatePath (p : ℝ → EuclideanSpace ℝ (Fin 2)) : Set (EuclideanSpace ℝ (Fin 2))

The sofa according to a rotation path $p : [0, \pi/2] \to \mathbb{R}^2$ as in [Ge92] is the intersection over $\alpha \in [0, \pi/2]$ of hallways each translated by $p(\alpha)$ and then rotated by $\alpha$, with the special cases that the hallway at $0$ is the horizontal side and the hallway at $\pi/2$ is the vertical side.

Equations

• One or more equations did not get rendered due to their size.

def MovingSofa.GerversSofa.ABφθSpec (A B φ θ : ℝ) : Prop

Eq. 1-4 of [Ro18], which specifies the constants $A$, $B$, $\varphi$, and $\theta$ of [Ge92].

Equations

• One or more equations did not get rendered due to their size.

theorem MovingSofa.GerversSofa.ABφθSpec.existsUnique : ∃! ABφθ : ℝ × ℝ × ℝ × ℝ, ABφθSpec ABφθ.1 ABφθ.2.1 ABφθ.2.2.1 ABφθ.2.2.2

There exist unique constants $A$, $B$, $\varphi$, and $\theta$ satisfying the spec.

noncomputable def MovingSofa.GerversSofa.A : ℝ

Gerver's constant $A$: the first component of the unique solution of ABφθSpec.

Equations

• MovingSofa.GerversSofa.A = (Exists.choose MovingSofa.GerversSofa.ABφθSpec.existsUnique).1

noncomputable def MovingSofa.GerversSofa.B : ℝ

Gerver's constant $B$: the second component of the unique solution of ABφθSpec.

Equations

• MovingSofa.GerversSofa.B = (Exists.choose MovingSofa.GerversSofa.ABφθSpec.existsUnique).2.1

noncomputable def MovingSofa.GerversSofa.φ : ℝ

Gerver's angle $\varphi$: the third component of the unique solution of ABφθSpec.

Equations

• MovingSofa.GerversSofa.φ = (Exists.choose MovingSofa.GerversSofa.ABφθSpec.existsUnique).2.2.1

noncomputable def MovingSofa.GerversSofa.θ : ℝ

Gerver's angle $\theta$: the fourth component of the unique solution of ABφθSpec.

Equations

• MovingSofa.GerversSofa.θ = (Exists.choose MovingSofa.GerversSofa.ABφθSpec.existsUnique).2.2.2

noncomputable def MovingSofa.GerversSofa.r (α : ℝ) : ℝ

The integral-path auxiliary function $r$, with break points $\varphi$, $\theta$, $\pi/2 - \theta$ and $\pi/2 - \varphi$. The functions x and y are integrals of it.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MovingSofa.GerversSofa.y (α : ℝ) : ℝ

$y(\alpha) = \int_\alpha^{\pi/2 - \varphi} r(t) \sin t \, dt$, used in the canonical integral-path definition.

Equations

• MovingSofa.GerversSofa.y α = ∫ (t : ℝ) in α..Real.pi / 2 - MovingSofa.GerversSofa.φ, MovingSofa.GerversSofa.r t * Real.sin t

noncomputable def MovingSofa.GerversSofa.x (α : ℝ) : ℝ

$x(\alpha) = 1 - \int_\alpha^{\pi/2 - \varphi} r(t) \cos t \, dt$, used in the canonical integral-path definition.

Equations

• MovingSofa.GerversSofa.x α = 1 - ∫ (t : ℝ) in α..Real.pi / 2 - MovingSofa.GerversSofa.φ, MovingSofa.GerversSofa.r t * Real.cos t

noncomputable def MovingSofa.GerversSofa.p (α : ℝ) : EuclideanSpace ℝ (Fin 2)

The rotation path of Gerver's sofa: p α is the translation applied to the hallway before it is rotated by the angle $\alpha \in [0, \pi/2]$, in the convention of rotateTranslate.

Equations

• One or more equations did not get rendered due to their size.

def MovingSofa.gerversSofa : Set (EuclideanSpace ℝ (Fin 2))

Gerver's sofa is the sofa according to the rotation path GerversSofa.p.

Equations

• MovingSofa.gerversSofa = MovingSofa.sofaOfRotateTranslatePath MovingSofa.GerversSofa.p

noncomputable def MovingSofa.sofaConstant : ENNReal

The sofa constant is the maximal area of a moving sofa.

Equations

• One or more equations did not get rendered due to their size.

Gerver's definitions in GerverSofaLean agree with the ones used here

Adapted from F07UpstreamAdapter in GerverSofaLean v1.1.0 (MIT). GerverSofaLean states its results for its own copy of the moving sofa definitions. This file identifies that copy with the definitions of MovingSofa.Canonical.Definitions.

theorem GerverSofa.PartF.ProjectAdapter.horizontalHallway_eq_model : MovingSofa.horizontalHallway = Model.horizontalHallway

theorem GerverSofa.PartF.ProjectAdapter.verticalHallway_eq_model : MovingSofa.verticalHallway = Model.verticalHallway

theorem GerverSofa.PartF.ProjectAdapter.hallway_eq_model : MovingSofa.hallway = Model.hallway

theorem GerverSofa.PartF.ProjectAdapter.isMovingSofa_iff_model (s : Set Plane) (m : ↑unitInterval → Rigid) : MovingSofa.IsMovingSofa s m ↔ Model.IsMovingSofa s m

theorem GerverSofa.PartF.ProjectAdapter.sofaOfRotateTranslatePath_eq_bodySofa (p : ℝ → Plane) : MovingSofa.sofaOfRotateTranslatePath p = bodySofa p Model.horizontalHallway Model.verticalHallway Model.hallway

noncomputable def GerverSofa.PartF.ProjectAdapter.selected : Reduced.Params

The reduced parameter tuple corresponding to the canonical choice of the unique angle solution.

Equations

• GerverSofa.PartF.ProjectAdapter.selected = GerverSofa.PartE.tupleEquiv (Exists.choose MovingSofa.GerversSofa.ABφθSpec.existsUnique)

theorem GerverSofa.PartF.ProjectAdapter.selected_eq_certified : selected = Integrals.certified

theorem GerverSofa.PartF.ProjectAdapter.p_eq_selected (t : ℝ) : MovingSofa.GerversSofa.p t = Coordinates.toPlane (Integrals.path selected t)

theorem GerverSofa.PartF.ProjectAdapter.p_eq_certified : MovingSofa.GerversSofa.p = fun (t : ℝ) => Coordinates.toPlane (Integrals.path Integrals.certified t)

theorem GerverSofa.PartF.ProjectAdapter.integral_rotation_to_full (t : ℝ) (ht : t ∈ Set.Icc 0 (Real.pi / 2)) : (rotation t) (MovingSofa.GerversSofa.p t) = Coordinates.toPlane (Romik.path PartC.params t)

theorem GerverSofa.PartF.ProjectAdapter.gerversSofa_eq_certified : MovingSofa.gerversSofa = EuclideanMotion.sofa

Moving sofa: related mathematical developments

• Geometry.Hallway.
• Geometry.HallwayParts.
• Geometry.HallwayPartsProperties.
• Geometry.HallwayRay.
• Geometry.HallwaySupport.
• Geometry.Parallelogram.
• Geometry.ParallelogramGap.
• Geometry.PathHalfPlaneCap.
• Geometry.Reflection.
• Geometry.SupportingHallway.

Geometry / Hallway

noncomputable def MovingSofa.rotationMap (t : Real.Angle) (p : Point) : Point

Counterclockwise rotation about the origin.

Equations

• MovingSofa.rotationMap t p = (EuclideanGeometry.o.rotation t) p

def MovingSofa.strips (ω : ℝ) : Set Point × Set Point × Set Point

The horizontal, vertical and rotated vertical strips.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MovingSofa.stripParallelogram (ω : ℝ) : Set Point × Point × Point

The intersection of strips and its two distinguished points.

Equations

• MovingSofa.stripParallelogram ω = ((MovingSofa.strips ω).1 ∩ (MovingSofa.strips ω).2.2, 0, !₂[Real.tan (Real.pi / 4 - ω / 2), 1])

structure MovingSofa.HallwayParts : Type

Corners, walls, rays and quadrants of a hallway.

• innerCorner : Point

  The inner reentrant corner of the hallway.

• outerCorner : Point

  The outer corner opposite the inner corner.

• a : Set Point

  The outer wall corresponding to the fixed hallway’s line x = 1.

• b : Set Point

  The inner wall corresponding to the fixed hallway’s line x = 0.

• c : Set Point

  The outer wall corresponding to the fixed hallway’s line y = 1.

• d : Set Point

  The inner wall corresponding to the fixed hallway’s line y = 0.

• bRay : Set Point

  The ray on the inner B wall extending away from the corner.

• dRay : Set Point

  The ray on the inner D wall extending away from the corner.

• outerQuadrant : Set Point

  The closed quadrant cut out by the two outer walls.

• innerQuadrant : Set Point

  The open forbidden quadrant behind the inner corner.

def MovingSofa.hallwayParts : HallwayParts

The named parts of the fixed hallway.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MovingSofa.supportingPlacement (s : Set Point) (t : Real.Angle) (p : Point) : Point

Rotation followed by the support-determined translation.

Equations

• One or more equations did not get rendered due to their size.

def MovingSofa.supportingHallway (s : Set Point) (t : Real.Angle) : Set Point

The supporting hallway of a nonempty compact set.

Equations

• MovingSofa.supportingHallway s t = MovingSofa.supportingPlacement s t '' MovingSofa.hallway

noncomputable def MovingSofa.rotatingHallwayParts (s : Set Point) (t : Real.Angle) : HallwayParts

The images of all named hallway parts under its supporting placement.

Equations

• One or more equations did not get rendered due to their size.

Geometry / Hallway Parts

theorem MovingSofa.rightAngleRotation_apply (p : Point) : EuclideanGeometry.o.rightAngleRotation p = !₂[-p.ofLp 1, p.ofLp 0]

theorem MovingSofa.inner_rotationMap_normalVector (p : Point) (t : Real.Angle) : inner ℝ (rotationMap t p) (normalVector t) = p.ofLp 0

theorem MovingSofa.inner_rotationMap_tangentVector (p : Point) (t : Real.Angle) : inner ℝ (rotationMap t p) (tangentVector t) = p.ofLp 1

theorem MovingSofa.normalVector_add_pi_div_two (t : Real.Angle) : normalVector (t + ↑(Real.pi / 2)) = tangentVector t

theorem MovingSofa.normalVector_add_pi_div_two_real (t : ℝ) : normalVector ↑(t + Real.pi / 2) = tangentVector ↑t

Rotating a real normal direction by a right angle gives the tangent direction.

theorem MovingSofa.inner_supportingPlacement_normalVector (s : Set Point) (t : Real.Angle) (p : Point) : inner ℝ (supportingPlacement s t p) (normalVector t) = p.ofLp 0 + supportValue s t - 1

theorem MovingSofa.inner_supportingPlacement_tangentVector (s : Set Point) (t : Real.Angle) (p : Point) : inner ℝ (supportingPlacement s t p) (tangentVector t) = p.ofLp 1 + supportValue s (t + ↑(Real.pi / 2)) - 1

theorem MovingSofa.hallway_eq_outerQuadrant_sdiff_innerQuadrant : hallway = hallwayParts.outerQuadrant \ hallwayParts.innerQuadrant

theorem MovingSofa.rotationMap_apply_zero (θ : Real.Angle) (x : Point) : (rotationMap θ x).ofLp 0 = θ.cos * x.ofLp 0 - θ.sin * x.ofLp 1

The first coordinate of a rotated point.

theorem MovingSofa.rotationMap_apply_one (θ : Real.Angle) (x : Point) : (rotationMap θ x).ofLp 1 = θ.sin * x.ofLp 0 + θ.cos * x.ofLp 1

The second coordinate of a rotated point.

theorem MovingSofa.mem_horizontalHallway_coordinates {p : Point} (hp : p ∈ horizontalHallway) : p.ofLp 0 ≤ 1 ∧ 0 ≤ p.ofLp 1 ∧ p.ofLp 1 ≤ 1

Coordinate bounds for a point of the horizontal side of the hallway.

theorem MovingSofa.mem_verticalHallway_coordinates {p : Point} (hp : p ∈ verticalHallway) : 0 ≤ p.ofLp 0 ∧ p.ofLp 0 ≤ 1 ∧ p.ofLp 1 ≤ 1

Coordinate bounds for a point of the vertical side of the hallway.

theorem MovingSofa.mem_hallway_iff (q : Point) : q ∈ hallway ↔ (q.ofLp 0 ≤ 1 ∧ q.ofLp 1 ≤ 1) ∧ (0 ≤ q.ofLp 0 ∨ 0 ≤ q.ofLp 1)

A point lies in the hallway exactly when it lies in the outer quadrant and is not strictly inside the inner one.

theorem MovingSofa.mem_horizontalHallway_of_coordinates (p : Point) (hx : p.ofLp 0 ≤ 1) (hy : p.ofLp 1 ∈ Set.Icc 0 1) : p ∈ horizontalHallway

Coordinate bounds place a point in the horizontal side of the hallway.

theorem MovingSofa.mem_verticalHallway_of_coordinates (p : Point) (hx : p.ofLp 0 ∈ Set.Icc 0 1) (hy : p.ofLp 1 ≤ 1) : p ∈ verticalHallway

Coordinate bounds place a point in the vertical side of the hallway.

Geometry / Hallway Parts Properties

theorem MovingSofa.supportingHallway_subset_outerQuadrant (s : Set Point) (t : Real.Angle) : supportingHallway s t ⊆ (rotatingHallwayParts s t).outerQuadrant

A supporting hallway lies in its outer quadrant.

theorem MovingSofa.rotatingHallwayParts_formulas (s : Set Point) (t : Real.Angle) : supportingHallway s t = (rotatingHallwayParts s t).outerQuadrant \ (rotatingHallwayParts s t).innerQuadrant ∧ (rotatingHallwayParts s t).innerCorner = (supportValue s t - 1) • normalVector t + (supportValue s (t + ↑(Real.pi / 2)) - 1) • tangentVector t ∧ (rotatingHallwayParts s t).outerCorner = supportValue s t • normalVector t + supportValue s (t + ↑(Real.pi / 2)) • tangentVector t ∧ (rotatingHallwayParts s t).a = normalLine t (supportValue s t) ∧ (rotatingHallwayParts s t).b = normalLine t (supportValue s t - 1) ∧ (rotatingHallwayParts s t).c = normalLine (t + ↑(Real.pi / 2)) (supportValue s (t + ↑(Real.pi / 2))) ∧ (rotatingHallwayParts s t).d = normalLine (t + ↑(Real.pi / 2)) (supportValue s (t + ↑(Real.pi / 2)) - 1) ∧ (rotatingHallwayParts s t).outerQuadrant = normalHalfPlane t (supportValue s t) false false ∩ normalHalfPlane (t + ↑(Real.pi / 2)) (supportValue s (t + ↑(Real.pi / 2))) false false ∧ (rotatingHallwayParts s t).innerQuadrant = normalHalfPlane t (supportValue s t - 1) false true ∩ normalHalfPlane (t + ↑(Real.pi / 2)) (supportValue s (t + ↑(Real.pi / 2)) - 1) false true

Geometry / Hallway Ray

theorem MovingSofa.mem_rotatingHallwayParts_bRay_iff (s : Set Point) (t : Real.Angle) (p : Point) : p ∈ (rotatingHallwayParts s t).bRay ↔ inner ℝ p (normalVector t) = supportValue s t - 1 ∧ inner ℝ p (tangentVector t) ≤ supportValue s (t + ↑(Real.pi / 2)) - 1

Coordinate description of the downward ray of a supporting hallway.

theorem MovingSofa.mem_rotatingHallwayParts_dRay_iff (s : Set Point) (t : Real.Angle) (p : Point) : p ∈ (rotatingHallwayParts s t).dRay ↔ inner ℝ p (normalVector t) ≤ supportValue s t - 1 ∧ inner ℝ p (tangentVector t) = supportValue s (t + ↑(Real.pi / 2)) - 1

Coordinate description of the leftward ray of a supporting hallway.

theorem MovingSofa.hausdorffMeasure_bRay_inter_normalHalfPlane (s : Set Point) (t u h : ℝ) (htrans : 0 < inner ℝ (tangentVector ↑t) (normalVector ↑u)) : (MeasureTheory.Measure.hausdorffMeasure 1) ((rotatingHallwayParts s ↑t).bRay ∩ normalHalfPlane (↑u) h true false) = ENNReal.ofReal (max 0 ((inner ℝ (rotatingHallwayParts s ↑t).innerCorner (normalVector ↑u) - h) / inner ℝ (tangentVector ↑t) (normalVector ↑u)))

The part of a supporting hallway ray above a transverse line has the expected length.

theorem MovingSofa.hausdorffMeasure_le_of_frame_bounds {S : Set Point} {t e lo hi : ℝ} (hS : ∀ p ∈ S, inner ℝ p (normalVector ↑t) = e ∧ lo ≤ inner ℝ p (tangentVector ↑t) ∧ inner ℝ p (tangentVector ↑t) ≤ hi) : (MeasureTheory.Measure.hausdorffMeasure 1) S ≤ ENNReal.ofReal (max 0 (hi - lo))

A planar set on one line of a moving frame, with bounded tangent coordinate, is short.

Geometry / Hallway Support

theorem MovingSofa.outerCorner_eq_support_sum (K : ConvexBody Point) (t : ℝ) : (rotatingHallwayParts ↑K ↑t).outerCorner = supportValue ↑K ↑t • normalVector ↑t + supportValue ↑K ↑(t + Real.pi / 2) • tangentVector ↑t

theorem MovingSofa.supportingIntersection_add_pi_div_two_eq_outerCorner (K : ConvexBody Point) (t : ℝ) : supportingIntersection K ↑t ↑(t + Real.pi / 2) = (rotatingHallwayParts ↑K ↑t).outerCorner

Two supporting lines at angular difference exactly π / 2 meet at the outer corner of the rotating supporting hallway.

theorem MovingSofa.outerCorner_eq_innerCorner_add (K : ConvexBody Point) (t : ℝ) : (rotatingHallwayParts ↑K ↑t).outerCorner = (rotatingHallwayParts ↑K ↑t).innerCorner + (normalVector ↑t + tangentVector ↑t)

The outer corner of the rotating supporting hallway is its inner corner translated by the frame sum u_t + v_t.

theorem MovingSofa.continuous_outerCorner (K : ConvexBody Point) : Continuous fun (s : ℝ) => (rotatingHallwayParts ↑K ↑s).outerCorner

Geometry / Parallelogram

theorem MovingSofa.mem_stripParallelogram_iff (ω : ℝ) (p : Point) : p ∈ (stripParallelogram ω).1 ↔ (0 ≤ p.ofLp 1 ∧ p.ofLp 1 ≤ 1) ∧ 0 ≤ inner ℝ p (normalVector ↑ω) ∧ inner ℝ p (normalVector ↑ω) ≤ 1

The strip intersection is described by its vertical and rotated coordinates.

theorem MovingSofa.inner_normalVector_three_pi_div_two (p : Point) : inner ℝ p (normalVector ↑(3 * Real.pi / 2)) = -p.ofLp 1

Projection on the downward unit normal negates the vertical coordinate.

theorem MovingSofa.inner_normalVector_zero (p : Point) : inner ℝ p (normalVector ↑0) = p.ofLp 0

The horizontal coordinate is the projection on the normal at angle zero.

theorem MovingSofa.inner_tangentVector_zero (p : Point) : inner ℝ p (tangentVector ↑0) = p.ofLp 1

The vertical coordinate is the projection on the tangent at angle zero.

theorem MovingSofa.inner_normalVector_pi_div_two (p : Point) : inner ℝ p (normalVector ↑(Real.pi / 2)) = p.ofLp 1

The vertical coordinate is the projection on the upward unit normal.

theorem MovingSofa.inner_tangentVector_pi_div_two (p : Point) : inner ℝ p (tangentVector ↑(Real.pi / 2)) = -p.ofLp 0

Projection on the leftward tangent at a right angle negates the horizontal coordinate.

theorem MovingSofa.inner_tangentVector_pi (p : Point) : inner ℝ p (tangentVector ↑Real.pi) = -p.ofLp 1

Projection on the leftward tangent at the straight angle negates the vertical coordinate.

theorem MovingSofa.inner_smul_normalVector_zero (x t : ℝ) : inner ℝ (x • normalVector 0) (normalVector ↑t) = x * Real.cos t

The projection of a multiple of the horizontal normal on another unit normal.

theorem MovingSofa.supportValue_stripParallelogram_bottom (ω : ℝ) : supportValue (stripParallelogram ω).1 ↑(3 * Real.pi / 2) = 0

The horizontal bottom of the strip intersection has zero downward support.

Geometry / Parallelogram Gap

theorem MovingSofa.parallelogram_gap (ω : ℝ) (hω : ω ∈ Set.Ico 0 (Real.pi / 2)) : (stripParallelogram ω).2.2 - tangentVector 0 = Real.tan ((Real.pi / 2 - ω) / 2) • normalVector 0 ∧ (stripParallelogram ω).2.2 - normalVector ↑ω = Real.tan ((Real.pi / 2 - ω) / 2) • tangentVector ↑ω ∧ (stripParallelogram ω).1 ∩ (supportingLineHalfPlane (stripParallelogram ω).1 ↑(3 * Real.pi / 2)).1 = segment ℝ 0 ((Real.cos ω)⁻¹ • normalVector 0) ∧ normalLine (↑(Real.pi / 2)) 0 ∩ normalLine (↑ω) 1 = {(Real.cos ω)⁻¹ • normalVector 0} ∧ Real.tan ((Real.pi / 2 - ω) / 2) = (Real.cos ω)⁻¹ - Real.tan ω

Geometry / Path Half Plane Cap

def MovingSofa.outerPathConstraintSet (x : ↑(Set.Icc 0 (Real.pi / 2)) → Point) : Set Point

The set satisfying the horizontal base and all upper support constraints of a path.

Equations

• One or more equations did not get rendered due to their size.

theorem MovingSofa.outerPathConstraintSet_isCap (x : ↑(Set.Icc 0 (Real.pi / 2)) → Point) (hx : x ⟨0, ⋯⟩ = 0) (hbottom : ∃ p ∈ outerPathConstraintSet x, p.ofLp 1 = 0) (htop : ∃ p ∈ outerPathConstraintSet x, p.ofLp 1 = 1) : ∃ (K : ConvexBody Point), ↑K = outerPathConstraintSet x ∧ IsCap (Real.pi / 2) K

Geometry / Reflection

noncomputable def MovingSofa.coordinateSwap : Point ≃ₗᵢ[ℝ] Point

Exchange the two coordinates of the Euclidean plane.

Equations

• MovingSofa.coordinateSwap = LinearIsometryEquiv.piLpCongrLeft 2 ℝ ℝ (Equiv.swap 0 1)

noncomputable def MovingSofa.capReflection (ω : ℝ) : Point ≃ₗᵢ[ℝ] Point

Reflection exchanging the normals at angles zero and ω + π / 2.

Equations

• MovingSofa.capReflection ω = MovingSofa.coordinateSwap.trans (EuclideanGeometry.o.rotation ↑ω)

theorem MovingSofa.capReflection_apply_zero (ω : ℝ) (p : Point) : ((capReflection ω) p).ofLp 0 = -Real.sin ω * p.ofLp 0 + Real.cos ω * p.ofLp 1

First coordinate of the cap reflection.

theorem MovingSofa.capReflection_apply_one (ω : ℝ) (p : Point) : ((capReflection ω) p).ofLp 1 = Real.cos ω * p.ofLp 0 + Real.sin ω * p.ofLp 1

Second coordinate of the cap reflection.

noncomputable def MovingSofa.stripTopReflection (ω : ℝ) (p : Point) : Point

Reflection across the line through the upper vertex of the cap strip.

Equations

• One or more equations did not get rendered due to their size.

theorem MovingSofa.stripTopReflection_eq_capReflection (ω : ℝ) (hω0 : 0 < ω) (hωle : ω ≤ Real.pi / 2) : stripTopReflection ω = ⇑(capReflection ω)

The strip-top reflection is the explicit cap reflection.

theorem MovingSofa.stripTopReflection_stripTop (ω : ℝ) : stripTopReflection ω (stripParallelogram ω).2.2 = (stripParallelogram ω).2.2

The strip-top reflection fixes the upper strip vertex.

theorem MovingSofa.capReflection_involutive (ω : ℝ) (p : Point) : (capReflection ω) ((capReflection ω) p) = p

The cap reflection is an involution.

noncomputable def MovingSofa.reflectedAngle (ω : ℝ) (a : Real.Angle) : Real.Angle

Reflection of a normal angle across the cap-reflection axis.

Equations

• MovingSofa.reflectedAngle ω a = ↑(ω + Real.pi / 2) - a

theorem MovingSofa.reflectedAngle_involutive (ω : ℝ) (a : Real.Angle) : reflectedAngle ω (reflectedAngle ω a) = a

Reflection of normal angles is involutive.

theorem MovingSofa.reflectedAngle_coe (ω t : ℝ) : reflectedAngle ω ↑t = ↑(ω + Real.pi / 2 - t)

Coercion formula for a reflected real angle.

theorem MovingSofa.capReflection_normalVector (ω a : ℝ) : (capReflection ω) (normalVector ↑a) = normalVector ↑(ω + Real.pi / 2 - a)

The cap reflection transports normal vectors at real angles.

theorem MovingSofa.capReflection_tangentVector (ω a : ℝ) : (capReflection ω) (tangentVector ↑a) = -tangentVector ↑(ω + Real.pi / 2 - a)

The cap reflection reverses tangent vectors at real angles.

theorem MovingSofa.capReflection_normalVector_angle (ω : ℝ) (a : Real.Angle) : (capReflection ω) (normalVector a) = normalVector (reflectedAngle ω a)

The cap reflection transports normal vectors by reflected angles.

theorem MovingSofa.capReflection_tangentVector_angle (ω : ℝ) (a : Real.Angle) : (capReflection ω) (tangentVector a) = -tangentVector (reflectedAngle ω a)

The cap reflection reverses tangent vectors at reflected angles.

theorem MovingSofa.inner_capReflection_normalVector (ω : ℝ) (p : Point) (a : Real.Angle) : inner ℝ ((capReflection ω) p) (normalVector a) = inner ℝ p (normalVector (reflectedAngle ω a))

Inner products with normals transform under the cap reflection.

theorem MovingSofa.inner_capReflection_tangentVector (ω : ℝ) (p : Point) (a : Real.Angle) : inner ℝ ((capReflection ω) p) (tangentVector a) = -inner ℝ p (tangentVector (reflectedAngle ω a))

Inner products with tangents transform under the cap reflection.

theorem MovingSofa.capReflection_image_normalHalfPlane (ω h : ℝ) (a : Real.Angle) (upper strict : Bool) : ⇑(capReflection ω) '' normalHalfPlane a h upper strict = normalHalfPlane (reflectedAngle ω a) h upper strict

The cap reflection transports every open or closed normal half-plane.

Geometry / Supporting Hallway

theorem MovingSofa.subset_supportingHallway (s : Set Point) (t : Real.Angle) (hs : s.Nonempty) (hc : IsCompact s) (hL : ∃ (v : Point), s ⊆ (fun (p : Point) => rotationMap t p + v) '' hallway) : s ⊆ supportingHallway s t

Moving sofa: related mathematical developments

• Analysis.SurfaceMeasure.UpperGraph.
• Analysis.SurfaceMeasure.ExposedFrontier.
• Analysis.SurfaceMeasure.RegularBoundaryHelpers.
• Analysis.SurfaceMeasure.GraphIntegral.
• Analysis.SurfaceMeasure.Construction.
• Analysis.SurfaceMeasure.GraphConvergence.
• Analysis.SurfaceMeasure.Properties.
• Analysis.SurfaceMeasure.BoundaryExtension.
• Analysis.SurfaceMeasure.Opposite.
• Analysis.SurfaceMeasure.WeakConvergence.
• Analysis.SurfaceMeasure.AtomLimits.
• Analysis.SurfaceMeasure.WeightedBoundary.

Analysis / Surface Measure / Upper Graph

theorem MovingSofa.upperGraphHeight_isGreatest (K : ConvexBody Point) (o : Point) (e : Point ≃ₗᵢ[ℝ] Point) {x : ℝ} (hx : x ∈ horizontalProjection K o e) : IsGreatest {y : ℝ | o + e.symm !₂[x, y] ∈ ↑K} (upperGraphHeight K o e x)

The upper graph height is the greatest vertical coordinate in its fiber.

theorem MovingSofa.upperGraphHeight_mem (K : ConvexBody Point) (o : Point) (e : Point ≃ₗᵢ[ℝ] Point) {x : ℝ} (hx : x ∈ horizontalProjection K o e) : o + e.symm !₂[x, upperGraphHeight K o e x] ∈ ↑K

An attained upper graph point belongs to the convex body.

theorem MovingSofa.eq_upperCoordinateGraph_of_isExteriorNormal_of_pos (K : ConvexBody Point) (o : Point) (e : Point ≃ₗᵢ[ℝ] Point) {p : Point} (hp : p ∈ K) {a : Real.Angle} (ha : IsExteriorNormal K p a) (hpos : 0 < (e (normalVector a)).ofLp 1) : p = o + e.symm !₂[(e (p - o)).ofLp 0, upperGraphHeight K o e ((e (p - o)).ofLp 0)]

A boundary point whose exterior normal has positive vertical coordinate lies on the upper coordinate graph.

theorem MovingSofa.concaveOn_upperGraphHeight (K : ConvexBody Point) (o : Point) (e : Point ≃ₗᵢ[ℝ] Point) : ConcaveOn ℝ (horizontalProjection K o e) (upperGraphHeight K o e)

The upper height function of a convex body is concave on its projection.

theorem MovingSofa.horizontalProjection_eq_Icc (K : ConvexBody Point) (o : Point) (e : Point ≃ₗᵢ[ℝ] Point) : horizontalProjection K o e = Set.Icc (horizontalBounds K o e).1 (horizontalBounds K o e).2

The horizontal projection is the interval between its compact extrema.

theorem MovingSofa.locallyLipschitzOn_upperGraphHeight (K : ConvexBody Point) (o : Point) (e : Point ≃ₗᵢ[ℝ] Point) : LocallyLipschitzOn (Set.Ioo (horizontalBounds K o e).1 (horizontalBounds K o e).2) (upperGraphHeight K o e)

The upper boundary height is locally Lipschitz inside its projection interval.

theorem MovingSofa.upperGraph_deriv_isExteriorNormal (K : ConvexBody Point) (o : Point) (e : Point ≃ₗᵢ[ℝ] Point) {x : ℝ} (hx : x ∈ Set.Ioo (horizontalBounds K o e).1 (horizontalBounds K o e).2) (hdiff : DifferentiableAt ℝ (upperGraphHeight K o e) x) : IsExteriorNormal K (o + e.symm !₂[x, upperGraphHeight K o e x]) (vectorNormalAngle (e.symm !₂[-deriv (upperGraphHeight K o e) x, 1]))

The upward normal determined by the derivative of an upper graph is exterior.

theorem MovingSofa.norm_normalVector (a : Real.Angle) : ‖normalVector a‖ = 1

Angular normal vectors have norm one.

theorem MovingSofa.mem_frontier_of_mem_of_isExteriorNormal (K : ConvexBody Point) {p : Point} (hp : p ∈ K) {a : Real.Angle} (ha : IsExteriorNormal K p a) : p ∈ frontier ↑K

A point of a convex body admitting an exterior unit normal belongs to its frontier.

theorem MovingSofa.upperGraph_mem_regularBoundary (K : ConvexBody Point) (hK : (interior ↑K).Nonempty) (o : Point) (e : Point ≃ₗᵢ[ℝ] Point) {x : ℝ} (hx : x ∈ Set.Ioo (horizontalBounds K o e).1 (horizontalBounds K o e).2) (hdiff : DifferentiableAt ℝ (upperGraphHeight K o e) x) : o + e.symm !₂[x, upperGraphHeight K o e x] ∈ regularBoundary K

A differentiable interior point of an upper boundary graph is regular.

def MovingSofa.irregularUpperGraph (K : ConvexBody Point) (o : Point) (e : Point ≃ₗᵢ[ℝ] Point) : Set Point

Points of an upper graph lying above nondifferentiability parameters.

Equations

• One or more equations did not get rendered due to their size.

theorem MovingSofa.hausdorffMeasure_irregularUpperGraph_eq_zero (K : ConvexBody Point) (o : Point) (e : Point ≃ₗᵢ[ℝ] Point) : (MeasureTheory.Measure.hausdorffMeasure 1) (irregularUpperGraph K o e) = 0

An irregular upper graph has zero one-dimensional Hausdorff measure.

theorem MovingSofa.hausdorffMeasure_irregularBoundary_eq_zero (K : ConvexBody Point) (hK : (interior ↑K).Nonempty) : (MeasureTheory.Measure.hausdorffMeasure 1) (frontier ↑K \ regularBoundary K) = 0

The irregular boundary of a planar convex body with nonempty interior has zero one-dimensional Hausdorff measure.

Exposed faces and the boundary of a convex body

The exposed faces of a convex body are exactly the sets of boundary points realizing a support value: each exposed face lies on the boundary, and, when the body has interior, every boundary point lies on some exposed face.

theorem MovingSofa.exists_mem_exposedEdge_of_mem_frontier (K : ConvexBody Point) (hK : (interior ↑K).Nonempty) {p : Point} (hp : p ∈ frontier ↑K) : ∃ (a : Real.Angle), p ∈ exposedEdge K a

Every boundary point of a convex body with nonempty interior lies on a supporting exposed face.

theorem MovingSofa.exposedEdge_subset_frontier (K : ConvexBody Point) (a : Real.Angle) : exposedEdge K a ⊆ frontier ↑K

Every exposed face of a convex body lies on its boundary.

Analysis / Surface Measure / Regular Boundary Helpers

theorem MovingSofa.not_exists_segmentPresentation_of_interior_nonempty (K : ConvexBody Point) (hint : (interior ↑K).Nonempty) : ¬∃ (d : Point × Point × Real.Angle), IsSegmentPresentation K d

A planar convex body with nonempty interior has no segment presentation.

theorem MovingSofa.not_subsingleton_of_interior_nonempty (K : ConvexBody Point) (hint : (interior ↑K).Nonempty) : ¬(↑K).Subsingleton

A convex body with nonempty interior is not a singleton.

theorem MovingSofa.isFiniteMeasure_surfaceAreaMeasure_of_interior_nonempty (K : ConvexBody Point) (hint : (interior ↑K).Nonempty) : MeasureTheory.IsFiniteMeasure (surfaceAreaMeasure K)

Surface area measure is finite when the convex body has nonempty interior.

theorem MovingSofa.surfaceAreaMeasure_eq_map_frontier_of_eq_on_regularBoundary (K : ConvexBody Point) (hK : (interior ↑K).Nonempty) (ν : Point → Real.Angle) (hν : ∀ p ∈ regularBoundary K, ν p = exteriorNormalAngle K p) : surfaceAreaMeasure K = MeasureTheory.Measure.map ν ((MeasureTheory.Measure.hausdorffMeasure 1).restrict (frontier ↑K))

Any extension of the exterior-normal angle from the regular boundary gives the surface area measure as a pushforward of frontier length.

Analysis / Surface Measure / Graph Integral

theorem MovingSofa.norm_upperGraphSurfaceIntegrand_le (K : ConvexBody Point) (o : Point) (e : Point ≃ₗᵢ[ℝ] Point) (ψ : Real.Angle → ℝ) {ε M : ℝ} (hε : 0 < ε) (hsupport : ∀ (t : Real.Angle), (e (normalVector t)).ofLp 1 < ε → ψ t = 0) (hM : ∀ (t : Real.Angle), ‖ψ t‖ ≤ M) (x : ℝ) : ‖upperGraphSurfaceIntegrand K o e ψ x‖ ≤ M * ε⁻¹

A normal support cutoff gives a uniform bound on the weighted graph density.

theorem MovingSofa.integrable_upperGraphSurfaceIntegrand (K : ConvexBody Point) (o : Point) (e : Point ≃ₗᵢ[ℝ] Point) (ψ : Real.Angle → ℝ) (hψ : Continuous ψ) {ε : ℝ} (hε : 0 < ε) (hsupport : ∀ (t : Real.Angle), (e (normalVector t)).ofLp 1 < ε → ψ t = 0) (a b : ℝ) : MeasureTheory.Integrable (upperGraphSurfaceIntegrand K o e ψ) (MeasureTheory.volume.restrict (Set.Icc a b))

The weighted surface integrand of an upper graph is integrable on its horizontal projection interval.

noncomputable def MovingSofa.upperGraphWeight (K : ConvexBody Point) (o : Point) (e : Point ≃ₗᵢ[ℝ] Point) (ψ : Real.Angle → ℝ) (p : Point) : ℝ

Evaluate an angular weight at the upper graph’s normal direction above a point’s abscissa.

Equations

• MovingSofa.upperGraphWeight K o e ψ p = ψ (MovingSofa.vectorNormalAngle (e.symm !₂[-deriv (MovingSofa.upperGraphHeight K o e) ((e (p - o)).ofLp 0), 1]))

theorem MovingSofa.eventually_integral_innerUpperGraph_eq_innerIcc (K : ConvexBody Point) (o : Point) (e : Point ≃ₗᵢ[ℝ] Point) (ψ : Real.Angle → ℝ) (hψ : Continuous ψ) (hwidth : (horizontalBounds K o e).1 < (horizontalBounds K o e).2) : ∀ᶠ (n : ℕ) in Filter.atTop, ∫ (p : Point) in (fun (x : ℝ) => o + e.symm !₂[x, upperGraphHeight K o e x]) '' Set.Icc ((horizontalBounds K o e).1 + 1 / (↑n + 1)) ((horizontalBounds K o e).2 - 1 / (↑n + 1)), upperGraphWeight K o e ψ p ∂MeasureTheory.Measure.hausdorffMeasure 1 = ∫ (x : ℝ) in Set.Icc ((horizontalBounds K o e).1 + 1 / (↑n + 1)) ((horizontalBounds K o e).2 - 1 / (↑n + 1)), upperGraphSurfaceIntegrand K o e ψ x

Integrals over the inner upper graph equal integrals over its coordinate interval.

theorem MovingSofa.tendsto_integral_innerUpperGraph (K : ConvexBody Point) (hK : (interior ↑K).Nonempty) (o : Point) (e : Point ≃ₗᵢ[ℝ] Point) (ψ : Real.Angle → ℝ) (hψ : Continuous ψ) {ε : ℝ} (hε : 0 < ε) (hsupport : ∀ (t : Real.Angle), (e (normalVector t)).ofLp 1 < ε → ψ t = 0) : Filter.Tendsto (fun (n : ℕ) => ∫ (p : Point) in (fun (x : ℝ) => o + e.symm !₂[x, upperGraphHeight K o e x]) '' Set.Icc ((horizontalBounds K o e).1 + 1 / (↑n + 1)) ((horizontalBounds K o e).2 - 1 / (↑n + 1)), upperGraphWeight K o e ψ p ∂MeasureTheory.Measure.hausdorffMeasure 1) Filter.atTop (nhds (∫ (p : Point) in frontier ↑K, ψ (exteriorNormalAngle K p) ∂MeasureTheory.Measure.hausdorffMeasure 1))

Weighted integrals over compact inner upper graphs converge to the weighted integral over the full frontier.

theorem MovingSofa.horizontalBounds_lt_of_interior_nonempty (K : ConvexBody Point) (hK : (interior ↑K).Nonempty) (o : Point) (e : Point ≃ₗᵢ[ℝ] Point) : (horizontalBounds K o e).1 < (horizontalBounds K o e).2

A planar convex body with nonempty interior has distinct horizontal bounds in every isometric coordinate frame.

Analysis / Surface Measure / Construction

theorem MovingSofa.surfaceAreaMeasure_construction (K : ConvexBody Point) : MeasureTheory.IsFiniteMeasure (surfaceAreaMeasure K) ∧ ((↑K).Subsingleton → surfaceAreaMeasure K = 0) ∧ (∀ (d : Point × Point × Real.Angle), IsSegmentPresentation K d → surfaceAreaMeasure K = ENNReal.ofReal (dist d.1 d.2.1) • (MeasureTheory.Measure.dirac d.2.2 + MeasureTheory.Measure.dirac (d.2.2 + ↑Real.pi))) ∧ ((interior ↑K).Nonempty → (MeasureTheory.Measure.hausdorffMeasure 1) (frontier ↑K) < ⊤ ∧ (MeasureTheory.Measure.hausdorffMeasure 1) (frontier ↑K \ regularBoundary K) = 0 ∧ ∀ (ν : Point → Real.Angle), (∀ p ∈ regularBoundary K, ν p = exteriorNormalAngle K p) → surfaceAreaMeasure K = MeasureTheory.Measure.map ν ((MeasureTheory.Measure.hausdorffMeasure 1).restrict (frontier ↑K))) ∧ ∀ (o : Point) (e : Point ≃ₗᵢ[ℝ] Point) (ψ : Real.Angle → ℝ), Continuous ψ → ∀ (ε : ℝ), 0 < ε → (∀ (t : Real.Angle), (e (normalVector t)).ofLp 1 < ε → ψ t = 0) → ((horizontalBounds K o e).1 < (horizontalBounds K o e).2 → MeasureTheory.Integrable (upperGraphSurfaceIntegrand K o e ψ) (MeasureTheory.volume.restrict (Set.Icc (horizontalBounds K o e).1 (horizontalBounds K o e).2)) ∧ ∫ (t : Real.Angle), ψ t ∂surfaceAreaMeasure K = ∫ (x : ℝ) in Set.Icc (horizontalBounds K o e).1 (horizontalBounds K o e).2, upperGraphSurfaceIntegrand K o e ψ x) ∧ ((horizontalBounds K o e).1 = (horizontalBounds K o e).2 → ∫ (t : Real.Angle), ψ t ∂surfaceAreaMeasure K = 0)

Analysis / Surface Measure / Graph Convergence

theorem MovingSofa.continuousAt_vectorNormalAngle {p : Point} (hp : p ≠ 0) : ContinuousAt vectorNormalAngle p

The angle of a planar vector varies continuously away from zero.

theorem MovingSofa.continuous_surfaceDensity_of_slope (e : Point ≃ₗᵢ[ℝ] Point) {ψ : Real.Angle → ℝ} (hψ : Continuous ψ) : Continuous fun (r : ℝ) => ψ (vectorNormalAngle (e.symm !₂[-r, 1])) * √(1 + r ^ 2)

The weighted upper-graph surface density is continuous as a function of slope.

theorem MovingSofa.exists_tendsto_points_with_horizontal_coordinate (K : ℕ → ConvexBody Point) (L : ConvexBody Point) (hlim : Filter.Tendsto (fun (n : ℕ) => Metric.hausdorffDist ↑(K n) ↑L) Filter.atTop (nhds 0)) (o : Point) (e : Point ≃ₗᵢ[ℝ] Point) {p : Point} (hp : p ∈ L) (hpint : (e (p - o)).ofLp 0 ∈ Set.Ioo (horizontalBounds L o e).1 (horizontalBounds L o e).2) : ∃ (q : ℕ → Point), (∀ (n : ℕ), q n ∈ K n) ∧ Filter.Tendsto q Filter.atTop (nhds p) ∧ ∀ᶠ (n : ℕ) in Filter.atTop, (e (q n - o)).ofLp 0 = (e (p - o)).ofLp 0

Points on an interior horizontal fiber can be approximated within the same fibers.

theorem MovingSofa.tendsto_upperGraphHeight_of_hausdorffDist (K : ℕ → ConvexBody Point) (L : ConvexBody Point) (hlim : Filter.Tendsto (fun (n : ℕ) => Metric.hausdorffDist ↑(K n) ↑L) Filter.atTop (nhds 0)) (o : Point) (e : Point ≃ₗᵢ[ℝ] Point) {x : ℝ} (hx : x ∈ Set.Ioo (horizontalBounds L o e).1 (horizontalBounds L o e).2) : Filter.Tendsto (fun (n : ℕ) => upperGraphHeight (K n) o e x) Filter.atTop (nhds (upperGraphHeight L o e x))

Upper graph heights converge at every interior point of the limit projection.

theorem MovingSofa.ae_tendsto_upperGraphSurfaceIntegrand_of_hausdorffDist (K : ℕ → ConvexBody Point) (L : ConvexBody Point) (hlim : Filter.Tendsto (fun (n : ℕ) => Metric.hausdorffDist ↑(K n) ↑L) Filter.atTop (nhds 0)) (o : Point) (e : Point ≃ₗᵢ[ℝ] Point) {ψ : Real.Angle → ℝ} (hψ : Continuous ψ) : ∀ᵐ (x : ℝ), x ∈ Set.Ioo (horizontalBounds L o e).1 (horizontalBounds L o e).2 → Filter.Tendsto (fun (n : ℕ) => upperGraphSurfaceIntegrand (K n) o e ψ x) Filter.atTop (nhds (upperGraphSurfaceIntegrand L o e ψ x))

Upper graph surface densities converge almost everywhere on the interior limit projection.

theorem MovingSofa.tendsto_integral_surfaceAreaMeasure_of_hausdorffDist (K : ℕ → ConvexBody Point) (L : ConvexBody Point) (hlim : Filter.Tendsto (fun (n : ℕ) => Metric.hausdorffDist ↑(K n) ↑L) Filter.atTop (nhds 0)) (o : Point) (e : Point ≃ₗᵢ[ℝ] Point) {ψ : Real.Angle → ℝ} (hψ : Continuous ψ) {ε : ℝ} (hε : 0 < ε) (hsupport : ∀ (t : Real.Angle), (e (normalVector t)).ofLp 1 < ε → ψ t = 0) : Filter.Tendsto (fun (n : ℕ) => ∫ (t : Real.Angle), ψ t ∂surfaceAreaMeasure (K n)) Filter.atTop (nhds (∫ (t : Real.Angle), ψ t ∂surfaceAreaMeasure L))

Weighted upper-normal surface integrals are continuous under Hausdorff convergence.

Analysis / Surface Measure / Properties

theorem MovingSofa.surfaceAreaMeasure_face_union (K : ConvexBody Point) : MeasureTheory.IsFiniteMeasure (surfaceAreaMeasure K) ∧ ((↑K).Subsingleton → surfaceAreaMeasure K = 0) ∧ (∀ (d : Point × Point × Real.Angle), IsSegmentPresentation K d → surfaceAreaMeasure K = ENNReal.ofReal (dist d.1 d.2.1) • (MeasureTheory.Measure.dirac d.2.2 + MeasureTheory.Measure.dirac (d.2.2 + ↑Real.pi))) ∧ ((interior ↑K).Nonempty → surfaceAreaMeasure K = MeasureTheory.Measure.map (exteriorNormalAngle K) ((MeasureTheory.Measure.hausdorffMeasure 1).restrict (regularBoundary K))) ∧ ∀ (E : Set Real.Angle), MeasurableSet E → ((interior ↑K).Nonempty ∨ ∃ (a : ℝ) (b : ℝ), a ≤ b ∧ b < a + Real.pi ∧ E ⊆ (fun (t : ℝ) => ↑t) '' Set.Icc a b) → (surfaceAreaMeasure K) E = (MeasureTheory.Measure.hausdorffMeasure 1) (⋃ t ∈ E, exposedEdge K t)

instance MovingSofa.isFiniteMeasure_surfaceAreaMeasure (K : ConvexBody Point) : MeasureTheory.IsFiniteMeasure (surfaceAreaMeasure K)

theorem MovingSofa.surfaceAreaMeasure_null_of_exposedEdge_subset_singleton (K : ConvexBody Point) {E : Set Real.Angle} (hE : MeasurableSet E) {a b : ℝ} (hab : a ≤ b) (hba : b < a + Real.pi) (hEab : E ⊆ (fun (t : ℝ) => ↑t) '' Set.Icc a b) (p : Point) (hsub : ∀ t ∈ E, exposedEdge K t ⊆ {p}) : (surfaceAreaMeasure K) E = 0

A measurable set of normal directions lying in an angular interval of width less than π, on which every face of K degenerates to one and the same point, is null for the surface area measure of K.

theorem MovingSofa.surfaceAreaMeasure_angleImage_Ioo_eq_zero_of_mem_exposedEdge (K : ConvexBody Point) {a b : ℝ} (hab : a < b) (hba : b < a + Real.pi) {p : Point} (hpa : p ∈ exposedEdge K ↑a) (hpb : p ∈ exposedEdge K ↑b) : (surfaceAreaMeasure K) ((fun (s : ℝ) => ↑s) '' Set.Ioo a b) = 0

The surface measure of a convex body vanishes on the open angular window strictly between two normal angles less than a half turn apart at which one and the same point attains the support.

Analysis / Surface Measure / Boundary Extension

theorem MovingSofa.intervalStieltjesMeasure_eq_surfaceIntegral_of_increment (K : ConvexBody Point) {a b : ℝ} (hab : a < b) (hturn : b ≤ a + 2 * Real.pi) (f : Fin 2 → RightContinuousIntervalBV a b) (hf : ∀ (i : Fin 2) (t : ↑(Set.Icc a b)), (f i).toFun t = (edgeVertices K ↑↑t).1.ofLp i) (hinc : ∀ (c d : ↑(Set.Icc a b)), c < d → ∀ (i : Fin 2), (edgeVertices K ↑↑d).1.ofLp i - (edgeVertices K ↑↑c).1.ofLp i = ∫ (u : Real.Angle) in (fun (t : ℝ) => ↑t) '' Set.Ioc ↑c ↑d, (tangentVector u).ofLp i ∂surfaceAreaMeasure K) (i : Fin 2) (E : Set ↑(Set.Icc a b)) : MeasurableSet E → (∀ t ∈ E, a < ↑t) → (intervalStieltjesMeasure (f i)) E = ∫ (u : Real.Angle) in (fun (t : ↑(Set.Icc a b)) => ↑↑t) '' E, (tangentVector u).ofLp i ∂surfaceAreaMeasure K

Agreement of positive-vertex increments with tangent-coordinate surface integrals extends from half-open subintervals to every measurable set avoiding the initial endpoint.

Analysis / Surface Measure / Opposite

noncomputable def MovingSofa.oppositeSurfaceData (K : ConvexBody Point) : MeasureTheory.Measure Real.Angle × (Real.Angle → ℝ)

The opposite-angle surface measure and support function.

Equations

• One or more equations did not get rendered due to their size.

theorem MovingSofa.oppositeSurfaceData_fst (K : ConvexBody Point) : (oppositeSurfaceData K).1 = MeasureTheory.Measure.map (fun (t : Real.Angle) => t - ↑Real.pi) (surfaceAreaMeasure K)

The opposite surface measure is the half-turn translate of the surface measure.

instance MovingSofa.isFiniteMeasure_oppositeSurfaceData (K : ConvexBody Point) : MeasureTheory.IsFiniteMeasure (oppositeSurfaceData K).1

theorem MovingSofa.continuous_oppositeSurfaceData_snd (K : ConvexBody Point) : Continuous (oppositeSurfaceData K).2

The opposite support function of a convex body is continuous in the normal direction.

theorem MovingSofa.setIntegral_oppositeSurfaceData_angleImage_Ioo (K : ConvexBody Point) {a b a' b' : ℝ} (ha : a' = a + Real.pi) (hb : b' = b + Real.pi) {f : Real.Angle → ℝ} (hf : Measurable f) : ∫ (t : Real.Angle) in (fun (s : ℝ) => ↑s) '' Set.Ioo a b, f (t + ↑Real.pi) ∂(oppositeSurfaceData K).1 = ∫ (t : Real.Angle) in (fun (s : ℝ) => ↑s) '' Set.Ioo a' b', f t ∂surfaceAreaMeasure K

Integrating a π-shifted integrand against the opposite surface measure over an open angular window is integrating the integrand itself against the surface-area measure over the π-translated window. The endpoints of the translated window are given as hypotheses so that call sites may normalize them arithmetically.

theorem MovingSofa.oppositeSurfaceData_angleImage_Ioo_eq_zero_of_mem_exposedEdge (K : ConvexBody Point) {a b : ℝ} (hab : a < b) (hba : b < a + Real.pi) {p : Point} (hpa : p ∈ exposedEdge K ↑(a + Real.pi)) (hpb : p ∈ exposedEdge K ↑(b + Real.pi)) : (oppositeSurfaceData K).1 ((fun (s : ℝ) => ↑s) '' Set.Ioo a b) = 0

The opposite surface measure vanishes on an open angular window whose half-turn translate carries a single support point.

Analysis / Surface Measure / Weak Convergence

theorem MovingSofa.exists_normalCoordinate_partition : ∃ (e : Fin 4 → Point ≃ₗᵢ[ℝ] Point) (χ : Fin 4 → Real.Angle → ℝ), (∀ (i : Fin 4), Continuous (χ i)) ∧ (∀ (t : Real.Angle), ∑ i : Fin 4, χ i t = 1) ∧ ∀ (i : Fin 4) (t : Real.Angle), ((e i) (normalVector t)).ofLp 1 < 1 / 2 → χ i t = 0

Four coordinate half-circles admit a continuous partition of unity supported where the upward component of the normal is at least one half.

theorem MovingSofa.tendsto_surfaceIntegral_of_normal_patches (K : ℕ → ConvexBody Point) (L : ConvexBody Point) (hpatch : ∀ (e : Point ≃ₗᵢ[ℝ] Point) (ψ : Real.Angle → ℝ), Continuous ψ → (∀ (t : Real.Angle), (e (normalVector t)).ofLp 1 < 1 / 2 → ψ t = 0) → Filter.Tendsto (fun (n : ℕ) => ∫ (t : Real.Angle), ψ t ∂surfaceAreaMeasure (K n)) Filter.atTop (nhds (∫ (t : Real.Angle), ψ t ∂surfaceAreaMeasure L))) (φ : Real.Angle → ℝ) (hφ : Continuous φ) : Filter.Tendsto (fun (n : ℕ) => ∫ (t : Real.Angle), φ t ∂surfaceAreaMeasure (K n)) Filter.atTop (nhds (∫ (t : Real.Angle), φ t ∂surfaceAreaMeasure L))

Convergence for test functions supported in upward normal patches implies convergence for all continuous test functions.

theorem MovingSofa.surfaceAreaMeasure_weak_continuity (K : ℕ → ConvexBody Point) (L : ConvexBody Point) (hlim : Filter.Tendsto (fun (n : ℕ) => Metric.hausdorffDist ↑(K n) ↑L) Filter.atTop (nhds 0)) (φ : Real.Angle → ℝ) (hφ : Continuous φ) : Filter.Tendsto (fun (n : ℕ) => ∫ (u : Real.Angle), φ u ∂surfaceAreaMeasure (K n)) Filter.atTop (nhds (∫ (u : Real.Angle), φ u ∂surfaceAreaMeasure L))

Analysis / Surface Measure / Atom Limits

theorem MovingSofa.le_surfaceAreaMeasure_atom_of_tendsto {K : ℕ → ConvexBody Point} {L : ConvexBody Point} (hK : Filter.Tendsto (fun (n : ℕ) => Metric.hausdorffDist ↑(K n) ↑L) Filter.atTop (nhds 0)) {u : Real.Angle} {x : ℕ → ℝ} {a : ℝ} (hx : Filter.Tendsto x Filter.atTop (nhds a)) (hle : ∀ (n : ℕ), x n ≤ ((surfaceAreaMeasure (K n)) {u}).toReal) : a ≤ ((surfaceAreaMeasure L) {u}).toReal

An upper bound by a moving surface atom passes to a Hausdorff limit.

Analysis / Surface Measure / Weighted Boundary

theorem MovingSofa.measurableEmbedding_angleCoe_Ioc {a b : ℝ} (hturn : b ≤ a + 2 * Real.pi) : MeasurableEmbedding fun (t : ↑(Set.Ioc a b)) => ↑↑t

On a half-open parameter interval of at most one turn, the angular projection is a measurable embedding.

theorem MovingSofa.exists_bounded_measurable_angle_extension {a b : ℝ} (hturn : b ≤ a + 2 * Real.pi) (ψ : ↑(Set.Ioc a b) → ℝ) (hψm : Measurable ψ) (C : ℝ) (hC : 0 ≤ C) (hψb : ∀ (t : ↑(Set.Ioc a b)), ‖ψ t‖ ≤ C) : ∃ (Q : Real.Angle → ℝ), Measurable Q ∧ (∀ (u : Real.Angle), ‖Q u‖ ≤ C) ∧ ∀ (t : ↑(Set.Ioc a b)), Q ↑↑t = ψ t

A bounded measurable function on a half-open parameter interval of at most one full turn extends to a bounded measurable function of the angle.

theorem MovingSofa.intervalStieltjesIntegral_positiveVertex_coordinate_of_measurable (K : ConvexBody Point) {a b : ℝ} (hab : a < b) (hturn : b ≤ a + 2 * Real.pi) (f : Fin 2 → RightContinuousIntervalBV a b) (hf : ∀ (i : Fin 2) (E : Set ↑(Set.Icc a b)), MeasurableSet E → (∀ t ∈ E, a < ↑t) → (intervalStieltjesMeasure (f i)) E = ∫ (u : Real.Angle) in (fun (t : ↑(Set.Icc a b)) => ↑↑t) '' E, (tangentVector u).ofLp i ∂surfaceAreaMeasure K) (i : Fin 2) (Q : Real.Angle → ℝ) (C : ℝ) (hQm : Measurable fun (t : ↑(Set.Ioc a b)) => Q ↑↑t) (hQb : ∀ (u : Real.Angle), ‖Q u‖ ≤ C) (E : Set ↑(Set.Icc a b)) (hE : MeasurableSet E) (hEa : ∀ t ∈ E, a < ↑t) : intervalStieltjesIntegral (f i) (fun (t : ↑(Set.Icc a b)) => Q ↑↑t) E = ∫ (u : Real.Angle) in (fun (t : ↑(Set.Icc a b)) => ↑↑t) '' E, Q u * (tangentVector u).ofLp i ∂surfaceAreaMeasure K

A bounded measurable angular weight may be transported through the positive-vertex Stieltjes identity, coordinate by coordinate.

theorem MovingSofa.intervalStieltjesIntegral_positiveVertex_coordinate (K : ConvexBody Point) {a b : ℝ} (hab : a < b) (hturn : b ≤ a + 2 * Real.pi) (f : Fin 2 → RightContinuousIntervalBV a b) (hf : ∀ (i : Fin 2) (E : Set ↑(Set.Icc a b)), MeasurableSet E → (∀ t ∈ E, a < ↑t) → (intervalStieltjesMeasure (f i)) E = ∫ (u : Real.Angle) in (fun (t : ↑(Set.Icc a b)) => ↑↑t) '' E, (tangentVector u).ofLp i ∂surfaceAreaMeasure K) (i : Fin 2) (Q : Real.Angle → ℝ) (hQ : Continuous Q) (E : Set ↑(Set.Icc a b)) (hE : MeasurableSet E) (hEa : ∀ t ∈ E, a < ↑t) : intervalStieltjesIntegral (f i) (fun (t : ↑(Set.Icc a b)) => Q ↑↑t) E = ∫ (u : Real.Angle) in (fun (t : ↑(Set.Icc a b)) => ↑↑t) '' E, Q u * (tangentVector u).ofLp i ∂surfaceAreaMeasure K

A continuous angular weight may be transported through the positive-vertex Stieltjes identity, coordinate by coordinate.

theorem MovingSofa.integrableOn_mul_tangentVector_of_bounded (K : ConvexBody Point) {a b : ℝ} (hturn : b ≤ a + 2 * Real.pi) (i : Fin 2) (Q : Real.Angle → ℝ) (C : ℝ) (hQm : Measurable fun (t : ↑(Set.Ioc a b)) => Q ↑↑t) (hQb : ∀ (u : Real.Angle), ‖Q u‖ ≤ C) (S : Set Real.Angle) (hS : MeasurableSet S) (hSsub : S ⊆ Set.range fun (t : ↑(Set.Ioc a b)) => ↑↑t) : MeasureTheory.IntegrableOn (fun (u : Real.Angle) => Q u * (tangentVector u).ofLp i) S (surfaceAreaMeasure K)

A bounded measurable angular weight times a frame tangent coordinate is integrable against the surface measure on every measurable set of angles represented in the half-open parameter interval.

theorem MovingSofa.sum_intervalStieltjesIntegral_positiveVertex_dot (K : ConvexBody Point) {a b : ℝ} (hab : a < b) (hturn : b ≤ a + 2 * Real.pi) (f : Fin 2 → RightContinuousIntervalBV a b) (hf : ∀ (i : Fin 2) (E : Set ↑(Set.Icc a b)), MeasurableSet E → (∀ t ∈ E, a < ↑t) → (intervalStieltjesMeasure (f i)) E = ∫ (u : Real.Angle) in (fun (t : ↑(Set.Icc a b)) => ↑↑t) '' E, (tangentVector u).ofLp i ∂surfaceAreaMeasure K) (φ : Fin 2 → ↑(Set.Icc a b) → ℝ) (C : ℝ) (hC : 0 ≤ C) (hφm : ∀ (i : Fin 2), Measurable (φ i)) (hφb : ∀ (i : Fin 2) (t : ↑(Set.Icc a b)), ‖φ i t‖ ≤ C) (g : Real.Angle → ℝ) (hg : ∀ (t : ↑(Set.Icc a b)), a < ↑t → ∑ i : Fin 2, φ i t * (tangentVector ↑↑t).ofLp i = g ↑↑t) (E : Set ↑(Set.Icc a b)) (hE : MeasurableSet E) (hEa : ∀ t ∈ E, a < ↑t) : ∑ i : Fin 2, intervalStieltjesIntegral (f i) (φ i) E = ∫ (u : Real.Angle) in (fun (t : ↑(Set.Icc a b)) => ↑↑t) '' E, g u ∂surfaceAreaMeasure K

Pairing the positive-vertex Stieltjes measures with a bounded measurable planar weight is the surface integral of the pointwise contraction of that weight with the tangent frame.

theorem MovingSofa.sum_intervalStieltjesIntegral_positiveVertex_tangent (K : ConvexBody Point) {a b : ℝ} (hab : a < b) (hturn : b ≤ a + 2 * Real.pi) (f : Fin 2 → RightContinuousIntervalBV a b) (hf : ∀ (i : Fin 2) (E : Set ↑(Set.Icc a b)), MeasurableSet E → (∀ t ∈ E, a < ↑t) → (intervalStieltjesMeasure (f i)) E = ∫ (u : Real.Angle) in (fun (t : ↑(Set.Icc a b)) => ↑↑t) '' E, (tangentVector u).ofLp i ∂surfaceAreaMeasure K) (E : Set ↑(Set.Icc a b)) (hE : MeasurableSet E) (hEa : ∀ t ∈ E, a < ↑t) : ∑ i : Fin 2, intervalStieltjesIntegral (f i) (fun (t : ↑(Set.Icc a b)) => (tangentVector ↑↑t).ofLp i) E = ((surfaceAreaMeasure K) ((fun (t : ↑(Set.Icc a b)) => ↑↑t) '' E)).toReal

Pairing the positive-vertex Stieltjes measure with the tangent frame gives surface mass.

theorem MovingSofa.sum_intervalStieltjesIntegral_positiveVertex_normal (K : ConvexBody Point) {a b : ℝ} (hab : a < b) (hturn : b ≤ a + 2 * Real.pi) (f : Fin 2 → RightContinuousIntervalBV a b) (hf : ∀ (i : Fin 2) (E : Set ↑(Set.Icc a b)), MeasurableSet E → (∀ t ∈ E, a < ↑t) → (intervalStieltjesMeasure (f i)) E = ∫ (u : Real.Angle) in (fun (t : ↑(Set.Icc a b)) => ↑↑t) '' E, (tangentVector u).ofLp i ∂surfaceAreaMeasure K) (E : Set ↑(Set.Icc a b)) (hE : MeasurableSet E) (hEa : ∀ t ∈ E, a < ↑t) : ∑ i : Fin 2, intervalStieltjesIntegral (f i) (fun (t : ↑(Set.Icc a b)) => (normalVector ↑↑t).ofLp i) E = 0

Pairing the positive-vertex Stieltjes measure with the normal frame vanishes.

Moving sofa: related mathematical developments

• Cap.Contacts.
• Cap.ArmCoordinates.
• Cap.ContactIdentities.
• Cap.HalfPlanes.
• Cap.FanProjection.
• Cap.HallwayQuadrant.
• Cap.LowerNormalMeasure.
• Cap.ReflectionGeometry.
• Cap.SupportIntersections.
• Cap.TopCorner.
• Cap.Vertical.

Cap / Contacts

noncomputable def MovingSofa.directionalWidth (s : Set Point) (t : Real.Angle) : ℝ

Width in a normal direction, for geometric use on nonempty compact sets.

Equations

• MovingSofa.directionalWidth s t = MovingSofa.supportValue s t + MovingSofa.supportValue s (t + ↑Real.pi)

noncomputable def MovingSofa.capVertices {ω : ℝ} (K : CapSpace ω) (t : ℝ) : (Point × Point) × Point × Point

The positive/negative contacts at the two outer supporting walls.

Equations

• MovingSofa.capVertices K t = (MovingSofa.edgeVertices ↑K ↑t, MovingSofa.edgeVertices ↑K ↑(t + Real.pi / 2))

noncomputable def MovingSofa.tangentArmLengths (K : RightAngleCapSpace) (t : ℝ) : (ℝ × ℝ) × ℝ × ℝ

The positive/negative right and left tangent arm lengths of a right-angle cap.

Equations

• One or more equations did not get rendered due to their size.

def MovingSofa.capWedge {ω : ℝ} (K : CapSpace ω) (t : ℝ) : Set Point

The open inner quadrant clipped by the fan.

Equations

• MovingSofa.capWedge K t = MovingSofa.capFan ω ∩ (MovingSofa.rotatingHallwayParts ↑↑K ↑t).innerQuadrant

noncomputable def MovingSofa.wedgeEndpoints {ω : ℝ} (K : CapSpace ω) (t : ℝ) : Point × Point

The two inner-wall intersections with the lower fan boundary lines.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MovingSofa.wedgeGaps {ω : ℝ} (K : CapSpace ω) (t : ℝ) : ℝ × ℝ

Signed right and left gaps between the wedge endpoints and bottom cap contacts.

Equations

• One or more equations did not get rendered due to their size.

def MovingSofa.convexBoundaryArc (K : ConvexBody Point) (a b : ℝ) : Set Point

The selected short boundary arc, including only the specified endpoints.

Equations

• MovingSofa.convexBoundaryArc K a b = ({(MovingSofa.edgeVertices K ↑a).1} ∪ ⋃ t ∈ Set.Ioo a b, MovingSofa.exposedEdge K ↑t) ∪ {(MovingSofa.edgeVertices K ↑b).2}

theorem MovingSofa.wedgeGaps_fst_eq_supportValue {ω : ℝ} (K : CapSpace ω) (t : ℝ) : (wedgeGaps K t).1 = supportValue (↑↑K) 0 - (supportValue ↑↑K ↑t - 1) / Real.cos t

The right wedge gap in support-function coordinates.

theorem MovingSofa.wedgeGaps_snd_eq_supportValue {ω : ℝ} (K : CapSpace ω) (t : ℝ) : (wedgeGaps K t).2 = supportValue ↑↑K ↑(ω + Real.pi / 2) - (supportValue ↑↑K ↑(t + Real.pi / 2) - 1) / Real.cos (ω - t)

The left wedge gap in support-function coordinates.

theorem MovingSofa.wedgeEndpoints_fst_coords {ω : ℝ} (K : CapSpace ω) (t : ℝ) : (wedgeEndpoints K t).1.ofLp 0 = (supportValue ↑↑K ↑t - 1) / Real.cos t ∧ (wedgeEndpoints K t).1.ofLp 1 = 0

The right wedge endpoint lies on the horizontal axis, at the horizontal intercept of the right inner wall.

theorem MovingSofa.wedgeEndpoints_snd_coords (K : RightAngleCapSpace) (t : ℝ) : (wedgeEndpoints K t).2.ofLp 0 = -((supportValue ↑↑K ↑(t + Real.pi / 2) - 1) / Real.sin t) ∧ (wedgeEndpoints K t).2.ofLp 1 = 0

For a right-angle cap the left wedge endpoint also lies on the horizontal axis, at the horizontal intercept of the left inner wall.

Cap / Arm Coordinates

theorem MovingSofa.tangentArmLengths_positive_frame (K : RightAngleCapSpace) (t : ℝ) : (tangentArmLengths K t).1.1 = supportValue ↑↑K ↑(t + Real.pi / 2) - inner ℝ (edgeVertices ↑K ↑t).1 (tangentVector ↑t) ∧ (tangentArmLengths K t).2.1 = inner ℝ (edgeVertices ↑K ↑t).1 (normalVector ↑t) + inner ℝ (edgeVertices ↑K ↑(t + Real.pi / 2)).1 (tangentVector ↑(t + Real.pi / 2))

Express the two positive arm lengths through support and moving-frame coordinates.

Cap / Contact Identities

theorem MovingSofa.capTangentArm_identities (K : RightAngleCapSpace) (t : ℝ) : (rotatingHallwayParts ↑↑K ↑t).outerCorner = (capVertices K t).1.1 + (tangentArmLengths K t).1.1 • tangentVector ↑t ∧ (rotatingHallwayParts ↑↑K ↑t).outerCorner = (capVertices K t).1.2 + (tangentArmLengths K t).1.2 • tangentVector ↑t ∧ (rotatingHallwayParts ↑↑K ↑t).outerCorner = (capVertices K t).2.1 + (tangentArmLengths K t).2.1 • normalVector ↑t ∧ (rotatingHallwayParts ↑↑K ↑t).outerCorner = (capVertices K t).2.2 + (tangentArmLengths K t).2.2 • normalVector ↑t

theorem MovingSofa.surfaceAreaMeasure_atom_length (K : ConvexBody Point) (t : Real.Angle) : (surfaceAreaMeasure K) {t} = (MeasureTheory.Measure.hausdorffMeasure 1) (exposedEdge K t) ∧ (surfaceAreaMeasure K) {t} = ENNReal.ofReal (dist (edgeVertices K t).1 (edgeVertices K t).2) ∧ (edgeVertices K t).1 = (edgeVertices K t).2 + ((surfaceAreaMeasure K) {t}).toReal • tangentVector t

Cap / Half Planes

theorem MovingSofa.HasHalfPlaneRepresentation.finite_constraints {K : ConvexBody Point} {N : Set Real.Angle} (hN : N.Finite) (hK : HasHalfPlaneRepresentation (↑K) N) : ∃ (constraints : Set (Real.Angle × ℝ)), constraints.Finite ∧ (∀ c ∈ constraints, c.1 ∈ N) ∧ ↑K = ⋂ c ∈ constraints, normalHalfPlane c.1 c.2 false false

A finite set of allowed normals gives a finite supporting-half-plane representation.

theorem MovingSofa.HasHalfPlaneRepresentation.translate {K : ConvexBody Point} {N : Set Real.Angle} (hK : HasHalfPlaneRepresentation (↑K) N) (v : Point) : HasHalfPlaneRepresentation (↑(K.translate v)) N

Translation preserves a half-plane representation's allowed normals.

theorem MovingSofa.CapSpace.subset_capFan {ω : ℝ} (K : CapSpace ω) : ↑↑K ⊆ capFan ω

A normalized cap is contained in its lower fan.

theorem MovingSofa.CapSpace.mem_of_mem_capFan_of_lt_supportValue {ω : ℝ} (K : CapSpace ω) {p : Point} (hp : p ∈ capFan ω) (hupper : ∀ t ∈ Set.Icc 0 (ω + Real.pi / 2), inner ℝ p (normalVector ↑t) < supportValue ↑↑K ↑t) : p ∈ ↑↑K

Fan membership and strict upper support inequalities imply cap membership.

theorem MovingSofa.CapSpace.subset_stripParallelogram {ω : ℝ} (K : CapSpace ω) : ↑↑K ⊆ (stripParallelogram ω).1

A normalized cap lies in the intersection of its two unit strips.

theorem MovingSofa.HasHalfPlaneRepresentation.eq_iInter_supportValue {K : ConvexBody Point} {N : Set Real.Angle} (hK : HasHalfPlaneRepresentation (↑K) N) : ↑K = ⋂ t ∈ N, normalHalfPlane t (supportValue (↑K) t) false false

A half-plane representation can be tightened at every allowed normal.

theorem MovingSofa.CapSpace.mem_of_mem_capFan_of_le_supportValue {ω : ℝ} (K : CapSpace ω) {p : Point} (hp : p ∈ capFan ω) (hupper : ∀ t ∈ capUpperAngles ω, inner ℝ p (normalVector ↑t) ≤ supportValue ↑↑K ↑t) : p ∈ ↑↑K

A fan point satisfying all upper supporting inequalities belongs to the cap.

theorem MovingSofa.CapSpace.supportValue_upper_bounds {ω t : ℝ} (K : CapSpace ω) (ht : t ∈ Set.Ioo 0 ω) : supportValue ↑↑K ↑t ≤ Real.cos t * supportValue (↑↑K) 0 + Real.sin t ∧ supportValue ↑↑K ↑(t + Real.pi / 2) ≤ Real.sin (ω - t) + Real.cos (ω - t) * supportValue ↑↑K ↑(ω + Real.pi / 2)

Upper support bounds supplied by the two unit-height constraints of a cap.

theorem MovingSofa.CapSpace.inner_normalVector_pi_div_two_nonneg {ω : ℝ} (K : CapSpace ω) {q : Point} (hq : q ∈ ↑↑K) : 0 ≤ inner ℝ q (normalVector ↑(Real.pi / 2))

Every point of a cap lies above the horizontal base line.

theorem MovingSofa.CapSpace.base_projection_mem (K : CapSpace (Real.pi / 2)) {q : Point} (hq : q ∈ ↑↑K) : q - q.ofLp 1 • normalVector ↑(Real.pi / 2) ∈ ↑↑K

Lowering a point of a right-angle cap onto the base line keeps it inside the cap: every upper normal of such a cap has nonnegative vertical component, so no upper constraint is tightened, and the two base constraints of the fan coincide here and hold with equality.

theorem MovingSofa.CapSpace.apply_one_eq_one (K : CapSpace (Real.pi / 2)) {p : Point} (hp : inner ℝ p (normalVector ↑(Real.pi / 2)) = supportValue ↑↑K ↑(Real.pi / 2)) : p.ofLp 1 = 1

The top supporting line of a right-angle cap is the horizontal line of height one, so every point attaining the support value at the vertical normal has height one.

theorem MovingSofa.CapSpace.edgeVertices_fst_apply_one_eq_zero (K : CapSpace (Real.pi / 2)) {s : ℝ} (hs : Real.sin s = 0) (hface : (edgeVertices ↑K ↑s).1 = (edgeVertices ↑K ↑s).2) : (edgeVertices ↑K ↑s).1.ofLp 1 = 0

A singleton extreme face of a right-angle cap at a horizontal normal lies on the base line. Lowering its unique point onto the base line keeps it in the cap, and a horizontal normal does not see that vertical displacement, so the lowered point lies in the same face; the face being a singleton, the displacement vanishes.

theorem MovingSofa.hasHalfPlaneRepresentation_of_base_projection (M : ConvexBody Point) (hbase : supportValue ↑M ↑(3 * Real.pi / 2) = 0) (hproj : ∀ q ∈ ↑M, q - q.ofLp 1 • normalVector ↑(Real.pi / 2) ∈ ↑M) : HasHalfPlaneRepresentation (↑M) ((fun (t : ℝ) => ↑t) '' capUpperAngles (Real.pi / 2) ∪ capLowerNormals (Real.pi / 2))

A convex body with vanishing base support value that is stable under vertical projection to the base line is cut out by upper half-planes together with the base half-plane.

Cap / Fan Projection

theorem MovingSofa.supportValue_nonneg_of_mem_capUpperAngles {ω : ℝ} (K : CapSpace ω) (hω : ω < Real.pi / 2) {φ : ℝ} (hφ : φ ∈ capUpperAngles ω) : 0 ≤ supportValue ↑↑K ↑φ

Support values in the upper angular range of a non-right cap are nonnegative.

theorem MovingSofa.zero_mem_cap_of_lt {ω : ℝ} (K : CapSpace ω) (hω : ω < Real.pi / 2) : 0 ∈ ↑↑K

The origin belongs to every cap of angle strictly below a right angle.

theorem MovingSofa.supportValue_zero_smul_normalVector_mem {ω : ℝ} (K : CapSpace ω) : supportValue (↑↑K) 0 • normalVector 0 ∈ ↑↑K

The normal projection of the zero-angle support value belongs to the cap.

theorem MovingSofa.supportValue_pi_smul_normalVector_mem_of_eq {ω : ℝ} (K : CapSpace ω) (hω : ω = Real.pi / 2) : supportValue ↑↑K ↑Real.pi • normalVector ↑Real.pi ∈ ↑↑K

At a right angle, the opposite normal projection belongs to the cap.

theorem MovingSofa.supportValue_add_pi_div_two_smul_tangentVector_mem_of_lt {ω : ℝ} (K : CapSpace ω) (hω : ω < Real.pi / 2) : supportValue ↑↑K ↑(ω + Real.pi / 2) • tangentVector ↑ω ∈ ↑↑K

For a non-right cap, the terminal tangent projection belongs to the cap.

Cap / Hallway Quadrant

theorem MovingSofa.rotatingHallwayParts_innerQuadrant (s : Set Point) (t : ℝ) : (rotatingHallwayParts s ↑t).innerQuadrant = innerQuadrant s t

The inward quadrant of the supporting hallway at angle t is the inward quadrant of s written in support-value coordinates.

The surface area measure of a right-angle cap at its lower normals

A right-angle cap lies above its base line and is stable under vertical projection onto it, so at a strictly downward normal direction the support value is attained only on the base line, at whichever horizontal extremum the sign of the horizontal normal component selects. Both open quarter arcs of lower normals therefore carry faces that degenerate to a single base corner, and the surface area measure vanishes on them (MovingSofa.CapSpace.surfaceAreaMeasure_image_Ioo_lower_eq_zero). Outside the closed upper semicircle only the bottom normal 3π / 2 is left, so an integrand vanishing there integrates to zero (MovingSofa.CapSpace.setIntegral_compl_image_Icc_zero_pi_eq_zero).

theorem MovingSofa.CapSpace.exposedEdge_subset_singleton_of_isMaxOn (K : CapSpace (Real.pi / 2)) {q : Point} (hq : q ∈ ↑↑K) {t : ℝ} (hcos : Real.cos t ≠ 0) (hsin : Real.sin t < 0) (hmax : IsMaxOn (fun (p : Point) => p.ofLp 0 * Real.cos t) (↑↑K) q) : exposedEdge ↑K ↑t ⊆ {q - q.ofLp 1 • normalVector ↑(Real.pi / 2)}

At a strictly downward normal direction the face of a right-angle cap degenerates to the base point below a horizontal extremum: positive height strictly lowers the normal coordinate, and on the base line the sign of Real.cos t selects a horizontal extremum.

theorem MovingSofa.CapSpace.exists_exposedEdge_subset_singleton (K : CapSpace (Real.pi / 2)) : ∃ (pl : Point) (pr : Point), (∀ (t : ℝ), Real.cos t < 0 → Real.sin t < 0 → exposedEdge ↑K ↑t ⊆ {pl}) ∧ ∀ (t : ℝ), 0 < Real.cos t → Real.sin t < 0 → exposedEdge ↑K ↑t ⊆ {pr}

The two base corners of a right-angle cap: on the open lower left quarter of normals every face degenerates to the base point below a leftmost point of the cap, and on the open lower right quarter to the base point below a rightmost one.

theorem MovingSofa.CapSpace.surfaceAreaMeasure_image_Ioo_lower_eq_zero (K : CapSpace (Real.pi / 2)) : (surfaceAreaMeasure ↑K) ((fun (s : ℝ) => ↑s) '' Set.Ioo Real.pi (3 * Real.pi / 2)) = 0 ∧ (surfaceAreaMeasure ↑K) ((fun (s : ℝ) => ↑s) '' Set.Ioo (3 * Real.pi / 2) (2 * Real.pi)) = 0

The surface area measure of a right-angle cap vanishes on both open quarter arcs of lower normals, because there every face degenerates to a single base corner.

theorem MovingSofa.CapSpace.setIntegral_compl_image_Icc_zero_pi_eq_zero (K : CapSpace (Real.pi / 2)) (f : Real.Angle → ℝ) (hf : f ↑(3 * Real.pi / 2) = 0) : ∫ (t : Real.Angle) in ((fun (s : ℝ) => ↑s) '' Set.Icc 0 Real.pi)ᶜ, f t ∂surfaceAreaMeasure ↑K = 0

Outside the closed upper semicircle the surface area measure of a right-angle cap is carried by the single downward normal 3π / 2, so any integrand vanishing there integrates to zero.

Cap / Reflection Geometry

def MovingSofa.reflectedBody (ω : ℝ) (K : ConvexBody Point) : ConvexBody Point

Image of a convex body under the cap reflection.

Equations

• MovingSofa.reflectedBody ω K = { carrier := ⇑(MovingSofa.capReflection ω) '' ↑K, convex' := ⋯, isCompact' := ⋯, nonempty' := ⋯ }

theorem MovingSofa.supportValue_reflectedBody (ω : ℝ) (K : ConvexBody Point) (a : Real.Angle) : supportValue (↑(reflectedBody ω K)) a = supportValue (↑K) (reflectedAngle ω a)

Support values of a reflected body are indexed by reflected normal angles.

theorem MovingSofa.reflectedAngle_mem_capNormals {ω : ℝ} (a : Real.Angle) (ha : a ∈ (fun (t : ℝ) => ↑t) '' capUpperAngles ω ∪ capLowerNormals ω) : reflectedAngle ω a ∈ (fun (t : ℝ) => ↑t) '' capUpperAngles ω ∪ capLowerNormals ω

A reflected normal remains among the allowed cap normals.

theorem MovingSofa.HasHalfPlaneRepresentation.reflectedBody {ω : ℝ} {K : ConvexBody Point} {N N' : Set Real.Angle} (hK : HasHalfPlaneRepresentation (↑K) N) (hN : ∀ a ∈ N, reflectedAngle ω a ∈ N') : HasHalfPlaneRepresentation (↑(MovingSofa.reflectedBody ω K)) N'

Reflect a half-plane presentation when its allowed normals are transported.

theorem MovingSofa.reflectedBody_halfPlaneRepresentation {ω : ℝ} (K : ConvexBody Point) (hK : HasHalfPlaneRepresentation (↑K) ((fun (t : ℝ) => ↑t) '' capUpperAngles ω ∪ capLowerNormals ω)) : HasHalfPlaneRepresentation (↑(reflectedBody ω K)) ((fun (t : ℝ) => ↑t) '' capUpperAngles ω ∪ capLowerNormals ω)

Reflection preserves the standard cap half-plane presentation.

theorem MovingSofa.reflectedAngle_at_omega (ω : ℝ) : reflectedAngle ω ↑ω = ↑(Real.pi / 2)

Reflection exchanges the normalized upper normal at ω with the vertical normal.

theorem MovingSofa.reflectedAngle_at_pi_div_two (ω : ℝ) : reflectedAngle ω ↑(Real.pi / 2) = ↑ω

Reflection exchanges the vertical normal with the normalized upper normal at ω.

theorem MovingSofa.reflectedAngle_at_omega_add_pi (ω : ℝ) : reflectedAngle ω ↑(ω + Real.pi) = ↑(3 * Real.pi / 2)

Reflection exchanges the two lower cap normals.

theorem MovingSofa.reflectedAngle_at_three_pi_div_two (ω : ℝ) : reflectedAngle ω ↑(3 * Real.pi / 2) = ↑(ω + Real.pi)

Reflection exchanges the two lower cap normals.

theorem MovingSofa.reflectedBody_isCap {ω : ℝ} (K : CapSpace ω) : IsCap ω (reflectedBody ω ↑K)

Reflection preserves the normalized cap conditions.

theorem MovingSofa.capReflection_image_capFan (ω : ℝ) : ⇑(capReflection ω) '' capFan ω = capFan ω

The cap reflection preserves the lower fan.

theorem MovingSofa.reflectedAngle_sub (ω t : ℝ) : reflectedAngle ω ↑(ω - t) = ↑(t + Real.pi / 2)

Reflection sends the complementary normal to its paired normal.

theorem MovingSofa.reflectedAngle_sub_add_pi_div_two (ω t : ℝ) : reflectedAngle ω ↑(ω - t + Real.pi / 2) = ↑t

Reflection sends the complementary paired normal back to the original normal.

theorem MovingSofa.reflectedAngle_add_pi_div_two (ω t : ℝ) : reflectedAngle ω ↑(t + Real.pi / 2) = ↑(ω - t)

Reflection sends a paired normal to the complementary normal.

theorem MovingSofa.innerQuadrant_reflection (ω t : ℝ) (K : ConvexBody Point) : innerQuadrant (↑(reflectedBody ω K)) t = ⇑(capReflection ω) '' innerQuadrant (↑K) (ω - t)

Reflection transports inward quadrants at complementary angles.

theorem MovingSofa.capReflection_preimage_eq_image (ω : ℝ) (S : Set Point) : ⇑(capReflection ω) ⁻¹' S = ⇑(capReflection ω) '' S

The preimage and image of a set agree under the involutive cap reflection.

theorem MovingSofa.area_image_capReflection (ω : ℝ) (S : Set Point) (hS : MeasurableSet S) : ClassicalResults.area (⇑(capReflection ω) '' S) = ClassicalResults.area S

The cap reflection preserves the real Lebesgue area of measurable sets.

theorem MovingSofa.supportValue_reflectedBody_pi_div_two (K : ConvexBody Point) (u : ℝ) : supportValue ↑(reflectedBody (Real.pi / 2) K) ↑u = supportValue ↑K ↑(Real.pi - u)

The vertical reflection of a body has mirrored support values.

theorem MovingSofa.inner_capReflection_pi_div_two (p : Point) (u : ℝ) : inner ℝ ((capReflection (Real.pi / 2)) p) (normalVector ↑u) = inner ℝ p (normalVector ↑(Real.pi - u))

The vertical reflection mirrors normal projections.

Cap / Support Intersections

theorem MovingSofa.HasHalfPlaneRepresentation.supportingIntersection_mem_of_gap (K : ConvexBody Point) (R : Set ℝ) {a b : ℝ} (hab : 0 < b - a) (hpi : b - a < Real.pi) (hK : HasHalfPlaneRepresentation (↑K) ((fun (r : ℝ) => ↑r) '' R)) (hR : ∀ r ∈ R, r ∈ Set.Icc (a - Real.pi) a ∨ r ∈ Set.Icc b (b + Real.pi)) : supportingIntersection K ↑a ↑b ∈ K

Adjacent allowed support normals meet in the represented convex body.

Cap / Top Corner

theorem MovingSofa.stripParallelogram_top_mem_of_angle_lt (Θ : AngleSet) (hΘ : Θ.angle < Real.pi / 2) (K : PolygonCapSpace Θ) : (stripParallelogram Θ.angle).2.2 ∈ ↑↑↑K

Every polygon cap of angle less than pi/2 contains the top parallelogram corner.

Cap / Vertical

theorem MovingSofa.CapSpace.mem_of_fst_eq_of_snd_le {ω : ℝ} (K : CapSpace ω) {p q : Point} (hp : p ∈ ↑↑K) (hq : q ∈ capFan ω) (hx : q.ofLp 0 = p.ofLp 0) (hy : q.ofLp 1 ≤ p.ofLp 1) : q ∈ ↑↑K

A cap is closed under downward vertical movement that remains inside its fan.

Moving sofa: related mathematical developments

• Analysis.SurfaceMeasure.ArcConvergence.

Analysis / Surface Measure / Arc Convergence

theorem MovingSofa.tendsto_integral_surfaceAreaMeasure_Ioc_of_fixed_atoms (K : ℕ → ConvexBody Point) (L : ConvexBody Point) (hlim : Filter.Tendsto (fun (n : ℕ) => Metric.hausdorffDist ↑(K n) ↑L) Filter.atTop (nhds 0)) {a b : ℝ} (hab : a < b) (hturn : b ≤ a + 2 * Real.pi) (ha : ∀ (n : ℕ), (surfaceAreaMeasure (K n)) {↑a} = (surfaceAreaMeasure L) {↑a}) (hb : ∀ (n : ℕ), (surfaceAreaMeasure (K n)) {↑b} = (surfaceAreaMeasure L) {↑b}) (f : Real.Angle → ℝ) (hf : Continuous f) : Filter.Tendsto (fun (n : ℕ) => ∫ (u : Real.Angle) in (fun (t : ℝ) => ↑t) '' Set.Ioc a b, f u ∂surfaceAreaMeasure (K n)) Filter.atTop (nhds (∫ (u : Real.Angle) in (fun (t : ℝ) => ↑t) '' Set.Ioc a b, f u ∂surfaceAreaMeasure L))

Hausdorff convergence with fixed endpoint atoms preserves half-open surface integrals.

theorem MovingSofa.tendsto_integral_surfaceAreaMeasure_Ioc_of_preserves_faces (K : ℕ → ConvexBody Point) (L : ConvexBody Point) (hlim : Filter.Tendsto (fun (n : ℕ) => Metric.hausdorffDist ↑(K n) ↑L) Filter.atTop (nhds 0)) {a b : ℝ} (hab : a < b) (hturn : b ≤ a + 2 * Real.pi) (ha : ∀ (n : ℕ), exposedEdge (K n) ↑a = exposedEdge L ↑a) (hb : ∀ (n : ℕ), exposedEdge (K n) ↑b = exposedEdge L ↑b) (f : Real.Angle → ℝ) (hf : Continuous f) : Filter.Tendsto (fun (n : ℕ) => ∫ (u : Real.Angle) in (fun (t : ℝ) => ↑t) '' Set.Ioc a b, f u ∂surfaceAreaMeasure (K n)) Filter.atTop (nhds (∫ (u : Real.Angle) in (fun (t : ℝ) => ↑t) '' Set.Ioc a b, f u ∂surfaceAreaMeasure L))

Preserving the two endpoint faces supplies the atomic hypotheses for arc convergence.

Moving sofa: related mathematical developments

• Convex.CurveCut.
• Convex.ArcCutArea.
• Convex.OuterCornerPath.

Convex / Curve Cut

theorem MovingSofa.convexBoundaryArc_cut (K : ConvexBody Point) (a b : ℝ) (hab : a < b) (hba : b < a + Real.pi) (P Q O : Point) (hP : P = (edgeVertices K ↑a).1) (hQ : Q = (edgeVertices K ↑b).2) (hO : O = supportingIntersection K ↑a ↑b) : (P = Q → O = P ∧ convexBoundaryArc K a b = {P}) ∧ (P ≠ Q → ¬Collinear ℝ {P, Q, O} ∧ ∃ (t : ℝ) (c : ℝ) (K' : ConvexBody Point), a < t ∧ t < b ∧ inner ℝ P (normalVector ↑t) = c ∧ inner ℝ Q (normalVector ↑t) = c ∧ c < inner ℝ O (normalVector ↑t) ∧ ↑K' = ↑K ∩ normalHalfPlane (↑t) c true false ∧ (∀ s ∈ Set.Ioc (t - Real.pi) a, exposedEdge K' ↑s = {P}) ∧ (∀ s ∈ Set.Ioo a b, exposedEdge K' ↑s = exposedEdge K ↑s) ∧ (∀ s ∈ Set.Ico b (t + Real.pi), exposedEdge K' ↑s = {Q}) ∧ exposedEdge K' (↑t + ↑Real.pi) = segment ℝ Q P)

Convex / Arc Cut Area

theorem MovingSofa.exists_rectifiableOrientedArc_of_cut_with_area (K : ConvexBody Point) {t c d α β : ℝ} {P Q : Point} {U : Set Point} {x : ContinuousBVPaths α β} (hαβ : α < β) (hx : IsOrientedJordanParametrization ⋯ (frontier ↑K) true ↑x) (hPQ : P ≠ Q) (hbase : ↑x ⟨α, ⋯⟩ ∉ segment ℝ P Q) (hfrontier : frontier ↑K = U ∪ segment ℝ P Q) (hinter : U ∩ segment ℝ P Q = {P, Q}) (hPt : inner ℝ P (normalVector ↑t) = c) (hQt : inner ℝ Q (normalVector ↑t) = c) (hterminal : exposedEdge K (↑t + ↑Real.pi) = segment ℝ Q P) (hd : 0 < d) (hdir : Q - P = d • tangentVector ↑t) : ∃ (A : RectifiableOrientedArc), (↑A).carrier = U ∧ (↑A).startPoint = P ∧ (↑A).endPoint = Q ∧ curveAreaFunctional x = jordanArcArea A + segmentArea Q P

A supporting chord of a convex-body frontier cuts off a rectifiable oriented arc, and the closed signed area is the sum of the arc area and the oppositely oriented chord area.

The outer corner of a convex body as a path of bounded variation

The outer corner of the rotating supporting hallway of a convex body K is h_K(t) • u_t + h_K(t + π/2) • v_t. Support values are Lipschitz in the angle and bounded on a compact interval, so this expression is a Lipschitz, hence continuous bounded-variation, path on every compact interval of angles; and it is convex-linear in K because support values are. These are the two hypotheses of Mamikon convexity for the middle summand of the sofa area.

theorem MovingSofa.exists_outerCornerBV (K : ConvexBody Point) (a b : ℝ) : ∃ (γ : ContinuousBVPaths a b), ∀ (s : ↑(Set.Icc a b)), ↑γ s = (rotatingHallwayParts ↑K ↑↑s).outerCorner

The outer corner of a convex body traces a continuous path of bounded variation over every compact interval of angles.

theorem MovingSofa.exists_outerCornerBV_convexLinear (a b : ℝ) : ∃ (γ : ConvexBody Point → ContinuousBVPaths a b), (∀ (K : ConvexBody Point) (s : ↑(Set.Icc a b)), ↑(γ K) s = (rotatingHallwayParts ↑K ↑↑s).outerCorner) ∧ IsConvexLinear convexBodyCombination (fun (r : ↑unitInterval) (x y : ContinuousBVPaths a b) => (1 - ↑r) • x + ↑r • y) γ

The outer-corner paths of a convex body may be chosen convex-linearly in the body. The barycentric operation on paths is bvPathCombination, spelled out here because it is defined downstream of this module.

Moving sofa: related mathematical developments

• Geometry.Convex.HorizontalExtrema.

Geometry / Convex / Horizontal Extrema

theorem MovingSofa.ConvexBody.eq_of_mem_of_fst_eq_of_fst_extremal (K : ConvexBody Point) (N : Set Real.Angle) (hN : N.Finite) (hK : HasHalfPlaneRepresentation (↑K) N) (hsin : ∀ t ∈ N, t.sin ≠ 0) {a b : Point} (ha : a ∈ ↑K) (hb : b ∈ ↑K) (hab : a.ofLp 0 = b.ofLp 0) (hext : (∀ q ∈ ↑K, q.ofLp 0 ≤ a.ofLp 0) ∨ ∀ q ∈ ↑K, a.ofLp 0 ≤ q.ofLp 0) : a = b

A horizontal extreme slice is a singleton when every defining normal has nonzero sine.

theorem MovingSofa.ConvexBody.exists_mem_fst_eq_of_mem_Icc (K : ConvexBody Point) {a b : Point} (ha : a ∈ ↑K) (hb : b ∈ ↑K) (hab : a.ofLp 0 < b.ofLp 0) {x : ℝ} (hx : x ∈ Set.Icc (a.ofLp 0) (b.ofLp 0)) : ∃ q ∈ ↑K, q.ofLp 0 = x

Every horizontal coordinate between two points of a convex body is attained.

Moving sofa: related mathematical developments

• Gerver.Motion.
• Gerver.PaperPath.
• Gerver.PaperSet.
• Gerver.Parameters.
• Gerver.ParameterDictionary.
• Gerver.Partition.
• Gerver.ReversePhysicalDomain.
• Gerver.DirectRegularity.
• Gerver.LiteralSets.
• Gerver.LiteralConnected.
• Gerver.ParameterIdentification.
• Gerver.Contacts.
• Gerver.Niche.Roof.
• Gerver.ODEs.
• Gerver.OuterContacts.
• Gerver.StageRegularity.
• Gerver.Area.Grid.
• Gerver.Niche.RoofProperties.

Adapted from GerverSofaLean v1.1.0, F07UpstreamMotion (MIT).

noncomputable def MovingSofa.gerversSofaMotion : ↑unitInterval → GerverSofa.PartF.Rigid

The certified continuous rigid motion carrying Gerver’s sofa through the hallway.

Equations

• MovingSofa.gerversSofaMotion = GerverSofa.PartF.EuclideanMotion.motion

theorem MovingSofa.isMovingSofa_gerversSofa_motion : IsMovingSofa gerversSofa gerversSofaMotion

theorem MovingSofa.isMovingSofa_gerversSofa : ∃ (m : ↑unitInterval → EuclideanSpace ℝ (Fin 2) ≃ᵃⁱ[ℝ] EuclideanSpace ℝ (Fin 2)), IsMovingSofa gerversSofa m

theorem MovingSofa.volume_gerversSofa_le_sofaConstant : MeasureTheory.volume gerversSofa ≤ sofaConstant

The paper's Gerver path and the vendor coordinate transport

paperGerverPath is the certified direct five-phase Gerver path read through the vendor coordinate identification GerverSofa.PartF.Coordinates.toPlane. This file records the transport lemmas for that identification (derivatives, smoothness, continuity) and the frame readers that express the moving frame normalVector/tangentVector in the same coordinates.

The frame readers live here rather than in MovingSofa/Geometry/Basic.lean because their statements mention toPlane, which Geometry/Basic.lean does not import; this is the lowest module that sees both the vendor coordinates and MovingSofa.frame.

noncomputable def MovingSofa.paperGerverPath (t : ℝ) : Point

The certified direct five-phase Gerver path, taking the earlier branch at each switch.

Equations

• MovingSofa.paperGerverPath t = GerverSofa.PartF.Coordinates.toPlane (GerverSofa.Romik.path GerverSofa.PartB.params t)

theorem MovingSofa.canonical_path_rotation_eq_paper (t : ℝ) (ht : t ∈ Set.Icc 0 (Real.pi / 2)) : rotationMap (↑t) (GerversSofa.p t) = paperGerverPath t

Transport along the coordinate identification

theorem MovingSofa.hasDerivAt_toPlane {q : ℝ → GerverSofa.Point} {q' : GerverSofa.Point} {t : ℝ} (hq : HasDerivAt q q' t) : HasDerivAt (fun (s : ℝ) => GerverSofa.PartF.Coordinates.toPlane (q s)) (GerverSofa.PartF.Coordinates.toPlane q') t

The coordinate identification toPlane is a continuous linear map, so it transports derivatives of plane-valued curves.

theorem MovingSofa.contDiff_toPlane {q : ℝ → GerverSofa.Point} (hq : ContDiff ℝ (↑⊤) q) : ContDiff ℝ ↑⊤ fun (t : ℝ) => GerverSofa.PartF.Coordinates.toPlane (q t)

The coordinate identification toPlane preserves smoothness of plane-valued curves.

Frame readers

theorem MovingSofa.normalVector_coe_eq_toPlane (t : ℝ) : normalVector ↑t = GerverSofa.PartF.Coordinates.toPlane (Real.cos t, Real.sin t)

The angular frame normal is the coordinate image of the standard trigonometric pair.

theorem MovingSofa.tangentVector_coe_eq_toPlane (t : ℝ) : tangentVector ↑t = GerverSofa.PartF.Coordinates.toPlane (-Real.sin t, Real.cos t)

The angular frame tangent is the coordinate image of the rotated trigonometric pair.

theorem MovingSofa.inner_toPlane_rot_normalVector (t : ℝ) (z : GerverSofa.Point) : inner ℝ (GerverSofa.PartF.Coordinates.toPlane (GerverSofa.Romik.rot t z)) (normalVector ↑t) = z.1

The normal component of a body-frame vector rotated by t is its first coordinate.

theorem MovingSofa.inner_toPlane_rot_tangentVector (t : ℝ) (z : GerverSofa.Point) : inner ℝ (GerverSofa.PartF.Coordinates.toPlane (GerverSofa.Romik.rot t z)) (tangentVector ↑t) = z.2

The tangential component of a body-frame vector rotated by t is its second coordinate.

theorem MovingSofa.inner_normalVector_eq_dot (q : Point) (s : ℝ) : inner ℝ q (normalVector ↑s) = GerverSofa.dot (GerverSofa.PartF.Coordinates.fromPlane q) (GerverSofa.u s)

The normal frame component of a plane point is the vendor scalar product of its coordinate pair with the vendor normal u.

theorem MovingSofa.inner_tangentVector_eq_dot (q : Point) (s : ℝ) : inner ℝ q (tangentVector ↑s) = GerverSofa.dot (GerverSofa.PartF.Coordinates.fromPlane q) (GerverSofa.v s)

The tangent frame component of a plane point is the vendor scalar product of its coordinate pair with the vendor tangent v.

theorem MovingSofa.contDiff_normalVector : ContDiff ℝ ↑⊤ fun (t : ℝ) => normalVector ↑t

The angular frame normal is a smooth function of the angle.

theorem MovingSofa.contDiff_tangentVector : ContDiff ℝ ↑⊤ fun (t : ℝ) => tangentVector ↑t

The angular frame tangent is a smooth function of the angle.

The paper path as a transported direct path

The hypothesis ContDiff ℝ 1 (path GerverSofa.PartB.params) in the lemmas below is the first conjunct of MovingSofa.gerver_direct_path_regularity, which lives in a later module; passing it as a hypothesis keeps this file free of that dependency.

theorem MovingSofa.paperGerverPath_eq_toPlane : paperGerverPath = fun (t : ℝ) => GerverSofa.PartF.Coordinates.toPlane (GerverSofa.Romik.path GerverSofa.PartB.params t)

The paper path is the coordinate image of the certified direct path.

theorem MovingSofa.hasDerivAt_paperGerverPath (hC1 : ContDiff ℝ 1 (GerverSofa.Romik.path GerverSofa.PartB.params)) (t : ℝ) : HasDerivAt paperGerverPath (GerverSofa.PartF.Coordinates.toPlane (deriv (GerverSofa.Romik.path GerverSofa.PartB.params) t)) t

The paper path differentiates by transporting the derivative of the direct path.

theorem MovingSofa.deriv_paperGerverPath (hC1 : ContDiff ℝ 1 (GerverSofa.Romik.path GerverSofa.PartB.params)) (t : ℝ) : deriv paperGerverPath t = GerverSofa.PartF.Coordinates.toPlane (deriv (GerverSofa.Romik.path GerverSofa.PartB.params) t)

The derivative of the paper path is the transported derivative of the direct path.

theorem MovingSofa.continuous_paperGerverPath (hC1 : ContDiff ℝ 1 (GerverSofa.Romik.path GerverSofa.PartB.params)) : Continuous paperGerverPath

The paper path is continuous.

theorem MovingSofa.continuous_deriv_paperGerverPath (hC1 : ContDiff ℝ 1 (GerverSofa.Romik.path GerverSofa.PartB.params)) : Continuous (deriv paperGerverPath)

The paper path is continuously differentiable.

Gerver / Paper Set

def MovingSofa.paperGerverSofa : Set Point

Gerver's paper-frame set, cut out by the explicit path of rotated hallways.

Equations

• One or more equations did not get rendered due to their size.

Gerver / Parameters

noncomputable def MovingSofa.paperGerverConstants : (ℝ × ℝ) × ℝ × ℝ

The two Gerver switching angles and the right/left distinguished angles.

Equations

• MovingSofa.paperGerverConstants = ((MovingSofa.GerversSofa.φ, MovingSofa.GerversSofa.θ), MovingSofa.GerversSofa.φ, Real.pi / 2 - MovingSofa.GerversSofa.φ)

noncomputable def MovingSofa.gerverStageTimes : Fin 6 → ℝ

The six endpoints of the five Gerver stages.

Equations

• MovingSofa.gerverStageTimes = ![0, MovingSofa.GerversSofa.φ, MovingSofa.GerversSofa.θ, Real.pi / 2 - MovingSofa.GerversSofa.θ, Real.pi / 2 - MovingSofa.GerversSofa.φ, Real.pi / 2]

def MovingSofa.gerverStageIntervals (i : Fin 5) : Set ℝ

The five closed stage intervals in their source order.

Equations

• MovingSofa.gerverStageIntervals i = Set.Icc (MovingSofa.gerverStageTimes i.castSucc) (MovingSofa.gerverStageTimes i.succ)

def MovingSofa.gerverDirectEquations (p : GerverSofa.Romik.Params) : Prop

The exact direct 22-equation Gerver system, with the certified phase-map convention.

Equations

• MovingSofa.gerverDirectEquations p = GerverSofa.Romik.Equations p

def MovingSofa.gerverDirectBox : Set GerverSofa.Romik.Params

The exact closed rational box for the direct Gerver parameters.

Equations

• MovingSofa.gerverDirectBox = GerverSofa.Romik.box

theorem MovingSofa.gerverDirectBox_b1_lower_bound {p : GerverSofa.Romik.Params} (hp : p ∈ gerverDirectBox) : -53 / 100 ≤ p.b1

The exact box bounds the second-stage linear coefficient b₁ from below by -53/100.

theorem MovingSofa.gerverDirectBox_d1_upper_bound {p : GerverSofa.Romik.Params} (hp : p ∈ gerverDirectBox) : p.d1 ≤ 33 / 25

The exact box bounds the fourth-stage linear coefficient d₁ from above by 33/25.

Gerver / Parameter Dictionary

noncomputable def MovingSofa.gerverParameterDictionary : (GerverSofa.Reduced.Params → GerverSofa.Romik.Params) × (GerverSofa.Romik.Params → GerverSofa.Reduced.Params)

Bundle the forward and reverse dictionaries between reduced and full Romik parameters.

Equations

• MovingSofa.gerverParameterDictionary = (GerverSofa.PartF.Phases.dictionary, GerverSofa.PartF.Phases.undictionary)

Gerver / Partition

def MovingSofa.gerverPhaseIntervals (j : Fin 10) : Set ℝ

The ten half-open Gerver phase intervals, indexed from zero.

Equations

• One or more equations did not get rendered due to their size.

theorem MovingSofa.gerverPhaseIntervals_explicit (j : Fin 10) : gerverPhaseIntervals j = ![Set.Ico 0 GerversSofa.φ, Set.Ico GerversSofa.φ GerversSofa.θ, Set.Ico GerversSofa.θ (Real.pi / 2 - GerversSofa.θ), Set.Ico (Real.pi / 2 - GerversSofa.θ) (Real.pi / 2 - GerversSofa.φ), Set.Ico (Real.pi / 2 - GerversSofa.φ) (Real.pi / 2), Set.Ioc (Real.pi / 2) (Real.pi / 2 + GerversSofa.φ), Set.Ioc (Real.pi / 2 + GerversSofa.φ) (Real.pi / 2 + GerversSofa.θ), Set.Ioc (Real.pi / 2 + GerversSofa.θ) (Real.pi - GerversSofa.θ), Set.Ioc (Real.pi - GerversSofa.θ) (Real.pi - GerversSofa.φ), Set.Ioc (Real.pi - GerversSofa.φ) Real.pi] j

The ten Gerver phase intervals, written out as explicit half-open real intervals.

Gerver / Reverse Physical Domain

theorem MovingSofa.gerver_reverse_physical_domain (p : GerverSofa.Romik.Params) (hp : p ∈ gerverDirectBox) : 0 < (gerverParameterDictionary.2 p).phi ∧ (gerverParameterDictionary.2 p).phi < (gerverParameterDictionary.2 p).theta ∧ (gerverParameterDictionary.2 p).theta < Real.pi / 4 ∧ 0 < (gerverParameterDictionary.2 p).a ∧ 0 < (gerverParameterDictionary.2 p).b ∧ 39 / 1000 ≤ (gerverParameterDictionary.2 p).phi ∧ (gerverParameterDictionary.2 p).phi ≤ 40 / 1000

Matching and C¹ regularity of the direct Gerver path

The vendor library assembles the Gerver path GerverSofa.Romik.path from five smooth branches path1, …, path5 switched at φ < θ < π/2 - θ < π/2 - φ. This file supplies the differential interface for those branches — each pathᵢ has derivative rot t (alphaBetaᵢ p t) — and deduces from the direct equations that values and derivatives agree at all four switches, hence that path p is continuously differentiable with path p 0 = 0.

It also records, for each stage, that the glued path agrees with its analytic branch on the closed stage interval and that deriv (path p) is the corresponding rot t (alphaBetaᵢ p t) there, endpoints included.

Differential interface for the five direct branches

theorem GerverSofa.Romik.hasDerivAt_addK_rot {z₁ z₂ : ℝ → ℝ} {z₁' z₂' k₁ k₂ t : ℝ} (hz₁ : HasDerivAt z₁ z₁' t) (hz₂ : HasDerivAt z₂ z₂' t) : HasDerivAt (fun (s : ℝ) => addK (rot s (z₁ s, z₂ s)) k₁ k₂) (rot t (z₁' - z₂ t, z₂' + z₁ t)) t

Rotating a differentiable body-frame curve and translating it differentiates by the product rule, contributing the infinitesimal rotation (z₁, z₂) ↦ (-z₂, z₁).

theorem GerverSofa.Romik.hasDerivAt_path1 (p : Params) (t : ℝ) : HasDerivAt (path1 p) (rot t (alphaBeta1 p t)) t

The first direct branch has body-frame velocity alphaBeta1.

theorem GerverSofa.Romik.hasDerivAt_path2 (p : Params) (t : ℝ) : HasDerivAt (path2 p) (rot t (alphaBeta2 p t)) t

The second direct branch has body-frame velocity alphaBeta2.

theorem GerverSofa.Romik.hasDerivAt_path3 (p : Params) (t : ℝ) : HasDerivAt (path3 p) (rot t (alphaBeta3 p t)) t

The third direct branch has body-frame velocity alphaBeta3.

theorem GerverSofa.Romik.hasDerivAt_path4 (p : Params) (t : ℝ) : HasDerivAt (path4 p) (rot t (alphaBeta4 p t)) t

The fourth direct branch has body-frame velocity alphaBeta4.

theorem GerverSofa.Romik.hasDerivAt_path5 (p : Params) (t : ℝ) : HasDerivAt (path5 p) (rot t (alphaBeta5 p t)) t

The fifth direct branch has body-frame velocity alphaBeta5.

theorem GerverSofa.Romik.continuous_rot_alphaBeta1 (p : Params) : Continuous fun (t : ℝ) => rot t (alphaBeta1 p t)

Continuity of the body-frame velocity field on each branch, transported to the world frame by the rotation.

theorem GerverSofa.Romik.continuous_rot_alphaBeta2 (p : Params) : Continuous fun (t : ℝ) => rot t (alphaBeta2 p t)

Continuity of the body-frame velocity field on each branch, transported to the world frame by the rotation.

theorem GerverSofa.Romik.continuous_rot_alphaBeta3 (p : Params) : Continuous fun (t : ℝ) => rot t (alphaBeta3 p t)

Continuity of the body-frame velocity field on each branch, transported to the world frame by the rotation.

theorem GerverSofa.Romik.continuous_rot_alphaBeta4 (p : Params) : Continuous fun (t : ℝ) => rot t (alphaBeta4 p t)

Continuity of the body-frame velocity field on each branch, transported to the world frame by the rotation.

theorem GerverSofa.Romik.continuous_rot_alphaBeta5 (p : Params) : Continuous fun (t : ℝ) => rot t (alphaBeta5 p t)

Continuity of the body-frame velocity field on each branch, transported to the world frame by the rotation.

theorem GerverSofa.Romik.k11_eq_one_sub_a1_of_equations {p : Params} (heq : Equations p) : p.k11 = 1 - p.a1

Equation 32 of the direct system. The remaining scalar consequences used here are already extracted by the vendor in GerverSofa/KernelOnly/EndpointSymmetry.lean.

Reflection identities for the body-frame velocities

With S (r, s) = (-s, -r) the direct equations give w₃(π/2 - t) = S w₃(t), w₄(π/2 - t) = S w₂(t) and w₅(π/2 - t) = S w₁(t).

theorem GerverSofa.Romik.alphaBeta3_pi_div_two_sub {p : Params} (heq : Equations p) (t : ℝ) : alphaBeta3 p (Real.pi / 2 - t) = (-(alphaBeta3 p t).2, -(alphaBeta3 p t).1)

The middle branch velocity is anti-symmetric about π/4.

theorem GerverSofa.Romik.alphaBeta4_pi_div_two_sub {p : Params} (heq : Equations p) (t : ℝ) : alphaBeta4 p (Real.pi / 2 - t) = (-(alphaBeta2 p t).2, -(alphaBeta2 p t).1)

The fourth branch velocity reflects onto the second.

theorem GerverSofa.Romik.alphaBeta5_pi_div_two_sub {p : Params} (heq : Equations p) (t : ℝ) : alphaBeta5 p (Real.pi / 2 - t) = (-(alphaBeta1 p t).2, -(alphaBeta1 p t).1)

The fifth branch velocity reflects onto the first.

theorem GerverSofa.Romik.alphaBeta34_eq {p : Params} (heq : Equations p) : alphaBeta3 p (Real.pi / 2 - p.theta) = alphaBeta4 p (Real.pi / 2 - p.theta)

Velocity matching at the third switch π/2 - θ, by reflecting the match at θ.

theorem GerverSofa.Romik.alphaBeta45_eq {p : Params} (heq : Equations p) : alphaBeta4 p (Real.pi / 2 - p.phi) = alphaBeta5 p (Real.pi / 2 - p.phi)

Velocity matching at the fourth switch π/2 - φ, by reflecting the match at φ.

Branch selection on the closed stages

Each stage interval is closed, so the two stages adjacent to a switch both contain it. The glued path picks the earlier branch there, and the certified value-matching equations say that this is also the later branch's value.

theorem GerverSofa.Romik.path_eq_ite (p : Params) (t : ℝ) : path p t = if t ≤ p.phi then path1 p t else if t ≤ p.theta then path2 p t else if t ≤ Real.pi / 2 - p.theta then path3 p t else if t ≤ Real.pi / 2 - p.phi then path4 p t else path5 p t

The glued direct path unfolds to the nested selection of its five analytic branches.

theorem GerverSofa.Romik.path_eq_path1_of_mem_Icc (p : Params) {s : ℝ} (hs : s ∈ Set.Icc 0 p.phi) : path p s = path1 p s

On the closed first stage [0, φ] the glued path is the first branch.

theorem GerverSofa.Romik.path_eq_path2_of_mem_Icc {p : Params} (heq : Equations p) {s : ℝ} (hs : s ∈ Set.Icc p.phi p.theta) : path p s = path2 p s

On the closed second stage [φ, θ] the glued path is the second branch; at the left endpoint this is the certified value match match_path12_of_equations.

theorem GerverSofa.Romik.path_eq_path3_of_mem_Icc {p : Params} (heq : Equations p) (hpt : p.phi < p.theta) {s : ℝ} (hs : s ∈ Set.Icc p.theta (Real.pi / 2 - p.theta)) : path p s = path3 p s

On the closed third stage [θ, π/2 - θ] the glued path is the third branch; at the left endpoint this is the certified value match match_path23_of_equations.

theorem GerverSofa.Romik.path_eq_path4_of_mem_Icc {p : Params} (heq : Equations p) (hpt : p.phi < p.theta) (hq : p.theta < Real.pi / 4) {s : ℝ} (hs : s ∈ Set.Icc (Real.pi / 2 - p.theta) (Real.pi / 2 - p.phi)) : path p s = path4 p s

On the closed fourth stage [π/2 - θ, π/2 - φ] the glued path is the fourth branch; at the left endpoint this is the certified value match match_path34_of_equations.

theorem GerverSofa.Romik.path_eq_path5_of_mem_Icc {p : Params} (heq : Equations p) (hpt : p.phi < p.theta) (hq : p.theta < Real.pi / 4) {s : ℝ} (hs : s ∈ Set.Icc (Real.pi / 2 - p.phi) (Real.pi / 2)) : path p s = path5 p s

On the closed fifth stage [π/2 - φ, π/2] the glued path is the fifth branch; at the left endpoint this is the certified value match match_path45_of_equations.

Smoothness of the branches and of their body-frame velocities

theorem GerverSofa.Romik.contDiff_path1 (p : Params) : ContDiff ℝ (↑⊤) (path1 p)

The first analytic branch is smooth on all of ℝ.

theorem GerverSofa.Romik.contDiff_path2 (p : Params) : ContDiff ℝ (↑⊤) (path2 p)

The first analytic branch is smooth on all of ℝ.

theorem GerverSofa.Romik.contDiff_path3 (p : Params) : ContDiff ℝ (↑⊤) (path3 p)

The first analytic branch is smooth on all of ℝ.

theorem GerverSofa.Romik.contDiff_path4 (p : Params) : ContDiff ℝ (↑⊤) (path4 p)

The first analytic branch is smooth on all of ℝ.

theorem GerverSofa.Romik.contDiff_path5 (p : Params) : ContDiff ℝ (↑⊤) (path5 p)

The first analytic branch is smooth on all of ℝ.

theorem GerverSofa.Romik.contDiff_alphaBeta1 (p : Params) : ContDiff ℝ (↑⊤) (alphaBeta1 p)

The first body-frame velocity pair is smooth on all of ℝ.

theorem GerverSofa.Romik.contDiff_alphaBeta2 (p : Params) : ContDiff ℝ (↑⊤) (alphaBeta2 p)

The first body-frame velocity pair is smooth on all of ℝ.

theorem GerverSofa.Romik.contDiff_alphaBeta3 (p : Params) : ContDiff ℝ (↑⊤) (alphaBeta3 p)

The first body-frame velocity pair is smooth on all of ℝ.

theorem GerverSofa.Romik.contDiff_alphaBeta4 (p : Params) : ContDiff ℝ (↑⊤) (alphaBeta4 p)

The first body-frame velocity pair is smooth on all of ℝ.

theorem GerverSofa.Romik.contDiff_alphaBeta5 (p : Params) : ContDiff ℝ (↑⊤) (alphaBeta5 p)

The first body-frame velocity pair is smooth on all of ℝ.

The stage derivatives, endpoints included

A nondegenerate closed interval has a unique tangent direction at each of its points, including its endpoints, so a C¹ function agreeing there with a differentiable curve already has that curve's derivative at every point of the interval.

theorem GerverSofa.Romik.deriv_path_of_eqOn_Icc {p : Params} (hC1 : ContDiff ℝ 1 (path p)) {X W : ℝ → Point} {a b t : ℝ} (hab : a < b) (hX : ∀ (s : ℝ), HasDerivAt X (rot s (W s)) s) (hXe : ∀ s ∈ Set.Icc a b, path p s = X s) (ht : t ∈ Set.Icc a b) : deriv (path p) t = rot t (W t)

If the C¹ glued path agrees on a nondegenerate closed interval with a curve whose derivative is rot s (W s), then that is its derivative everywhere on the interval, endpoints included.

theorem GerverSofa.Romik.deriv_path_eq_rot_alphaBeta1 {p : Params} (hC1 : ContDiff ℝ 1 (path p)) (hphi : 0 < p.phi) {t : ℝ} (ht : t ∈ Set.Icc 0 p.phi) : deriv (path p) t = rot t (alphaBeta1 p t)

On the closed first stage the glued path has body-frame velocity alphaBeta1.

theorem GerverSofa.Romik.deriv_path_eq_rot_alphaBeta2 {p : Params} (hC1 : ContDiff ℝ 1 (path p)) (heq : Equations p) (hpt : p.phi < p.theta) {t : ℝ} (ht : t ∈ Set.Icc p.phi p.theta) : deriv (path p) t = rot t (alphaBeta2 p t)

On the closed second stage the glued path has body-frame velocity alphaBeta2.

theorem GerverSofa.Romik.deriv_path_eq_rot_alphaBeta3 {p : Params} (hC1 : ContDiff ℝ 1 (path p)) (heq : Equations p) (hpt : p.phi < p.theta) (hq : p.theta < Real.pi / 4) {t : ℝ} (ht : t ∈ Set.Icc p.theta (Real.pi / 2 - p.theta)) : deriv (path p) t = rot t (alphaBeta3 p t)

On the closed third stage the glued path has body-frame velocity alphaBeta3.

theorem GerverSofa.Romik.deriv_path_eq_rot_alphaBeta4 {p : Params} (hC1 : ContDiff ℝ 1 (path p)) (heq : Equations p) (hpt : p.phi < p.theta) (hq : p.theta < Real.pi / 4) {t : ℝ} (ht : t ∈ Set.Icc (Real.pi / 2 - p.theta) (Real.pi / 2 - p.phi)) : deriv (path p) t = rot t (alphaBeta4 p t)

On the closed fourth stage the glued path has body-frame velocity alphaBeta4.

theorem GerverSofa.Romik.deriv_path_eq_rot_alphaBeta5 {p : Params} (hC1 : ContDiff ℝ 1 (path p)) (heq : Equations p) (hphi : 0 < p.phi) (hpt : p.phi < p.theta) (hq : p.theta < Real.pi / 4) {t : ℝ} (ht : t ∈ Set.Icc (Real.pi / 2 - p.phi) (Real.pi / 2)) : deriv (path p) t = rot t (alphaBeta5 p t)

On the closed fifth stage the glued path has body-frame velocity alphaBeta5.

noncomputable def MovingSofa.gerverDirectBranches (p : GerverSofa.Romik.Params) : Fin 5 → ℝ → GerverSofa.Point

The five explicit Romik path branches for a parameter tuple.

Equations

• MovingSofa.gerverDirectBranches p = ![GerverSofa.Romik.path1 p, GerverSofa.Romik.path2 p, GerverSofa.Romik.path3 p, GerverSofa.Romik.path4 p, GerverSofa.Romik.path5 p]

noncomputable def MovingSofa.gerverDirectSwitches (p : GerverSofa.Romik.Params) : Fin 4 → ℝ

The four switching times separating the explicit Romik path branches.

Equations

• MovingSofa.gerverDirectSwitches p = ![p.phi, p.theta, Real.pi / 2 - p.theta, Real.pi / 2 - p.phi]

theorem MovingSofa.gerver_direct_path_regularity (p : GerverSofa.Romik.Params) (hp : p ∈ gerverDirectBox) (heq : gerverDirectEquations p) : ContDiff ℝ 1 (GerverSofa.Romik.path p) ∧ GerverSofa.Romik.path p 0 = 0 ∧ ∀ (i : Fin 4), gerverDirectBranches p i.castSucc (gerverDirectSwitches p i) = gerverDirectBranches p i.succ (gerverDirectSwitches p i) ∧ deriv (gerverDirectBranches p i.castSucc) (gerverDirectSwitches p i) = deriv (gerverDirectBranches p i.succ) (gerverDirectSwitches p i)

Gerver / Literal Sets

def MovingSofa.gerverOuterCap : Set Point

The outer cap defined by all upper path support constraints and the horizontal base.

Equations

• One or more equations did not get rendered due to their size.

def MovingSofa.gerverLiteralNiche : Set Point

The union of strict forbidden inner corners above the horizontal base along the Gerver path.

Equations

• One or more equations did not get rendered due to their size.

def MovingSofa.gerverLiteralSofa : Set Point

The literal Gerver sofa obtained by removing its niche from its outer cap.

Equations

• MovingSofa.gerverLiteralSofa = MovingSofa.gerverOuterCap \ MovingSofa.gerverLiteralNiche

def MovingSofa.gerverLiteralSets : Set Point × Set Point

Bundle the literal niche and sofa sets for comparison with the canonical definitions.

Equations

• MovingSofa.gerverLiteralSets = (MovingSofa.gerverLiteralNiche, MovingSofa.gerverLiteralSofa)

theorem MovingSofa.mem_gerverOuterCap_iff (q : Point) : q ∈ gerverOuterCap ↔ GerverSofa.PartF.Coordinates.fromPlane q ∈ GerverSofa.Romik.K0 GerverSofa.PartB.params

The paper outer cap is the coordinate transport of the certified Romik cap K₀.

theorem MovingSofa.toPlane_mem_gerverOuterCap {x : GerverSofa.Point} (hx : x ∈ GerverSofa.Romik.K0 GerverSofa.PartB.params) : GerverSofa.PartF.Coordinates.toPlane x ∈ gerverOuterCap

A point whose coordinate pair lies in the certified Romik cap K₀ lies in the paper outer cap.

theorem MovingSofa.mem_gerverLiteralNiche_iff (q : Point) : q ∈ gerverLiteralNiche ↔ GerverSofa.PartF.Coordinates.fromPlane q ∈ GerverSofa.Romik.niche GerverSofa.PartB.params

The paper literal niche is the coordinate transport of the certified Romik niche.

theorem MovingSofa.paperGerverSofa_eq_literal : paperGerverSofa = gerverLiteralSofa

Gerver / Literal Connected

theorem MovingSofa.gerver_literal_connected : IsConnected gerverLiteralSofa

Gerver / Parameter Identification

theorem MovingSofa.selected_phi : GerverSofa.PartF.ProjectAdapter.selected.phi = GerversSofa.φ

The adapter's selected reverse parameter vector carries the paper's angle φ in its phi field. This is true by definition — selected is built from the very quadruple that defines GerversSofa.φ — but it is the only bridge from the vendor parameter vector to the paper's stage times gerverStageTimes, so it is recorded as a named lemma rather than left to an invisible unfolding at each use site.

theorem MovingSofa.selected_theta : GerverSofa.PartF.ProjectAdapter.selected.theta = GerversSofa.θ

The adapter's selected reverse parameter vector carries the paper's angle θ in its theta field; see selected_phi for why this rfl is worth naming.

theorem MovingSofa.gerver_parameter_identification : (∀ p ∈ gerverDirectBox, gerverDirectEquations p → p = gerverParameterDictionary.1 GerverSofa.PartF.ProjectAdapter.selected ∧ p.phi = GerverSofa.PartF.ProjectAdapter.selected.phi ∧ p.theta = GerverSofa.PartF.ProjectAdapter.selected.theta ∧ 0 < GerverSofa.PartF.ProjectAdapter.selected.phi ∧ GerverSofa.PartF.ProjectAdapter.selected.phi < GerverSofa.PartF.ProjectAdapter.selected.theta ∧ GerverSofa.PartF.ProjectAdapter.selected.theta < Real.pi / 4 ∧ 39 / 1000 ≤ GerverSofa.PartF.ProjectAdapter.selected.phi ∧ GerverSofa.PartF.ProjectAdapter.selected.phi ≤ 40 / 1000 ∧ GerversSofa.ABφθSpec GerverSofa.PartF.ProjectAdapter.selected.a GerverSofa.PartF.ProjectAdapter.selected.b GerverSofa.PartF.ProjectAdapter.selected.phi GerverSofa.PartF.ProjectAdapter.selected.theta) ∧ ∃ p ∈ gerverDirectBox, gerverDirectEquations p ∧ p = gerverParameterDictionary.1 GerverSofa.PartF.ProjectAdapter.selected

theorem MovingSofa.paperGerverConstants_snd_mem_Ioo : paperGerverConstants.2.1 ∈ Set.Ioo 0 (Real.pi / 2) ∧ paperGerverConstants.2.2 ∈ Set.Ioo 0 (Real.pi / 2) ∧ paperGerverConstants.2.1 + paperGerverConstants.2.2 = Real.pi / 2

The two distinguished Gerver angles are interior and complementary.

theorem MovingSofa.paperGerverConstants_snd_fst_lt_snd_snd : paperGerverConstants.2.1 < paperGerverConstants.2.2

The two distinguished angles are ordered: the certified bound φ ≤ 1/25 puts φ well below π/4 = π/2 - π/4.

The stage times as certified angles

gerverStageTimes is defined from the paper angles GerversSofa.φ and GerversSofa.θ, while the certified Part C geometry is indexed by the vendor parameter fields params.phi, params.theta and the derived angles eta, tau, T. The six lemmas below are the dictionary between the two indexings; they are the only place where gerver_parameter_identification is needed to see a stage time.

theorem MovingSofa.gerverStageTimes_zero : gerverStageTimes 0 = 0

The zeroth stage time is the start of the rotation interval.

theorem MovingSofa.gerverStageTimes_one : gerverStageTimes 1 = GerverSofa.PartC.params.phi

The first stage time is the certified first switching angle params.phi.

theorem MovingSofa.gerverStageTimes_two : gerverStageTimes 2 = GerverSofa.PartC.params.theta

The second stage time is the certified second switching angle params.theta.

theorem MovingSofa.gerverStageTimes_three : gerverStageTimes 3 = GerverSofa.PartC.eta

The third stage time is the certified reflected angle eta = T - params.theta.

theorem MovingSofa.gerverStageTimes_four : gerverStageTimes 4 = GerverSofa.PartC.tau

The fourth stage time is the certified reflected angle tau = T - params.phi.

theorem MovingSofa.gerverStageTimes_five : gerverStageTimes 5 = GerverSofa.PartC.T

The fifth stage time is the certified end T of the rotation interval.

Gerver / Contacts

noncomputable def MovingSofa.paperGerverVelocityComponents (t : ℝ) : ℝ × ℝ

Resolve the Gerver path derivative into its normal and tangent frame components.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MovingSofa.paperGerverContacts (t : ℝ) : Fin 4 → Point

The four standard support-contact points determined by the Gerver path and its derivative.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MovingSofa.paperGerverContactData : (ℝ → ℝ × ℝ) × (ℝ → Fin 4 → Point)

Bundle the path velocity components and the four contact curves.

Equations

• MovingSofa.paperGerverContactData = (MovingSofa.paperGerverVelocityComponents, MovingSofa.paperGerverContacts)

noncomputable def MovingSofa.gerverBranchVelocityComponents (i : Fin 5) (t : ℝ) : ℝ × ℝ

The explicit body-frame velocity coefficients on a selected Romik branch.

Equations

• One or more equations did not get rendered due to their size.

The common shape of the four contact curves

paperGerverContacts is an instance of a generic four-slot shape built from a base curve and two scalar coefficient functions. Continuity and smoothness of the shape are proved once here and reused for the ambient curve and for each analytic stage branch.

theorem MovingSofa.paperGerverContactData_properties : Continuous paperGerverVelocityComponents ∧ Continuous paperGerverContacts ∧ (∀ (i : Fin 5), ContDiffOn ℝ (↑⊤) paperGerverContacts (gerverStageIntervals i)) ∧ ∀ (i : Fin 5), ∀ t ∈ gerverStageIntervals i, paperGerverVelocityComponents t = gerverBranchVelocityComponents i t

Identification with the certified piecewise contact data

theorem MovingSofa.paperGerverVelocityComponents_eq_alphaBetaAt (t : ℝ) (ht : t ∈ Set.Icc 0 (Real.pi / 2)) : paperGerverVelocityComponents t = GerverSofa.PartC.alphaBetaAt t

On the physical rotation interval the paper velocity components agree with the vendor piecewise body-frame coefficients.

theorem MovingSofa.fromPlane_paperGerverContacts (t : ℝ) (ht : t ∈ Set.Icc 0 (Real.pi / 2)) (i : Fin 4) : GerverSofa.PartF.Coordinates.fromPlane (paperGerverContacts t i) = ![GerverSofa.PartC.A t, GerverSofa.PartC.B t, GerverSofa.PartC.C t, GerverSofa.PartC.D t] i

On the physical rotation interval the four paper contact curves are the coordinate transports of the four certified contact curves.

theorem MovingSofa.paperGerverContacts_one_eq_toPlane {t : ℝ} (ht : t ∈ Set.Icc 0 (Real.pi / 2)) : paperGerverContacts t 1 = GerverSofa.PartF.Coordinates.toPlane (GerverSofa.PartC.B t)

On the physical rotation interval the second paper contact curve is the certified curve B, read in plane coordinates.

theorem MovingSofa.paperGerverContacts_three_eq_toPlane {t : ℝ} (ht : t ∈ Set.Icc 0 (Real.pi / 2)) : paperGerverContacts t 3 = GerverSofa.PartF.Coordinates.toPlane (GerverSofa.PartC.D t)

On the physical rotation interval the fourth paper contact curve is the certified curve D, read in plane coordinates.

The Gerver niche roof

The upper boundary of the paper's literal Gerver niche is a three-piece graph over the rotation interval: the fourth contact curve up to the second stage time, the direct path run backwards through the affine reversal gerverRoofReverseTime on the middle stage, and the second contact curve from the third stage time on. gerverRoofCurve is that graph as a function of an unrestricted real parameter and gerverNicheRoof its restriction to the rotation interval; gerverRoofCurve_eq relates the two.

noncomputable def MovingSofa.gerverRoofReverseTime (s : ℝ) : ℝ

The affine reversal of the middle roof stage: it maps gerverStageTimes 2 to gerverStageTimes 4 and gerverStageTimes 3 to gerverStageTimes 1, so it reparametrizes the central part of the direct path backwards.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MovingSofa.gerverRoofCurve (s : ℝ) : Point

The Gerver niche roof as a curve of an unrestricted real parameter. On the rotation interval it agrees with gerverNicheRoof (gerverRoofCurve_eq); the unrestricted form is what the intermediate value theorem and continuous_if_le consume.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MovingSofa.gerverNicheRoof (s : ↑(Set.Icc 0 (Real.pi / 2))) : Point

The three-branch roof of the Gerver niche, using two contact arcs and the reversed path.

Equations

• One or more equations did not get rendered due to their size.

Gerver / ODEs

noncomputable def MovingSofa.gerverStageContactDerivatives (i : Fin 5) (t : ℝ) : Fin 4 → ℝ

Tangential components of the four contact-curve derivatives on a selected stage.

Equations

• One or more equations did not get rendered due to their size.

theorem MovingSofa.gerver_stageODEs (i : Fin 5) (t : ℝ) (ht : t ∈ gerverStageIntervals i) : (gerverStageContactDerivatives i t 0, gerverStageContactDerivatives i t 2) = ![(0, gerverStageContactDerivatives i t 3), ((paperGerverVelocityComponents t).2, gerverStageContactDerivatives i t 3 - (paperGerverVelocityComponents t).1), ((paperGerverVelocityComponents t).2, -(paperGerverVelocityComponents t).1), (-gerverStageContactDerivatives i t 1 + (paperGerverVelocityComponents t).2, -(paperGerverVelocityComponents t).1), (-gerverStageContactDerivatives i t 1, 0)] i

Gerver / Outer Contacts

theorem MovingSofa.gerver_outer_contact_A (t : ℝ) (ht : t ∈ Set.Icc 0 (Real.pi / 2)) : paperGerverContacts t 0 ∈ gerverOuterCap

theorem MovingSofa.gerver_outer_contact_C (t : ℝ) (ht : t ∈ Set.Icc 0 (Real.pi / 2)) : paperGerverContacts t 2 ∈ gerverOuterCap

Regularity of the certified Gerver stage data

The five Gerver stages are nondegenerate: the six stage endpoints increase strictly from 0 to π / 2 (gerverStageTimes_strictMono), and gerverStageIntervals_zero through gerverStageIntervals_four name the resulting closed stage intervals. The certified direct path is continuously differentiable on the whole rotation interval (contDiff_paperGerverPath), while each contact curve is only continuous globally (continuous_paperGerverContact) and continuously differentiable on a single stage (contDiffOn_paperGerverContact). Gluing two consecutive stages presents the two inner contact curves on the parameter ranges where they touch the cap as continuous paths of bounded variation (gerverRightContactBV, gerverLeftContactBV).

The second half of the file differentiates the two inner contact curves stagewise. Writing the velocity components of the direct path as (α, β), the contact formulas are B = x + α v and D = x - β u, so the product rule and the frame derivatives hasDerivAt_normalVector, hasDerivAt_tangentVector give B' = (β + α') v and D' = (α - β') u (hasDerivWithinAt_paperGerverContacts_one, hasDerivWithinAt_paperGerverContacts_three). Feeding the five analytic stage branches of paperGerverContactData_properties into these two lemmas yields the signs of the two speeds on the stages where they are needed (hasDerivWithinAt_paperGerverContacts_one_neg_smul, hasDerivWithinAt_paperGerverContacts_three_pos_smul); the two nonconstant coefficients are signed by the coarse box bounds gerverDirectBox_b1_lower_bound, gerverDirectBox_d1_upper_bound and gerverStageTimes_two_le_seven_div_ten.

The last two sections record the consequences used downstream: the frame coordinates s ↦ x s ⋅ u_s and s ↦ x s ⋅ v_s of the direct path are differentiable with derivatives B ⋅ v and -D ⋅ u (hasDerivAt_inner_paperGerverPath_normalVector, hasDerivAt_inner_paperGerverPath_tangentVector), and against a fixed frame direction outside the stage the two inner contact curves are strictly monotone on each stage (strictAntiOn_inner_paperGerverContacts_three, strictMonoOn_inner_paperGerverContacts_one).

theorem MovingSofa.gerverStageTimes_strictMono : StrictMono gerverStageTimes

The six Gerver stage endpoints increase strictly along the rotation interval.

theorem MovingSofa.gerverStageTimes_two_le_seven_div_ten : gerverStageTimes 2 ≤ 7 / 10

The second Gerver stage time is at most 7/10. This coarse bound on the certified switching angle θ is what the stage speed estimates below consume.

theorem MovingSofa.gerverStageIntervals_zero : gerverStageIntervals 0 = Set.Icc (gerverStageTimes 0) (gerverStageTimes 1)

The first Gerver stage runs between the first two stage times.

theorem MovingSofa.gerverStageIntervals_one : gerverStageIntervals 1 = Set.Icc (gerverStageTimes 1) (gerverStageTimes 2)

The second Gerver stage runs between the second and third stage times.

theorem MovingSofa.gerverStageIntervals_three : gerverStageIntervals 3 = Set.Icc (gerverStageTimes 3) (gerverStageTimes 4)

The fourth Gerver stage runs between the fourth and fifth stage times.

theorem MovingSofa.gerverStageIntervals_four : gerverStageIntervals 4 = Set.Icc (gerverStageTimes 4) (gerverStageTimes 5)

The fifth Gerver stage runs between the last two stage times.

theorem MovingSofa.contDiff_paperGerverPath : ContDiff ℝ 1 paperGerverPath

The certified direct Gerver path is continuously differentiable.

theorem MovingSofa.continuous_paperGerverContact (i : Fin 4) : Continuous fun (t : ℝ) => paperGerverContacts t i

Each Gerver contact curve is continuous.

theorem MovingSofa.contDiffOn_paperGerverContact (i : Fin 4) (j : Fin 5) : ContDiffOn ℝ 1 (fun (t : ℝ) => paperGerverContacts t i) (gerverStageIntervals j)

Each Gerver contact curve is continuously differentiable on each closed stage interval.

The two inner contact curves as bounded-variation paths

noncomputable def MovingSofa.gerverRightContactBV : ContinuousBVPaths (gerverStageTimes 3) (gerverStageTimes 5)

The second Gerver contact curve, on the two stages [t₃, t₅] where it is an inner contact of the cap, as a continuous path of bounded variation.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MovingSofa.gerverLeftContactBV : ContinuousBVPaths (gerverStageTimes 0) (gerverStageTimes 2)

The fourth Gerver contact curve, on the two stages [t₀, t₂] where it is an inner contact of the cap, as a continuous path of bounded variation.

Equations

• One or more equations did not get rendered due to their size.

theorem MovingSofa.gerverRightContactBV_apply (t : ↑(Set.Icc (gerverStageTimes 3) (gerverStageTimes 5))) : ↑gerverRightContactBV t = paperGerverContacts (↑t) 1

gerverRightContactBV is the second Gerver contact curve.

theorem MovingSofa.gerverLeftContactBV_apply (t : ↑(Set.Icc (gerverStageTimes 0) (gerverStageTimes 2))) : ↑gerverLeftContactBV t = paperGerverContacts (↑t) 3

gerverLeftContactBV is the fourth Gerver contact curve.

Stage derivatives of the two inner contact curves

theorem MovingSofa.deriv_paperGerverPath_eq_smul_add_smul {t a b : ℝ} (h : paperGerverVelocityComponents t = (a, b)) : deriv paperGerverPath t = a • normalVector ↑t + b • tangentVector ↑t

The velocity components are the frame coordinates of the derivative of the direct path.

theorem MovingSofa.hasDerivWithinAt_paperGerverContacts_one {i : Fin 5} {t c α' : ℝ} {α β : ℝ → ℝ} (ht : t ∈ gerverStageIntervals i) (hα : HasDerivAt α α' t) (hαβ : ∀ s ∈ gerverStageIntervals i, paperGerverVelocityComponents s = (α s, β s)) (hc : β t + α' = c) : HasDerivWithinAt (fun (s : ℝ) => paperGerverContacts s 1) (c • tangentVector ↑t) (gerverStageIntervals i) t

On a stage where the direct path has velocity components (α, β), the second contact curve B = x + α v has derivative (β + α') v: the frame derivative v' = -u cancels the normal component α u of x', leaving the tangential component β v and the derivative of the coefficient.

theorem MovingSofa.hasDerivWithinAt_paperGerverContacts_three {i : Fin 5} {t c β' : ℝ} {α β : ℝ → ℝ} (ht : t ∈ gerverStageIntervals i) (hβ : HasDerivAt β β' t) (hαβ : ∀ s ∈ gerverStageIntervals i, paperGerverVelocityComponents s = (α s, β s)) (hc : α t - β' = c) : HasDerivWithinAt (fun (s : ℝ) => paperGerverContacts s 3) (c • normalVector ↑t) (gerverStageIntervals i) t

On a stage where the direct path has velocity components (α, β), the fourth contact curve D = x - β u has derivative (α - β') u; see hasDerivWithinAt_paperGerverContacts_one for the shape of the computation.

theorem MovingSofa.hasDerivWithinAt_paperGerverContacts_one_neg_smul {i : Fin 5} (hi : i = 3 ∨ i = 4) {t : ℝ} (ht : t ∈ gerverStageIntervals i) : ∃ c < 0, HasDerivWithinAt (fun (s : ℝ) => paperGerverContacts s 1) (c • tangentVector ↑t) (gerverStageIntervals i) t

On each of the last two stages the second contact curve moves strictly backwards along the tangent direction: its one-sided derivative is a negative multiple of v_t. On the fourth stage the tangential speed is d₁ - 1 - t/2, negative because t ≥ π/2 - θ > 4/5 and d₁ ≤ 33/25; on the fifth it is the exact constant -1/2.

theorem MovingSofa.hasDerivWithinAt_paperGerverContacts_three_pos_smul {i : Fin 5} (hi : i = 0 ∨ i = 1) {t : ℝ} (ht : t ∈ gerverStageIntervals i) : ∃ (c : ℝ), 0 < c ∧ HasDerivWithinAt (fun (s : ℝ) => paperGerverContacts s 3) (c • normalVector ↑t) (gerverStageIntervals i) t

On each of the first two stages the fourth contact curve moves strictly forwards along the normal direction: its one-sided derivative is a positive multiple of u_t. On the first stage the normal speed is the exact constant 1/2; on the second it is 1 + b₁ - t/2, positive because t ≤ θ ≤ 7/10 and b₁ ≥ -53/100.

Frame coordinates of the direct path

theorem MovingSofa.hasDerivAt_paperGerverPath_frame (t : ℝ) : HasDerivAt paperGerverPath ((paperGerverVelocityComponents t).1 • normalVector ↑t + (paperGerverVelocityComponents t).2 • tangentVector ↑t) t

The derivative of the direct Gerver path in the moving frame.

theorem MovingSofa.hasDerivAt_inner_paperGerverPath_normalVector (t : ℝ) : HasDerivAt (fun (s : ℝ) => inner ℝ (paperGerverPath s) (normalVector ↑s)) (inner ℝ (paperGerverContacts t 1) (tangentVector ↑t)) t

The angular derivative of the normal frame coordinate of the Gerver path is the tangent coordinate of the second contact curve: with B = x + α v the frame derivative u' = v contributes x ⋅ v and the normal component of x' contributes α.

theorem MovingSofa.hasDerivAt_inner_paperGerverPath_tangentVector (t : ℝ) : HasDerivAt (fun (s : ℝ) => inner ℝ (paperGerverPath s) (tangentVector ↑s)) (-inner ℝ (paperGerverContacts t 3) (normalVector ↑t)) t

The angular derivative of the tangent frame coordinate of the Gerver path is minus the normal coordinate of the fourth contact curve: with D = x - β u the frame derivative v' = -u contributes -x ⋅ u and the tangent component of x' contributes β.

Stagewise monotonicity of the inner contact curves against a fixed direction

theorem MovingSofa.strictAntiOn_inner_paperGerverContacts_three {i : Fin 5} (hi : i = 0 ∨ i = 1) {c : ℝ} (hlt : ∀ s ∈ gerverStageIntervals i, s < c) (hwide : ∀ s ∈ gerverStageIntervals i, c - Real.pi < s) : StrictAntiOn (fun (s : ℝ) => inner ℝ (paperGerverContacts s 3) (tangentVector ↑c)) (gerverStageIntervals i)

Against the tangent direction at a later angle c, the fourth Gerver contact curve is strictly antitone on each of its first two stages: its stage speed is a positive multiple of u_s, whose v_c coordinate is sin (s - c) < 0.

theorem MovingSofa.strictMonoOn_inner_paperGerverContacts_one {i : Fin 5} (hi : i = 3 ∨ i = 4) {c : ℝ} (hlt : ∀ s ∈ gerverStageIntervals i, c < s) (hwide : ∀ s ∈ gerverStageIntervals i, s < c + Real.pi) : StrictMonoOn (fun (s : ℝ) => inner ℝ (paperGerverContacts s 1) (normalVector ↑c)) (gerverStageIntervals i)

Against the normal direction at an earlier angle c, the second Gerver contact curve is strictly monotone on each of its last two stages: its stage speed is a negative multiple of v_s, whose u_c coordinate is sin (c - s) < 0.

Stage endpoints, grid angles and branch selection

The certificate subdivides each of the five analytic stages of Gerver's sofa into NN = 64 equal parts. This module carries the real-valued mirror of that grid: gerverStageTime re-indexes the six stage endpoints by a natural number, gerverGridTime m is the m-th grid angle, gerverContactPoint is the dictionary of the four contact curves and the ambient path, and GerverAreaCert.stageOf m is the analytic branch that the piecewise definitions select at the m-th angle. The soundness statements endZ_sound and ttZ_sound say that the integer data of the certificate encloses these real quantities; the remaining lemmas are the order facts the evaluator needs.

noncomputable def MovingSofa.gerverStageTime (s : ℕ) : ℝ

The six stage endpoints indexed by a natural number, constant past 5.

Equations

• MovingSofa.gerverStageTime s = MovingSofa.gerverStageTimes ⟨min 5 s, ⋯⟩

noncomputable def MovingSofa.gerverGridTime (m : ℕ) : ℝ

The real grid angle at index m, mirroring GerverAreaCert.ttZ.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MovingSofa.gerverContactPoint : ℕ → ℝ → Point

The curve selected by a certificate kind: 0 the path, 1 A, 2 B, 3 C, 4 D.

Equations

• MovingSofa.gerverContactPoint 0 = MovingSofa.paperGerverPath
• MovingSofa.gerverContactPoint 1 = fun (t : ℝ) => MovingSofa.paperGerverContacts t 0
• MovingSofa.gerverContactPoint 2 = fun (t : ℝ) => MovingSofa.paperGerverContacts t 1
• MovingSofa.gerverContactPoint 3 = fun (t : ℝ) => MovingSofa.paperGerverContacts t 2
• MovingSofa.gerverContactPoint x✝ = fun (t : ℝ) => MovingSofa.paperGerverContacts t 3

theorem MovingSofa.gerverStageTime_zero : gerverStageTime 0 = 0

The rotation interval starts at the first stage endpoint 0.

theorem MovingSofa.gerverStageTime_one : gerverStageTime 1 = GerverSofa.PartB.params.phi

The first stage ends at φ.

theorem MovingSofa.gerverStageTime_two : gerverStageTime 2 = GerverSofa.PartB.params.theta

The second stage ends at θ.

theorem MovingSofa.gerverStageTime_three : gerverStageTime 3 = GerverSofa.PartC.eta

The third stage ends at η = π / 2 - θ.

theorem MovingSofa.gerverStageTime_four : gerverStageTime 4 = GerverSofa.PartC.tau

The fourth stage ends at τ = π / 2 - φ.

theorem MovingSofa.gerverStageTime_five : gerverStageTime 5 = Real.pi / 2

The fifth stage ends at π / 2.

Order properties of the stage endpoints and the grid

theorem MovingSofa.gerverStageTime_lt_succ (s : ℕ) (hs : s < 5) : gerverStageTime s < gerverStageTime (s + 1)

The five stage endpoints are strictly increasing.

theorem MovingSofa.endZ_sound (s : ℕ) (hs : s ≤ 5) : (GerverAreaCert.endZ s).Contains (gerverStageTime s)

The integer stage endpoints enclose the real ones.

theorem MovingSofa.ttZ_sound (m : ℕ) (hm : m ≤ 5 * GerverAreaCert.NN) : (GerverAreaCert.ttZ m).Contains (gerverGridTime m)

The integer grid angles enclose the real ones.

theorem MovingSofa.gerverGridTime_succ_sub (m : ℕ) : gerverGridTime (m + 1) - gerverGridTime m = (gerverStageTime (m / GerverAreaCert.NN + 1) - gerverStageTime (m / GerverAreaCert.NN)) / ↑GerverAreaCert.NN

The grid step is uniform across stage joins.

theorem MovingSofa.gerverGridTime_lt_succ (m : ℕ) (hm : m < 5 * GerverAreaCert.NN) : gerverGridTime m < gerverGridTime (m + 1)

The grid angles are strictly increasing.

theorem MovingSofa.gerverGridTime_lt_of_lt {m n : ℕ} (hmn : m < n) (hn : n ≤ 5 * GerverAreaCert.NN) : gerverGridTime m < gerverGridTime n

Strict monotonicity of the grid angles below the top index, from gerverGridTime_lt_succ.

theorem MovingSofa.gerverGridTime_le_of_le {m n : ℕ} (hmn : m ≤ n) (hn : n ≤ 5 * GerverAreaCert.NN) : gerverGridTime m ≤ gerverGridTime n

Weak monotonicity of the grid angles below the top index, from gerverGridTime_lt_succ.

theorem MovingSofa.gerverGridTime_mul_NN (s : ℕ) : gerverGridTime (s * GerverAreaCert.NN) = gerverStageTime s

The grid angle at a stage boundary is the stage endpoint itself.

theorem MovingSofa.gerverGridTime_zero : gerverGridTime 0 = 0

The grid starts at 0.

theorem MovingSofa.gerverGridTime_top : gerverGridTime (5 * GerverAreaCert.NN) = Real.pi / 2

The grid ends at π / 2.

theorem MovingSofa.gerverGridTime_mem_Icc (m : ℕ) (hm : m ≤ 5 * GerverAreaCert.NN) : gerverGridTime m ∈ Set.Icc 0 (Real.pi / 2)

Every grid angle lies in the rotation interval.

theorem MovingSofa.stageOf_mem (m : ℕ) (hm : m ≤ 5 * GerverAreaCert.NN) : 1 ≤ GerverAreaCert.stageOf m ∧ GerverAreaCert.stageOf m ≤ 5

The branch index is one of the five stages.

theorem MovingSofa.gerverGridTime_le_stageTime (m : ℕ) (hm : m ≤ 5 * GerverAreaCert.NN) : gerverGridTime m ≤ gerverStageTime (GerverAreaCert.stageOf m)

The grid angle does not exceed the right endpoint of its branch.

theorem MovingSofa.stageTime_lt_gerverGridTime (m : ℕ) (hm : m ≤ 5 * GerverAreaCert.NN) (h2 : 2 ≤ GerverAreaCert.stageOf m) : gerverStageTime (GerverAreaCert.stageOf m - 1) < gerverGridTime m

The grid angle strictly exceeds the left endpoint of its branch, except on the first branch.

Properties of the Gerver niche roof

The main results of this file describe the upper boundary of the paper's literal Gerver niche: the three graph pieces join up (gerver_niche_piece_endpoints), each piece stays inside the outer cap (gerver_niche_roof_membership), the roof is a strictly monotone positive graph (gerver_niche_roof_strictMono, gerver_niche_roof_positive), and the niche is exactly the strict vertical region under that roof (gerver_niche_vertical_fills). The three pieces are identified branch by branch in gerverNicheRoof_of_le_two, gerverNicheRoof_mid and gerverNicheRoof_of_ge_three, each valid on the closed stage.

Alongside them sits the elementary API of the reverse-time reparametrization (continuous_gerverRoofReverseTime, gerverRoofReverseTime_two, gerverRoofReverseTime_three, gerverRoofReverseTime_mem_Icc) and the continuity of the roof, in both its real-parameter and its restricted form (continuous_gerverRoofCurve, continuous_gerverNicheRoof).

Every one of them is the certified Part C niche geometry read through the coordinate dictionary GerverSofa.PartF.Coordinates.toPlane. The dictionary itself is supplied by the public readers of the lower modules — paperGerverContacts_one_eq_toPlane and paperGerverContacts_three_eq_toPlane for the contact curves, gerverStageTimes_zero through gerverStageTimes_five for the stage times, and mem_gerverLiteralNiche_iff, toPlane_mem_gerverOuterCap for the two literal sets. What remains here, and is kept private, is the roof-specific part of the dictionary: the reverse-time reparametrization and the identification of gerverNicheRoof with the certified upper arc.

theorem MovingSofa.gerver_niche_piece_endpoints : paperGerverContacts (gerverStageTimes 3) 1 = paperGerverPath (gerverStageTimes 1) ∧ paperGerverContacts (gerverStageTimes 2) 3 = paperGerverPath (gerverStageTimes 4) ∧ (paperGerverContacts (Real.pi / 2) 1).ofLp 1 = 0 ∧ (paperGerverContacts 0 3).ofLp 1 = 0

The three graph pieces of the niche roof join up: the second contact curve at eta meets the ambient path at params.phi, the fourth contact curve at params.theta meets the ambient path at tau, and the two outer ends touch the wall.

The reverse-time reparametrization, and continuity of the roof

theorem MovingSofa.continuous_gerverRoofReverseTime : Continuous gerverRoofReverseTime

The reverse-time reparametrization is affine, hence continuous.

theorem MovingSofa.gerverRoofReverseTime_two : gerverRoofReverseTime (gerverStageTimes 2) = gerverStageTimes 4

The reverse-time map sends the start of the middle roof stage to the late path time.

theorem MovingSofa.gerverRoofReverseTime_three : gerverRoofReverseTime (gerverStageTimes 3) = gerverStageTimes 1

The reverse-time map sends the end of the middle roof stage to the early path time.

theorem MovingSofa.gerverRoofReverseTime_mem_Icc {s : ℝ} (h1 : gerverStageTimes 2 ≤ s) (h2 : s ≤ gerverStageTimes 3) : gerverRoofReverseTime s ∈ Set.Icc (gerverStageTimes 1) (gerverStageTimes 4)

The reverse-time map carries the middle roof interval into the central path interval.

The three graph pieces of the roof

theorem MovingSofa.gerverNicheRoof_of_le_two {s : ℝ} (hs : s ∈ Set.Icc 0 (Real.pi / 2)) (h : s ≤ gerverStageTimes 2) : gerverNicheRoof ⟨s, hs⟩ = paperGerverContacts s 3

Up to the second stage time the niche roof is the fourth contact curve.

theorem MovingSofa.gerverNicheRoof_mid {s : ℝ} (hs : s ∈ Set.Icc 0 (Real.pi / 2)) (h1 : gerverStageTimes 2 ≤ s) (h2 : s ≤ gerverStageTimes 3) : gerverNicheRoof ⟨s, hs⟩ = paperGerverPath (gerverRoofReverseTime s)

On the middle stage the niche roof is the reverse-time ambient path. The identification extends to the left endpoint of the stage by the piece-endpoint gluing.

theorem MovingSofa.gerverNicheRoof_of_ge_three {s : ℝ} (hs : s ∈ Set.Icc 0 (Real.pi / 2)) (h : gerverStageTimes 3 ≤ s) : gerverNicheRoof ⟨s, hs⟩ = paperGerverContacts s 1

From the third stage time on the niche roof is the second contact curve. The identification extends to the left endpoint of the stage by the piece-endpoint gluing.

theorem MovingSofa.gerverRoofCurve_eq (s : ↑(Set.Icc 0 (Real.pi / 2))) : gerverRoofCurve ↑s = gerverNicheRoof s

On the rotation interval the real-parameter roof curve is the niche roof.

theorem MovingSofa.continuous_gerverRoofCurve : Continuous gerverRoofCurve

The roof curve is continuous: its three graph pieces join up at the two cut times, by the two endpoint identities of gerver_niche_piece_endpoints.

theorem MovingSofa.continuous_gerverNicheRoof : Continuous gerverNicheRoof

The niche roof is continuous.

theorem MovingSofa.gerver_niche_roof_strictMono : StrictMono fun (s : ↑(Set.Icc 0 (Real.pi / 2))) => (gerverNicheRoof s).ofLp 0

The first coordinate of the niche roof is strictly increasing, so the roof really is a graph over the horizontal axis.

theorem MovingSofa.gerver_niche_roof_positive (s : ↑(Set.Icc 0 (Real.pi / 2))) (hs : 0 < ↑s ∧ ↑s < Real.pi / 2) : 0 < (gerverNicheRoof s).ofLp 1

The niche roof has positive height strictly inside the rotation interval.

theorem MovingSofa.gerver_niche_roof_membership : (∀ t ∈ Set.Icc (gerverStageTimes 0) (gerverStageTimes 2), paperGerverContacts t 3 ∈ gerverOuterCap) ∧ (∀ t ∈ Set.Icc (gerverStageTimes 1) (gerverStageTimes 4), paperGerverPath t ∈ gerverOuterCap) ∧ ∀ t ∈ Set.Icc (gerverStageTimes 3) (gerverStageTimes 5), paperGerverContacts t 1 ∈ gerverOuterCap

Each of the three graph pieces of the niche roof stays inside the paper outer cap.

def MovingSofa.strictVerticalFill (f : ℝ → Point) (I : Set ℝ) : Set Point

The strict region between the wall and the graph of f over the parameter set I.

Equations

• MovingSofa.strictVerticalFill f I = {q : MovingSofa.Point | ∃ t ∈ I, q.ofLp 0 = (f t).ofLp 0 ∧ 0 ≤ q.ofLp 1 ∧ q.ofLp 1 < (f t).ofLp 1}

theorem MovingSofa.gerver_niche_vertical_fills : gerverLiteralNiche = strictVerticalFill (fun (t : ℝ) => paperGerverContacts t 3) (Set.Icc (gerverStageTimes 0) (gerverStageTimes 2)) ∪ strictVerticalFill paperGerverPath (Set.Icc (gerverStageTimes 1) (gerverStageTimes 4)) ∪ strictVerticalFill (fun (t : ℝ) => paperGerverContacts t 1) (Set.Icc (gerverStageTimes 3) (gerverStageTimes 5))

The paper literal niche is exactly the union of the three strict vertical fills under the three graph pieces of the niche roof.

Moving sofa: related mathematical developments

• Cap.Tail.Arcs.
• Cap.Tail.Space.
• Cap.CornerMeasure.
• Cap.CornerPaths.
• Cap.Tail.Canonical.

Cap / Tail / Arcs

structure MovingSofa.DirectedArcData : Type

A planar carrier set equipped with ordered start and end points.

• carrier : Set Point

  The set traced by the directed arc.

• startPoint : Point

  The starting point of the arc.

• endPoint : Point

  The ending point of the arc.

noncomputable def MovingSofa.rightLeftTailArcs (B D : ConvexBody Point) : DirectedArcData × DirectedArcData

The directed convex boundary arcs used for the right and left tail bodies.

Equations

• One or more equations did not get rendered due to their size.

Cap / Tail / Space

noncomputable def MovingSofa.capInnerCorner (K : RightAngleCapSpace) (t : ℝ) : Point

The real-angle inner-corner path of a cap.

Equations

• MovingSofa.capInnerCorner K t = (MovingSofa.rotatingHallwayParts ↑↑K ↑t).innerCorner

def MovingSofa.HasCapDensities (K : RightAngleCapSpace) (r s : ℝ → NNReal) : Prop

The two surface densities on the upper half-circle, with the top atom excluded.

Equations

• One or more equations did not get rendered due to their size.

def MovingSofa.SatisfiesInjectivityCondition (K : RightAngleCapSpace) : Prop

The density, corner regularity and strict interior signs of the injectivity condition.

Equations

• One or more equations did not get rendered due to their size.

def MovingSofa.SpecialCapSpace : Type

Right-angle caps satisfying injectivity and the cap-area threshold.

Equations

• MovingSofa.SpecialCapSpace = { K : MovingSofa.RightAngleCapSpace // MovingSofa.SatisfiesInjectivityCondition K ∧ 11 / 5 ≤ MovingSofa.ClassicalResults.area ↑↑K }

structure MovingSofa.CapTailSpace : Type

A special cap and two convex tails satisfying the support constraints.

• cap : SpecialCapSpace

  The special cap forming the central component of the triple.

• rightBody : ConvexBody Point

  The convex body used as the right tail.

• leftBody : ConvexBody Point

  The convex body used as the left tail.

• right_subset : ↑self.rightBody ⊆ ↑↑↑self.cap
• left_subset : ↑self.leftBody ⊆ ↑↑↑self.cap
• right_bound (t : ℝ) : t ∈ Set.Icc paperGerverConstants.2.1 (Real.pi / 2) → supportValue ↑↑↑self.cap ↑t + supportValue ↑self.rightBody ↑(Real.pi + t) ≤ 1
• right_eq (t : ℝ) : t ∈ {paperGerverConstants.2.1, Real.pi / 2} → supportValue ↑↑↑self.cap ↑t + supportValue ↑self.rightBody ↑(Real.pi + t) = 1
• left_bound (t : ℝ) : t ∈ Set.Icc 0 paperGerverConstants.2.2 → supportValue ↑↑↑self.cap ↑(Real.pi / 2 + t) + supportValue ↑self.leftBody ↑(3 * Real.pi / 2 + t) ≤ 1
• left_eq (t : ℝ) : t ∈ {0, paperGerverConstants.2.2} → supportValue ↑↑↑self.cap ↑(Real.pi / 2 + t) + supportValue ↑self.leftBody ↑(3 * Real.pi / 2 + t) = 1

Cap / Corner Measure

noncomputable def MovingSofa.capVelocityCoefficients (K : SpecialCapSpace) (t : ℝ) : ℝ × ℝ

The normal and tangent components of the inner-corner path derivative.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MovingSofa.capCornerDensity (K : SpecialCapSpace) (s : ℝ) : ℝ

The density formed by joining the two signed corner-velocity components over [0, π].

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MovingSofa.capCornerMeasure (K : SpecialCapSpace) : MeasureTheory.Measure ℝ

The measure on the real angle interval defined by the nonnegative corner density.

Equations

• MovingSofa.capCornerMeasure K = (MeasureTheory.volume.restrict (Set.Icc 0 Real.pi)).withDensity fun (s : ℝ) => ENNReal.ofReal (MovingSofa.capCornerDensity K s)

noncomputable def MovingSofa.capCornerAngleMeasure (K : SpecialCapSpace) : MeasureTheory.Measure Real.Angle

Push the corner-density measure to angles modulo a full turn.

Equations

• MovingSofa.capCornerAngleMeasure K = MeasureTheory.Measure.map (fun (s : ℝ) => ↑s) (MovingSofa.capCornerMeasure K)

noncomputable def MovingSofa.capCornerMeasureData (K : SpecialCapSpace) : (ℝ → ℝ) × MeasureTheory.Measure ℝ × MeasureTheory.Measure Real.Angle

Bundle the corner density and its real and angular measures.

Equations

• MovingSofa.capCornerMeasureData K = (MovingSofa.capCornerDensity K, MovingSofa.capCornerMeasure K, MovingSofa.capCornerAngleMeasure K)

theorem MovingSofa.capCornerAngleMeasure_angleImage_eq_setLIntegral (K : SpecialCapSpace) {T : Set ℝ} (hT : MeasurableSet T) (hT' : T ⊆ Set.Icc 0 Real.pi) : (capCornerAngleMeasure K) ((fun (s : ℝ) => ↑s) '' T) = ∫⁻ (s : ℝ) in T, ENNReal.ofReal (capCornerDensity K s)

The corner measure of a special cap reads its density on the angular image of every measurable subset of [0, π].

Regularity and signs of the corner density

The injectivity condition makes the inner corner continuously differentiable on the closed quarter turn, so both frame coefficients of its velocity are continuous there; the strict interior signs then extend to the two endpoints by continuity. The corner density is the sum of the two branches extended by zero, whence its measurability and its bound.

theorem MovingSofa.continuousOn_derivWithin_capInnerCorner (K : SpecialCapSpace) : ContinuousOn (derivWithin (capInnerCorner ↑K) (Set.Icc 0 (Real.pi / 2))) (Set.Icc 0 (Real.pi / 2))

The inner-corner velocity of a special cap is continuous on the cap domain.

theorem MovingSofa.continuousOn_capVelocityCoefficients (K : SpecialCapSpace) : ContinuousOn (fun (s : ℝ) => (capVelocityCoefficients K s).1) (Set.Icc 0 (Real.pi / 2)) ∧ ContinuousOn (fun (s : ℝ) => (capVelocityCoefficients K s).2) (Set.Icc 0 (Real.pi / 2))

Both frame components of the inner-corner velocity are continuous on the cap domain.

theorem MovingSofa.exists_bound_capCornerDensity (K : SpecialCapSpace) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (s : ℝ), capCornerDensity K s ≤ C

The corner density is bounded, being continuous on the two compact halves of the cap domain and zero outside.

Finiteness and atomlessness of the corner measure

instance MovingSofa.isFiniteMeasure_capCornerMeasure (K : SpecialCapSpace) : MeasureTheory.IsFiniteMeasure (capCornerMeasure K)

instance MovingSofa.isFiniteMeasure_capCornerAngleMeasure (K : SpecialCapSpace) : MeasureTheory.IsFiniteMeasure (capCornerAngleMeasure K)

instance MovingSofa.nullSingletonClass_capCornerAngleMeasure (K : SpecialCapSpace) : MeasureTheory.NullSingletonClass (capCornerAngleMeasure K)

Cap / Corner Paths

noncomputable def MovingSofa.capCornerBV (K : SpecialCapSpace) {a b : ℝ} (h : Set.Icc a b ⊆ Set.Icc 0 (Real.pi / 2)) : ContinuousBVPaths a b

The inner-corner path restricted and bundled as a continuous BV path.

Equations

• MovingSofa.capCornerBV K h = MovingSofa.continuousBVOfContDiffOn (MovingSofa.capInnerCorner ↑K) ⋯

noncomputable def MovingSofa.capMiddleBV (K : SpecialCapSpace) : ContinuousBVPaths paperGerverConstants.2.1 paperGerverConstants.2.2

The corner BV path between the two reflected Gerver switching angles.

Equations

• MovingSofa.capMiddleBV K = MovingSofa.capCornerBV K MovingSofa.capMiddleBV._proof_1

Cap / Tail / Canonical

def MovingSofa.innerWallUpperHalfPlanes (K : RightAngleCapSpace) (t : ℝ) : Set Point × Set Point

The closed half-planes above the right and left inner supporting walls.

Equations

• One or more equations did not get rendered due to their size.

def MovingSofa.canonicalTailSets (K : SpecialCapSpace) : Set Point × Set Point

The right and left canonical tail sets, before bundling their convex-body proofs.

Equations

• One or more equations did not get rendered due to their size.