Moving sofa: related mathematical developments

• Polygon.Foundations.Development002.
• Bounds.Foundations.Development003.
• Cap.Foundations.Development005.
• Sofa.Foundations.Development001.
• Cap.Foundations.Development006.
• Bounds.Foundations.Development004.
• Cap.Foundations.Development007.
• Area.Foundations.Development003.
• Bounds.Foundations.Development005.
• Bounds.Foundations.Development006.
• Motion.Foundations.Development002.
• Sofa.Foundations.Development002.

Moving sofa: related mathematical developments

• Polygon.Approximation.
• Polygon.CapWidthBound.
• Polygon.DiscreteCapData.
• Polygon.Height.Properties.
• Polygon.Nef.Slices.
• Polygon.Nef.Variation.LocalSlices.
• Polygon.Nef.Variation.Area.
• Polygon.Nef.Variation.Boundary.
• Polygon.Nef.Variation.
• Polygon.Nef.SignedVariation.
• Polygon.Height.WallVariation.
• Polygon.RightAngleGrid.
• Polygon.Translation.
• Polygon.Height.Reconstruction.
• Polygon.Height.PositiveIncrement.Contacts.
• Polygon.Height.PositiveIncrement.

Polygon / Approximation

theorem MovingSofa.mem_angleCap_iff (Θ : AngleSet) (K : CapSpace Θ.angle) (p : Point) : p ∈ angleCap Θ K ↔ ((0 ≤ p.ofLp 1 ∧ p.ofLp 1 ≤ 1) ∧ 0 ≤ inner ℝ p (normalVector ↑Θ.angle) ∧ inner ℝ p (normalVector ↑Θ.angle) ≤ 1) ∧ ∀ t ∈ Θ.directions, inner ℝ p (normalVector ↑t) ≤ supportValue ↑↑K ↑t ∧ inner ℝ p (normalVector ↑(t + Real.pi / 2)) ≤ supportValue ↑↑K ↑(t + Real.pi / 2)

Membership in a polygon cap is given by the strip and selected support inequalities.

theorem MovingSofa.subset_angleCap (Θ : AngleSet) (K : CapSpace Θ.angle) : ↑↑K ⊆ angleCap Θ K

The polygon-cap approximation contains the original cap.

theorem MovingSofa.angleCap_eq_iInter_supportValue (Θ : AngleSet) (K : CapSpace Θ.angle) : angleCap Θ K = ⋂ t ∈ (fun (t : ℝ) => ↑t) '' angleDomain Θ ∪ capLowerNormals Θ.angle, normalHalfPlane t (supportValue (↑↑K) t) false false

A polygon cap is the intersection of its selected support half-planes.

theorem MovingSofa.isClosed_angleCap (Θ : AngleSet) (K : CapSpace Θ.angle) : IsClosed (angleCap Θ K)

Polygon-cap approximations are closed.

theorem MovingSofa.convex_angleCap (Θ : AngleSet) (K : CapSpace Θ.angle) : Convex ℝ (angleCap Θ K)

Polygon-cap approximations are convex.

theorem MovingSofa.supportValue_angleCap (Θ : AngleSet) (K : CapSpace Θ.angle) {t : Real.Angle} (ht : t ∈ (fun (t : ℝ) => ↑t) '' angleDomain Θ ∪ capLowerNormals Θ.angle) : supportValue (angleCap Θ K) t = supportValue (↑↑K) t

Polygon-cap approximation preserves support at every selected normal.

theorem MovingSofa.angleCap_eq_self (Θ : AngleSet) (P : PolygonCapSpace Θ) : angleCap Θ ↑P = ↑↑↑P

Polygon-cap approximation fixes caps with the prescribed normals.

theorem MovingSofa.isBounded_angleCap (Θ : AngleSet) (K : CapSpace Θ.angle) : Bornology.IsBounded (angleCap Θ K)

An interior selected direction bounds the polygon cap, including at right angle.

theorem MovingSofa.isCompact_angleCap (Θ : AngleSet) (K : CapSpace Θ.angle) : IsCompact (angleCap Θ K)

Polygon-cap approximations are compact.

theorem MovingSofa.angleCap_properties (Θ : AngleSet) (K : CapSpace Θ.angle) : (∃ (P : PolygonCapSpace Θ), ↑↑↑P = angleCap Θ K) ∧ ↑↑K ⊆ angleCap Θ K ∧ (∀ t ∈ (fun (t : ℝ) => ↑t) '' angleDomain Θ ∪ capLowerNormals Θ.angle, supportValue (angleCap Θ K) t = supportValue (↑↑K) t) ∧ ∀ (P : PolygonCapSpace Θ), angleCap Θ ↑P = ↑↑↑P

theorem MovingSofa.polygonNiche_angleCap (Θ : AngleSet) (K P : CapSpace Θ.angle) (hP : ↑↑P = angleCap Θ K) : polygonNiche Θ K = polygonNiche Θ P ∧ polygonNiche Θ K ⊆ capNiche K

theorem MovingSofa.polygonArea_upperBound (Θ : AngleSet) : (∀ (K : PolygonCapSpace Θ), polygonAreaFunctional Θ ↑K = ClassicalResults.area ↑↑↑K - ClassicalResults.area (polygonNiche Θ ↑K)) ∧ ∀ (K : CapSpace Θ.angle), capAreaFunctional K ≤ polygonAreaFunctional Θ K

theorem MovingSofa.polygonAreaFunctional_le_maximum (Θ : AngleSet) (P : PolygonCapSpace Θ) (hP : IsMaximumPolygonCap Θ P) (K : CapSpace Θ.angle) : polygonAreaFunctional Θ K ≤ polygonAreaFunctional Θ ↑P

A maximum polygon cap dominates every cap under the polygon area functional.

Polygon / Cap Width Bound

theorem MovingSofa.polygonCap_width_bound (ω t : ℝ) (hω : 0 < ω) (hω' : ω ≤ Real.pi / 2) (ht : t ∈ Set.Ioo 0 ω) : ∃ (c : ℝ), 0 < c ∧ ∀ (Θ : AngleSet), Θ.angle = ω → t ∈ Θ.directions → ∀ (K : PolygonCapSpace Θ), 0 ≤ polygonAreaFunctional Θ ↑K → directionalWidth (↑↑↑K) 0 ≤ c

Polygon / Discrete Cap Data

noncomputable def MovingSofa.rightAngleSet (n : ℕ) (hn : 2 ≤ n) : AngleSet

The uniformly spaced interior directions for a right-angle polygonal approximation.

Equations

• MovingSofa.rightAngleSet n hn = MovingSofa.uniformAngleSet (Real.pi / 2) MovingSofa.rightAngleSet._proof_1 MovingSofa.rightAngleSet._proof_3 n hn

noncomputable def MovingSofa.polygonStepSize (n : ℕ) : ℝ

The angular mesh size π/(2n).

Equations

• MovingSofa.polygonStepSize n = Real.pi / 2 / ↑n

def MovingSofa.IsMaximumPolygonCapSteps (n : ℕ) (K : RightAngleCapSpace) : Prop

The cap maximizes the polygonal functional on a uniform mesh with a power-of-two step count.

Equations

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

noncomputable def MovingSofa.magicFunctions : (NNReal → ℝ) × (NNReal → ℝ)

The two piecewise scalar functions used in the arm-length inequalities.

Equations

• MovingSofa.magicFunctions = (fun (x : NNReal) => max |↑x - 1| ((|↑x - 1| + 1) / 2), fun (x : NNReal) => ↑x - max |↑x - 1| ((|↑x - 1| + 1) / 2))

theorem MovingSofa.magicFunctions_snd_monotone : Monotone magicFunctions.2

The magic function m₀ is nondecreasing: it is 3 * x / 2 - 1 on [0, 1], x / 2 on [1, 2], and constant equal to 1 afterwards.

Polygon / Height / Properties

theorem MovingSofa.polygonHeightCap_of_translate {Θ : AngleSet} (K : PolygonCapTranslateSpace Θ) : polygonHeightCap (polygonTranslateHeight K) = ↑K

theorem MovingSofa.polygonTranslateHeight_injective (Θ : AngleSet) : Function.Injective polygonTranslateHeight

theorem MovingSofa.polygonHeightNiche_of_cap {Θ : AngleSet} (K : PolygonCapSpace Θ) : (polygonHeightNiche fun (t : ↑(angleDomain Θ)) => supportValue ↑↑↑K ↑↑t) = polygonNiche Θ ↑K ∧ (polygonHeightArea fun (t : ↑(angleDomain Θ)) => supportValue ↑↑↑K ↑↑t) = polygonAreaFunctional Θ ↑K

theorem MovingSofa.polygonTranslateExtensions_eq {Θ : AngleSet} (K : PolygonCapSpace Θ) (q : Point) (K' : PolygonCapTranslateSpace Θ) (hK : ↑K' = (fun (p : Point) => p + q) '' ↑↑↑K) : (polygonTranslateExtensions K').1 = (fun (p : Point) => p + q) '' polygonNiche Θ ↑K ∧ (polygonTranslateExtensions K').2 = polygonAreaFunctional Θ ↑K

Polygon / Nef / Slices

noncomputable def MovingSofa.Nef.framePoint (a : Real.Angle) (x y : ℝ) : Point

Convert normal and tangent coordinates into a point in the frame at angle a.

Equations

• MovingSofa.Nef.framePoint a x y = MovingSofa.rotationMap a !₂[x, y]

theorem MovingSofa.Nef.framePoint_eq (a : Real.Angle) (x y : ℝ) : framePoint a x y = x • normalVector a + y • tangentVector a

@[simp]

theorem MovingSofa.Nef.inner_framePoint_normalVector (a : Real.Angle) (x y : ℝ) : inner ℝ (framePoint a x y) (normalVector a) = x

@[simp]

theorem MovingSofa.Nef.inner_framePoint_tangentVector (a : Real.Angle) (x y : ℝ) : inner ℝ (framePoint a x y) (tangentVector a) = y

@[simp]

theorem MovingSofa.Nef.norm_tangentVector_angle (a : Real.Angle) : ‖tangentVector a‖ = 1

noncomputable def MovingSofa.Nef.frameNormalCoeff (a b : Real.Angle) : ℝ

The normal-normal coefficient for changing between two oriented frames.

Equations

• MovingSofa.Nef.frameNormalCoeff a b = inner ℝ (MovingSofa.normalVector a) (MovingSofa.normalVector b)

noncomputable def MovingSofa.Nef.frameTangentCoeff (a b : Real.Angle) : ℝ

The tangent-normal coefficient for changing between two oriented frames.

Equations

• MovingSofa.Nef.frameTangentCoeff a b = inner ℝ (MovingSofa.tangentVector a) (MovingSofa.normalVector b)

theorem MovingSofa.Nef.inner_framePoint_normalVector_eq (a b : Real.Angle) (x y : ℝ) : inner ℝ (framePoint a x y) (normalVector b) = frameNormalCoeff a b * x + frameTangentCoeff a b * y

def MovingSofa.Nef.cellUpper {n : ℕ} (H : Fin n → PlanarHalfPlaneData) (P : Fin n → Bool) (j : Fin n) : Bool

Select the half-plane side required by a Boolean cell’s membership pattern.

Equations

• MovingSofa.Nef.cellUpper H P j = if P j = true then (H j).upper else !(H j).upper

noncomputable def MovingSofa.Nef.frameBoundaryValue (a : Real.Angle) (H : PlanarHalfPlaneData) (x : ℝ) : ℝ

Solve the wall equation for the tangent coordinate at a fixed normal coordinate.

Equations

• MovingSofa.Nef.frameBoundaryValue a H x = (H.height - MovingSofa.Nef.frameNormalCoeff a H.angle * x) / MovingSofa.Nef.frameTangentCoeff a H.angle

theorem MovingSofa.Nef.frameBoundaryValue_sub (a : Real.Angle) (H : PlanarHalfPlaneData) (x z : ℝ) : frameBoundaryValue a H x - frameBoundaryValue a H z = -(frameNormalCoeff a H.angle / frameTangentCoeff a H.angle) * (x - z)

theorem MovingSofa.Nef.abs_frameBoundaryValue_sub (a : Real.Angle) (H : PlanarHalfPlaneData) (x z : ℝ) : |frameBoundaryValue a H x - frameBoundaryValue a H z| = |frameNormalCoeff a H.angle / frameTangentCoeff a H.angle| * |x - z|

def MovingSofa.Nef.isUpperEndpoint {n : ℕ} (a : Real.Angle) (H : Fin n → PlanarHalfPlaneData) (P : Fin n → Bool) (j : Fin n) : Prop

The wall bounds a Boolean cell’s slice from above in the selected frame.

Equations

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

def MovingSofa.Nef.isLowerEndpoint {n : ℕ} (a : Real.Angle) (H : Fin n → PlanarHalfPlaneData) (P : Fin n → Bool) (j : Fin n) : Prop

The wall bounds a Boolean cell’s slice from below in the selected frame.

Equations

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

noncomputable def MovingSofa.Nef.upperBoundaryFunctions {n : ℕ} (a : Real.Angle) (H : Fin n → PlanarHalfPlaneData) (P : Fin n → Bool) : List (ℝ → ℝ)

The affine wall functions imposing upper bounds on the slice.

Equations

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

noncomputable def MovingSofa.Nef.lowerBoundaryFunctions {n : ℕ} (a : Real.Angle) (H : Fin n → PlanarHalfPlaneData) (P : Fin n → Bool) : List (ℝ → ℝ)

The affine wall functions imposing lower bounds on the slice.

Equations

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

noncomputable def MovingSofa.Nef.upperEnvelope {n : ℕ} (a : Real.Angle) (H : Fin n → PlanarHalfPlaneData) (P : Fin n → Bool) (R x : ℝ) : ℝ

The minimum of all upper wall functions, capped by the truncation height R.

Equations

• MovingSofa.Nef.upperEnvelope a H P R x = List.foldr (fun (f : ℝ → ℝ) (r : ℝ) => min (f x) r) R (MovingSofa.Nef.upperBoundaryFunctions a H P)

noncomputable def MovingSofa.Nef.lowerEnvelope {n : ℕ} (a : Real.Angle) (H : Fin n → PlanarHalfPlaneData) (P : Fin n → Bool) (R x : ℝ) : ℝ

The maximum of all lower wall functions, bounded below by -R.

Equations

• MovingSofa.Nef.lowerEnvelope a H P R x = List.foldr (fun (f : ℝ → ℝ) (r : ℝ) => max (f x) r) (-R) (MovingSofa.Nef.lowerBoundaryFunctions a H P)

noncomputable def MovingSofa.Nef.slopeBound {n : ℕ} (a : Real.Angle) (H : Fin n → PlanarHalfPlaneData) : ℝ

The sum of absolute wall slopes, bounding the variation of slice envelopes.

Equations

• MovingSofa.Nef.slopeBound a H = ∑ j : Fin n, |MovingSofa.Nef.frameNormalCoeff a (H j).angle / MovingSofa.Nef.frameTangentCoeff a (H j).angle|

theorem MovingSofa.Nef.slopeBound_nonneg {n : ℕ} (a : Real.Angle) (H : Fin n → PlanarHalfPlaneData) : 0 ≤ slopeBound a H

theorem MovingSofa.Nef.abs_upperEnvelope_sub_le {n : ℕ} (a : Real.Angle) (H : Fin n → PlanarHalfPlaneData) (P : Fin n → Bool) (R x z : ℝ) : |upperEnvelope a H P R x - upperEnvelope a H P R z| ≤ slopeBound a H * |x - z|

theorem MovingSofa.Nef.abs_lowerEnvelope_sub_le {n : ℕ} (a : Real.Angle) (H : Fin n → PlanarHalfPlaneData) (P : Fin n → Bool) (R x z : ℝ) : |lowerEnvelope a H P R x - lowerEnvelope a H P R z| ≤ slopeBound a H * |x - z|

noncomputable def MovingSofa.Nef.cellSliceLength {n : ℕ} (a : Real.Angle) (H : Fin n → PlanarHalfPlaneData) (P : Fin n → Bool) (R x : ℝ) : ℝ

The nonnegative difference between the truncated upper and lower slice envelopes.

Equations

• MovingSofa.Nef.cellSliceLength a H P R x = max (MovingSofa.Nef.upperEnvelope a H P R x - MovingSofa.Nef.lowerEnvelope a H P R x) 0

theorem MovingSofa.Nef.abs_cellSliceLength_sub_le {n : ℕ} (a : Real.Angle) (H : Fin n → PlanarHalfPlaneData) (P : Fin n → Bool) (R x z : ℝ) : |cellSliceLength a H P R x - cellSliceLength a H P R z| ≤ 2 * slopeBound a H * |x - z|

theorem MovingSofa.Nef.continuous_cellSliceLength {n : ℕ} (a : Real.Angle) (H : Fin n → PlanarHalfPlaneData) (P : Fin n → Bool) (R : ℝ) : Continuous (cellSliceLength a H P R)

def MovingSofa.Nef.closedCellSlice {n : ℕ} (a : Real.Angle) (H : Fin n → PlanarHalfPlaneData) (P : Fin n → Bool) (R x : ℝ) : Set ℝ

The closed Boolean cell’s slice at a fixed normal coordinate, truncated to [-R, R].

Equations

• MovingSofa.Nef.closedCellSlice a H P R x = {y : ℝ | MovingSofa.Nef.framePoint a x y ∈ MovingSofa.Nef.closedBooleanCell H P} ∩ Set.Icc (-R) R

def MovingSofa.Nef.parallelCellFeasible {n : ℕ} (a : Real.Angle) (H : Fin n → PlanarHalfPlaneData) (P : Fin n → Bool) (x : ℝ) : Prop

Every wall parallel to the slice is satisfied at the selected normal coordinate.

Equations

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

theorem MovingSofa.Nef.mem_closedCellSlice_iff {n : ℕ} (a : Real.Angle) (H : Fin n → PlanarHalfPlaneData) (P : Fin n → Bool) (R x y : ℝ) (hparallel : parallelCellFeasible a H P x) : y ∈ closedCellSlice a H P R x ↔ lowerEnvelope a H P R x ≤ y ∧ y ≤ upperEnvelope a H P R x

theorem MovingSofa.Nef.volume_closedCellSlice_toReal {n : ℕ} (a : Real.Angle) (H : Fin n → PlanarHalfPlaneData) (P : Fin n → Bool) (R x : ℝ) (hparallel : parallelCellFeasible a H P x) : (MeasureTheory.volume (closedCellSlice a H P R x)).toReal = cellSliceLength a H P R x

def MovingSofa.Nef.booleanCellSlice {n : ℕ} (a : Real.Angle) (H : Fin n → PlanarHalfPlaneData) (P : Fin n → Bool) (R x : ℝ) : Set ℝ

The actual Boolean membership cell’s slice, truncated to [-R, R].

Equations

• MovingSofa.Nef.booleanCellSlice a H P R x = {y : ℝ | MovingSofa.Nef.framePoint a x y ∈ MovingSofa.Nef.booleanCell (fun (j : Fin n) => (H j).carrier) P} ∩ Set.Icc (-R) R

def MovingSofa.Nef.noParallelBoundaryAt {n : ℕ} (a : Real.Angle) (H : Fin n → PlanarHalfPlaneData) (x : ℝ) : Prop

No wall parallel to the slice has its boundary at the selected normal coordinate.

Equations

• MovingSofa.Nef.noParallelBoundaryAt a H x = ∀ (j : Fin n), MovingSofa.Nef.frameTangentCoeff a (H j).angle = 0 → MovingSofa.Nef.frameNormalCoeff a (H j).angle * x ≠ (H j).height

def MovingSofa.Nef.cellSliceBoundaryExceptions {n : ℕ} (a : Real.Angle) (H : Fin n → PlanarHalfPlaneData) (x : ℝ) : Set ℝ

The tangent coordinates at which the slice meets a wall boundary.

Equations

• MovingSofa.Nef.cellSliceBoundaryExceptions a H x = ⋃ (j : Fin n), {y : ℝ | inner ℝ (MovingSofa.Nef.framePoint a x y) (MovingSofa.normalVector (H j).angle) = (H j).height}

theorem MovingSofa.Nef.finite_cellSliceBoundaryExceptions {n : ℕ} (a : Real.Angle) (H : Fin n → PlanarHalfPlaneData) (x : ℝ) (hx : noParallelBoundaryAt a H x) : (cellSliceBoundaryExceptions a H x).Finite

theorem MovingSofa.Nef.volume_booleanCellSlice_eq_closedCellSlice {n : ℕ} (a : Real.Angle) (H : Fin n → PlanarHalfPlaneData) (P : Fin n → Bool) (R x : ℝ) (hx : noParallelBoundaryAt a H x) : MeasureTheory.volume (booleanCellSlice a H P R x) = MeasureTheory.volume (closedCellSlice a H P R x)

theorem MovingSofa.Nef.volume_booleanCellSlice_toReal {n : ℕ} (a : Real.Angle) (H : Fin n → PlanarHalfPlaneData) (P : Fin n → Bool) (R x : ℝ) (hparallel : parallelCellFeasible a H P x) (hx : noParallelBoundaryAt a H x) : (MeasureTheory.volume (booleanCellSlice a H P R x)).toReal = cellSliceLength a H P R x

theorem MovingSofa.Nef.normalVector_eq_frameCombination (a b : Real.Angle) : normalVector b = frameNormalCoeff a b • normalVector a + frameTangentCoeff a b • tangentVector a

theorem MovingSofa.Nef.normalLine_eq_of_frameTangentCoeff_eq_zero {a b : Real.Angle} {h k : ℝ} (hb : frameTangentCoeff a b = 0) (hk : frameNormalCoeff a b * h = k) : normalLine b k = normalLine a h

@[simp]

theorem MovingSofa.Nef.frameNormalCoeff_self (a : Real.Angle) : frameNormalCoeff a a = 1

theorem MovingSofa.Nef.measurableSet_booleanCellSlice {n : ℕ} (a : Real.Angle) (H : Fin n → PlanarHalfPlaneData) (P : Fin n → Bool) (R x : ℝ) : MeasurableSet (booleanCellSlice a H P R x)

noncomputable def MovingSofa.Nef.actualCellSliceLength {n : ℕ} (a : Real.Angle) (H : Fin n → PlanarHalfPlaneData) (P : Fin n → Bool) (R x : ℝ) : ℝ

The envelope slice length when parallel walls are feasible, and zero otherwise.

Equations

• MovingSofa.Nef.actualCellSliceLength a H P R x = if MovingSofa.Nef.parallelCellFeasible a H P x then MovingSofa.Nef.cellSliceLength a H P R x else 0

theorem MovingSofa.Nef.closedCellSlice_eq_empty_of_not_parallelCellFeasible {n : ℕ} (a : Real.Angle) (H : Fin n → PlanarHalfPlaneData) (P : Fin n → Bool) (R x : ℝ) (hparallel : ¬parallelCellFeasible a H P x) : closedCellSlice a H P R x = ∅

theorem MovingSofa.Nef.volume_booleanCellSlice_toReal_eq_actual {n : ℕ} (a : Real.Angle) (H : Fin n → PlanarHalfPlaneData) (P : Fin n → Bool) (R x : ℝ) (_hx : noParallelBoundaryAt a H x) : (MeasureTheory.volume (booleanCellSlice a H P R x)).toReal = actualCellSliceLength a H P R x

def MovingSofa.Nef.frameCoordinates : Point ≃ᵐ ℝ × ℝ

The measurable equivalence between the Euclidean plane and a pair of real coordinates.

Equations

• MovingSofa.Nef.frameCoordinates = (MeasurableEquiv.toLp 2 (Fin 2 → ℝ)).symm.trans MeasurableEquiv.finTwoArrow

theorem MovingSofa.Nef.frameCoordinates_measurePreserving : MeasureTheory.MeasurePreserving (⇑frameCoordinates) MeasureTheory.volume (MeasureTheory.volume.prod MeasureTheory.volume)

theorem MovingSofa.Nef.framePoint_measurePreserving (a : Real.Angle) : MeasureTheory.MeasurePreserving (fun (p : ℝ × ℝ) => framePoint a p.1 p.2) (MeasureTheory.volume.prod MeasureTheory.volume) MeasureTheory.volume

theorem MovingSofa.Nef.volume_toReal_eq_integral_frameSlice (a : Real.Angle) {S : Set Point} (hS : MeasurableSet S) (hSfinite : MeasureTheory.volume S ≠ ⊤) : (MeasureTheory.volume S).toReal = ∫ (x : ℝ), (MeasureTheory.volume {y : ℝ | framePoint a x y ∈ S}).toReal

Polygon / Nef / Variation / Local Slices

def MovingSofa.Nef.auxiliaryHalfPlaneFamily {n : ℕ} (H : Fin n → PlanarHalfPlaneData) (i : Fin n) (M : ℝ) : Fin n → PlanarHalfPlaneData

Replace one wall by a closed upper-bound wall at auxiliary height M.

Equations

• MovingSofa.Nef.auxiliaryHalfPlaneFamily H i M = Function.update H i { angle := (H i).angle, height := M, upper := false, strict := false }

@[simp]

theorem MovingSofa.Nef.auxiliaryHalfPlaneFamily_self {n : ℕ} (H : Fin n → PlanarHalfPlaneData) (i : Fin n) (M : ℝ) : auxiliaryHalfPlaneFamily H i M i = { angle := (H i).angle, height := M, upper := false, strict := false }

theorem MovingSofa.Nef.auxiliaryHalfPlaneFamily_of_ne {n : ℕ} (H : Fin n → PlanarHalfPlaneData) (i j : Fin n) (M : ℝ) (hji : j ≠ i) : auxiliaryHalfPlaneFamily H i M j = H j

theorem MovingSofa.Nef.noParallelBoundaryAt_auxiliary {n : ℕ} (H : Fin n → PlanarHalfPlaneData) (i : Fin n) (hLines : Function.Injective fun (j : Fin n) => (H j).boundaryLine) (R ε₀ : ℝ) (hR : 0 < R) (hε₀ : 0 < ε₀) : noParallelBoundaryAt (H i).angle (auxiliaryHalfPlaneFamily H i (|(H i).height| + ε₀ + R + 1)) (H i).height

theorem MovingSofa.Nef.eventually_parallel_inequalities_iff {n : ℕ} (a : Real.Angle) (H : Fin n → PlanarHalfPlaneData) (h : ℝ) (hh : noParallelBoundaryAt a H h) : ∀ᶠ (x : ℝ) in nhds h, ∀ (j : Fin n), frameTangentCoeff a (H j).angle = 0 → (frameNormalCoeff a (H j).angle * x ≤ (H j).height ↔ frameNormalCoeff a (H j).angle * h ≤ (H j).height) ∧ ((H j).height ≤ frameNormalCoeff a (H j).angle * x ↔ (H j).height ≤ frameNormalCoeff a (H j).angle * h)

theorem MovingSofa.Nef.eventually_parallelCellFeasible_iff {n : ℕ} (a : Real.Angle) (H : Fin n → PlanarHalfPlaneData) (h : ℝ) (hh : noParallelBoundaryAt a H h) : ∀ᶠ (x : ℝ) in nhds h, ∀ (P : Fin n → Bool), parallelCellFeasible a H P x ↔ parallelCellFeasible a H P h

theorem MovingSofa.Nef.exists_parallel_stability_radius {n : ℕ} (a : Real.Angle) (H : Fin n → PlanarHalfPlaneData) (h : ℝ) (hh : noParallelBoundaryAt a H h) : ∃ ε > 0, ∀ (x : ℝ), |x - h| ≤ ε → noParallelBoundaryAt a H x ∧ ∀ (P : Fin n → Bool), parallelCellFeasible a H P x ↔ parallelCellFeasible a H P h

theorem MovingSofa.Nef.setMembershipPattern_auxiliary {n : ℕ} (H : Fin n → PlanarHalfPlaneData) (i : Fin n) (M : ℝ) (p : Point) (hp : p ∈ (auxiliaryHalfPlaneFamily H i M i).carrier) : setMembershipPattern (fun (j : Fin n) => (auxiliaryHalfPlaneFamily H i M j).carrier) p = Function.update (setMembershipPattern (fun (j : Fin n) => (H j).carrier) p) i true

theorem MovingSofa.Nef.mem_activeBooleanRegion_iff_mem_booleanCell_auxiliary {n : ℕ} (E : BooleanFunction n) (H : Fin n → PlanarHalfPlaneData) (i : Fin n) (M : ℝ) (p : Point) (hp : p ∈ (auxiliaryHalfPlaneFamily H i M i).carrier) : p ∈ activeBooleanRegion E H i ↔ ∃ P ∈ activeBooleanPatterns E i, p ∈ booleanCell (fun (j : Fin n) => (auxiliaryHalfPlaneFamily H i M j).carrier) P

def MovingSofa.Nef.activeRegionSlice {n : ℕ} (a : Real.Angle) (E : BooleanFunction n) (H : Fin n → PlanarHalfPlaneData) (i : Fin n) (R x : ℝ) : Set ℝ

The slice of the region where the selected Boolean wall is active, truncated to [-R, R].

Equations

• MovingSofa.Nef.activeRegionSlice a E H i R x = {y : ℝ | MovingSofa.Nef.framePoint a x y ∈ MovingSofa.Nef.activeBooleanRegion E H i} ∩ Set.Icc (-R) R

theorem MovingSofa.Nef.frameSlice_perturbSdiff_eq {n : ℕ} {E : BooleanFunction n} (hE : IsMonotoneBooleanFunction E) (H : Fin n → PlanarHalfPlaneData) (i : Fin n) (hSide : (H i).upper = false) (R ε₀ δ ε x : ℝ) (hδ : |δ| ≤ ε₀) (hBound : ∀ (z : ℝ), |z| ≤ ε₀ → perturbNefHeight E H i z ⊆ Metric.closedBall 0 R) : (x ∈ heightInterval (H i).strict (H i).height δ ε → {y : ℝ | framePoint (H i).angle x y ∈ perturbNefHeight E H i δ \ perturbNefHeight E H i ε} = activeRegionSlice (H i).angle E H i R x) ∧ (x ∉ heightInterval (H i).strict (H i).height δ ε → {y : ℝ | framePoint (H i).angle x y ∈ perturbNefHeight E H i δ \ perturbNefHeight E H i ε} = ∅)

theorem MovingSofa.Nef.activeRegionSlice_eq_biUnion_booleanCellSlice_auxiliary {n : ℕ} (E : BooleanFunction n) (H : Fin n → PlanarHalfPlaneData) (i : Fin n) (M R x : ℝ) (hxM : x ≤ M) : activeRegionSlice (H i).angle E H i R x = ⋃ P ∈ activeBooleanPatterns E i, booleanCellSlice (H i).angle (auxiliaryHalfPlaneFamily H i M) P R x

theorem MovingSofa.Nef.measure_activeRegionSlice_eq_sum {n : ℕ} (E : BooleanFunction n) (H : Fin n → PlanarHalfPlaneData) (i : Fin n) (M R x : ℝ) (hxM : x ≤ M) : MeasureTheory.volume (activeRegionSlice (H i).angle E H i R x) = ∑ P ∈ activeBooleanPatterns E i, MeasureTheory.volume (booleanCellSlice (H i).angle (auxiliaryHalfPlaneFamily H i M) P R x)

noncomputable def MovingSofa.Nef.activeSliceLength {n : ℕ} (a : Real.Angle) (E : BooleanFunction n) (H : Fin n → PlanarHalfPlaneData) (i : Fin n) (R x : ℝ) : ℝ

Sum the feasible slice lengths over patterns where the selected wall is active.

Equations

• MovingSofa.Nef.activeSliceLength a E H i R x = ∑ P ∈ MovingSofa.Nef.activeBooleanPatterns E i, MovingSofa.Nef.actualCellSliceLength a H P R x

noncomputable def MovingSofa.Nef.frozenActiveSliceLength {n : ℕ} (a : Real.Angle) (E : BooleanFunction n) (H : Fin n → PlanarHalfPlaneData) (i : Fin n) (R h x : ℝ) : ℝ

Sum slice lengths while freezing all parallel-wall feasibility decisions at the reference height.

Equations

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

theorem MovingSofa.Nef.continuous_frozenActiveSliceLength {n : ℕ} (a : Real.Angle) (E : BooleanFunction n) (H : Fin n → PlanarHalfPlaneData) (i : Fin n) (R h : ℝ) : Continuous (frozenActiveSliceLength a E H i R h)

theorem MovingSofa.Nef.activeSliceLength_eq_frozen_of_stable {n : ℕ} (a : Real.Angle) (E : BooleanFunction n) (H : Fin n → PlanarHalfPlaneData) (i : Fin n) (R h x : ℝ) (hstable : ∀ (P : Fin n → Bool), parallelCellFeasible a H P x ↔ parallelCellFeasible a H P h) : activeSliceLength a E H i R x = frozenActiveSliceLength a E H i R h x

theorem MovingSofa.Nef.abs_frozenActiveSliceLength_sub_le {n : ℕ} (a : Real.Angle) (E : BooleanFunction n) (H : Fin n → PlanarHalfPlaneData) (i : Fin n) (R h x z : ℝ) : |frozenActiveSliceLength a E H i R h x - frozenActiveSliceLength a E H i R h z| ≤ ↑(activeBooleanPatterns E i).card * (2 * slopeBound a H) * |x - z|

theorem MovingSofa.Nef.volume_activeRegionSlice_toReal_eq_activeSliceLength {n : ℕ} (E : BooleanFunction n) (H : Fin n → PlanarHalfPlaneData) (i : Fin n) (M R x : ℝ) (hxM : x ≤ M) (hx : noParallelBoundaryAt (H i).angle (auxiliaryHalfPlaneFamily H i M) x) : (MeasureTheory.volume (activeRegionSlice (H i).angle E H i R x)).toReal = activeSliceLength (H i).angle E (auxiliaryHalfPlaneFamily H i M) i R x

Polygon / Nef / Variation / Area

theorem MovingSofa.Nef.volume_perturbSdiff_toReal_eq_integral_slice {n : ℕ} {E : BooleanFunction n} (hE : IsMonotoneBooleanFunction E) (H : Fin n → PlanarHalfPlaneData) (i : Fin n) (hSide : (H i).upper = false) (R ε₀ δ ε : ℝ) (hδ : |δ| ≤ ε₀) (hBound : ∀ (z : ℝ), |z| ≤ ε₀ → perturbNefHeight E H i z ⊆ Metric.closedBall 0 R) : (MeasureTheory.volume (perturbNefHeight E H i δ \ perturbNefHeight E H i ε)).toReal = ∫ (x : ℝ) in heightInterval (H i).strict (H i).height δ ε, (MeasureTheory.volume (activeRegionSlice (H i).angle E H i R x)).toReal

theorem MovingSofa.Nef.area_perturb_sub_eq_integral_activeSliceLength {n : ℕ} {E : BooleanFunction n} (hE : IsMonotoneBooleanFunction E) (H : Fin n → PlanarHalfPlaneData) (i : Fin n) (hSide : (H i).upper = false) (R ε₀ M δ ε : ℝ) (hεδ : ε ≤ δ) (hδ : |δ| ≤ ε₀) (hε : |ε| ≤ ε₀) (hBound : ∀ (z : ℝ), |z| ≤ ε₀ → perturbNefHeight E H i z ⊆ Metric.closedBall 0 R) (hxM : ∀ x ∈ heightInterval (H i).strict (H i).height δ ε, x ≤ M) (hxregular : ∀ x ∈ heightInterval (H i).strict (H i).height δ ε, noParallelBoundaryAt (H i).angle (auxiliaryHalfPlaneFamily H i M) x) : ClassicalResults.area (perturbNefHeight E H i δ) - ClassicalResults.area (perturbNefHeight E H i ε) = ∫ (x : ℝ) in heightInterval (H i).strict (H i).height δ ε, activeSliceLength (H i).angle E (auxiliaryHalfPlaneFamily H i M) i R x

theorem MovingSofa.Nef.area_perturb_sub_eq_intervalIntegral_activeSliceLength {n : ℕ} {E : BooleanFunction n} (hE : IsMonotoneBooleanFunction E) (H : Fin n → PlanarHalfPlaneData) (i : Fin n) (hSide : (H i).upper = false) (R ε₀ M ρ : ℝ) (hε₀ : 0 < ε₀) (hρ : 0 < ρ) (hM : (H i).height + ε₀ ≤ M) (hBound : ∀ (z : ℝ), |z| ≤ ε₀ → perturbNefHeight E H i z ⊆ Metric.closedBall 0 R) (hregular : ∀ (x : ℝ), |x - (H i).height| ≤ ρ → noParallelBoundaryAt (H i).angle (auxiliaryHalfPlaneFamily H i M) x) (δ : ℝ) : |δ| ≤ min ε₀ ρ → ClassicalResults.area (perturbNefHeight E H i δ) - ClassicalResults.area (perturbNefHeight E H i 0) = ∫ (x : ℝ) in (H i).height..(H i).height + δ, activeSliceLength (H i).angle E (auxiliaryHalfPlaneFamily H i M) i R x

theorem MovingSofa.Nef.area_perturb_remainder_le {n : ℕ} {E : BooleanFunction n} (hE : IsMonotoneBooleanFunction E) (H : Fin n → PlanarHalfPlaneData) (i : Fin n) (hSide : (H i).upper = false) (R ε₀ M ρ : ℝ) (hε₀ : 0 < ε₀) (hρ : 0 < ρ) (hM : (H i).height + ε₀ ≤ M) (hBound : ∀ (z : ℝ), |z| ≤ ε₀ → perturbNefHeight E H i z ⊆ Metric.closedBall 0 R) (hstable : ∀ (x : ℝ), |x - (H i).height| ≤ ρ → noParallelBoundaryAt (H i).angle (auxiliaryHalfPlaneFamily H i M) x ∧ ∀ (P : Fin n → Bool), parallelCellFeasible (H i).angle (auxiliaryHalfPlaneFamily H i M) P x ↔ parallelCellFeasible (H i).angle (auxiliaryHalfPlaneFamily H i M) P (H i).height) (δ : ℝ) : |δ| ≤ min ε₀ ρ → |ClassicalResults.area (perturbNefHeight E H i δ) - ClassicalResults.area (perturbNefHeight E H i 0) - activeSliceLength (H i).angle E (auxiliaryHalfPlaneFamily H i M) i R (H i).height * δ| ≤ ↑(activeBooleanPatterns E i).card * (2 * slopeBound (H i).angle (auxiliaryHalfPlaneFamily H i M)) * δ ^ 2

Polygon / Nef / Variation / Boundary

theorem MovingSofa.Nef.tendsto_sub_one_div_normalVector (p : Point) (a : Real.Angle) : Filter.Tendsto (fun (k : ℕ) => p - (1 / ↑(k + 1)) • normalVector a) Filter.atTop (nhds p)

theorem MovingSofa.Nef.tendsto_add_one_div_normalVector (p : Point) (a : Real.Angle) : Filter.Tendsto (fun (k : ℕ) => p + (1 / ↑(k + 1)) • normalVector a) Filter.atTop (nhds p)

theorem MovingSofa.Nef.sub_smul_normalVector_mem_carrier (H : PlanarHalfPlaneData) (hupper : H.upper = false) {p : Point} (hp : p ∈ H.boundaryLine) {t : ℝ} (ht : 0 < t) : p - t • normalVector H.angle ∈ H.carrier

theorem MovingSofa.Nef.add_smul_normalVector_not_mem_carrier (H : PlanarHalfPlaneData) (hupper : H.upper = false) {p : Point} (hp : p ∈ H.boundaryLine) {t : ℝ} (ht : 0 < t) : p + t • normalVector H.angle ∉ H.carrier

theorem MovingSofa.Nef.mem_frontier_booleanSet_of_active {n : ℕ} (E : BooleanFunction n) (H : Fin n → PlanarHalfPlaneData) (i : Fin n) (hupper : (H i).upper = false) (p : Point) (hline : p ∈ (H i).boundaryLine) (hother : ∀ (j : Fin n), j ≠ i → p ∉ (H j).boundaryLine) (hactive : IsActiveBooleanPattern E i (setMembershipPattern (fun (j : Fin n) => (H j).carrier) p)) : p ∈ frontier (booleanSet E fun (j : Fin n) => (H j).carrier)

theorem MovingSofa.Nef.not_mem_frontier_booleanSet_of_not_active {n : ℕ} {E : BooleanFunction n} (hE : IsMonotoneBooleanFunction E) (H : Fin n → PlanarHalfPlaneData) (i : Fin n) (p : Point) (hother : ∀ (j : Fin n), j ≠ i → p ∉ (H j).boundaryLine) (hinactive : ¬IsActiveBooleanPattern E i (setMembershipPattern (fun (j : Fin n) => (H j).carrier) p)) : p ∉ frontier (booleanSet E fun (j : Fin n) => (H j).carrier)

theorem MovingSofa.Nef.mem_frontier_booleanSet_iff_mem_activeBooleanRegion {n : ℕ} {E : BooleanFunction n} (hE : IsMonotoneBooleanFunction E) (H : Fin n → PlanarHalfPlaneData) (i : Fin n) (hupper : (H i).upper = false) (p : Point) (hline : p ∈ (H i).boundaryLine) (hother : ∀ (j : Fin n), j ≠ i → p ∉ (H j).boundaryLine) : p ∈ frontier (booleanSet E fun (j : Fin n) => (H j).carrier) ↔ p ∈ activeBooleanRegion E H i

def MovingSofa.Nef.frontierLineSlice {n : ℕ} (E : BooleanFunction n) (H : Fin n → PlanarHalfPlaneData) (i : Fin n) (R : ℝ) : Set ℝ

The truncated slice of the Boolean set’s frontier along a selected wall boundary.

Equations

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

theorem MovingSofa.Nef.volume_frontierLineSlice_eq_activeRegionSlice {n : ℕ} {E : BooleanFunction n} (hE : IsMonotoneBooleanFunction E) (H : Fin n → PlanarHalfPlaneData) (i : Fin n) (hupper : (H i).upper = false) (M R : ℝ) (hno : noParallelBoundaryAt (H i).angle (auxiliaryHalfPlaneFamily H i M) (H i).height) : MeasureTheory.volume (frontierLineSlice E H i R) = MeasureTheory.volume (activeRegionSlice (H i).angle E H i R (H i).height)

theorem MovingSofa.Nef.lineMap_framePoint (a : Real.Angle) (h y : ℝ) : (AffineMap.lineMap (framePoint a h 0) (framePoint a h 1)) y = framePoint a h y

theorem MovingSofa.Nef.dist_framePoint_zero_one (a : Real.Angle) (h : ℝ) : dist (framePoint a h 0) (framePoint a h 1) = 1

theorem MovingSofa.Nef.frontier_booleanSet_inter_boundaryLine_eq_image_frontierLineSlice {n : ℕ} (E : BooleanFunction n) (H : Fin n → PlanarHalfPlaneData) (i : Fin n) (R : ℝ) (hBound : (booleanSet E fun (j : Fin n) => (H j).carrier) ⊆ Metric.closedBall 0 R) : frontier (booleanSet E fun (j : Fin n) => (H j).carrier) ∩ (H i).boundaryLine = ⇑(AffineMap.lineMap (framePoint (H i).angle (H i).height 0) (framePoint (H i).angle (H i).height 1)) '' frontierLineSlice E H i R

theorem MovingSofa.Nef.hausdorffMeasure_frontier_inter_boundaryLine_eq_volume_slice {n : ℕ} (E : BooleanFunction n) (H : Fin n → PlanarHalfPlaneData) (i : Fin n) (R : ℝ) (hBound : (booleanSet E fun (j : Fin n) => (H j).carrier) ⊆ Metric.closedBall 0 R) : (MeasureTheory.Measure.hausdorffMeasure 1) (frontier (booleanSet E fun (j : Fin n) => (H j).carrier) ∩ (H i).boundaryLine) = MeasureTheory.volume (frontierLineSlice E H i R)

theorem MovingSofa.Nef.hausdorffMeasure_frontier_toReal_eq_activeSliceLength {n : ℕ} {E : BooleanFunction n} (hE : IsMonotoneBooleanFunction E) (H : Fin n → PlanarHalfPlaneData) (i : Fin n) (hupper : (H i).upper = false) (M R : ℝ) (hM : (H i).height ≤ M) (hBound : (booleanSet E fun (j : Fin n) => (H j).carrier) ⊆ Metric.closedBall 0 R) (hno : noParallelBoundaryAt (H i).angle (auxiliaryHalfPlaneFamily H i M) (H i).height) : ((MeasureTheory.Measure.hausdorffMeasure 1) (frontier (booleanSet E fun (j : Fin n) => (H j).carrier) ∩ (H i).boundaryLine)).toReal = activeSliceLength (H i).angle E (auxiliaryHalfPlaneFamily H i M) i R (H i).height

Polygon / Nef / Variation

theorem MovingSofa.simpleNefPolygon_area_variation {n : ℕ} (E : BooleanFunction n) (H : Fin n → PlanarHalfPlaneData) (i : Fin n) (hE : IsMonotoneBooleanFunction E) (hLines : Function.Injective fun (j : Fin n) => (H j).boundaryLine) (hSide : (H i).upper = false) (R ε₀ : ℝ) (hR : 0 < R) (hε₀ : 0 < ε₀) (hBound : ∀ (δ : ℝ), |δ| ≤ ε₀ → perturbNefHeight E H i δ ⊆ Metric.closedBall 0 R) : ∃ (C : ℝ) (ε : ℝ), 0 ≤ C ∧ 0 < ε ∧ ε ≤ ε₀ ∧ ∀ (δ : ℝ), |δ| ≤ ε → |ClassicalResults.area (perturbNefHeight E H i δ) - ClassicalResults.area (perturbNefHeight E H i 0) - ((MeasureTheory.Measure.hausdorffMeasure 1) (frontier (perturbNefHeight E H i 0) ∩ (H i).boundaryLine)).toReal * δ| ≤ C * δ ^ 2

Polygon / Nef / Signed Variation

theorem MovingSofa.simpleNefPolygon_area_variation_lower {n : ℕ} (E : BooleanFunction n) (H : Fin n → PlanarHalfPlaneData) (i : Fin n) (hE : IsMonotoneBooleanFunction E) (hLines : Function.Injective fun (j : Fin n) => (H j).boundaryLine) (hSide : (H i).upper = true) (R ε₀ : ℝ) (hR : 0 < R) (hε₀ : 0 < ε₀) (hBound : ∀ (δ : ℝ), |δ| ≤ ε₀ → perturbNefHeight E H i δ ⊆ Metric.closedBall 0 R) : ∃ (C : ℝ) (ε : ℝ), 0 ≤ C ∧ 0 < ε ∧ ε ≤ ε₀ ∧ ∀ (δ : ℝ), |δ| ≤ ε → |ClassicalResults.area (perturbNefHeight E H i δ) - ClassicalResults.area (perturbNefHeight E H i 0) + ((MeasureTheory.Measure.hausdorffMeasure 1) (frontier (perturbNefHeight E H i 0) ∩ (H i).boundaryLine)).toReal * δ| ≤ C * δ ^ 2

Quadratic area variation when the moved half-plane is a lower constraint.

theorem MovingSofa.simpleNefPolygon_area_variation_signed {n : ℕ} (E : BooleanFunction n) (H : Fin n → PlanarHalfPlaneData) (i : Fin n) (hE : IsMonotoneBooleanFunction E) (hLines : Function.Injective fun (j : Fin n) => (H j).boundaryLine) (R ε₀ : ℝ) (hR : 0 < R) (hε₀ : 0 < ε₀) (hBound : ∀ (δ : ℝ), |δ| ≤ ε₀ → perturbNefHeight E H i δ ⊆ Metric.closedBall 0 R) : ∃ (C : ℝ) (ε : ℝ), 0 ≤ C ∧ 0 < ε ∧ ε ≤ ε₀ ∧ ∀ (δ : ℝ), |δ| ≤ ε → |ClassicalResults.area (perturbNefHeight E H i δ) - ClassicalResults.area (perturbNefHeight E H i 0) - (if (H i).upper = true then -1 else 1) * ((MeasureTheory.Measure.hausdorffMeasure 1) (frontier (perturbNefHeight E H i 0) ∩ (H i).boundaryLine)).toReal * δ| ≤ C * δ ^ 2

Signed quadratic area variation for either orientation of a simple Nef wall.

Polygon / Height / Wall Variation

theorem MovingSofa.angleDomain_coe_injective (Θ : AngleSet) : Function.Injective fun (t : ↑(angleDomain Θ)) => ↑↑t

Angles in a polygon angle domain have distinct classes modulo a full turn.

theorem MovingSofa.independentWallNiche_sub_one {Θ : AngleSet} (h : PolygonHeightSpace Θ) : (independentWallNiche fun (s : ↑(angleDomain Θ)) => h s - 1) = polygonHeightNiche h

The niche with every lower wall shifted by one is the height-defined niche.

theorem MovingSofa.polygonNiche_wall_area_variation {Θ : AngleSet} (h : PolygonHeightSpace Θ) {n : ℕ} (H : Fin n → PlanarHalfPlaneData) (hH : Set.range H = polygonNicheWalls h) (hLines : Function.Injective fun (j : Fin n) => (H j).boundaryLine) (i : Fin n) : ∃ (t : ↑(angleDomain Θ)) (C : ℝ) (η : ℝ), (H i).angle = ↑↑t ∧ 0 ≤ C ∧ 0 < η ∧ ∀ (δ : ℝ), |δ| ≤ η → |ClassicalResults.area (independentWallNiche (Function.update (fun (s : ↑(angleDomain Θ)) => h s - 1) t (h t - 1 + δ))) - ClassicalResults.area (polygonHeightNiche h) - (if (H i).upper = true then -1 else 1) * ((MeasureTheory.Measure.hausdorffMeasure 1) (frontier (polygonHeightNiche h) ∩ (H i).boundaryLine)).toReal * δ| ≤ C * δ ^ 2

Quadratic area variation for any wall in a polygon-height niche presentation.

theorem MovingSofa.independentWallCap_sub_one {Θ : AngleSet} (h : PolygonHeightSpace Θ) : (independentWallCap h fun (s : ↑(angleDomain Θ)) => h s - 1) = polygonHeightCap h

The cap with every lower endpoint wall shifted by one is the height-defined cap.

theorem MovingSofa.polygonCap_upper_wall_area_variation {Θ : AngleSet} (h : PolygonHeightSpace Θ) {n : ℕ} (H : Fin n → PlanarHalfPlaneData) (hH : Set.range H = polygonCapWalls h) (hLines : Function.Injective fun (j : Fin n) => (H j).boundaryLine) (i : Fin n) (t : ↑(angleDomain Θ)) (hi : H i = { angle := ↑↑t, height := h t, upper := false, strict := false }) : ∃ (C : ℝ) (η : ℝ), 0 ≤ C ∧ 0 < η ∧ ∀ (δ : ℝ), |δ| ≤ η → |ClassicalResults.area (independentWallCap (Function.update h t (h t + δ)) fun (s : ↑(angleDomain Θ)) => h s - 1) - ClassicalResults.area (polygonHeightCap h) - ((MeasureTheory.Measure.hausdorffMeasure 1) (frontier (polygonHeightCap h) ∩ (H i).boundaryLine)).toReal * δ| ≤ C * δ ^ 2

Quadratic area variation for one upper wall of a polygon-height cap.

theorem MovingSofa.polygonCap_lower_wall_area_variation {Θ : AngleSet} (h : PolygonHeightSpace Θ) {n : ℕ} (H : Fin n → PlanarHalfPlaneData) (hH : Set.range H = polygonCapWalls h) (hLines : Function.Injective fun (j : Fin n) => (H j).boundaryLine) (i : Fin n) (t : ↑(angleDomain Θ)) (hi : H i = { angle := ↑↑t, height := h t - 1, upper := true, strict := false }) : ∃ (C : ℝ) (η : ℝ), 0 ≤ C ∧ 0 < η ∧ ∀ (δ : ℝ), |δ| ≤ η → |ClassicalResults.area (independentWallCap h (Function.update (fun (s : ↑(angleDomain Θ)) => h s - 1) t (h t - 1 + δ))) - ClassicalResults.area (polygonHeightCap h) + ((MeasureTheory.Measure.hausdorffMeasure 1) (frontier (polygonHeightCap h) ∩ (H i).boundaryLine)).toReal * δ| ≤ C * δ ^ 2

Quadratic area variation for one lower endpoint wall of a polygon-height cap.

theorem MovingSofa.independentWallCap_area_update_add {Θ : AngleSet} (h : PolygonHeightSpace Θ) (t : ↑(angleDomain Θ)) (ε R : ℝ) (hε : 0 ≤ ε) (hε' : ε ≤ 1) (hbound : ∀ (upper lower : PolygonHeightSpace Θ), upper = h ∨ upper = Function.update h t (h t + ε) → (lower = fun (s : ↑(angleDomain Θ)) => h s - 1) ∨ lower = Function.update (fun (s : ↑(angleDomain Θ)) => h s - 1) t (h t - 1 + ε) → independentWallCap upper lower ⊆ Metric.closedBall 0 R) : ClassicalResults.area (independentWallCap (Function.update h t (h t + ε)) (Function.update (fun (s : ↑(angleDomain Θ)) => h s - 1) t (h t - 1 + ε))) + ClassicalResults.area (independentWallCap h fun (s : ↑(angleDomain Θ)) => h s - 1) = ClassicalResults.area (independentWallCap (Function.update h t (h t + ε)) fun (s : ↑(angleDomain Θ)) => h s - 1) + ClassicalResults.area (independentWallCap h (Function.update (fun (s : ↑(angleDomain Θ)) => h s - 1) t (h t - 1 + ε)))

Simultaneous endpoint-wall variation is the sum of the two independent variations.

Polygon / Right Angle Grid

theorem MovingSofa.mem_rightAngleSet_directions_iff (n : ℕ) (hn : 2 ≤ n) (t : ℝ) : t ∈ (rightAngleSet n hn).directions ↔ ∃ i ∈ Finset.Ioo 0 n, t = ↑i * polygonStepSize n

Directions in the right-angle grid are positive integer multiples of its step size.

theorem MovingSofa.rightAngleSet_direction_le_pred_or_ge (n : ℕ) (hn : 2 ≤ n) {r t : ℝ} (hr : r ∈ (rightAngleSet n hn).directions) (ht : t ∈ (rightAngleSet n hn).directions) : r ≤ t - polygonStepSize n ∨ t ≤ r

No grid direction lies strictly between the predecessor of a grid point and the point.

theorem MovingSofa.rightAngleSet_direction_le_or_succ_le (n : ℕ) (hn : 2 ≤ n) {r t : ℝ} (hr : r ∈ (rightAngleSet n hn).directions) (ht : t ∈ (rightAngleSet n hn).directions) : r ≤ t ∨ t + polygonStepSize n ≤ r

No grid direction lies strictly between a grid point and its successor.

theorem MovingSofa.rightAngleSet_direction_bounds (n : ℕ) (hn : 2 ≤ n) {t : ℝ} (ht : t ∈ (rightAngleSet n hn).directions) : polygonStepSize n ≤ t ∧ t ≤ Real.pi / 2 - polygonStepSize n

Every interior grid direction stays at least one step from both endpoints.

theorem MovingSofa.rightAngle_polygon_normals_eq (n : ℕ) (hn : 2 ≤ n) : (fun (r : ℝ) => ↑r) '' angleDomain (rightAngleSet n hn) ∪ capLowerNormals (rightAngleSet n hn).angle = (fun (r : ℝ) => ↑r) '' (angleDomain (rightAngleSet n hn) ∪ {3 * Real.pi / 2})

The two lower normals of a right-angle polygon cap coincide at 3π/2.

theorem MovingSofa.rightAngleSet_sub_step (n : ℕ) (hn : 2 ≤ n) {t : ℝ} (ht : t ∈ (rightAngleSet n hn).directions) : t - polygonStepSize n = 0 ∨ t - polygonStepSize n ∈ (rightAngleSet n hn).directions

The predecessor of a right-angle grid direction is zero or again a grid direction.

theorem MovingSofa.rightAngleSet_add_step (n : ℕ) (hn : 2 ≤ n) {t : ℝ} (ht : t ∈ (rightAngleSet n hn).directions) : t + polygonStepSize n = Real.pi / 2 ∨ t + polygonStepSize n ∈ (rightAngleSet n hn).directions

The successor of a right-angle grid direction is the terminal angle or a grid direction.

Polygon / Translation

theorem MovingSofa.polygonCapTranslate_iff (Θ : AngleSet) (K : ConvexBody Point) : (∃ (K' : PolygonCapTranslateSpace Θ), ↑K' = ↑K) ↔ supportValue ↑K ↑Θ.angle + supportValue ↑K ↑(Θ.angle + Real.pi) = 1 ∧ supportValue ↑K ↑(Real.pi / 2) + supportValue ↑K ↑(3 * Real.pi / 2) = 1 ∧ ∃ (constraints : Set (Real.Angle × ℝ)), constraints.Finite ∧ (∀ c ∈ constraints, c.1 ∈ (fun (t : ℝ) => ↑t) '' angleDomain Θ ∪ capLowerNormals Θ.angle) ∧ ↑K = ⋂ c ∈ constraints, normalHalfPlane c.1 c.2 false false

theorem MovingSofa.polygonHeightArea_le_translateArea {Θ : AngleSet} (h : PolygonHeightSpace Θ) (K : PolygonCapTranslateSpace Θ) (hK : polygonHeightCap h = ↑K) : polygonHeightArea h ≤ (polygonTranslateExtensions K).2

Polygon / Height / Reconstruction

theorem MovingSofa.exists_polygonCapTranslate_eq_polygonHeightCap {Θ : AngleSet} (h : PolygonHeightSpace Θ) (hbounded : Bornology.IsBounded (polygonHeightCap h)) (hupper : ∀ t ∈ {Θ.angle, Real.pi / 2}, ∃ p ∈ polygonHeightCap h, inner ℝ p (normalVector ↑t) = polygonHeightValue h t) (hlower : ∀ t ∈ {Θ.angle, Real.pi / 2}, ∃ p ∈ polygonHeightCap h, inner ℝ p (normalVector ↑t) = polygonHeightValue h t - 1) : ∃ (K' : PolygonCapTranslateSpace Θ), ↑K' = polygonHeightCap h

Attainment of both endpoint strip bounds reconstructs a translated polygon cap.

Polygon / Height / Positive Increment / Contacts

theorem MovingSofa.polygonCap_positive_height_increment_of_not_endpoint {Θ : AngleSet} (K : PolygonCapSpace Θ) (t : ↑(angleDomain Θ)) (ht : ↑t ∉ {Θ.angle, Real.pi / 2}) : ∃ (ε₀ : ℝ), 0 < ε₀ ∧ ∀ (ε : ℝ), 0 < ε → ε < ε₀ → ∃ (K' : PolygonCapTranslateSpace Θ), ↑K' = polygonHeightCap (raisedPolygonSupport K t ε)

A sufficiently small interior height increase yields a translated polygon cap.

theorem MovingSofa.polygonCap_positive_height_increment_of_endpoint {Θ : AngleSet} (K : PolygonCapSpace Θ) (t : ↑(angleDomain Θ)) (ht : ↑t ∈ {Θ.angle, Real.pi / 2}) (hmass : 0 < (surfaceAreaMeasure ↑↑K) {↑↑t}) : ∃ (ε₀ : ℝ), 0 < ε₀ ∧ ∀ (ε : ℝ), 0 < ε → ε < ε₀ → ∃ (K' : PolygonCapTranslateSpace Θ), ↑K' = polygonHeightCap (raisedPolygonSupport K t ε)

A sufficiently small endpoint height increase preserves both unit widths.

Polygon / Height / Positive Increment

theorem MovingSofa.polygonCap_positive_height_increment {Θ : AngleSet} (K : PolygonCapSpace Θ) (t : ↑(angleDomain Θ)) (ht : 0 < (surfaceAreaMeasure ↑↑K) {↑↑t}) : ∃ (ε₀ : ℝ), 0 < ε₀ ∧ ∀ (ε : ℝ), 0 < ε → ε < ε₀ → ∃ (K' : PolygonCapTranslateSpace Θ), ↑K' = polygonHeightCap (raisedPolygonSupport K t ε)

Moving sofa: related mathematical developments

• Bounds.LegComputation.
• Bounds.Lower.Profile.
• Bounds.NicheLimits.

Bounds / Leg Computation

theorem MovingSofa.maximumPolygonCap_leg_lengths (n : ℕ) (hn : 2 ≤ n) (K : PolygonCapSpace (rightAngleSet n hn)) (t : ℝ) (ht : t ∈ (rightAngleSet n hn).directions) : (MeasureTheory.Measure.hausdorffMeasure 1) ((rotatingHallwayParts ↑↑↑K ↑t).bRay ∩ (innerWallUpperHalfPlanes (↑K) (t - polygonStepSize n)).2) = ENNReal.ofReal (Real.tan (polygonStepSize n) * max 0 ((tangentArmLengths (↑K) t).2.2 - 1 + Real.tan (polygonStepSize n / 2))) ∧ (MeasureTheory.Measure.hausdorffMeasure 1) ((rotatingHallwayParts ↑↑↑K ↑t).bRay ∩ (innerWallUpperHalfPlanes (↑K) (t + polygonStepSize n)).2) = ENNReal.ofReal (Real.tan (polygonStepSize n) * max 0 (1 - (tangentArmLengths (↑K) t).2.1 + Real.tan (polygonStepSize n / 2)))

theorem MovingSofa.hausdorffMeasure_faceLine_inter_innerWalls_le (K : ConvexBody Point) (t δ : ℝ) (hδ0 : 0 < δ) (hδ : δ < Real.pi) : (MeasureTheory.Measure.hausdorffMeasure 1) ({p : Point | inner ℝ p (normalVector ↑t) = supportValue ↑K ↑t - 1} ∩ (normalHalfPlane (↑(t - δ)) (supportValue ↑K ↑(t - δ) - 1) true false ∩ normalHalfPlane (↑(t + δ)) (supportValue ↑K ↑(t + δ) - 1) true false)) ≤ ENNReal.ofReal (max 0 (2 * Real.tan (δ / 2) - ((surfaceAreaMeasure K) {↑t}).toReal))

The face line of a convex body meets the two adjacent inner-wall half-planes in a set whose length is at most 2 tan(δ/2) less the face length.

Bounds / Lower / Profile

noncomputable def MovingSofa.armIntegralOperator (f : C(↑(Set.Icc 0 (Real.pi / 2)), NNReal)) : C(↑(Set.Icc 0 (Real.pi / 2)), ℝ)

Integrate the reflected arm profile through the second magic function and add one.

Equations

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

def MovingSofa.armLowerBoundSequence : ℕ → C(↑(Set.Icc 0 (Real.pi / 2)), NNReal)

Iteratively improve the nonnegative arm lower bound by taking the maximum with its integral update.

Equations

• One or more equations did not get rendered due to their size.
• MovingSofa.armLowerBoundSequence 0 = { toFun := fun (x : ↑(Set.Icc 0 (Real.pi / 2))) => 0, continuous_toFun := MovingSofa.armLowerBoundSequence._proof_1 }

def MovingSofa.lowerBoundProfile (c : ↑(Set.Icc 0 1)) : C(↑(Set.Icc 0 (Real.pi / 2)), ℝ)

The continuous profile max (1 - x) c on the quarter-turn interval.

Equations

• MovingSofa.lowerBoundProfile c = { toFun := fun (x : ↑(Set.Icc 0 (Real.pi / 2))) => max (1 - ↑x) ↑c, continuous_toFun := ⋯ }

Bounds / Niche Limits

theorem MovingSofa.tendsto_supportValue_of_hausdorff {ω : ℝ} (K : ℕ → CapSpace ω) (L : CapSpace ω) (hlim : Filter.Tendsto (fun (i : ℕ) => Metric.hausdorffDist ↑↑(K i) ↑↑L) Filter.atTop (nhds 0)) (t : ℝ) : Filter.Tendsto (fun (i : ℕ) => supportValue ↑↑(K i) ↑t) Filter.atTop (nhds (supportValue ↑↑L ↑t))

Support values converge under Hausdorff convergence of caps.

theorem MovingSofa.polygonArea_continuity (Θ : AngleSet) (K : ℕ → CapSpace Θ.angle) (L : CapSpace Θ.angle) (hlim : Filter.Tendsto (fun (i : ℕ) => Metric.hausdorffDist ↑↑(K i) ↑↑L) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (i : ℕ) => ClassicalResults.area (polygonNiche Θ (K i))) Filter.atTop (nhds (ClassicalResults.area (polygonNiche Θ L))) ∧ Filter.Tendsto (fun (i : ℕ) => polygonAreaFunctional Θ (K i)) Filter.atTop (nhds (polygonAreaFunctional Θ L))

theorem MovingSofa.eventually_mem_polygonNiche_of_mem_capNiche (ω : ℝ) (hω : 0 < ω) (hω' : ω ≤ Real.pi / 2) (n : ℕ → ℕ) (hn : ∀ (i : ℕ), 2 ≤ n i) (hmono : StrictMono n) (K : CapSpace ω) {p : Point} (hp : p ∈ capNiche K) : ∀ᶠ (i : ℕ) in Filter.atTop, p ∈ polygonNiche (uniformAngleSet ω hω hω' (n i) ⋯) K

Every niche point belongs to all sufficiently fine uniform polygon niches.

theorem MovingSofa.maximizingPolygon_nicheArea_limit (ω : ℝ) (hω : 0 < ω) (hω' : ω ≤ Real.pi / 2) (n : ℕ → ℕ) (hn : ∀ (i : ℕ), 2 ≤ n i) (hmono : StrictMono n) (hdyadic : ∀ (i : ℕ), ∃ (k : ℕ), n i = 2 ^ k) (P : (i : ℕ) → PolygonCapSpace (uniformAngleSet ω hω hω' (n i) ⋯)) (hmax : ∀ (i : ℕ), IsMaximumPolygonCap (uniformAngleSet ω hω hω' (n i) ⋯) (P i)) (K : CapSpace ω) (hlim : Filter.Tendsto (fun (i : ℕ) => Metric.hausdorffDist ↑↑↑(P i) ↑↑K) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (i : ℕ) => ClassicalResults.area (polygonNiche (uniformAngleSet ω hω hω' (n i) ⋯) ↑(P i))) Filter.atTop (nhds (ClassicalResults.area (capNiche K)))

Moving sofa: related mathematical developments

• Cap.NicheLimit.
• Cap.Reflection.

Cap / Niche Limit

theorem MovingSofa.capNiche_subset_of_uniform_polygonNiche_subset {ω : ℝ} (K : CapSpace ω) (n : ℕ → ℕ) (hn : ∀ (i : ℕ), 2 ≤ n i) (hmono : StrictMono n) (hdyadic : ∀ (i : ℕ), ∃ (k : ℕ), n i = 2 ^ k) (P : (i : ℕ) → PolygonCapSpace (uniformAngleSet ω ⋯ ⋯ (n i) ⋯)) (hcontain : ∀ (i : ℕ), polygonNiche (uniformAngleSet ω ⋯ ⋯ (n i) ⋯) ↑(P i) ⊆ ↑↑↑(P i)) (hlim : Filter.Tendsto (fun (i : ℕ) => Metric.hausdorffDist ↑↑↑(P i) ↑↑K) Filter.atTop (nhds 0)) : capNiche K ⊆ ↑↑K

Containment of uniformly approximating polygon niches persists in the cap limit.

Cap / Reflection

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

Reflect about the line through the origin and the distinguished parallelogram point.

Equations

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

noncomputable def MovingSofa.reflectedAngleSet (Θ : AngleSet) : AngleSet

Reflect every interior wall direction about half the terminal angle.

Equations

• MovingSofa.reflectedAngleSet Θ = { angle := Θ.angle, angle_pos := ⋯, angle_le := ⋯, directions := Finset.image (fun (t : ℝ) => Θ.angle - t) Θ.directions, nonempty := ⋯, interior := ⋯ }

theorem MovingSofa.maximumPolygonCap_mirror (Θ : AngleSet) (K : PolygonCapSpace Θ) (hK : IsMaximumPolygonCap Θ K) : ∃ (P : PolygonCapSpace (reflectedAngleSet Θ)), ↑↑↑P = mirrorReflection Θ.angle '' ↑↑↑K ∧ IsMaximumPolygonCap (reflectedAngleSet Θ) P

theorem MovingSofa.balancedMaximumCap_mirror {ω : ℝ} (K : CapSpace ω) (hK : IsBalancedMaximumCap K) : ∃ (P : CapSpace ω), ↑↑P = mirrorReflection ω '' ↑↑K ∧ IsBalancedMaximumCap P

Moving sofa: related mathematical developments

• Sofa.Support.
• Sofa.Cap.

Sofa / Support

theorem MovingSofa.standardPosition_subset_monotonization (s : Set Point) (ω : ℝ) (hs : IsStandardPosition s ω) : s ⊆ monotonization s ω

theorem MovingSofa.standardPosition_subset_cap (s : Set Point) (ω : ℝ) (hs : IsStandardPosition s ω) : s ⊆ monotonization s ω ∧ monotonization s ω ⊆ capOfSofa s ω

theorem MovingSofa.standardPosition_support_eq (s : Set Point) (ω : ℝ) (hs : IsStandardPosition s ω) : (∀ t ∈ capUpperAngles ω, supportValue (monotonization s ω) ↑t = supportValue s ↑t ∧ supportValue (capOfSofa s ω) ↑t = supportValue s ↑t) ∧ ∀ t ∈ Set.Icc 0 ω, supportingHallway (monotonization s ω) ↑t = supportingHallway s ↑t ∧ supportingHallway (capOfSofa s ω) ↑t = supportingHallway s ↑t

Sofa / Cap

theorem MovingSofa.standardPosition_cap (s : Set Point) (ω : ℝ) (hs : IsStandardPosition s ω) : ∃ (K : CapSpace ω), ↑↑K = capOfSofa s ω

theorem MovingSofa.standardPosition_monotonization (s : Set Point) (ω : ℝ) (hs : IsStandardPosition s ω) (K : CapSpace ω) (hK : ↑↑K = capOfSofa s ω) : monotonization s ω = ↑↑K \ capNiche K

Moving sofa: related mathematical developments

• Cap.Connectedness.
• Cap.MirrorFeatures.

Cap / Connectedness

theorem MovingSofa.cap_niche_connected_iff {ω : ℝ} (K : CapSpace ω) : (capNiche K ⊆ ↑↑K ↔ capNiche K ⊆ ↑↑K \ capUpperBoundary K) ∧ (capNiche K ⊆ ↑↑K \ capUpperBoundary K ↔ ∀ t ∈ Set.Ioo 0 ω, (rotatingHallwayParts ↑↑K ↑t).innerCorner ∉ interior (capFan ω) ∨ (rotatingHallwayParts ↑↑K ↑t).innerCorner ∈ ↑↑K) ∧ ((∀ t ∈ Set.Ioo 0 ω, (rotatingHallwayParts ↑↑K ↑t).innerCorner ∉ interior (capFan ω) ∨ (rotatingHallwayParts ↑↑K ↑t).innerCorner ∈ ↑↑K) ↔ IsConnected (↑↑K \ capNiche K))

theorem MovingSofa.standardPosition_monotonization_connected (s : Set Point) (ω : ℝ) (hs : IsStandardPosition s ω) : IsConnected (monotonization s ω)

Cap / Mirror Features

theorem MovingSofa.cap_mirror_features {ω : ℝ} (K : CapSpace ω) : ∃ (P : CapSpace ω), ↑↑P = mirrorReflection ω '' ↑↑K ∧ (∀ t ∈ Set.Icc 0 ω, supportingHallway ↑↑P ↑t = mirrorReflection ω '' supportingHallway ↑↑K ↑(ω - t) ∧ (rotatingHallwayParts ↑↑P ↑t).innerCorner = mirrorReflection ω (rotatingHallwayParts ↑↑K ↑(ω - t)).innerCorner ∧ (rotatingHallwayParts ↑↑P ↑t).outerCorner = mirrorReflection ω (rotatingHallwayParts ↑↑K ↑(ω - t)).outerCorner ∧ (rotatingHallwayParts ↑↑P ↑t).outerQuadrant = mirrorReflection ω '' (rotatingHallwayParts ↑↑K ↑(ω - t)).outerQuadrant ∧ (rotatingHallwayParts ↑↑P ↑t).innerQuadrant = mirrorReflection ω '' (rotatingHallwayParts ↑↑K ↑(ω - t)).innerQuadrant ∧ (rotatingHallwayParts ↑↑P ↑t).a = mirrorReflection ω '' (rotatingHallwayParts ↑↑K ↑(ω - t)).c ∧ (rotatingHallwayParts ↑↑P ↑t).c = mirrorReflection ω '' (rotatingHallwayParts ↑↑K ↑(ω - t)).a ∧ (rotatingHallwayParts ↑↑P ↑t).b = mirrorReflection ω '' (rotatingHallwayParts ↑↑K ↑(ω - t)).d ∧ (rotatingHallwayParts ↑↑P ↑t).d = mirrorReflection ω '' (rotatingHallwayParts ↑↑K ↑(ω - t)).b ∧ (rotatingHallwayParts ↑↑P ↑t).bRay = mirrorReflection ω '' (rotatingHallwayParts ↑↑K ↑(ω - t)).dRay ∧ (rotatingHallwayParts ↑↑P ↑t).dRay = mirrorReflection ω '' (rotatingHallwayParts ↑↑K ↑(ω - t)).bRay ∧ (capVertices P t).1.1 = mirrorReflection ω (capVertices K (ω - t)).2.2 ∧ (capVertices P t).1.2 = mirrorReflection ω (capVertices K (ω - t)).2.1 ∧ (capVertices P t).2.1 = mirrorReflection ω (capVertices K (ω - t)).1.2 ∧ (capVertices P t).2.2 = mirrorReflection ω (capVertices K (ω - t)).1.1) ∧ (∀ t ∈ Set.Ioo 0 ω, (wedgeEndpoints P t).1 = mirrorReflection ω (wedgeEndpoints K (ω - t)).2 ∧ (wedgeEndpoints P t).2 = mirrorReflection ω (wedgeEndpoints K (ω - t)).1 ∧ (wedgeGaps P t).1 = (wedgeGaps K (ω - t)).2 ∧ (wedgeGaps P t).2 = (wedgeGaps K (ω - t)).1 ∧ capWedge P t = mirrorReflection ω '' capWedge K (ω - t)) ∧ capUpperBoundary P = mirrorReflection ω '' capUpperBoundary K ∧ capNiche P = mirrorReflection ω '' capNiche K ∧ ∀ (E : Set Real.Angle), MeasurableSet E → (surfaceAreaMeasure ↑P) E = (surfaceAreaMeasure ↑K) ((fun (a : Real.Angle) => ↑(ω + Real.pi / 2) - a) '' E)

Moving sofa: related mathematical developments

• Bounds.Arm.Geometry.

Bounds / Arm / Geometry

theorem MovingSofa.tangentArms_mirror (K P : RightAngleCapSpace) (hP : ↑↑P = mirrorReflection (Real.pi / 2) '' ↑↑K) (t : ℝ) (ht : t ∈ Set.Icc 0 (Real.pi / 2)) : (tangentArmLengths P t).1.1 = (tangentArmLengths K (Real.pi / 2 - t)).2.2 ∧ (tangentArmLengths P t).1.2 = (tangentArmLengths K (Real.pi / 2 - t)).2.1 ∧ (tangentArmLengths P t).2.1 = (tangentArmLengths K (Real.pi / 2 - t)).1.2 ∧ (tangentArmLengths P t).2.2 = (tangentArmLengths K (Real.pi / 2 - t)).1.1

theorem MovingSofa.capCorners_oneSided_derivatives (K : RightAngleCapSpace) : (∀ t ∈ Set.Ico 0 (Real.pi / 2), HasDerivWithinAt (fun (s : ℝ) => (rotatingHallwayParts ↑↑K ↑s).outerCorner) (-(tangentArmLengths K t).1.1 • normalVector ↑t + (tangentArmLengths K t).2.1 • tangentVector ↑t) (Set.Ici t) t ∧ HasDerivWithinAt (fun (s : ℝ) => (rotatingHallwayParts ↑↑K ↑s).innerCorner) (-((tangentArmLengths K t).1.1 - 1) • normalVector ↑t + ((tangentArmLengths K t).2.1 - 1) • tangentVector ↑t) (Set.Ici t) t) ∧ ∀ t ∈ Set.Ioc 0 (Real.pi / 2), HasDerivWithinAt (fun (s : ℝ) => (rotatingHallwayParts ↑↑K ↑s).outerCorner) (-(tangentArmLengths K t).1.2 • normalVector ↑t + (tangentArmLengths K t).2.2 • tangentVector ↑t) (Set.Iic t) t ∧ HasDerivWithinAt (fun (s : ℝ) => (rotatingHallwayParts ↑↑K ↑s).innerCorner) (-((tangentArmLengths K t).1.2 - 1) • normalVector ↑t + ((tangentArmLengths K t).2.2 - 1) • tangentVector ↑t) (Set.Iic t) t

Moving sofa: related mathematical developments

• Cap.Regularity.
• Cap.Tail.Contacts.
• Cap.Tail.Bodies.
• Cap.Tail.Extension.
• Cap.Tail.Separation.

Cap / Regularity

theorem MovingSofa.nondegenerateCap_continuity (K : RightAngleCapSpace) (hD : ∃ (r : ℝ → NNReal) (s : ℝ → NNReal), HasCapDensities K r s) : Continuous (nondegenerateCapData K hD).1.1 ∧ Continuous (nondegenerateCapData K hD).1.2 ∧ Continuous (nondegenerateCapData K hD).2.1 ∧ Continuous (nondegenerateCapData K hD).2.2 ∧ ContDiffOn ℝ 1 (capInnerCorner K) (Set.Icc 0 (Real.pi / 2)) ∧ ContDiffOn ℝ 1 (fun (s : ℝ) => (rotatingHallwayParts ↑↑K ↑s).outerCorner) (Set.Icc 0 (Real.pi / 2)) ∧ ∀ (t : ↑(Set.Icc 0 (Real.pi / 2))), HasDerivWithinAt (capInnerCorner K) (-((nondegenerateCapData K hD).2.1 t - 1) • normalVector ↑↑t + ((nondegenerateCapData K hD).2.2 t - 1) • tangentVector ↑↑t) (Set.Icc 0 (Real.pi / 2)) ↑t ∧ HasDerivWithinAt (fun (s : ℝ) => (rotatingHallwayParts ↑↑K ↑s).outerCorner) (-(nondegenerateCapData K hD).2.1 t • normalVector ↑↑t + (nondegenerateCapData K hD).2.2 t • tangentVector ↑↑t) (Set.Icc 0 (Real.pi / 2)) ↑t

theorem MovingSofa.inner_capInnerCorner (K : RightAngleCapSpace) (t : ℝ) : inner ℝ (capInnerCorner K t) (normalVector ↑t) = supportValue ↑↑K ↑t - 1 ∧ inner ℝ (capInnerCorner K t) (tangentVector ↑t) = supportValue ↑↑K ↑(t + Real.pi / 2) - 1

The corner coordinates of a right-angle cap in its moving frame.

theorem MovingSofa.capSupport_hasDerivAt (K : RightAngleCapSpace) (hinj : SatisfiesInjectivityCondition K) : ∃ (dh : ℝ → ℝ) (dj : ℝ → ℝ), (∀ t ∈ Set.Ioo 0 (Real.pi / 2), HasDerivAt (fun (u : ℝ) => supportValue ↑↑K ↑u) (dh t) t) ∧ (∀ t ∈ Set.Ioo 0 (Real.pi / 2), HasDerivAt (fun (u : ℝ) => supportValue ↑↑K ↑u) (dj t) (t + Real.pi / 2)) ∧ (∀ t ∈ Set.Ioo 0 (Real.pi / 2), dh t - supportValue ↑↑K ↑(t + Real.pi / 2) + 1 < 0) ∧ ∀ t ∈ Set.Ioo 0 (Real.pi / 2), 0 < dj t + supportValue ↑↑K ↑t - 1

The injectivity condition supplies the support derivatives with their strict signs.

Endpoint contacts for the canonical cap tails

The right and left canonical tails of a special cap are cut out of the cap by the upper half-planes of its inner supporting walls. This file supplies the contact points that make the tail support values meet their endpoint bounds.

The mathematical content is the frame-free lemma exists_mem_inner_eq_sub_one_of_deriv_signs: let s be a nonempty compact convex planar set lying above the horizontal axis with h_s(pi/2) = 1, whose support function h is differentiable on the two quarter-turn families with the strict corner velocity signs h'(t) - h(t + pi/2) + 1 < 0 and h'(t + pi/2) + h(t) - 1 > 0 for t in (0, pi/2). Then every interior cut line {q | inner q (normalVector t) = h(t) - 1} meets s in a point that stays above the whole cut family on [t, pi/2].

The proof selects the transverse maximum p of the first cut section and studies the deficiency g(t) = h(t) - inner p (normalVector t). Wherever g(t) = 1, the chord joining the two frame contacts has nonpositive signed area (planeCrossProduct_nonpos_of_isMaxOn), which forces g to decrease strictly at the cut angle; at a first return of g to level one the same determinant is strictly positive, a contradiction.

The left tail follows from the same lemma applied to reflectedBody (pi/2) K, whose support derivatives are the negated right-hand ones read backwards; see exists_left_tail_contact.

This argument replaces the step in the paper's proof of lem:right-left-body which infers that the upper boundary avoids the niche; that inference fails for the stated class of caps (P46 in NOTES.md).

theorem MovingSofa.basePoint_mem_of_rightAngleCap (K : RightAngleCapSpace) {q : Point} (hq : q ∈ ↑↑K) : !₂[q.ofLp 0, 0] ∈ ↑↑K

Lowering a right-angle cap point vertically to the base line keeps it inside the cap.

theorem MovingSofa.exists_frame_contacts {s : Set Point} (hcomp : IsCompact s) (hne : s.Nonempty) {t dh dj : ℝ} (hdh : HasDerivAt (fun (u : ℝ) => supportValue s ↑u) dh t) (hdj : HasDerivAt (fun (u : ℝ) => supportValue s ↑u) dj (t + Real.pi / 2)) : ∃ A ∈ s, ∃ C ∈ s, inner ℝ A (normalVector ↑t) = supportValue s ↑t ∧ inner ℝ A (tangentVector ↑t) = dh ∧ inner ℝ C (normalVector ↑t) = -dj ∧ inner ℝ C (tangentVector ↑t) = supportValue s ↑(t + Real.pi / 2)

The two frame contacts at an interior angle, with their derivative coordinates.

theorem MovingSofa.planeCrossProduct_nonpos_of_isMaxOn {s : Set Point} (hconv : Convex ℝ s) {r c₀ : ℝ} {p : Point} (hpline : inner ℝ p (normalVector ↑r) = c₀) (hmax : ∀ q ∈ s, inner ℝ q (normalVector ↑r) = c₀ → inner ℝ q (tangentVector ↑r) ≤ inner ℝ p (tangentVector ↑r)) {A C : Point} (hA : A ∈ s) (hC : C ∈ s) (hApos : 0 < inner ℝ (A - p) (normalVector ↑r)) (hCneg : inner ℝ (C - p) (normalVector ↑r) < 0) : planeCrossProduct (A - p) (C - p) ≤ 0

A transverse chord through a maximizing section point has nonpositive signed area.

theorem MovingSofa.exists_mem_inner_eq_sub_one_of_deriv_signs {s : Set Point} (hcomp : IsCompact s) (hconv : Convex ℝ s) (hne : s.Nonempty) (dh dj : ℝ → ℝ) (hdh : ∀ t ∈ Set.Ioo 0 (Real.pi / 2), HasDerivAt (fun (u : ℝ) => supportValue s ↑u) (dh t) t) (hdj : ∀ t ∈ Set.Ioo 0 (Real.pi / 2), HasDerivAt (fun (u : ℝ) => supportValue s ↑u) (dj t) (t + Real.pi / 2)) (halpha : ∀ t ∈ Set.Ioo 0 (Real.pi / 2), dh t - supportValue s ↑(t + Real.pi / 2) + 1 < 0) (hbeta : ∀ t ∈ Set.Ioo 0 (Real.pi / 2), 0 < dj t + supportValue s ↑t - 1) (htop : supportValue s ↑(Real.pi / 2) = 1) (hlow : ∀ q ∈ s, 0 ≤ inner ℝ q (normalVector ↑(Real.pi / 2))) {r : ℝ} (hr : r ∈ Set.Ioo 0 (Real.pi / 2)) : ∃ p ∈ s, inner ℝ p (normalVector ↑r) = supportValue s ↑r - 1 ∧ ∀ t ∈ Set.Icc r (Real.pi / 2), supportValue s ↑t - 1 ≤ inner ℝ p (normalVector ↑t)

Endpoint contact for the upper cut family of a strip body with strict corner velocities.

theorem MovingSofa.exists_cap_base_points (K : RightAngleCapSpace) : ∃ pR ∈ ↑↑K, ∃ pL ∈ ↑↑K, inner ℝ pR (normalVector ↑(Real.pi / 2)) = 0 ∧ inner ℝ pL (normalVector ↑(Real.pi / 2)) = 0 ∧ (∀ t ∈ Set.Icc 0 (Real.pi / 2), supportValue ↑↑K ↑t - 1 ≤ inner ℝ pR (normalVector ↑t)) ∧ ∀ t ∈ Set.Icc 0 (Real.pi / 2), supportValue ↑↑K ↑(t + Real.pi / 2) - 1 ≤ inner ℝ pL (normalVector ↑(t + Real.pi / 2))

The lowered horizontal extremes of a right-angle cap lie under all right and left cuts.

theorem MovingSofa.exists_right_tail_contact (K : RightAngleCapSpace) (hinj : SatisfiesInjectivityCondition K) {r : ℝ} (hr : r ∈ Set.Ioo 0 (Real.pi / 2)) : ∃ p ∈ ↑↑K, inner ℝ p (normalVector ↑r) = supportValue ↑↑K ↑r - 1 ∧ ∀ t ∈ Set.Icc r (Real.pi / 2), supportValue ↑↑K ↑t - 1 ≤ inner ℝ p (normalVector ↑t)

The right cut line meets the cap, below the whole right cut family.

theorem MovingSofa.exists_left_tail_contact (K : RightAngleCapSpace) (hinj : SatisfiesInjectivityCondition K) {l : ℝ} (hl : l ∈ Set.Ioo 0 (Real.pi / 2)) : ∃ p ∈ ↑↑K, inner ℝ p (normalVector ↑(l + Real.pi / 2)) = supportValue ↑↑K ↑(l + Real.pi / 2) - 1 ∧ ∀ t ∈ Set.Icc 0 l, supportValue ↑↑K ↑(t + Real.pi / 2) - 1 ≤ inner ℝ p (normalVector ↑(t + Real.pi / 2))

The left cut line meets the cap, below the whole left cut family.

Cap / Tail / Bodies

structure MovingSofa.DistinguishedCapSide : Type

The distinguished inner wall, upper half-plane, fan point and corner on one side.

• wall : Set Point

  The distinguished inner supporting wall.

• upperHalfPlane : Set Point

  The upper half-plane selected at the distinguished wall.

• fanPoint : Point

  The corresponding endpoint of the cap fan.

• corner : Point

  The inner hallway corner at the distinguished angle.

noncomputable def MovingSofa.distinguishedCapSides (K : RightAngleCapSpace) : DistinguishedCapSide × DistinguishedCapSide

The right and left cap geometry at the two distinguished Gerver angles.

Equations

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

theorem MovingSofa.distinguishedCapSides_fst_fanPoint (K : RightAngleCapSpace) : (distinguishedCapSides K).1.fanPoint = (wedgeEndpoints K paperGerverConstants.2.1).1

The right distinguished fan point is the right wedge endpoint at the right Gerver angle.

theorem MovingSofa.distinguishedCapSides_fst_corner (K : RightAngleCapSpace) : (distinguishedCapSides K).1.corner = capInnerCorner K paperGerverConstants.2.1

The right distinguished corner is the inner corner at the right Gerver angle.

theorem MovingSofa.distinguishedCapSides_snd_fanPoint (K : RightAngleCapSpace) : (distinguishedCapSides K).2.fanPoint = (wedgeEndpoints K paperGerverConstants.2.2).2

The left distinguished fan point is the left wedge endpoint at the left Gerver angle.

theorem MovingSofa.distinguishedCapSides_snd_corner (K : RightAngleCapSpace) : (distinguishedCapSides K).2.corner = capInnerCorner K paperGerverConstants.2.2

The left distinguished corner is the inner corner at the left Gerver angle.

theorem MovingSofa.canonicalTailSets_properties (K : SpecialCapSpace) : (canonicalTailSets K).1.Nonempty ∧ IsCompact (canonicalTailSets K).1 ∧ Convex ℝ (canonicalTailSets K).1 ∧ (canonicalTailSets K).1 ⊆ ↑↑↑K ∧ (canonicalTailSets K).2.Nonempty ∧ IsCompact (canonicalTailSets K).2 ∧ Convex ℝ (canonicalTailSets K).2 ∧ (canonicalTailSets K).2 ⊆ ↑↑↑K ∧ (∀ t ∈ Set.Icc paperGerverConstants.2.1 (Real.pi / 2), supportValue ↑↑↑K ↑t + supportValue (canonicalTailSets K).1 ↑(Real.pi + t) ≤ 1) ∧ (∀ t ∈ {paperGerverConstants.2.1, Real.pi / 2}, supportValue ↑↑↑K ↑t + supportValue (canonicalTailSets K).1 ↑(Real.pi + t) = 1) ∧ (supportingLineHalfPlane (canonicalTailSets K).1 ↑(3 * Real.pi / 2)).1 = normalLine (↑(Real.pi / 2)) 0 ∧ (supportingLineHalfPlane (canonicalTailSets K).1 ↑(Real.pi + paperGerverConstants.2.1)).1 = (distinguishedCapSides ↑K).1.wall ∧ (∀ t ∈ Set.Icc 0 paperGerverConstants.2.2, supportValue ↑↑↑K ↑(Real.pi / 2 + t) + supportValue (canonicalTailSets K).2 ↑(3 * Real.pi / 2 + t) ≤ 1) ∧ (∀ t ∈ {0, paperGerverConstants.2.2}, supportValue ↑↑↑K ↑(Real.pi / 2 + t) + supportValue (canonicalTailSets K).2 ↑(3 * Real.pi / 2 + t) = 1) ∧ (supportingLineHalfPlane (canonicalTailSets K).2 ↑(3 * Real.pi / 2)).1 = normalLine (↑(Real.pi / 2)) 0 ∧ (supportingLineHalfPlane (canonicalTailSets K).2 ↑(3 * Real.pi / 2 + paperGerverConstants.2.2)).1 = (distinguishedCapSides ↑K).2.wall

Canonical tails are convex bodies and satisfy all support and endpoint-line identities.

theorem MovingSofa.inner_capInnerCorner_normalVector (K : RightAngleCapSpace) (t : ℝ) : inner ℝ (capInnerCorner K t) (normalVector ↑t) = supportValue ↑↑K ↑t - 1

The inner corner's normal support coordinate is the cap's support value less one.

theorem MovingSofa.inner_capInnerCorner_tangentVector (K : RightAngleCapSpace) (t : ℝ) : inner ℝ (capInnerCorner K t) (tangentVector ↑t) = supportValue ↑↑K ↑(t + Real.pi / 2) - 1

The inner corner's tangent support coordinate is the quarter-turned support value less one.

theorem MovingSofa.mem_innerQuadrant_of_frame_coordinates_neg (K : RightAngleCapSpace) (t : ℝ) (q : Point) (h1 : (q.ofLp 0 - (capInnerCorner K t).ofLp 0) * Real.cos t + (q.ofLp 1 - (capInnerCorner K t).ofLp 1) * Real.sin t < 0) (h2 : -((q.ofLp 0 - (capInnerCorner K t).ofLp 0) * Real.sin t) + (q.ofLp 1 - (capInnerCorner K t).ofLp 1) * Real.cos t < 0) : q ∈ innerQuadrant (↑↑K) t

A point whose displacement from the inner corner has negative coordinates in the rotating frame at time t lies in the open inward quadrant at that time.

Cap / Tail / Extension

theorem MovingSofa.exists_canonicalCapTail (K : SpecialCapSpace) : ∃ (T : CapTailSpace), T.cap = K ∧ ↑T.rightBody = (canonicalTailSets K).1 ∧ ↑T.leftBody = (canonicalTailSets K).2

The canonical tail sets give an admissible cap-tail triple with exactly these carriers.

Cap / Tail / Separation

theorem MovingSofa.cap_and_niche_tail_separation (K : SpecialCapSpace) : ↑↑↑K ∩ (distinguishedCapSides ↑K).1.upperHalfPlane ∩ (distinguishedCapSides ↑K).2.upperHalfPlane = ∅ ∧ capNiche ↑K ∩ (distinguishedCapSides ↑K).1.upperHalfPlane ∩ (distinguishedCapSides ↑K).2.upperHalfPlane = ∅

Moving sofa: related mathematical developments

• Area.NicheDecomposition.

Area / Niche Decomposition

theorem MovingSofa.niche_three_regions_area (K : SpecialCapSpace) (E₀ Eᵣ Eₗ : Set Point) : E₀ = capNiche ↑K \ ((distinguishedCapSides ↑K).1.upperHalfPlane ∪ (distinguishedCapSides ↑K).2.upperHalfPlane) → Eᵣ = capNiche ↑K ∩ (distinguishedCapSides ↑K).1.upperHalfPlane → Eₗ = capNiche ↑K ∩ (distinguishedCapSides ↑K).2.upperHalfPlane → MeasurableSet E₀ ∧ MeasurableSet Eᵣ ∧ MeasurableSet Eₗ ∧ MeasureTheory.volume E₀ < ⊤ ∧ MeasureTheory.volume Eᵣ < ⊤ ∧ MeasureTheory.volume Eₗ < ⊤ ∧ Disjoint E₀ Eᵣ ∧ Disjoint E₀ Eₗ ∧ Disjoint Eᵣ Eₗ ∧ E₀ ∪ Eᵣ ∪ Eₗ = capNiche ↑K ∧ ClassicalResults.area (capNiche ↑K) = ClassicalResults.area E₀ + ClassicalResults.area Eᵣ + ClassicalResults.area Eₗ

Moving sofa: related mathematical developments

• Bounds.MonotonicityIntervals.
• Bounds.WedgeEndpoints.

Monotonicity intervals for the distinguished cap sides

cap_tail_monotonicity_intervals records that on the right interval (φ, π/2] the inner corner has left the distinguished right half-plane, and that inside that half-plane the inner quadrant is cut out by the single inner wall b(t); symmetrically on [0, π/2 - φ) for the left side. Intersecting with the fan gives the two wedge forms.

theorem MovingSofa.cap_tail_monotonicity_intervals (K : SpecialCapSpace) : (∀ t ∈ Set.Ioc paperGerverConstants.2.1 (Real.pi / 2), capInnerCorner (↑K) t ∉ (distinguishedCapSides ↑K).1.upperHalfPlane ∧ (distinguishedCapSides ↑K).1.upperHalfPlane ∩ innerQuadrant (↑↑↑K) t = (distinguishedCapSides ↑K).1.upperHalfPlane \ (innerWallUpperHalfPlanes (↑K) t).1) ∧ (∀ t ∈ Set.Ico 0 paperGerverConstants.2.2, capInnerCorner (↑K) t ∉ (distinguishedCapSides ↑K).2.upperHalfPlane ∧ (distinguishedCapSides ↑K).2.upperHalfPlane ∩ innerQuadrant (↑↑↑K) t = (distinguishedCapSides ↑K).2.upperHalfPlane \ (innerWallUpperHalfPlanes (↑K) t).2) ∧ (∀ t ∈ Set.Ioc paperGerverConstants.2.1 (Real.pi / 2), t ∈ Set.Ioo 0 (Real.pi / 2) → (distinguishedCapSides ↑K).1.upperHalfPlane ∩ capWedge (↑K) t = ((distinguishedCapSides ↑K).1.upperHalfPlane ∩ {p : Point | 0 ≤ p.ofLp 1}) \ (innerWallUpperHalfPlanes (↑K) t).1) ∧ ∀ t ∈ Set.Ico 0 paperGerverConstants.2.2, t ∈ Set.Ioo 0 (Real.pi / 2) → (distinguishedCapSides ↑K).2.upperHalfPlane ∩ capWedge (↑K) t = ((distinguishedCapSides ↑K).2.upperHalfPlane ∩ {p : Point | 0 ≤ p.ofLp 1}) \ (innerWallUpperHalfPlanes (↑K) t).2

theorem MovingSofa.strictAntiOn_capInnerCorner_fst (K : SpecialCapSpace) {a b : ℝ} (ha : 0 ≤ a) (hb : b ≤ Real.pi / 2) : StrictAntiOn (fun (t : ℝ) => (capInnerCorner (↑K) t).ofLp 0) (Set.Icc a b)

On any subinterval of [0, π/2] the inner corner of a special cap has strictly decreasing horizontal coordinate: the injectivity condition makes its horizontal derivative negative.

Bounds / Wedge Endpoints

theorem MovingSofa.wedgeGaps_positive_lower_bound {ω : ℝ} (K : CapSpace ω) (t : ℝ) (ht : t ∈ Set.Ioo 0 ω) : (1 - Real.sin t) / Real.cos t ≤ (wedgeGaps K t).1 ∧ 0 < (1 - Real.sin t) / Real.cos t ∧ (1 - Real.sin (ω - t)) / Real.cos (ω - t) ≤ (wedgeGaps K t).2 ∧ 0 < (1 - Real.sin (ω - t)) / Real.cos (ω - t)

theorem MovingSofa.specialCap_wedgeEndpoints_in_bottomEdge (K : SpecialCapSpace) : (distinguishedCapSides ↑K).1.fanPoint ∈ exposedEdge ↑↑K ↑(3 * Real.pi / 2) \ {(capVertices (↑K) 0).1.2, (capVertices (↑K) (Real.pi / 2)).2.1} ∧ (distinguishedCapSides ↑K).2.fanPoint ∈ exposedEdge ↑↑K ↑(3 * Real.pi / 2) \ {(capVertices (↑K) 0).1.2, (capVertices (↑K) (Real.pi / 2)).2.1}

Moving sofa: related mathematical developments

• Bounds.Upper.Q.

Bounds / Upper / Q

noncomputable def MovingSofa.upperBoundQ (T : CapTailSpace) : ℝ

The cap-tail upper-bound functional Q assembled from cap area, tail arcs and endpoint segments.

Equations

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

Moving sofa: related mathematical developments

• Motion.Monotonization.

Motion / Monotonization

theorem MovingSofa.standardPosition_monotonization_standard (s : Set Point) (ω : ℝ) (hs : IsStandardPosition s ω) : IsStandardPosition (monotonization s ω) ω ∧ s ⊆ monotonization s ω

Moving sofa: related mathematical developments

• Sofa.Area.

Sofa / Area

theorem MovingSofa.monotoneSofa_structure (s : Set Point) (ω : ℝ) (hs : ∃ (s₀ : Set Point), IsStandardPosition s₀ ω ∧ s = monotonization s₀ ω) (K : CapSpace ω) (hK : ↑↑K = capOfSofa s ω) : s = ↑↑K \ capNiche K

theorem MovingSofa.capAreaFunctional_eq_sofaArea (s : Set Point) (ω : ℝ) (hs : ∃ (s₀ : Set Point), IsStandardPosition s₀ ω ∧ s = monotonization s₀ ω) (K : CapSpace ω) (hK : ↑↑K = capOfSofa s ω) : capAreaFunctional K = ClassicalResults.area s