Moving sofa: related mathematical developments

• Bounds.Applications.Development001.
• Cap.Applications.Development002.
• Polygon.Applications.Development002.
• Cap.Applications.Development003.
• Bounds.Applications.Development002.
• Cap.Applications.Development004.
• Gerver.Applications.Development003.
• Cap.Applications.Development005.
• Cap.Applications.Development006.
• Area.Applications.Development004.

Moving sofa: related mathematical developments

• Bounds.Arm.Estimates.
• Bounds.WedgeGap.Infimum.
• Bounds.WedgeGap.Limit.

Bounds / Arm / Estimates

theorem MovingSofa.aestronglyMeasurable_tangentArm_fst (C : RightAngleCapSpace) : MeasureTheory.AEStronglyMeasurable (fun (t : ℝ) => (tangentArmLengths C t).2.1) (MeasureTheory.volume.restrict (Set.Ioc 0 (Real.pi / 2)))

The positive tangent arm length is almost everywhere strongly measurable.

theorem MovingSofa.tangentArm_fst_nonneg (C : RightAngleCapSpace) {t : ℝ} : 0 ≤ (tangentArmLengths C t).2.1

The positive tangent arm length is nonnegative: it is the integral of the sine of a quarter-turn of normal directions against the surface area measure.

theorem MovingSofa.tangentArmLengths_right_nonneg (K : RightAngleCapSpace) (t : ℝ) : 0 ≤ (tangentArmLengths K t).1.1 ∧ 0 ≤ (tangentArmLengths K t).1.2

Both right tangent arm lengths of a right-angle cap are nonnegative: the outer corner realizes the support value in the tangent direction, while the two contacts lie in the cap.

theorem MovingSofa.abs_tangentArm_fst_le (C : RightAngleCapSpace) {t : ℝ} : |(tangentArmLengths C t).2.1| ≤ (surfaceAreaMeasure ↑C).real Set.univ

The positive tangent arm length is bounded by the total mass of the surface area measure.

theorem MovingSofa.intervalIntegrable_tangentArm_fst (C : RightAngleCapSpace) : IntervalIntegrable (fun (t : ℝ) => (tangentArmLengths C t).2.1) MeasureTheory.volume 0 (Real.pi / 2)

The positive tangent arm length is bounded by the total surface mass, hence integrable.

theorem MovingSofa.maximumPolygonCap_arm_bound (n : ℕ) (K : RightAngleCapSpace) (hK : IsMaximumPolygonCapSteps n K) : Metric.diam ↑↑K ≤ 5 ∧ ∀ t ∈ Set.Icc 0 (Real.pi / 2), (tangentArmLengths K t).1.1 ∈ Set.Icc 0 5 ∧ (tangentArmLengths K t).1.2 ∈ Set.Icc 0 5 ∧ (tangentArmLengths K t).2.1 ∈ Set.Icc 0 5 ∧ (tangentArmLengths K t).2.2 ∈ Set.Icc 0 5

Helpers for the discrete arm bound

theorem MovingSofa.maximumPolygonCap_arm_cell (n : ℕ) (hn : 2 ≤ n) (K : RightAngleCapSpace) (hK : IsMaximumPolygonCapSteps n K) (t : ℝ) (ht : t = 0 ∨ t ∈ (rightAngleSet n hn).directions) : (∀ u ∈ Set.Ioo t (t + polygonStepSize n), (tangentArmLengths K u).2.1 ≤ (tangentArmLengths K t).2.1 ∧ (tangentArmLengths K u).2.1 = (tangentArmLengths K u).2.2 ∧ (tangentArmLengths K (t + polygonStepSize n)).2.2 ≤ (tangentArmLengths K u).2.2) ∧ (tangentArmLengths K t).2.1 - (tangentArmLengths K (t + polygonStepSize n)).2.2 ≤ 5 * polygonStepSize n

theorem MovingSofa.polygonCap_arm_integral_limit (K : ℕ → RightAngleCapSpace) (L : RightAngleCapSpace) (hlim : Filter.Tendsto (fun (i : ℕ) => Metric.hausdorffDist ↑↑(K i) ↑↑L) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (i : ℕ) => ∫ (t : ℝ) in 0..Real.pi / 2, |(tangentArmLengths (K i) t).2.1 - (tangentArmLengths L t).2.1|) Filter.atTop (nhds 0)

Bounds / Wedge Gap / Infimum

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

The two infima of the wedge-gap components over interior rotation angles.

Equations

• MovingSofa.wedgeGapInfimum K = (sInf ((fun (t : ℝ) => (MovingSofa.wedgeGaps K t).1) '' Set.Ioo 0 ω), sInf ((fun (t : ℝ) => (MovingSofa.wedgeGaps K t).2) '' Set.Ioo 0 ω))

theorem MovingSofa.maximumPolygonCap_gap_le_surface {Θ : AngleSet} (K : PolygonCapSpace Θ) (hK : IsMaximumPolygonCap Θ K) (hω : Θ.angle < Real.pi / 2) : (wedgeGapInfimum ↑K).1 ≤ ((surfaceAreaMeasure ↑↑K) {↑(Real.pi / 2)}).toReal ∧ (wedgeGapInfimum ↑K).2 ≤ ((surfaceAreaMeasure ↑↑K) {↑Θ.angle}).toReal

Bounds / Wedge Gap / Limit

theorem MovingSofa.wedgeGapInfimum_hausdorff_bound {ω : ℝ} (K L : CapSpace ω) (hω : ω < Real.pi / 2) : |(wedgeGapInfimum K).1 - (wedgeGapInfimum L).1| ≤ (1 + (Real.cos ω)⁻¹) * Metric.hausdorffDist ↑↑K ↑↑L

theorem MovingSofa.wedgeGapInfimum_snd_hausdorff_bound {ω : ℝ} (K L : CapSpace ω) (hω : ω < Real.pi / 2) : |(wedgeGapInfimum K).2 - (wedgeGapInfimum L).2| ≤ (1 + (Real.cos ω)⁻¹) * Metric.hausdorffDist ↑↑K ↑↑L

The left wedge-gap infimum obeys the same Hausdorff estimate as the right one.

theorem MovingSofa.balancedMaximumCap_gap_le_surface {ω : ℝ} (K : CapSpace ω) (hK : IsBalancedMaximumCap K) (hω : ω < Real.pi / 2) : (wedgeGapInfimum K).1 ≤ ((surfaceAreaMeasure ↑K) {↑(Real.pi / 2)}).toReal ∧ (wedgeGapInfimum K).2 ≤ ((surfaceAreaMeasure ↑K) {↑ω}).toReal

Moving sofa: related mathematical developments

• Cap.BalancedExistence.

Cap / Balanced Existence

theorem MovingSofa.exists_maximumPolygonCap (Θ : AngleSet) : ∃ (K : PolygonCapSpace Θ), IsMaximumPolygonCap Θ K ∧ 0 ≤ polygonAreaFunctional Θ ↑K

theorem MovingSofa.maximumPolygonCap_niche_subset {Θ : AngleSet} (K : PolygonCapSpace Θ) (hK : IsMaximumPolygonCap Θ K) : polygonNiche Θ ↑K ⊆ ↑↑↑K

theorem MovingSofa.exists_balancedMaximumCap (ω : ℝ) (hω : 0 < ω) (hω' : ω ≤ Real.pi / 2) : ∃ (K : CapSpace ω), IsBalancedMaximumCap K

theorem MovingSofa.balancedMaximumCap_niche_subset {ω : ℝ} (K : CapSpace ω) (hK : IsBalancedMaximumCap K) : capNiche K ⊆ ↑↑K

theorem MovingSofa.balancedMaximumCap_maximizes_area {ω : ℝ} (K : CapSpace ω) (hK : IsBalancedMaximumCap K) (L : CapSpace ω) : capAreaFunctional L ≤ capAreaFunctional K

Moving sofa: related mathematical developments

• Polygon.BalancedInequalities.

Polygon / Balanced Inequalities

noncomputable def MovingSofa.magicDensity (x : ℝ) : ℝ

The magic function k₀ read as a function on all reals through truncation.

Equations

• MovingSofa.magicDensity x = MovingSofa.magicFunctions.1 x.toNNReal

theorem MovingSofa.maximumPolygonCap_surfaceAtom_bound (n : ℕ) (hn : 2 ≤ n) (K : RightAngleCapSpace) (hK : IsMaximumPolygonCapSteps n K) (t : ℝ) (ht : t = 0 ∨ t ∈ (rightAngleSet n hn).directions) : (surfaceAreaMeasure ↑K) {↑t} ≤ ENNReal.ofReal (magicFunctions.1 (tangentArmLengths K t).2.1.toNNReal * polygonStepSize n + 8 * polygonStepSize n ^ 2)

The magic density

theorem MovingSofa.magicDensity_nonneg (x : ℝ) : 0 ≤ magicDensity x

The magic function k₀ is nonnegative.

theorem MovingSofa.magicDensity_le_abs_add_one (x : ℝ) : magicDensity x ≤ |x| + 1

The magic function k₀ grows at most linearly: k₀ x ≤ |x| + 1.

Integrability of the magic density

theorem MovingSofa.aestronglyMeasurable_magicDensity_tangentArm_fst (C : RightAngleCapSpace) : MeasureTheory.AEStronglyMeasurable (fun (t : ℝ) => magicDensity (tangentArmLengths C t).2.1) (MeasureTheory.volume.restrict (Set.Ioc 0 (Real.pi / 2)))

The magic density of the positive tangent arm length is almost everywhere strongly measurable on the rotation interval.

The density measure of a cap

Surface measure support of a right-angle polygon cap

Discrete cell bounds

The per-level grid bound

Passing to the limit

theorem MovingSofa.balancedMaximumCap_surface_domination (K : RightAngleCapSpace) (hK : IsBalancedMaximumCap K) (E : Set ℝ) (hE : MeasurableSet E) (hET : E ⊆ Set.Ico 0 (Real.pi / 2)) : (surfaceAreaMeasure ↑K) ((fun (t : ℝ) => ↑t) '' E) ≤ ENNReal.ofReal (∫ (t : ℝ) in E, magicFunctions.1 (tangentArmLengths K t).2.1.toNNReal)

Moving sofa: related mathematical developments

• Cap.DensityExistence.
• Cap.Interpolation.

Existence and uniqueness of the surface densities of a balanced maximum cap

A balanced maximum cap of rotation angle π / 2 satisfies the density clause of the injectivity condition: its surface area measure has nonnegative measurable densities on the quarter arcs [0, π / 2) and (π / 2, π], unique up to Lebesgue-null sets.

On the first arc the density comes from the limiting inequality balancedMaximumCap_surface_domination together with the Radon–Nikodym construction exists_nnreal_density_of_domination. On the second arc the mirror image of the cap is again a balanced maximum cap, and the surface-measure identity of cap_mirror_features transports its first-arc density back along the reflection a ↦ π - a of normal angles.

On the first arc the domination inequality also bounds the density: the real density produced by exists_capDensity_right_le_magicDensity is at most k₀ of the positive tangent arm length.

A continuous section of the angular projection

Densities on an arc from a domination inequality

The density on the first arc

theorem MovingSofa.exists_capDensity_right_le_magicDensity (K : RightAngleCapSpace) (hK : IsBalancedMaximumCap K) : ∃ (ρ : ℝ → ℝ), MeasureTheory.IntegrableOn ρ (Set.Icc 0 (Real.pi / 2)) MeasureTheory.volume ∧ (∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc 0 (Real.pi / 2)), 0 ≤ ρ t ∧ ρ t ≤ magicDensity (tangentArmLengths K t).2.1) ∧ ∀ (E : Set ℝ), MeasurableSet E → E ⊆ Set.Ico 0 (Real.pi / 2) → ((surfaceAreaMeasure ↑K) ((fun (t : ℝ) => ↑t) '' E)).toReal = ∫ (t : ℝ) in E, ρ t

On the first quarter arc the surface area measure of a balanced maximum cap is the integral of a real density on the rotation interval which is bounded by the magic density of the positive tangent arm length. This refines exists_capDensity_right, which only records the existence of a density, by the pointwise bound carried by the limiting inequality balancedMaximumCap_surface_domination.

The mirrored cap and the density on the second arc

Uniqueness of the densities

theorem MovingSofa.HasCapDensities.ae_eq {K : RightAngleCapSpace} {r s r' s' : ℝ → NNReal} (h : HasCapDensities K r s) (h' : HasCapDensities K r' s') : r =ᵐ[MeasureTheory.volume.restrict (Set.Icc 0 (Real.pi / 2))] r' ∧ s =ᵐ[MeasureTheory.volume.restrict (Set.Icc 0 (Real.pi / 2))] s'

A right-angle cap determines its two surface densities up to Lebesgue-null sets: any two pairs of densities of the same cap agree almost everywhere on [0, π / 2].

theorem MovingSofa.balancedMaximumCap_hasDensities (K : RightAngleCapSpace) (hK : IsBalancedMaximumCap K) : ∃ (r : ℝ → NNReal) (s : ℝ → NNReal), HasCapDensities K r s ∧ ∀ (r' s' : ℝ → NNReal), HasCapDensities K r' s' → r =ᵐ[MeasureTheory.volume.restrict (Set.Icc 0 (Real.pi / 2))] r' ∧ s =ᵐ[MeasureTheory.volume.restrict (Set.Icc 0 (Real.pi / 2))] s'

Minkowski interpolation of right-angle caps

The cap conditions of IsCap (π / 2) and the injectivity condition of SatisfiesInjectivityCondition are preserved by the Minkowski interpolation convexBodyCombination t K L = (1 - t) • K + t • L of two right-angle caps. Each statement about the interpolation is phrased for an arbitrary cap whose underlying convex body is that interpolation, so that it applies both to the cap produced by isCap_convexBodyCombination and to an interpolated cap obtained by choice.

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

Lowering a point of an interpolated right-angle cap onto the base line keeps it inside, because the same projection can be applied to both summands.

theorem MovingSofa.isCap_convexBodyCombination (t : ↑unitInterval) (K L : RightAngleCapSpace) : IsCap (Real.pi / 2) (convexBodyCombination t ↑K ↑L)

Right-angle caps are closed under Minkowski interpolation.

theorem MovingSofa.hasCapDensities_of_eq_convexBodyCombination {t : ↑unitInterval} {K L M : RightAngleCapSpace} (hM : ↑M = convexBodyCombination t ↑K ↑L) {r₁ s₁ r₂ s₂ : ℝ → NNReal} (hK : HasCapDensities K r₁ s₁) (hL : HasCapDensities L r₂ s₂) : HasCapDensities M (fun (x : ℝ) => (1 - ↑t).toNNReal * r₁ x + (↑t).toNNReal * r₂ x) fun (x : ℝ) => (1 - ↑t).toNNReal * s₁ x + (↑t).toNNReal * s₂ x

An interpolated right-angle cap carries the interpolated surface densities: its surface measure is the interpolation of the two surface measures, and pushing a weighted measure forward is linear in the weight.

theorem MovingSofa.capInnerCorner_of_eq_convexBodyCombination {t : ↑unitInterval} {K L M : RightAngleCapSpace} (hM : ↑M = convexBodyCombination t ↑K ↑L) (x : ℝ) : capInnerCorner M x = (1 - ↑t) • capInnerCorner K x + ↑t • capInnerCorner L x

The inner corner of an interpolated cap is the interpolation of the two inner corners.

theorem MovingSofa.satisfiesInjectivityCondition_of_eq_convexBodyCombination {t : ↑unitInterval} {K L M : RightAngleCapSpace} (hM : ↑M = convexBodyCombination t ↑K ↑L) (hK : SatisfiesInjectivityCondition K) (hL : SatisfiesInjectivityCondition L) : SatisfiesInjectivityCondition M

The injectivity condition is inherited by Minkowski interpolations of right-angle caps: the inner corner interpolates, so its two frame velocity components are the same combinations of the original ones, and a combination with nonnegative weights summing to one preserves their strict signs even at the two degenerate weights.

Moving sofa: related mathematical developments

• Bounds.Arm.Regularity.
• Bounds.Lower.Sequence.

Regularity of the arm length function of a balanced maximum cap

For a balanced maximum cap K of rotation angle π / 2 the arm length function f_K is absolutely continuous on [0, π / 2] and satisfies f_K' ≥ m₀ ∘ g_K almost everywhere on (0, π / 2).

The argument combines three inputs. The differentiation identity positiveArm_stieltjes_surface for the positive arm length, read on an interval (0, t] with t < π / 2, expresses f_K(t) - f_K(0) as the integral of g_K minus the surface measure of the arc traversed. The surface measure on that arc has a real density bounded by k₀ ∘ g_K, by exists_capDensity_right_le_magicDensity. Together they present f_K on [0, π / 2) as the primitive of w = g_K - ρ; continuity of f_K on the closed interval (nondegenerateCap_continuity) upgrades the representation to [0, π / 2], whence absolute continuity and f_K' = w ≥ g_K - k₀ ∘ g_K = m₀ ∘ g_K almost everywhere.

The module also records the pointwise data accompanying that differential inequality: both arm length functions of a nondegenerate cap are nonnegative, and the right one has initial value f_K(0) = 1.

noncomputable def MovingSofa.extendIntervalScalar {a b : ℝ} (f : ↑(Set.Icc a b) → ℝ) (t : ℝ) : ℝ

A function on the interval subtype Set.Icc a b, extended to ℝ by zero.

Equations

• MovingSofa.extendIntervalScalar f t = if h : t ∈ Set.Icc a b then f ⟨t, h⟩ else 0

theorem MovingSofa.extendIntervalScalar_of_mem {a b : ℝ} (f : ↑(Set.Icc a b) → ℝ) {t : ℝ} (ht : t ∈ Set.Icc a b) : extendIntervalScalar f t = f ⟨t, ht⟩

Inside its interval the zero extension agrees with the original subtype function.

theorem MovingSofa.tangentArmLengths_right_zero_eq_one (K : RightAngleCapSpace) (hD : ∃ (r : ℝ → NNReal) (s : ℝ → NNReal), HasCapDensities K r s) : (tangentArmLengths K 0).1.1 = 1

The right arm length of a nondegenerate right-angle cap at the horizontal normal equals one. Lowering the contact there onto the base line stays inside the cap and meets the same supporting line, so the infimum of the tangent heights of that edge is at most zero; the contacts coincide, so the contact itself has height zero, and the outer corner at that angle has height h_K(π / 2) = 1.

theorem MovingSofa.nondegenerateCapData_arm_nonneg (K : RightAngleCapSpace) (hD : ∃ (r : ℝ → NNReal) (s : ℝ → NNReal), HasCapDensities K r s) (t : ↑(Set.Icc 0 (Real.pi / 2))) : 0 ≤ (nondegenerateCapData K hD).2.1 t ∧ 0 ≤ (nondegenerateCapData K hD).2.2 t

Both arm length functions of a nondegenerate right-angle cap are nonnegative.

theorem MovingSofa.balancedMaximumCap_arm_regularity (K : RightAngleCapSpace) (hK : IsBalancedMaximumCap K) : ∃ (hD : ∃ (r : ℝ → NNReal) (s : ℝ → NNReal), HasCapDensities K r s), AbsolutelyContinuousOnInterval (extendIntervalScalar (nondegenerateCapData K hD).2.1) 0 (Real.pi / 2) ∧ ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 (Real.pi / 2)), magicFunctions.2 (extendIntervalScalar (nondegenerateCapData K hD).2.2 t).toNNReal ≤ deriv (extendIntervalScalar (nondegenerateCapData K hD).2.1) t

Bounds / Lower / Sequence

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

The nonnegative-real version of the continuous lower-bound profile.

Equations

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

theorem MovingSofa.armIntegralOperator_monotone (f g : C(↑(Set.Icc 0 (Real.pi / 2)), NNReal)) (hfg : ∀ (x : ↑(Set.Icc 0 (Real.pi / 2))), f x ≤ g x) (x : ↑(Set.Icc 0 (Real.pi / 2))) : (armIntegralOperator f) x ≤ (armIntegralOperator g) x

theorem MovingSofa.armIntegralOperator_profile_step (c : ℝ) (hc : 0 ≤ c) (hc' : c ≤ 2 / 3) (x : ↑(Set.Icc 0 (Real.pi / 2))) : (lowerBoundProfile ⟨c + 1 / 12, ⋯⟩) x ≤ (armIntegralOperator (nonnegativeLowerBoundProfile ⟨c, ⋯⟩)) x

theorem MovingSofa.armLowerBoundSequence_threshold (x : ↑(Set.Icc 0 (Real.pi / 2))) : 0 < ↑x → 1 < ↑((armLowerBoundSequence 11) x)

theorem MovingSofa.balancedMaximumCap_sequence_bound (K : RightAngleCapSpace) (hK : IsBalancedMaximumCap K) : ∃ (hD : ∃ (r : ℝ → NNReal) (s : ℝ → NNReal), HasCapDensities K r s), ∀ (n : ℕ) (t : ↑(Set.Icc 0 (Real.pi / 2))), ↑((armLowerBoundSequence n) t) ≤ (nondegenerateCapData K hD).2.1 t ∧ ↑((armLowerBoundSequence n) ⟨Real.pi / 2 - ↑t, ⋯⟩) ≤ (nondegenerateCapData K hD).2.2 t

theorem MovingSofa.balancedMaximumCap_arm_gt_one (K : RightAngleCapSpace) (hK : IsBalancedMaximumCap K) : ∃ (hD : ∃ (r : ℝ → NNReal) (s : ℝ → NNReal), HasCapDensities K r s), (∀ (t : ↑(Set.Icc 0 (Real.pi / 2))), 0 < ↑t → 1 < (nondegenerateCapData K hD).2.1 t) ∧ ∀ (t : ↑(Set.Icc 0 (Real.pi / 2))), ↑t < Real.pi / 2 → 1 < (nondegenerateCapData K hD).2.2 t

Moving sofa: related mathematical developments

• Cap.Injectivity.

The injectivity condition for balanced maximum caps

Every balanced maximum cap of rotation angle π / 2 satisfies the injectivity condition: its surface measure has densities that are unique up to null sets, its inner corner is continuously differentiable, and the two frame components of the corner velocity have strict signs on the open rotation interval.

The theorem lives downstream of MovingSofa/Cap/Regularity.lean because its inputs balancedMaximumCap_hasDensities and balancedMaximumCap_arm_gt_one depend on that module.

theorem MovingSofa.balancedMaximumCap_injectivity (K : RightAngleCapSpace) (hK : IsBalancedMaximumCap K) : SatisfiesInjectivityCondition K

Moving sofa: related mathematical developments

• Gerver.Injectivity.

Gerver / Injectivity

theorem MovingSofa.capInnerCorner_eq_paperGerverPath (K : RightAngleCapSpace) (hK : ↑↑K = capOfSofa paperGerverSofa (Real.pi / 2)) {t : ℝ} (ht : t ∈ Set.Icc 0 (Real.pi / 2)) : capInnerCorner K t = paperGerverPath t

On the rotation interval the inner corner of the cap of Gerver's sofa is the certified direct Gerver path. The rotating-hallway coordinates of the inner corner are the cap's two support values at t and t + π / 2, and gerver_capSupport_identification evaluates those at the frame coordinates of the paper path.

theorem MovingSofa.derivWithin_capInnerCorner_eq_deriv_paperGerverPath (K : RightAngleCapSpace) (hK : ↑↑K = capOfSofa paperGerverSofa (Real.pi / 2)) {t : ℝ} (ht : t ∈ Set.Ioo 0 (Real.pi / 2)) : derivWithin (capInnerCorner K) (Set.Icc 0 (Real.pi / 2)) t = deriv paperGerverPath t

On the open rotation interval the inner-corner velocity of the cap of Gerver's sofa is the velocity of the certified direct Gerver path.

theorem MovingSofa.paperGerverCap_injectivity : ∃ (K : RightAngleCapSpace), ↑↑K = capOfSofa paperGerverSofa (Real.pi / 2) ∧ SatisfiesInjectivityCondition K

Moving sofa: related mathematical developments

• Cap.Special.Domain.
• Cap.Special.AreaVariation.
• Cap.Tail.Interpolation.

Cap / Special / Domain

noncomputable def MovingSofa.specialCapCombination (t : ↑unitInterval) (K L : SpecialCapSpace) : SpecialCapSpace

Choose the special cap representing a convex body combination, with a fallback to the first cap.

Equations

• MovingSofa.specialCapCombination t K L = if h : ∃ (M : MovingSofa.SpecialCapSpace), ↑↑M = MovingSofa.convexBodyCombination t ↑↑K ↑↑L then h.choose else K

theorem MovingSofa.specialCap_isConvexDomain : (∀ (t : ↑unitInterval) (K L : SpecialCapSpace), ↑↑(specialCapCombination t K L) = convexBodyCombination t ↑↑K ↑↑L) ∧ IsConvexDomain specialCapCombination ∧ (∀ (K : RightAngleCapSpace), IsBalancedMaximumCap K → ∃ (L : SpecialCapSpace), ↑L = K) ∧ ∃ (K : SpecialCapSpace), ↑↑↑K = capOfSofa paperGerverSofa (Real.pi / 2)

theorem MovingSofa.specialCap_maps_linear (t : ↑unitInterval) (K L : SpecialCapSpace) : (∀ (a : Real.Angle), (edgeVertices (↑↑(specialCapCombination t K L)) a).1 = (1 - ↑t) • (edgeVertices (↑↑K) a).1 + ↑t • (edgeVertices (↑↑L) a).1 ∧ (edgeVertices (↑↑(specialCapCombination t K L)) a).2 = (1 - ↑t) • (edgeVertices (↑↑K) a).2 + ↑t • (edgeVertices (↑↑L) a).2) ∧ ∀ (a b : ℝ), a < b → b < a + Real.pi → supportingIntersection ↑↑(specialCapCombination t K L) ↑a ↑b = (1 - ↑t) • supportingIntersection ↑↑K ↑a ↑b + ↑t • supportingIntersection ↑↑L ↑a ↑b

The extreme face vertices and the intersections of supporting lines of a special cap are convex-linear along specialCapCombination: the underlying bodies interpolate, and both quantities are convex-linear in the body.

Cap / Special / Area Variation

theorem MovingSofa.specialCapArea_variation : (IsQuadraticFunctional specialCapCombination fun (K : SpecialCapSpace) => ClassicalResults.area ↑↑↑K) ∧ ∀ (K L : SpecialCapSpace), convexDirectionalDerivative specialCapCombination (fun (M : SpecialCapSpace) => ClassicalResults.area ↑↑↑M) K L = ∫ (t : Real.Angle) in (fun (s : ℝ) => ↑s) '' Set.Icc 0 Real.pi, supportValue (↑↑↑L) t - supportValue (↑↑↑K) t ∂surfaceAreaMeasure ↑↑K

Cap / Tail / Interpolation

def MovingSofa.IsCapTailCombination (t : ↑unitInterval) (X Y Z : CapTailSpace) : Prop

The cap and both tail bodies are the corresponding convex body combinations.

Equations

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

noncomputable def MovingSofa.capTailCombination (t : ↑unitInterval) (X Y : CapTailSpace) : CapTailSpace

Choose a cap-tail triple representing componentwise convex combination, with a fallback to X.

Equations

• MovingSofa.capTailCombination t X Y = if h : ∃ (Z : MovingSofa.CapTailSpace), MovingSofa.IsCapTailCombination t X Y Z then h.choose else X

theorem MovingSofa.capTail_isConvexDomain : (∀ (t : ↑unitInterval) (X Y : CapTailSpace), IsCapTailCombination t X Y (capTailCombination t X Y)) ∧ IsConvexDomain capTailCombination

Moving sofa: related mathematical developments

• Cap.InnerCornerVariation.
• Cap.CornerModuloLinear.
• Cap.Tail.AreaBounds.
• Cap.UpperBoundaryTracing.

The inner-corner variation on the middle window

On the middle window I = [φᴿ, φᴸ] the inner corner of a special cap is (h_K(t) - 1) • u_t + (h_K(t + π/2) - 1) • v_t, an affine expression in two support values, so it depends convex-linearly on the cap. capInnerCorner_variation pulls the quadratic curve-area functional back along that convex-linear map, which gives quadraticity of K ↦ 𝒥(x_K|_I) and reduces its directional derivative to the curve-variation formula.

The remaining work is to recognize the two mixed Stieltjes integrals of that formula as the pairing of the support increment against the corner measure. The inner corner is C¹ on the cap domain by the injectivity condition, so its Stieltjes measure is its classical velocity times Lebesgue measure; the frame identity planeCrossProduct_eq_inner_frame then turns the pointwise cross product into the corner density against the support increment, on I and on I + π/2 separately.

The middle window

Regularity of the inner corner of a special cap

The corner density on the two middle windows

Integrating against the corner angle measure

The middle Stieltjes integrals as weighted Lebesgue integrals

The variation of the inner corner

theorem MovingSofa.capInnerCorner_variation : IsConvexLinear specialCapCombination bvPathCombination capMiddleBV ∧ (IsQuadraticFunctional specialCapCombination fun (K : SpecialCapSpace) => curveAreaFunctional (capMiddleBV K)) ∧ ∀ (K L : SpecialCapSpace), convexDirectionalDerivative specialCapCombination (fun (M : SpecialCapSpace) => curveAreaFunctional (capMiddleBV M)) K L = ∫ (t : Real.Angle) in (fun (s : ℝ) => ↑s) '' (Set.Icc paperGerverConstants.2.1 paperGerverConstants.2.2 ∪ Set.Icc (Real.pi / 2 + paperGerverConstants.2.1) (Real.pi / 2 + paperGerverConstants.2.2)), supportValue (↑↑↑L) t - supportValue (↑↑↑K) t ∂capCornerAngleMeasure K + (segmentArea (distinguishedCapSides ↑K).2.corner (distinguishedCapSides ↑L).2.corner - segmentArea (distinguishedCapSides ↑K).1.corner (distinguishedCapSides ↑L).1.corner)

The outer corner and the two wedge segments, modulo convex-linear functionals

On the middle window I = [φᴿ, φᴸ] the outer corner of a cap is its inner corner translated by the K-independent frame sum c t = u_t + v_t, so the two curve-area functionals differ by the two mixed Stieltjes cross integrals, each convex-linear in K, plus the constant area of c.

The same happens at the two ends of the window: the tangent-line intersection point and the wedge endpoint differ by a fixed vector, as do the outer and the inner corner, so each of the two segment-area comparisons differs by a determinant that is affine in the support values and in the inner corner, hence convex-linear in K as well.

The outer corner path on the middle window

noncomputable def MovingSofa.frameSumBV (a b : ℝ) : ContinuousBVPaths a b

The frame sum t ↦ u_t + v_t, as a continuous path of bounded variation.

Equations

• MovingSofa.frameSumBV a b = MovingSofa.continuousBVOfContDiffOn (fun (t : ℝ) => MovingSofa.normalVector ↑t + MovingSofa.tangentVector ↑t) ⋯

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

The outer corner of a special cap on the middle window, as a continuous path of bounded variation: the inner-corner path translated by the frame sum.

Equations

• MovingSofa.capOuterMiddleBV K = MovingSofa.capMiddleBV K + MovingSofa.frameSumBV MovingSofa.paperGerverConstants.2.1 MovingSofa.paperGerverConstants.2.2

theorem MovingSofa.capOuterMiddleBV_val (K : SpecialCapSpace) (s : ↑(Set.Icc paperGerverConstants.2.1 paperGerverConstants.2.2)) : ↑(capOuterMiddleBV K) s = (rotatingHallwayParts ↑↑↑K ↑↑s).outerCorner

The outer middle path of a special cap traces the outer corner of its body.

The two end segments

The main equivalence

theorem MovingSofa.cornerArea_equivalent_modulo_linear : ∃ (F : SpecialCapSpace → ContinuousBVPaths paperGerverConstants.2.1 paperGerverConstants.2.2), (∀ (K : SpecialCapSpace), ↑(F K) = fun (t : ↑(Set.Icc paperGerverConstants.2.1 paperGerverConstants.2.2)) => (rotatingHallwayParts ↑↑↑K ↑↑t).outerCorner) ∧ (EquivalentModuloConvexLinear specialCapCombination (fun (K : SpecialCapSpace) => curveAreaFunctional (F K)) fun (K : SpecialCapSpace) => curveAreaFunctional (capMiddleBV K)) ∧ (EquivalentModuloConvexLinear specialCapCombination (fun (K : SpecialCapSpace) => segmentArea (supportingIntersection ↑↑K ↑paperGerverConstants.2.1 ↑(Real.pi / 2)) (rotatingHallwayParts ↑↑↑K ↑paperGerverConstants.2.1).outerCorner) fun (K : SpecialCapSpace) => segmentArea (distinguishedCapSides ↑K).1.fanPoint (distinguishedCapSides ↑K).1.corner) ∧ EquivalentModuloConvexLinear specialCapCombination (fun (K : SpecialCapSpace) => segmentArea (supportingIntersection ↑↑K ↑(Real.pi / 2) ↑(Real.pi / 2 + paperGerverConstants.2.2)) (rotatingHallwayParts ↑↑↑K ↑paperGerverConstants.2.2).outerCorner) fun (K : SpecialCapSpace) => segmentArea (distinguishedCapSides ↑K).2.fanPoint (distinguishedCapSides ↑K).2.corner

Cap / Tail / Area Bounds

theorem MovingSofa.canonicalTail_niche_area_lower_bounds (K : SpecialCapSpace) (B D : ConvexBody Point) (hB : ↑B = (canonicalTailSets K).1) (hD : ↑D = (canonicalTailSets K).2) : segmentArea (rightLeftTailArcs B D).1.startPoint (distinguishedCapSides ↑K).1.fanPoint - convexArcArea B (Real.pi + paperGerverConstants.2.1) (3 * Real.pi / 2) ≤ ClassicalResults.area (capNiche ↑K ∩ (distinguishedCapSides ↑K).1.upperHalfPlane) ∧ segmentArea (distinguishedCapSides ↑K).2.fanPoint (rightLeftTailArcs B D).2.endPoint - convexArcArea D (3 * Real.pi / 2) (3 * Real.pi / 2 + paperGerverConstants.2.2) ≤ ClassicalResults.area (capNiche ↑K ∩ (distinguishedCapSides ↑K).2.upperHalfPlane)

Tracing the area of a special cap along its upper boundary

The area of a convex body is half the integral of its support function against its surface area measure. For a special cap that measure is carried by the closed upper semicircle of normals, because the two open quarter arcs of lower normals carry degenerate faces (MovingSofa.CapSpace.surfaceAreaMeasure_image_Ioo_lower_eq_zero) and the bottom normal carries support value zero. The injectivity condition provides angular densities on the two upper quarter circles, so the four distinguished angles 0, φᴿ, φᴸ and π are not atoms, and the semicircle splits — up to a null set — into the four open arcs (0, φᴿ), (φᴿ, φᴸ), (φᴸ, π / 2), (π / 2, π) and the top normal π / 2. Each open arc is shorter than π, so the convex arc area formula applies to it, and the top normal contributes half the mass of a single atom (MovingSofa.HasCapDensities.area_eq_upper_arcs_add_top_atom). Evaluating the surface area measure at that fixed angle is convex-linear on the convex domain of special caps, whence the cap area agrees with the sum of the four arc areas modulo convex-linear functionals (MovingSofa.specialCapArea_equivalent_upper_arcs).

theorem MovingSofa.HasCapDensities.area_eq_upper_arcs_add_top_atom {C : RightAngleCapSpace} {dr dl : ℝ → NNReal} (hdens : HasCapDensities C dr dl) : ClassicalResults.area ↑↑C = convexArcArea (↑C) 0 paperGerverConstants.2.1 + convexArcArea (↑C) paperGerverConstants.2.1 paperGerverConstants.2.2 + convexArcArea (↑C) paperGerverConstants.2.2 (Real.pi / 2) + convexArcArea (↑C) (Real.pi / 2) Real.pi + ((surfaceAreaMeasure ↑C) {↑(Real.pi / 2)}).toReal / 2

Up to half the mass of the atom at its top normal, the area of a right-angle cap carrying angular densities is the sum of the areas of the four upper boundary arcs cut out by the two distinguished Gerver angles.

theorem MovingSofa.specialCapArea_equivalent_upper_arcs : EquivalentModuloConvexLinear specialCapCombination (fun (K : SpecialCapSpace) => ClassicalResults.area ↑↑↑K) fun (K : SpecialCapSpace) => convexArcArea (↑↑K) 0 paperGerverConstants.2.1 + convexArcArea (↑↑K) paperGerverConstants.2.1 paperGerverConstants.2.2 + convexArcArea (↑↑K) paperGerverConstants.2.2 (Real.pi / 2) + convexArcArea (↑↑K) (Real.pi / 2) Real.pi

Moving sofa: related mathematical developments

• Area.Mamikon.Middle.
• Area.Mamikon.TangentValues.
• Area.Mamikon.SofaConvex.
• Area.QVariation.

The middle Mamikon functional of a special cap

middleMamikon is the evaluated four-term Mamikon decomposition of the part of a special cap's niche cut out by the two straight tangent paths on [0, φᴿ] and [φᴸ, π / 2], the outer-corner arc on the middle window [φᴿ, φᴸ] and the terminal tangent path on [π / 2, π]. This module proves that it agrees with -upperBoundMiddle modulo convex-linear functionals of the cap.

The four summands already express their straight paths as endpoint segment areas, so the whole functional is a sum of eleven signed segment areas, one curve area and four convex arc areas. The four arc areas add up to the cap area modulo a convex-linear functional (specialCapArea_equivalent_upper_arcs), which supplies the -|K| of the upper bound. Of the eleven segments, five are convex-linear and therefore discarded (middleMamikon_segments_isConvexLinear): all their endpoints move convex-linearly with the cap and stay on the two fixed horizontal lines y = 0 and y = 1, the latter being the top supporting line, so no determinant of two moving coordinates ever appears. Two more pairs collapse at the two Gerver angles, where the extreme faces are singletons: at φᴿ the tangent-line intersection, the face and the outer corner are collinear, so the two segments merge (middleMamikon_segments_merge_right), and at φᴸ the tangent-line intersection is the outer corner, so the two segments cancel (middleMamikon_segments_cancel_left). What remains are exactly the three comparisons of cornerArea_equivalent_modulo_linear, the last of them reversed.

noncomputable def MovingSofa.straightMamikonValue (K : ConvexBody Point) (a b : ℝ) (p q : Point) : ℝ

The signed area between a convex boundary arc and the specified broken straight path.

Equations

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

noncomputable def MovingSofa.middleMamikon (K : SpecialCapSpace) : ℝ

The middle Mamikon functional constructed from the special cap’s hallway-corner geometry.

Equations

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

The singleton faces of a special cap and their positions

The convex-linear segments

The two collapsing pairs at the Gerver angles

The equivalence

theorem MovingSofa.middleMamikon_equivalent_neg_upperBoundMiddle : EquivalentModuloConvexLinear specialCapCombination middleMamikon fun (K : SpecialCapSpace) => -upperBoundMiddle K

Mamikon values of tangent-line chords

For a fixed tangent normal q, the tangent-line parametrization of a convex body is a continuous bounded-variation path, convex-linear in the body, each of whose values lies on the supporting line at its own path parameter. Mamikon convexity therefore makes the enclosed area straightMamikonValue a convex quadratic functional of the body, and the terminal case q = b does the same for tangentMamikonValue.

theorem MovingSofa.straightMamikon_quadratic_convex (t a b : ℝ) (ha : a ∈ Set.Ioc (t - Real.pi) t) (hb : b ∈ Set.Ioc (t - Real.pi) t) (hab : a < b) (hba : b < a + Real.pi) : (IsQuadraticFunctional convexBodyCombination fun (K : ConvexBody Point) => straightMamikonValue K a b (tangentLinePath K t ⟨a, ha⟩) (tangentLinePath K t ⟨b, hb⟩)) ∧ IsConvexFunctional convexBodyCombination (fun (K : ConvexBody Point) => straightMamikonValue K a b (tangentLinePath K t ⟨a, ha⟩) (tangentLinePath K t ⟨b, hb⟩)) false

The Mamikon value of a straight tangent-line chord is a convex quadratic functional of the body.

theorem MovingSofa.tangentMamikon_quadratic_convex (a b : ℝ) (hab : a < b) (hba : b < a + Real.pi) : (IsQuadraticFunctional convexBodyCombination fun (K : ConvexBody Point) => tangentMamikonValue K a b) ∧ IsConvexFunctional convexBodyCombination (fun (K : ConvexBody Point) => tangentMamikonValue K a b) false

The Mamikon value of a terminal tangent normal is a convex quadratic functional of the body.

Area / Mamikon / Sofa Convex

theorem MovingSofa.sofaMamikon_quadratic_convex : IsConvexFunctional specialCapCombination middleMamikon false ∧ IsQuadraticFunctional specialCapCombination middleMamikon ∧ IsConvexFunctional convexBodyCombination rightTailMamikon false ∧ IsQuadraticFunctional convexBodyCombination rightTailMamikon ∧ IsConvexFunctional convexBodyCombination leftTailMamikon false ∧ IsQuadraticFunctional convexBodyCombination leftTailMamikon

The directional derivative of the upper bound 𝒬

upperBoundQ is a signed sum of six area functionals of a cap-tail triple: the cap area, the two tail arc areas, the inner-corner curve area and the two areas of the segments joining a tail endpoint to the corresponding cap corner. Each summand is quadratic along the barycentric interpolation of cap-tail triples, so each segment function is differentiable at the base point with the summand's convexDirectionalDerivative as its derivative; adding those six derivatives computes the derivative of the segment function of 𝒬 itself.

Five of the twelve endpoint contributions cancel in pairs. The remaining two are the segment areas at the far ends of the two tails, and they vanish because the cap-tail constraints force the support value of both tails in the direction 3π/2 to be zero, so all four points involved lie on the horizontal axis. What survives is qVariationIntegral: the cap surface integral, the inner-corner integral, and the two tail integrals rewritten in opposite-angle coordinates.

noncomputable def MovingSofa.qVariationIntegral (X Y : CapTailSpace) : ℝ

The support-function variation integral for the cap and its two tail bodies.

Equations

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

theorem MovingSofa.upperBoundQ_variation (X Y : CapTailSpace) (hR : (rightLeftTailArcs X.rightBody X.leftBody).1.startPoint = (distinguishedCapSides ↑X.cap).1.corner) (hL : (rightLeftTailArcs X.rightBody X.leftBody).2.endPoint = (distinguishedCapSides ↑X.cap).2.corner) : convexDirectionalDerivative capTailCombination upperBoundQ X Y = qVariationIntegral X Y