IsCompact s ∧ (∃ (v : Point), s ⊆ (fun (p : Point) => p + v) '' (strips ω).1) ∧ (∃ (v : Point), s ⊆ (fun (p : Point) => p + v) '' (strips ω).2.2) ∧ (∀ t ∈ Set.Icc 0 ω, ∃ (v : Point), s ⊆ (fun (p : Point) => rotationMap (↑t) p + v) '' hallway) ∧ sSup ((fun (p : Point) => p.ofLp 1) '' s) - sInf ((fun (p : Point) => p.ofLp 1) '' s) ≤ 1 ∧ sSup ((fun (p : Point) => inner ℝ p (normalVector ↑ω)) '' s) - sInf ((fun (p : Point) => inner ℝ p (normalVector ↑ω)) '' s) ≤ 1 ∧ (IsStandardPosition s ω → s ⊆ (strips ω).1 ∩ (strips ω).2.2)

Motion / Compactness #

source

theorem MovingSofa.IsMovingSofa.isBounded {s : Set Point} {m : ↑unitInterval → Point ≃ᵃⁱ[ℝ ] Point} (h : IsMovingSofa s m) :

Bornology.IsBounded s

A set admitting a canonical hallway motion is bounded.

Motion / Rotation #

source

theorem MovingSofa.continuous_motion_linear_apply (m : ↑unitInterval → Point ≃ᵃⁱ[ℝ ] Point) (hm : Continuous m) (x : Point) :

Continuous fun (t : ↑unitInterval) => (m t).linearIsometryEquiv x

The linear part of a continuous rigid motion varies continuously on each vector.

source

theorem MovingSofa.motion_linear_det_pos (m : ↑unitInterval → Point ≃ᵃⁱ[ℝ ] Point) (hm : Continuous m) (hzero : m 0 = AffineIsometryEquiv.refl ℝ Point) (t : ↑unitInterval) :

0 < LinearMap.det ↑(m t).linearIsometryEquiv.toLinearEquiv

The linear parts of an identity-starting continuous rigid motion have positive determinant.

source

theorem MovingSofa.exists_motion_rotation (m : ↑unitInterval → Point ≃ᵃⁱ[ℝ ] Point) (hm : Continuous m) (hzero : m 0 = AffineIsometryEquiv.refl ℝ Point) (t : ↑unitInterval) :

∃ (θ : Real.Angle), ∀ (x : Point), (m t) x = rotationMap θ x + (m t) 0

Each placement of an identity-starting continuous rigid motion is a rotation and translation.

source

theorem MovingSofa.continuous_vaddConst_trans_rotation :

Continuous fun (q : Real.Angle × Point) => (AffineIsometryEquiv.vaddConst ℝ q.2).trans (EuclideanGeometry.o.rotation q.1).toAffineIsometryEquiv

Translation followed by a varying rotation depends continuously on both parameters.

source

theorem MovingSofa.continuous_rotation_trans_vaddConst {X : Type u_1} [TopologicalSpace X] {θ : X → Real.Angle} {c : X → Point} (hθ : Continuous θ) (hc : Continuous c) :

Continuous fun (x : X) => (EuclideanGeometry.o.rotation (θ x)).toAffineIsometryEquiv.trans (AffineIsometryEquiv.vaddConst ℝ (c x))

A continuously varying rotation about the origin followed by a continuously varying translation is a continuous family of rigid motions.

source

theorem MovingSofa.area_image_rotationMap (α : Real.Angle) (S : Set Point) :

ClassicalResults.area (rotationMap α '' S) = ClassicalResults.area S

Planar area is invariant under rotation about the origin, with no measurability hypothesis on the set.

Motion / Angle Lift #

source

theorem MovingSofa.exists_continuous_motion_angle_lift (m : ↑unitInterval → Point ≃ᵃⁱ[ℝ ] Point) (hm : Continuous m) (hzero : m 0 = AffineIsometryEquiv.refl ℝ Point) :

∃ (α : ↑unitInterval → ℝ) (p : ↑unitInterval → Point), Continuous α ∧ Continuous p ∧ α 0 = 0 ∧ p 0 = 0 ∧ ∀ (t : ↑unitInterval) (x : Point), (m t) x = rotationMap (↑(α t)) x + p t

An identity-starting continuous rigid motion has a normalized continuous real angle lift.

Motion / Rotation Angle Calculation #

source

@[reducible, inline]

abbrev MovingSofa.RotationCalculationAngle :

Set ℝ

The rotation-angle interval from arccos(5/11) up to, but excluding, π/2.

Equations

MovingSofa.RotationCalculationAngle = Set.Ico (Real.arccos (5 / 11)) (Real.pi / 2)

Instances For

source

noncomputable def MovingSofa.rotationCalculationMinimum (ω : ↑RotationCalculationAngle) :

ℝ

The piecewise lower cutoff on the auxiliary distance used in the rotation estimate.

Equations

MovingSofa.rotationCalculationMinimum ω = if ↑ω < Real.arctan (11 / 5) then 5 / 4 else 11 / 10

Instances For

source

noncomputable def MovingSofa.rotationCalculationValues (ω : ↑RotationCalculationAngle) (d : ↑(Set.Icc (rotationCalculationMinimum ω) (Real.tan ↑ω))) :

ℝ × ℝ × Point × Point

Auxiliary radii and points determined by an admissible rotation angle and distance.

Equations

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

Instances For

source

theorem MovingSofa.rotationCalculation_convex (d : ℝ) (hd : 1 ≤ d) :

(ConvexOn ℝ (Set.Icc (Real.pi / 4) (Real.pi / 2)) fun (t : ℝ) => (1 - d * (Real.cos t / Real.sin t)) ^ 2) ∧ ConvexOn ℝ (Set.Icc (Real.pi / 4) (Real.pi / 2)) fun (t : ℝ) => Real.cos t ^ 2

source

theorem MovingSofa.rotationCalculation_angle_bounds :

Real.pi / 4 < Real.arccos (5 / 11) ∧ Real.arccos (5 / 11) < Real.arctan (11 / 5) ∧ Real.arctan (11 / 5) < Real.pi / 2

The three landmark angles of the rotation calculation are strictly ordered: π / 4 < arccos (5 / 11) < arctan (11 / 5) < π / 2.

source

theorem MovingSofa.rotationCalculation_inequalities (ω : ↑RotationCalculationAngle) (d : ↑(Set.Icc (rotationCalculationMinimum ω) (Real.tan ↑ω))) (hr : 0 ≤ (rotationCalculationValues ω d).1) :

1 < inner ℝ ((rotationCalculationValues ω d).2.2.1 - ((stripParallelogram ↑ω).2.2 - tangentVector 0)) (normalVector ↑(Real.pi / 2 - ↑ω)) ∧ 1 < inner ℝ ((rotationCalculationValues ω d).2.2.2 - ((stripParallelogram ↑ω).2.2 - normalVector ↑↑ω)) (tangentVector ↑(Real.pi / 2 - ↑ω))

Motion / Supporting Hallways #

source

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

Point ≃ᵃⁱ[ℝ ] Point

The supporting placement regarded as an affine isometry equivalence.

Equations

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

Instances For

source

theorem MovingSofa.supportingPlacementEquiv_apply (s : Set Point) (t : Real.Angle) (p : Point) :

(supportingPlacementEquiv s t) p = supportingPlacement s t p

source

theorem MovingSofa.hasRotationAngle_of_subset_supportingHallways (s S : Set Point) (ω : ℝ) (hsne : s.Nonempty) (hscompact : IsCompact s) (hω : 0 ≤ ω) (hsω : supportValue s ↑ω = 1) (hsπ : supportValue s ↑(Real.pi / 2) = 1) (hSconn : IsConnected S) (hSclosed : IsClosed S) (hSsub : S ⊆ monotonization s ω) :

HasRotationAngle S ω

A closed connected subset of the supporting-hallway intersection inherits its clockwise hallway motion from the reference compact set.

Motion / Translation #

source

theorem MovingSofa.hasRotationAngle_image_add (s : Set Point) (v : Point) (ω : ℝ) (hs : HasRotationAngle s ω) :

HasRotationAngle ((fun (p : Point) => p + v) '' s) ω

Translating a sofa preserves each admitted rotation angle.

Motion / Standard Position #

source

theorem MovingSofa.exists_standardPosition_translation (s : Set Point) (ω : ℝ) (hs : HasRotationAngle s ω) (hω : ω ∈ Set.Ioc 0 (Real.pi / 2)) :

(∃ (v : Point), IsStandardPosition ((fun (p : Point) => p + v) '' s) ω) ∧ (∀ (v w : Point), IsStandardPosition ((fun (p : Point) => p + v) '' s) ω → IsStandardPosition ((fun (p : Point) => p + w) '' s) ω → (ω < Real.pi / 2 → v = w) ∧ (ω = Real.pi / 2 → v.ofLp 1 = w.ofLp 1)) ∧ (∀ (v : Point), IsStandardPosition ((fun (p : Point) => p + v) '' s) ω → ω = Real.pi / 2 → ∀ (a : ℝ), IsStandardPosition ((fun (p : Point) => p + (v + a • normalVector 0)) '' s) ω) ∧ ∀ (v : Point), IsStandardPosition ((fun (p : Point) => p + v) '' s) ω → (fun (p : Point) => p + v) '' s ⊆ (stripParallelogram ω).1

Bounds.WedgeContainment.

Bounds / Wedge Containment #

source

theorem MovingSofa.capWedge_subset_of_innerCorner_mem {ω : ℝ} (K : CapSpace ω) (t : ℝ) (ht : t ∈ Set.Ioo 0 ω) (hz : (rotatingHallwayParts ↑↑K ↑t).innerCorner ∈ ↑↑K) :

capWedge K t ⊆ ↑↑K

Cap.Balanced.
Cap.Clipped.Estimates.
Cap.Clipped.
Cap.Densities.
Cap.UpperBoundary.

Cap / Balanced #

source

noncomputable def MovingSofa.polygonAreaFunctional (Θ : AngleSet) (K : CapSpace Θ.angle) :

ℝ

The polygonal cap area minus the area of its polygonal niche.

Equations

MovingSofa.polygonAreaFunctional Θ K = MovingSofa.ClassicalResults.area (MovingSofa.angleCap Θ K) - MovingSofa.ClassicalResults.area (MovingSofa.polygonNiche Θ K)

Instances For

source

def MovingSofa.IsMaximumPolygonCap (Θ : AngleSet) (K : PolygonCapSpace Θ) :

Prop

A cap containing the distinguished fan point maximizes the polygonal area functional.

Equations

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

Instances For

source

def MovingSofa.IsBalancedMaximumCap {ω : ℝ} (K : CapSpace ω) :

Prop

The cap is a Hausdorff limit of polygonal maxima on increasingly fine dyadic meshes.

Equations

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

Instances For

Cap / Clipped / Estimates #

source

theorem MovingSofa.rotationCalculation_area_estimate (ω : ↑RotationCalculationAngle) :

1 / Real.cos ↑ω - (Real.tan ↑ω - rotationCalculationMinimum ω) ^ 2 * (Real.cos ↑ω / Real.sin ↑ω) < 11 / 5

source

theorem MovingSofa.rotationCalculationMinimum_pos (ω : ↑RotationCalculationAngle) :

0 < rotationCalculationMinimum ω

source

theorem MovingSofa.rotationCalculationMinimum_lt_tan (ω : ↑RotationCalculationAngle) :

rotationCalculationMinimum ω < Real.tan ↑ω

Cap / Clipped #

source

def MovingSofa.clippedCap (ω d : ℝ) :

Set Point

Clip the strip parallelogram by the two additional symmetric wall constraints.

Equations

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

Instances For

source

theorem MovingSofa.mem_clippedCap_iff (ω d : ℝ) (p : Point) :

p ∈ clippedCap ω d ↔ (0 ≤ p.ofLp 1 ∧ p.ofLp 1 ≤ 1) ∧ (0 ≤ Real.cos ω * p.ofLp 0 + Real.sin ω * p.ofLp 1 ∧ Real.cos ω * p.ofLp 0 + Real.sin ω * p.ofLp 1 ≤ 1) ∧ p.ofLp 0 ≤ d + Real.tan ((Real.pi / 2 - ω) / 2) ∧ -Real.sin ω * p.ofLp 0 + Real.cos ω * p.ofLp 1 ≤ d + Real.tan ((Real.pi / 2 - ω) / 2)

source

theorem MovingSofa.clippedCap_removed_pieces_disjoint {C S c d : ℝ} (hC : 0 < C) (hS : 0 ≤ S) (hd : 0 ≤ d) (hc : c * (1 + S) = C) :

Disjoint {p : Point | p.ofLp 1 ≤ 1 ∧ c + d < p.ofLp 0} {p : Point | c + d < -S * p.ofLp 0 + C * p.ofLp 1}

source

theorem MovingSofa.clippedCap_area_formula (ω d : ℝ) (hω : ω ∈ Set.Ioo 0 (Real.pi / 2)) (hd0 : 0 ≤ d) (hdt : d ≤ Real.tan ω) :

ClassicalResults.area (clippedCap ω d) = 1 / Real.cos ω - (Real.tan ω - d) ^ 2 * (Real.cos ω / Real.sin ω)

source

theorem MovingSofa.clippedCap_minimum_area (ω : ↑RotationCalculationAngle) :

ClassicalResults.area (clippedCap (↑ω) (rotationCalculationMinimum ω)) < 11 / 5

Cap / Densities #

source

theorem MovingSofa.HasCapDensities.surfaceAreaMeasure_singleton_eq_zero_of_mem_Ico {K : RightAngleCapSpace} {r s : ℝ → NNReal} (hK : HasCapDensities K r s) {t : ℝ} (ht : t ∈ Set.Ico 0 (Real.pi / 2)) :

(surfaceAreaMeasure ↑K) {↑t} = 0

A right-angle cap whose surface area measure has angular densities on the two upper quarter circles has no atom at a normal direction of the right upper quarter.

source

theorem MovingSofa.HasCapDensities.surfaceAreaMeasure_singleton_eq_zero_of_mem_Ioc {K : RightAngleCapSpace} {r s : ℝ → NNReal} (hK : HasCapDensities K r s) {t : ℝ} (ht : t ∈ Set.Ioc 0 (Real.pi / 2)) :

(surfaceAreaMeasure ↑K) {↑(t + Real.pi / 2)} = 0

A right-angle cap whose surface area measure has angular densities on the two upper quarter circles has no atom at a normal direction of the left upper quarter.

source

theorem MovingSofa.capDensities_contact_eq (K : RightAngleCapSpace) (hK : ∃ (r : ℝ → NNReal) (s : ℝ → NNReal), HasCapDensities K r s) :

(∀ t ∈ Set.Ico 0 (Real.pi / 2), (capVertices K t).1.1 = (capVertices K t).1.2 ∧ (tangentArmLengths K t).1.1 = (tangentArmLengths K t).1.2) ∧ ∀ t ∈ Set.Ioc 0 (Real.pi / 2), (capVertices K t).2.1 = (capVertices K t).2.2 ∧ (tangentArmLengths K t).2.1 = (tangentArmLengths K t).2.2

source

theorem MovingSofa.capDensities_edgeVertices_eq (K : RightAngleCapSpace) (hK : ∃ (r : ℝ → NNReal) (s : ℝ → NNReal), HasCapDensities K r s) {t : ℝ} (ht : t ∈ Set.Icc 0 Real.pi) (htop : t ≠ Real.pi / 2) :

(edgeVertices ↑K ↑t).1 = (edgeVertices ↑K ↑t).2

A right-angle cap carrying angular densities has singleton extreme faces at every upper normal direction except possibly the vertical one: the densities exclude atoms of the surface area measure on the two open quarter circles, so the corresponding faces have zero side length.

source

noncomputable def MovingSofa.nondegenerateCapData (K : RightAngleCapSpace) (_hK : ∃ (r : ℝ → NNReal) (s : ℝ → NNReal), HasCapDensities K r s) :

((↑(Set.Icc 0 (Real.pi / 2)) → Point) × (↑(Set.Icc 0 (Real.pi / 2)) → Point)) × (↑(Set.Icc 0 (Real.pi / 2)) → ℝ) × (↑(Set.Icc 0 (Real.pi / 2)) → ℝ)

The two cap contact paths and their scalar density functions on the quarter-turn interval.

Equations

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

Instances For

Cap / Upper Boundary #

source

def MovingSofa.capUpperBoundary {ω : ℝ} (K : CapSpace ω) :

Set Point

The union of exposed cap edges over the upper range of normal directions.

Equations

MovingSofa.capUpperBoundary K = ⋃ t ∈ Set.Icc 0 (ω + Real.pi / 2), MovingSofa.exposedEdge ↑K ↑t

Instances For

source

theorem MovingSofa.capUpperBoundary_connected {ω : ℝ} (K : CapSpace ω) :

IsConnected (capUpperBoundary K)

source

theorem MovingSofa.capUpperBoundary_relativeBoundary {ω : ℝ} (K : CapSpace ω) :

capUpperBoundary K = Subtype.val '' frontier {p : ↑(capFan ω) | ↑p ∈ ↑↑K}

Bounds.Niche.

Bounds / Niche #

source

noncomputable def MovingSofa.horizontalMin (S : Set Point) :

ℝ

The infimum of the set’s horizontal coordinates.

Equations

MovingSofa.horizontalMin S = sInf ((fun (p : MovingSofa.Point) => p.ofLp 0) '' S)

Instances For

source

noncomputable def MovingSofa.horizontalMax (S : Set Point) :

ℝ

The supremum of the set’s horizontal coordinates.

Equations

MovingSofa.horizontalMax S = sSup ((fun (p : MovingSofa.Point) => p.ofLp 0) '' S)

Instances For

source

def MovingSofa.HasNicheRectangleBounds (S N : Set Point) :

Prop

The niche is measurable, finite-area and enclosed by the specified horizontal-span rectangle.

Equations

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

Instances For

source

theorem MovingSofa.horizontalMin_le (K : ConvexBody Point) {p : Point} (hp : p ∈ K) :

horizontalMin ↑K ≤ p.ofLp 0

source

theorem MovingSofa.le_horizontalMax (K : ConvexBody Point) {p : Point} (hp : p ∈ K) :

p.ofLp 0 ≤ horizontalMax ↑K

source

theorem MovingSofa.horizontalMin_le_horizontalMax (K : ConvexBody Point) :

horizontalMin ↑K ≤ horizontalMax ↑K

source

theorem MovingSofa.supportValue_zero_eq_horizontalMax (S : Set Point) :

supportValue S ↑0 = horizontalMax S

The support value at the horizontal normal is the horizontal maximum.

source

theorem MovingSofa.supportValue_pi_eq_neg_horizontalMin (S : Set Point) :

supportValue S ↑Real.pi = -horizontalMin S

The support value at the straight angle negates the horizontal minimum.

source

theorem MovingSofa.exists_horizontal_extrema (K : ConvexBody Point) :

∃ (l : Point) (r : Point), l ∈ ↑K ∧ r ∈ ↑K ∧ l.ofLp 0 = horizontalMin ↑K ∧ r.ofLp 0 = horizontalMax ↑K

Both horizontal extrema of a compact convex body are attained.

source

theorem MovingSofa.CapSpace.mem_horizontalStrip {ω : ℝ} (K : CapSpace ω) {p : Point} (hp : p ∈ ↑K) :

0 ≤ p.ofLp 1 ∧ p.ofLp 1 ≤ 1

source

theorem MovingSofa.CapSpace.area_le_horizontalWidth {ω : ℝ} (K : CapSpace ω) :

ClassicalResults.area ↑↑K ≤ horizontalMax ↑↑K - horizontalMin ↑↑K

A cap has area at most its horizontal width.

source

theorem MovingSofa.CapSpace.supportValue_horizontal_bounds {ω t : ℝ} (K : CapSpace ω) (ht : t ∈ Set.Ioo 0 ω) :

supportValue ↑↑K ↑t ≤ Real.cos t * horizontalMax ↑↑K + Real.sin t ∧ supportValue ↑↑K ↑(t + Real.pi / 2) ≤ -Real.sin t * horizontalMin ↑↑K + Real.cos t

Upper support bounds from the horizontal extrema and the unit-height strip.

source

theorem MovingSofa.CapSpace.horizontal_le_supportValue {ω t : ℝ} (K : CapSpace ω) (hs : 0 ≤ Real.sin t) (hc : 0 ≤ Real.cos t) :

Real.cos t * horizontalMax ↑↑K ≤ supportValue ↑↑K ↑t ∧ -Real.sin t * horizontalMin ↑↑K ≤ supportValue ↑↑K ↑(t + Real.pi / 2)

Lower support bounds from the horizontal extrema and the nonnegative heights of a cap.

source

theorem MovingSofa.capNiche_subset_rectangle {ω : ℝ} (K : CapSpace ω) :

capNiche K ⊆ {p : Point | horizontalMin ↑↑K < p.ofLp 0 ∧ p.ofLp 0 < horizontalMax ↑↑K ∧ 0 ≤ p.ofLp 1 ∧ p.ofLp 1 < (horizontalMax ↑↑K - horizontalMin ↑↑K) / 2}

source

theorem MovingSofa.polygonNiche_subset_capNiche (Θ : AngleSet) (K : CapSpace Θ.angle) :

polygonNiche Θ K ⊆ capNiche K

source

theorem MovingSofa.measurableSet_capNiche {ω : ℝ} (K : CapSpace ω) :

MeasurableSet (capNiche K)

source

theorem MovingSofa.measurableSet_polygonNiche (Θ : AngleSet) (K : CapSpace Θ.angle) :

MeasurableSet (polygonNiche Θ K)

source

theorem MovingSofa.niche_uniform_bounds :

(∀ (ω : ℝ) (K : CapSpace ω), HasNicheRectangleBounds (↑↑K) (capNiche K)) ∧ (∀ (Θ : AngleSet) (K : CapSpace Θ.angle), HasNicheRectangleBounds (↑↑K) (polygonNiche Θ K)) ∧ ∀ (ω : ℕ → ℝ) (K : (i : ℕ) → CapSpace (ω i)) (L : ConvexBody Point), Filter.Tendsto (fun (i : ℕ) => Metric.hausdorffDist ↑↑(K i) ↑L) Filter.atTop (nhds 0) → ∃ (R : ℝ), 0 ≤ R ∧ (∀ (i : ℕ), capNiche (K i) ⊆ {p : Point | |p.ofLp 0| ≤ R ∧ 0 ≤ p.ofLp 1 ∧ p.ofLp 1 ≤ R}) ∧ ∀ (i : ℕ) (Θ : AngleSet) (P : CapSpace Θ.angle), ↑↑P = ↑↑(K i) → polygonNiche Θ P ⊆ {p : Point | |p.ofLp 0| ≤ R ∧ 0 ≤ p.ofLp 1 ∧ p.ofLp 1 ≤ R}

Geometry.ContactGeometry.

Geometry / Contact Geometry #

source

theorem MovingSofa.contact_oneSided_limits (K : ConvexBody Point) (t : ℝ) :

Filter.Tendsto (fun (s : ℝ) => (edgeVertices K ↑s).1) (nhdsWithin t (Set.Ioi t)) (nhds (edgeVertices K ↑t).1) ∧ Filter.Tendsto (fun (s : ℝ) => (edgeVertices K ↑s).2) (nhdsWithin t (Set.Ioi t)) (nhds (edgeVertices K ↑t).1) ∧ Filter.Tendsto (fun (s : ℝ) => supportingIntersection K ↑t ↑s) (nhdsWithin t (Set.Ioi t)) (nhds (edgeVertices K ↑t).1) ∧ Filter.Tendsto (fun (s : ℝ) => (edgeVertices K ↑s).1) (nhdsWithin t (Set.Iio t)) (nhds (edgeVertices K ↑t).2) ∧ Filter.Tendsto (fun (s : ℝ) => (edgeVertices K ↑s).2) (nhdsWithin t (Set.Iio t)) (nhds (edgeVertices K ↑t).2) ∧ Filter.Tendsto (fun (s : ℝ) => supportingIntersection K ↑s ↑t) (nhdsWithin t (Set.Iio t)) (nhds (edgeVertices K ↑t).2)

Both face endpoints and the supporting intersections have the stated one-sided limits.

Analysis.Stieltjes.ConvexBoundary.
Analysis.SurfaceMeasure.Polygon.
Analysis.SurfaceMeasure.BoundaryLimit.
Analysis.SurfaceMeasure.DiscreteBounds.
Analysis.SurfaceMeasure.Integrals.
Analysis.SurfaceMeasure.VertexBoundary.
Analysis.SurfaceMeasure.AngularDensity.
Analysis.SurfaceMeasure.FrameProducts.
Analysis.SurfaceMeasure.Boundary.
Analysis.SurfaceMeasure.Linearity.
Analysis.SurfaceMeasure.OppositeDensity.

Analysis / Stieltjes / Convex Boundary #

source

theorem MovingSofa.exists_positiveVertex_intervalBV (K : ConvexBody Point) {a b : ℝ} (hab : a ≤ b) :

∃ (f : Fin 2 → RightContinuousIntervalBV a b), ∀ (i : Fin 2) (t : ↑(Set.Icc a b)), (f i).toFun t = (edgeVertices K ↑↑t).1.ofLp i

Each coordinate of the positive vertex is right-continuous and has bounded variation on its closed interval domain.

source

theorem MovingSofa.measurable_positiveVertex_coordinate (K : ConvexBody Point) {a b : ℝ} (hab : a ≤ b) (i : Fin 2) :

Measurable fun (t : ↑(Set.Icc a b)) => (edgeVertices K ↑↑t).1.ofLp i

Each coordinate of the positive vertex is measurable on the closed parameter interval, being the difference of two monotone functions by bounded variation.

source

theorem MovingSofa.measurable_positiveVertex_coordinate_Ioc (K : ConvexBody Point) {a b : ℝ} (hab : a ≤ b) (i : Fin 2) :

Measurable fun (t : ↑(Set.Ioc a b)) => (edgeVertices K ↑↑t).1.ofLp i

Each coordinate of the positive vertex is measurable on the half-open parameter interval.

source

theorem MovingSofa.measurable_negativeVertex_coordinate (K : ConvexBody Point) {a b : ℝ} (hab : a ≤ b) (i : Fin 2) :

Measurable fun (t : ↑(Set.Ioc a b)) => (edgeVertices K ↑↑t).2.ofLp i

Each coordinate of the negative vertex is measurable on the half-open parameter interval, being the pointwise left limit of the positive vertex.

Analysis / Surface Measure / Polygon #

source

theorem MovingSofa.finite_orthogonalNormal_angles {p : Point} (hp : p ≠ 0) :

{t : Real.Angle | inner ℝ p (normalVector t) = 0}.Finite

A nonzero planar direction has only finitely many perpendicular angular normals.

source

theorem MovingSofa.finite_pairDifferenceNormal_angles (V : Finset Point) :

{t : Real.Angle | ∃ p ∈ V, ∃ q ∈ V, p ≠ q ∧ inner ℝ (p - q) (normalVector t) = 0}.Finite

The possible normals perpendicular to differences of points in a finite set are finite.

source

theorem MovingSofa.isExposed_exposedEdge (K : ConvexBody Point) (t : Real.Angle) :

IsExposed ℝ (↑K) (exposedEdge K t)

The support edge of a convex body is an exposed face.

source

theorem MovingSofa.edgeVertices_mem_of_eq_convexHull (K : ConvexBody Point) (V : Finset Point) (hKV : ↑K = (convexHull ℝ) ↑V) (t : Real.Angle) :

(edgeVertices K t).1 ∈ V ∧ (edgeVertices K t).2 ∈ V

Both endpoints of a polygon's exposed edge belong to its finite generating set.

source

theorem MovingSofa.finite_properEdgeNormal_angles (K : ConvexBody Point) (V : Finset Point) (hKV : ↑K = (convexHull ℝ) ↑V) :

{t : Real.Angle | (edgeVertices K t).1 ≠ (edgeVertices K t).2}.Finite

Every proper edge normal of a finite convex hull is one of finitely many pair normals.

source

theorem MovingSofa.eventuallyEq_positiveVertex_of_eq_convexHull (K : ConvexBody Point) (V : Finset Point) (hKV : ↑K = (convexHull ℝ) ↑V) (t : ℝ) (ht : (edgeVertices K ↑t).1 = (edgeVertices K ↑t).2) :

∀ᶠ (s : ℝ) in nhds t, (edgeVertices K ↑s).1 = (edgeVertices K ↑t).1

Away from a proper-edge normal, the positive vertex of a finite convex hull is locally constant.

source

theorem MovingSofa.surfaceAreaMeasure_compl_properEdgeNormals_eq_zero (K : ConvexBody Point) (V : Finset Point) (hKV : ↑K = (convexHull ℝ) ↑V) (hint : (interior ↑K).Nonempty) :

(surfaceAreaMeasure K) {t : Real.Angle | (edgeVertices K t).1 = (edgeVertices K t).2} = 0

For a two-dimensional finite convex hull, surface measure is supported on its finite set of proper-edge normals.

source

theorem MovingSofa.surfaceAreaMeasure_compl_properEdgeNormals_eq_zero_of_eq_convexHull (K : ConvexBody Point) (V : Finset Point) (hKV : ↑K = (convexHull ℝ) ↑V) :

(surfaceAreaMeasure K) {t : Real.Angle | (edgeVertices K t).1 = (edgeVertices K t).2} = 0

Surface measure of any finite convex hull, including a point or segment, is supported on its finite set of proper-edge normals.

source

theorem MovingSofa.surfaceAreaMeasure_compl_properEdgeNormals_eq_zero_of_finite_carrier (K : ConvexBody Point) (hN : {t : Real.Angle | (edgeVertices K t).1 ≠ (edgeVertices K t).2}.Finite) (V : Set Point) (hV : (MeasureTheory.Measure.hausdorffMeasure 1) V = 0) (hcarrier : ⋃ t ∈ {t : Real.Angle | (edgeVertices K t).1 = (edgeVertices K t).2}, exposedEdge K t ⊆ V) :

(surfaceAreaMeasure K) {t : Real.Angle | (edgeVertices K t).1 = (edgeVertices K t).2} = 0

Surface measure is carried by the proper edge normals as soon as these are finitely many and the degenerate faces lie in a one-dimensional null set.

source

theorem MovingSofa.integral_surfaceAreaMeasure_eq_sum_properEdgeNormals (K : ConvexBody Point) (V : Finset Point) (hKV : ↑K = (convexHull ℝ) ↑V) (φ : Real.Angle → ℝ) (E : Set Real.Angle) (hE : MeasurableSet E) :

∫ (t : Real.Angle) in E, φ t ∂surfaceAreaMeasure K = ∑ t ∈ ⋯.toFinset, (surfaceAreaMeasure K).real {t} * φ t

The surface integral of an arbitrary integrand over a finite convex hull is the sum of its proper-edge atoms, including the point and segment cases. No regularity of the integrand is needed: the measure is carried by a finite set.

source

theorem MovingSofa.integral_tangentCoordinate_surfaceAreaMeasure_eq_sum_properEdgeNormals (K : ConvexBody Point) (V : Finset Point) (hKV : ↑K = (convexHull ℝ) ↑V) (i : Fin 2) (E : Set Real.Angle) (hE : MeasurableSet E) :

∫ (t : Real.Angle) in E, (tangentVector t).ofLp i ∂surfaceAreaMeasure K = ∑ t ∈ ⋯.toFinset, (surfaceAreaMeasure K).real {t} * (tangentVector t).ofLp i

The coordinate tangent integral of a finite convex hull is the sum of its proper-edge atoms, including the point and segment cases.

source

theorem MovingSofa.intervalStieltjesMeasure_variation_eq_zero_off_properEdgeNormals (K : ConvexBody Point) (V : Finset Point) (hKV : ↑K = (convexHull ℝ) ↑V) {a b : ℝ} (hab : a < b) (f : Fin 2 → RightContinuousIntervalBV a b) (hf : ∀ (i : Fin 2) (t : ↑(Set.Icc a b)), (f i).toFun t = (edgeVertices K ↑↑t).1.ofLp i) (i : Fin 2) :

(MeasureTheory.VectorMeasure.variation (intervalStieltjesMeasure (f i))) {t : ↑(Set.Icc a b) | a < ↑t ∧ (edgeVertices K ↑↑t).1 = (edgeVertices K ↑↑t).2} = 0

On a real interval, the coordinate Stieltjes measure of a polygon's positive vertex is supported at proper-edge normals (apart from the excluded left endpoint).

source

theorem MovingSofa.leftLim_positiveVertex_coordinate (K : ConvexBody Point) {a b : ℝ} (f : Fin 2 → RightContinuousIntervalBV a b) (hf : ∀ (i : Fin 2) (t : ↑(Set.Icc a b)), (f i).toFun t = (edgeVertices K ↑↑t).1.ofLp i) (i : Fin 2) (t : ↑(Set.Icc a b)) (ht : a < ↑t) :

Function.leftLim (f i).toFun t = (edgeVertices K ↑↑t).2.ofLp i

The left limit of a positive-vertex coordinate at a noninitial parameter is the corresponding coordinate of the negative vertex.

source

theorem MovingSofa.intervalStieltjesMeasure_singleton_positiveVertex (K : ConvexBody Point) {a b : ℝ} (f : Fin 2 → RightContinuousIntervalBV a b) (hf : ∀ (i : Fin 2) (t : ↑(Set.Icc a b)), (f i).toFun t = (edgeVertices K ↑↑t).1.ofLp i) (i : Fin 2) (t : ↑(Set.Icc a b)) (ht : a < ↑t) :

(intervalStieltjesMeasure (f i)) {t} = ((surfaceAreaMeasure K) {↑↑t}).toReal * (tangentVector ↑↑t).ofLp i

Each noninitial Stieltjes atom of a positive-vertex coordinate is the corresponding coordinate of the tangent-weighted surface-measure atom.

source

theorem MovingSofa.finite_properEdgeNormal_lifts (K : ConvexBody Point) (V : Finset Point) (hKV : ↑K = (convexHull ℝ) ↑V) {a b : ℝ} (hturn : b ≤ a + 2 * Real.pi) :

{t : ↑(Set.Icc a b) | a < ↑t ∧ (edgeVertices K ↑↑t).1 ≠ (edgeVertices K ↑↑t).2}.Finite

A proper-edge normal has only finitely many lifts in a half-open interval of length at most one full turn.

source

theorem MovingSofa.intervalStieltjesMeasure_eq_sum_properEdgeNormals (K : ConvexBody Point) (V : Finset Point) (hKV : ↑K = (convexHull ℝ) ↑V) {a b : ℝ} (hab : a < b) (hturn : b ≤ a + 2 * Real.pi) (f : Fin 2 → RightContinuousIntervalBV a b) (hf : ∀ (i : Fin 2) (t : ↑(Set.Icc a b)), (f i).toFun t = (edgeVertices K ↑↑t).1.ofLp i) (i : Fin 2) (E : Set ↑(Set.Icc a b)) (hE : MeasurableSet E) (hEa : ∀ t ∈ E, a < ↑t) :

(intervalStieltjesMeasure (f i)) E = ∑ t ∈ ⋯.toFinset, ((surfaceAreaMeasure K) {↑↑t}).toReal * (tangentVector ↑↑t).ofLp i

On a polygon, every measurable noninitial set has Stieltjes mass equal to the finite sum of its proper-edge atoms.

source

theorem MovingSofa.integral_surfaceAreaMeasure_image_eq_sum_properEdgeNormal_lifts (K : ConvexBody Point) (V : Finset Point) (hKV : ↑K = (convexHull ℝ) ↑V) {a b : ℝ} (hturn : b ≤ a + 2 * Real.pi) (φ : Real.Angle → ℝ) (E : Set ↑(Set.Icc a b)) (hE : MeasurableSet E) (hEa : ∀ t ∈ E, a < ↑t) :

∫ (u : Real.Angle) in (fun (t : ↑(Set.Icc a b)) => ↑↑t) '' E, φ u ∂surfaceAreaMeasure K = ∑ t ∈ ⋯.toFinset, (surfaceAreaMeasure K).real {↑↑t} * φ ↑↑t

The surface integral of an arbitrary integrand over the angular image of a measurable interval set, as a finite sum indexed by the angular lifts carrying a proper edge. The left endpoint a is excluded from E so that each angle has at most one lift in E.

source

theorem MovingSofa.integral_tangentCoordinate_image_eq_sum_properEdgeNormal_lifts (K : ConvexBody Point) (V : Finset Point) (hKV : ↑K = (convexHull ℝ) ↑V) {a b : ℝ} (hturn : b ≤ a + 2 * Real.pi) (i : Fin 2) (E : Set ↑(Set.Icc a b)) (hE : MeasurableSet E) (hEa : ∀ t ∈ E, a < ↑t) :

∫ (u : Real.Angle) in (fun (t : ↑(Set.Icc a b)) => ↑↑t) '' E, (tangentVector u).ofLp i ∂surfaceAreaMeasure K = ∑ t ∈ ⋯.toFinset, ((surfaceAreaMeasure K) {↑↑t}).toReal * (tangentVector ↑↑t).ofLp i

The tangent-coordinate surface integral over the angular image of a measurable interval set is the same finite proper-edge sum as the positive-vertex Stieltjes measure.

source

theorem MovingSofa.positiveVertex_stieltjes_surface_of_eq_convexHull (K : ConvexBody Point) (V : Finset Point) (hKV : ↑K = (convexHull ℝ) ↑V) (a b : ℝ) (hab : a < b) (hturn : b ≤ a + 2 * Real.pi) :

∃ (f : Fin 2 → RightContinuousIntervalBV a b), (∀ (i : Fin 2) (t : ↑(Set.Icc a b)), (f i).toFun t = (edgeVertices K ↑↑t).1.ofLp i) ∧ ∀ (i : Fin 2) (E : Set ↑(Set.Icc a b)), MeasurableSet E → (∀ t ∈ E, a < ↑t) → (intervalStieltjesMeasure (f i)) E = ∫ (u : Real.Angle) in (fun (t : ↑(Set.Icc a b)) => ↑↑t) '' E, (tangentVector u).ofLp i ∂surfaceAreaMeasure K

Polygon case of the positive-vertex Stieltjes/surface-measure identity, including degenerate point and segment convex hulls.

source

theorem MovingSofa.positiveVertex_sub_eq_integral_of_eq_convexHull (K : ConvexBody Point) (V : Finset Point) (hKV : ↑K = (convexHull ℝ) ↑V) {a b : ℝ} (hab : a < b) (hturn : b ≤ a + 2 * Real.pi) (i : Fin 2) :

(edgeVertices K ↑b).1.ofLp i - (edgeVertices K ↑a).1.ofLp i = ∫ (u : Real.Angle) in (fun (t : ℝ) => ↑t) '' Set.Ioc a b, (tangentVector u).ofLp i ∂surfaceAreaMeasure K

The positive vertex increment of a polygon is the tangent-coordinate surface integral over the corresponding angular interval.

Analysis / Surface Measure / Boundary Limit #

source

theorem MovingSofa.positiveVertex_sub_eq_integral (K : ConvexBody Point) {a b : ℝ} (hab : a < b) (hturn : b ≤ a + 2 * Real.pi) (i : Fin 2) :

(edgeVertices K ↑b).1.ofLp i - (edgeVertices K ↑a).1.ofLp i = ∫ (u : Real.Angle) in (fun (t : ℝ) => ↑t) '' Set.Ioc a b, (tangentVector u).ofLp i ∂surfaceAreaMeasure K

The positive vertex increment is the tangent-coordinate surface integral over the corresponding half-open angular interval.

Analysis / Surface Measure / Discrete Bounds #

source

theorem MovingSofa.integral_tangentVector_surfaceAreaMeasure (K : ConvexBody Point) {a b : ℝ} (hab : a < b) (hturn : b ≤ a + 2 * Real.pi) :

∫ (u : Real.Angle) in (fun (t : ℝ) => ↑t) '' Set.Ioc a b, tangentVector u ∂surfaceAreaMeasure K = (edgeVertices K ↑b).1 - (edgeVertices K ↑a).1

The integral of tangent vectors gives the increment of the positive supporting vertex.

source

theorem MovingSofa.integral_inner_tangentVector_eq_support_sub (K : ConvexBody Point) {s : ℝ} (hs : s ∈ Set.Ioo 0 Real.pi) :

∫ (u : Real.Angle) in (fun (t : ℝ) => ↑t) '' Set.Ioc 0 s, inner ℝ (normalVector ↑s) (tangentVector u) ∂surfaceAreaMeasure K = supportValue ↑K ↑s - inner ℝ (normalVector ↑s) (edgeVertices K 0).1

The projected boundary integral computes the support value relative to the initial vertex.

source

theorem MovingSofa.sum_surfaceAreaMeasure_mul_pos_sin_le (K : ConvexBody Point) (D : Finset ℝ) (hD : ∀ t ∈ D, t ∈ Set.Ioo 0 Real.pi) {s : ℝ} (hs : s ∈ Set.Ioo 0 Real.pi) :

∑ t ∈ D, ((surfaceAreaMeasure K) {↑t}).toReal * max (Real.sin (s - t)) 0 ≤ supportValue ↑K ↑s - inner ℝ (normalVector ↑s) (edgeVertices K 0).1

Positive atomic sine contributions are bounded by the corresponding support increment.

source

theorem MovingSofa.inner_negativeVertex_zero_le_positiveVertex (K : ConvexBody Point) {s : ℝ} (hs : s ∈ Set.Icc 0 Real.pi) :

inner ℝ (normalVector ↑s) (edgeVertices K 0).2 ≤ inner ℝ (normalVector ↑s) (edgeVertices K 0).1

For upper normals, the negative zero-angle vertex projects below the positive vertex.

Analysis / Surface Measure / Integrals #

source

theorem MovingSofa.tangentArm_convolution (K : RightAngleCapSpace) (t : ℝ) :

(tangentArmLengths K t).2.1 = ∫ (u : Real.Angle) in (fun (s : ℝ) => ↑s) '' Set.Ioc t (t + Real.pi / 2), (u - ↑t).sin ∂surfaceAreaMeasure ↑K

Analysis / Surface Measure / Vertex Boundary #

source

theorem MovingSofa.positiveVertex_stieltjes_surface (K : ConvexBody Point) (a b : ℝ) (hab : a < b) (hturn : b ≤ a + 2 * Real.pi) :

Angular densities of the surface-area measure #

On an angular window of at most one turn the positive vertex of a convex body is a function of bounded variation whose Stieltjes measure, paired with the moving tangent, is the surface-area measure (sum_intervalStieltjesIntegral_positiveVertex_tangent). If on such a window the positive vertex happens to be a differentiable curve with derivative g s • tangentVector s, this identifies the surface-area measure with the Lebesgue density g.

This file records that identification (surfaceAreaMeasure_angleImage_eq_setLIntegral, surfaceAreaMeasure_angleImage_eq_withDensity_of_hasDerivAt), and the bookkeeping that glues finitely many or countably many such windows together (measure_angleImage_eq_of_union, measure_angleImage_eq_of_iUnion) and turns the resulting set-level identities into the Measure.restrict = Measure.map (Measure.withDensity …) form used by cap-density statements (measure_restrict_eq_map_withDensity, surfaceAreaMeasure_restrict_eq_map_withDensity, surfaceAreaMeasure_restrict_eq_map_add_withDensity).

The gluing lemmas are stated for an arbitrary pair of measures on Real.Angle and on ℝ, since they only use additivity and the injectivity of the angular projection on a window of at most one turn.

The surface measure of an arc with a differentiable positive vertex #

source

theorem MovingSofa.surfaceAreaMeasure_angleImage_eq_setLIntegral (K : ConvexBody Point) {a b : ℝ} (hab : a < b) (hturn : b ≤ a + 2 * Real.pi) (F : ℝ → Point) (g : ℝ → ℝ) (hF : ∀ (s : ℝ), HasDerivAt F (g s • tangentVector ↑s) s) (hg : Continuous g) (hgnn : ∀ s ∈ Set.Ioc a b, 0 ≤ g s) (hvertex : ∀ s ∈ Set.Icc a b, (edgeVertices K ↑s).1 = F s) {S : Set ℝ} (hS : MeasurableSet S) (hSsub : S ⊆ Set.Ioc a b) :

(surfaceAreaMeasure K) ((fun (s : ℝ) => ↑s) '' S) = ∫⁻ (s : ℝ) in S, ENNReal.ofReal (g s)

Suppose that on the angular window Ioc a b, of at most one turn, the positive vertex of K is traced by a curve F with derivative g s • tangentVector s, where g is continuous and nonnegative. Then the surface-area measure of the angular image of a measurable S ⊆ Ioc a b is the Lebesgue integral of g over S.

source

theorem MovingSofa.surfaceAreaMeasure_angleImage_eq_withDensity_of_hasDerivAt (K : ConvexBody Point) {a b : ℝ} (hab : a < b) (hturn : b ≤ a + 2 * Real.pi) (F : ℝ → Point) (g w : ℝ → ℝ) (hF : ∀ (s : ℝ), HasDerivAt F (g s • tangentVector ↑s) s) (hg : Continuous g) (hvertex : ∀ s ∈ Set.Icc a b, (edgeVertices K ↑s).1 = F s) (hw : ∀ s ∈ Set.Ioc a b, w s = g s) (hwnn : ∀ s ∈ Set.Ioc a b, 0 ≤ w s) (S : Set ℝ) (hS : MeasurableSet S) (hSsub : S ⊆ Set.Ioc a b) :

(surfaceAreaMeasure K) ((fun (s : ℝ) => ↑s) '' S) = (MeasureTheory.volume.withDensity fun (s : ℝ) => ENNReal.ofReal (w s)) S

The same identification as surfaceAreaMeasure_angleImage_eq_setLIntegral, phrased as agreement with a Measure.withDensity for any nonnegative weight w that agrees with the derivative factor g on the window.

Gluing angular density identities #

source

theorem MovingSofa.measure_angleImage_eq_of_union {μ : MeasureTheory.Measure Real.Angle} {ν : MeasureTheory.Measure ℝ} {c d : ℝ} (hturn : d ≤ c + 2 * Real.pi) {I J : Set ℝ} (hI : I ⊆ Set.Ioc c d) (hJ : J ⊆ Set.Ioc c d) (hImeas : MeasurableSet I) (hJmeas : MeasurableSet J) (hdisj : Disjoint I J) (hA : ∀ (S : Set ℝ), MeasurableSet S → S ⊆ I → μ ((fun (s : ℝ) => ↑s) '' S) = ν S) (hB : ∀ (S : Set ℝ), MeasurableSet S → S ⊆ J → μ ((fun (s : ℝ) => ↑s) '' S) = ν S) (S : Set ℝ) (hS : MeasurableSet S) (hSsub : S ⊆ I ∪ J) :

μ ((fun (s : ℝ) => ↑s) '' S) = ν S

Two measures that read one another through the angular projection on each of two disjoint measurable subsets of a window of at most one turn do so on their union.

source

theorem MovingSofa.measure_angleImage_eq_of_iUnion {μ : MeasureTheory.Measure Real.Angle} {ν : MeasureTheory.Measure ℝ} {J : ℕ → Set ℝ} (hmono : Monotone J) (hJmeas : ∀ (n : ℕ), MeasurableSet (J n)) (hA : ∀ (n : ℕ) (S : Set ℝ), MeasurableSet S → S ⊆ J n → μ ((fun (s : ℝ) => ↑s) '' S) = ν S) (S : Set ℝ) (hS : MeasurableSet S) (hSsub : S ⊆ ⋃ (n : ℕ), J n) :

μ ((fun (s : ℝ) => ↑s) '' S) = ν S

Two measures that read one another through the angular projection on each member of a monotone sequence of measurable sets do so on the union of that sequence.

From set-level identities to restricted measures #

source

theorem MovingSofa.measure_restrict_eq_map_withDensity {μ : MeasureTheory.Measure Real.Angle} {I : Set ℝ} {w : ℝ → ENNReal} (hImeas : MeasurableSet I) (hagree : ∀ (S : Set ℝ), MeasurableSet S → S ⊆ I → μ ((fun (s : ℝ) => ↑s) '' S) = (MeasureTheory.volume.withDensity w) S) :

μ.restrict ((fun (s : ℝ) => ↑s) '' I) = MeasureTheory.Measure.map (fun (s : ℝ) => ↑s) ((MeasureTheory.volume.restrict I).withDensity w)

A set-level angular density identity on a measurable parameter set I says exactly that the measure restricted to the angular image of I is the pushforward of the weighted Lebesgue measure on I.

source

theorem MovingSofa.surfaceAreaMeasure_restrict_eq_map_withDensity {K : ConvexBody Point} {I : Set ℝ} {w : ℝ → ENNReal} (hImeas : MeasurableSet I) (hagree : ∀ (S : Set ℝ), MeasurableSet S → S ⊆ I → (surfaceAreaMeasure K) ((fun (s : ℝ) => ↑s) '' S) = (MeasureTheory.volume.withDensity w) S) :

(surfaceAreaMeasure K).restrict ((fun (s : ℝ) => ↑s) '' I) = MeasureTheory.Measure.map (fun (s : ℝ) => ↑s) ((MeasureTheory.volume.restrict I).withDensity w)

The surface-area measure instance of measure_restrict_eq_map_withDensity.

source

theorem MovingSofa.surfaceAreaMeasure_restrict_eq_map_add_withDensity {K : ConvexBody Point} {c T : ℝ} {w : ℝ → ENNReal} (hagree : ∀ (S : Set ℝ), MeasurableSet S → S ⊆ Set.Ioc c (c + T) → (surfaceAreaMeasure K) ((fun (s : ℝ) => ↑s) '' S) = (MeasureTheory.volume.withDensity fun (u : ℝ) => w (u - c)) S) :

(surfaceAreaMeasure K).restrict ((fun (s : ℝ) => ↑s) '' Set.Ioc c (c + T)) = MeasureTheory.Measure.map (fun (t : ℝ) => ↑(t + c)) ((MeasureTheory.volume.restrict (Set.Ioc 0 T)).withDensity w)

The shifted form of surfaceAreaMeasure_restrict_eq_map_withDensity: an angular density identity on the translated window Ioc c (c + T) with the translated weight u ↦ w (u - c) says that the surface-area measure restricted to that angular arc is the pushforward of the w-weighted Lebesgue measure on Ioc 0 T along t ↦ ↑(t + c).

Analysis / Surface Measure / Frame Products #

source

theorem MovingSofa.exists_positiveVertex_frame_products (K : ConvexBody Point) {a b : ℝ} (hab : a < b) (hturn : b ≤ a + 2 * Real.pi) :

∃ (H : RightContinuousIntervalBV a b) (P : RightContinuousIntervalBV a b), (∀ (t : ↑(Set.Icc a b)), H.toFun t = inner ℝ (edgeVertices K ↑↑t).1 (normalVector ↑↑t)) ∧ (∀ (t : ↑(Set.Icc a b)), P.toFun t = inner ℝ (edgeVertices K ↑↑t).1 (tangentVector ↑↑t)) ∧ ∀ (E : Set ↑(Set.Icc a b)), MeasurableSet E → (∀ t ∈ E, a < ↑t) → (intervalStieltjesMeasure H) E = ∫ (t : ℝ) in Subtype.val '' E, inner ℝ (edgeVertices K ↑t).1 (tangentVector ↑t) ∧ (intervalStieltjesMeasure P) E = ((surfaceAreaMeasure K) ((fun (t : ↑(Set.Icc a b)) => ↑↑t) '' E)).toReal - ∫ (t : ℝ) in Subtype.val '' E, inner ℝ (edgeVertices K ↑t).1 (normalVector ↑t)

The normal and tangent projections of the positive vertex, with their Stieltjes measures.

Analysis / Surface Measure / Boundary #

source

theorem MovingSofa.positiveArm_stieltjes_surface (K : RightAngleCapSpace) :

∃ (f : RightContinuousIntervalBV 0 (Real.pi / 2)), (∀ (t : ↑(Set.Icc 0 (Real.pi / 2))), f.toFun t = (tangentArmLengths K ↑t).1.1) ∧ ∀ (E : Set ↑(Set.Icc 0 (Real.pi / 2))), MeasurableSet E → (∀ t ∈ E, 0 < ↑t) → (intervalStieltjesMeasure f) E = (∫ (t : ℝ) in (fun (s : ↑(Set.Icc 0 (Real.pi / 2))) => ↑s) '' E, (tangentArmLengths K t).2.1) - ((surfaceAreaMeasure ↑K) ((fun (s : ↑(Set.Icc 0 (Real.pi / 2))) => ↑↑s) '' E)).toReal

Analysis / Surface Measure / Linearity #

source

theorem MovingSofa.surfaceAreaMeasure_convexBodyCombination (t : ↑unitInterval) (K L : ConvexBody Point) :

surfaceAreaMeasure (convexBodyCombination t K L) = ENNReal.ofReal (1 - ↑t) • surfaceAreaMeasure K + ENNReal.ofReal ↑t • surfaceAreaMeasure L

Planar surface area measures commute with convex combinations.

Angular densities of the opposite surface measure #

The opposite surface measure (oppositeSurfaceData K).1 is the surface-area measure of K translated by π, so it reads the negative vertex data of K at the angle s as the positive vertex data at π + s. Transporting surfaceAreaMeasure_angleImage_eq_setLIntegral along that translation identifies it with a Lebesgue density whenever the positive vertex of K at normal π + s is traced by a differentiable curve F with derivative -(g s) • tangentVector s (oppositeSurfaceData_angleImage_eq_withDensity); the extra minus sign is exactly tangentVector_add_pi.

The two variants oppositeSurfaceData_angleImage_eq_withDensity_of_openLeft and …_of_openRight drop the vertex information at one endpoint of the window by exhausting the window from the other side with measure_angleImage_eq_of_iUnion.

source

theorem MovingSofa.oppositeSurfaceData_angleImage (K : ConvexBody Point) {S : Set ℝ} (hS : MeasurableSet ((fun (s : ℝ) => ↑s) '' S)) :

(oppositeSurfaceData K).1 ((fun (s : ℝ) => ↑s) '' S) = (surfaceAreaMeasure K) ((fun (s : ℝ) => ↑s) '' (fun (s : ℝ) => s + Real.pi) '' S)

The angular projection reads the opposite surface measure through the π-shifted window.

source

theorem MovingSofa.oppositeSurfaceData_angleImage_eq_withDensity (K : ConvexBody Point) {a b : ℝ} (hab : a < b) (hturn : b ≤ a + 2 * Real.pi) (F : ℝ → Point) (f g : ℝ → ℝ) (hF : ∀ (s : ℝ), HasDerivAt F (-g s • tangentVector ↑s) s) (hg : Continuous g) (hgnn : ∀ s ∈ Set.Ioc a b, 0 ≤ g s) (hfg : ∀ s ∈ Set.Ioo a b, f s = g s) (hvertex : ∀ s ∈ Set.Icc a b, (edgeVertices K ↑(Real.pi + s)).1 = F s) {S : Set ℝ} (hS : MeasurableSet S) (hSsub : S ⊆ Set.Ioc a b) :

(oppositeSurfaceData K).1 ((fun (s : ℝ) => ↑s) '' S) = (MeasureTheory.volume.withDensity fun (s : ℝ) => ENNReal.ofReal (f s)) S

Suppose that on the angular window (π + a, π + b], of at most one turn, the positive vertex of K at normal π + s is traced by a curve F with derivative -(g s) • v_s, where g is continuous and nonnegative. Then the opposite surface measure of the angular image of a measurable S ⊆ (a, b] is the weighted Lebesgue measure of S for any weight f agreeing with g on the open window.

source

theorem MovingSofa.oppositeSurfaceData_angleImage_eq_withDensity_of_openLeft (K : ConvexBody Point) {a b : ℝ} (hab : a < b) (hturn : b ≤ a + 2 * Real.pi) (F : ℝ → Point) (f g : ℝ → ℝ) (hF : ∀ (s : ℝ), HasDerivAt F (-g s • tangentVector ↑s) s) (hg : Continuous g) (hgnn : ∀ s ∈ Set.Ioc a b, 0 ≤ g s) (hfg : ∀ s ∈ Set.Ioo a b, f s = g s) (hvertex : ∀ s ∈ Set.Ioc a b, (edgeVertices K ↑(Real.pi + s)).1 = F s) {S : Set ℝ} (hS : MeasurableSet S) (hSsub : S ⊆ Set.Ioc a b) :

(oppositeSurfaceData K).1 ((fun (s : ℝ) => ↑s) '' S) = (MeasureTheory.volume.withDensity fun (s : ℝ) => ENNReal.ofReal (f s)) S

The variant of oppositeSurfaceData_angleImage_eq_withDensity whose left endpoint carries no vertex information: the window is exhausted from the right.

source

theorem MovingSofa.oppositeSurfaceData_angleImage_eq_withDensity_of_openRight (K : ConvexBody Point) {a b : ℝ} (hab : a < b) (hturn : b ≤ a + 2 * Real.pi) (F : ℝ → Point) (f g : ℝ → ℝ) (hF : ∀ (s : ℝ), HasDerivAt F (-g s • tangentVector ↑s) s) (hg : Continuous g) (hgnn : ∀ s ∈ Set.Ioo a b, 0 ≤ g s) (hfg : ∀ s ∈ Set.Ioo a b, f s = g s) (hvertex : ∀ s ∈ Set.Ico a b, (edgeVertices K ↑(Real.pi + s)).1 = F s) {S : Set ℝ} (hS : MeasurableSet S) (hSsub : S ⊆ Set.Ioo a b) :

(oppositeSurfaceData K).1 ((fun (s : ℝ) => ↑s) '' S) = (MeasureTheory.volume.withDensity fun (s : ℝ) => ENNReal.ofReal (f s)) S

The variant of oppositeSurfaceData_angleImage_eq_withDensity whose right endpoint carries no vertex information: the window is exhausted from the left.

Convex.SupportArea.
Convex.Linearity.
Convex.MixedArea.
Convex.TangentLinePath.

The area of a convex body as a support-function surface integral #

The planar area of a nonempty compact convex set is one half of the integral of its support function against its surface area measure. The identity is proved for finite convex hulls by fanning the polygon into triangles over an interior base point, and then transported to an arbitrary body by polygon approximation and weak convergence of surface measures. The same integral, taken with the two bodies decoupled, is convex-bilinear.

source

theorem MovingSofa.edgeVertices_fst_sub_snd_eq_dist_smul_tangentVector (K : ConvexBody Point) (t : Real.Angle) :

(edgeVertices K t).1 - (edgeVertices K t).2 = dist (edgeVertices K t).1 (edgeVertices K t).2 • tangentVector t

The ordered endpoints of an exposed edge differ by its length in the positive tangent direction.

source

theorem MovingSofa.supportIntegral_bilinear :

IsConvexBilinear convexBodyCombination convexBodyCombination realCombination fun (K L : ConvexBody Point) => 1 / 2 * ∫ (t : Real.Angle), supportValue (↑K) t ∂surfaceAreaMeasure L

The half support integral is convex-bilinear in the two body arguments.

source

theorem MovingSofa.tendsto_integral_supportValue_of_hausdorff_pair (P Q : ℕ → ConvexBody Point) (K L : ConvexBody Point) (hPK : Filter.Tendsto (fun (n : ℕ) => Metric.hausdorffDist ↑(P n) ↑K) Filter.atTop (nhds 0)) (hQL : Filter.Tendsto (fun (n : ℕ) => Metric.hausdorffDist ↑(Q n) ↑L) Filter.atTop (nhds 0)) :

Filter.Tendsto (fun (n : ℕ) => ∫ (u : Real.Angle), supportValue (↑(P n)) u ∂surfaceAreaMeasure (Q n)) Filter.atTop (nhds (∫ (u : Real.Angle), supportValue (↑K) u ∂surfaceAreaMeasure L))

The mixed support integral is Hausdorff continuous in the two bodies simultaneously.

source

theorem MovingSofa.tendsto_integral_supportValue_of_hausdorff (K : ℕ → ConvexBody Point) (L : ConvexBody Point) (hlim : Filter.Tendsto (fun (n : ℕ) => Metric.hausdorffDist ↑(K n) ↑L) Filter.atTop (nhds 0)) :

Filter.Tendsto (fun (n : ℕ) => ∫ (u : Real.Angle), supportValue (↑(K n)) u ∂surfaceAreaMeasure (K n)) Filter.atTop (nhds (∫ (u : Real.Angle), supportValue (↑L) u ∂surfaceAreaMeasure L))

The support integral of a body against its own surface measure is Hausdorff continuous.

source

theorem MovingSofa.integral_supportValue_surfaceAreaMeasure_eq_sum_edgeLength (K : ConvexBody Point) (V : Finset Point) (hKV : ↑K = (convexHull ℝ) ↑V) :

∫ (t : Real.Angle), supportValue (↑K) t ∂surfaceAreaMeasure K = ∑ t ∈ ⋯.toFinset, dist (edgeVertices K t).1 (edgeVertices K t).2 * supportValue (↑K) t

On a finite convex hull, each coefficient in the support sum is the corresponding edge length.

source

theorem MovingSofa.integral_tangentVector_surfaceAreaMeasure_eq_zero (K : ConvexBody Point) :

∫ (t : Real.Angle), tangentVector t ∂surfaceAreaMeasure K = 0

The total tangent vector of the surface-area measure vanishes.

source

theorem MovingSofa.exists_mem_properExposedEdge_of_mem_frontier (K : ConvexBody Point) (V : Finset Point) (hKV : ↑K = (convexHull ℝ) ↑V) (hK : (interior ↑K).Nonempty) {p : Point} (hp : p ∈ frontier ↑K) (hpV : p ∉ V) :

∃ (t : Real.Angle), (edgeVertices K t).1 ≠ (edgeVertices K t).2 ∧ p ∈ exposedEdge K t

Every non-generating boundary point of a two-dimensional finite convex hull lies on a proper exposed edge.

source

theorem MovingSofa.convexBody_area_support_integral_of_subsingleton (K : ConvexBody Point) (hK : (↑K).Subsingleton) :

ClassicalResults.area ↑K = 1 / 2 * ∫ (t : Real.Angle), supportValue (↑K) t ∂surfaceAreaMeasure K

The support-area identity holds for a singleton convex body.

source

theorem MovingSofa.convexBody_area_support_integral_of_segmentPresentation (K : ConvexBody Point) (d : Point × Point × Real.Angle) (hd : IsSegmentPresentation K d) :

ClassicalResults.area ↑K = 1 / 2 * ∫ (t : Real.Angle), supportValue (↑K) t ∂surfaceAreaMeasure K

The support-area identity holds for a nondegenerate segment presentation.

source

theorem MovingSofa.convexBody_area_support_integral_of_finiteHull (hpolygon : ∀ (P : ConvexBody Point) (V : Finset Point), V.Nonempty → ↑P = (convexHull ℝ) ↑V → ClassicalResults.area ↑P = 1 / 2 * ∫ (t : Real.Angle), supportValue (↑P) t ∂surfaceAreaMeasure P) (K : ConvexBody Point) :

ClassicalResults.area ↑K = 1 / 2 * ∫ (t : Real.Angle), supportValue (↑K) t ∂surfaceAreaMeasure K

The support-area identity for finite convex hulls extends to every convex body.

source

theorem MovingSofa.convexBody_area_support_integral_of_area_identity (harea : ∀ (K : ConvexBody Point), ClassicalResults.area ↑K = 1 / 2 * ∫ (t : Real.Angle), supportValue (↑K) t ∂surfaceAreaMeasure K) :

(∀ (K : ConvexBody Point), ClassicalResults.area ↑K = 1 / 2 * ∫ (t : Real.Angle), supportValue (↑K) t ∂surfaceAreaMeasure K) ∧ (IsConvexBilinear convexBodyCombination convexBodyCombination realCombination fun (K L : ConvexBody Point) => 1 / 2 * ∫ (t : Real.Angle), supportValue (↑K) t ∂surfaceAreaMeasure L) ∧ IsQuadraticFunctional convexBodyCombination fun (K : ConvexBody Point) => ClassicalResults.area ↑K

The area identity and the explicit support integral's bilinearity give quadraticity.

source

theorem MovingSofa.inner_eq_supportValue_of_mem_exposedEdge (K : ConvexBody Point) (t : Real.Angle) {p : Point} (hp : p ∈ exposedEdge K t) :

inner ℝ p (normalVector t) = supportValue (↑K) t

An exposed-edge point realizes the support value.

source

theorem MovingSofa.inner_lt_supportValue_of_mem_interior (K : ConvexBody Point) {o : Point} (ho : o ∈ interior ↑K) (t : Real.Angle) :

inner ℝ o (normalVector t) < supportValue (↑K) t

An interior base point lies strictly inside every supporting line.

source

theorem MovingSofa.edgeLength_mul_supportValue_sub_eq_planeCrossProduct (K : ConvexBody Point) (o : Point) (t : Real.Angle) :

dist (edgeVertices K t).1 (edgeVertices K t).2 * (supportValue (↑K) t - inner ℝ o (normalVector t)) = planeCrossProduct ((edgeVertices K t).2 - o) ((edgeVertices K t).1 - o)

Each exposed-edge summand is the oriented determinant of its triangle over the base point.

source

theorem MovingSofa.subsingleton_exposedEdge_inter (K : ConvexBody Point) {o : Point} (ho : o ∈ interior ↑K) {s t : Real.Angle} (hst : s ≠ t) :

(exposedEdge K s ∩ exposedEdge K t).Subsingleton

Distinct normal directions share at most one exposed-edge point.

source

theorem MovingSofa.integral_tangentCoordinate_surfaceAreaMeasure_eq_zero (K : ConvexBody Point) (i : Fin 2) :

∫ (t : Real.Angle), (tangentVector t).ofLp i ∂surfaceAreaMeasure K = 0

The coordinate tangent integral of a surface measure vanishes.

source

theorem MovingSofa.sum_edgeLength_mul_tangentCoordinate_eq_zero (K : ConvexBody Point) (V : Finset Point) (hKV : ↑K = (convexHull ℝ) ↑V) (i : Fin 2) :

∑ t ∈ ⋯.toFinset, dist (edgeVertices K t).1 (edgeVertices K t).2 * (tangentVector t).ofLp i = 0

The proper-edge lengths of a polygon weight its tangent coordinates to zero.

source

theorem MovingSofa.sum_edgeLength_mul_inner_normalVector_eq_zero (K : ConvexBody Point) (V : Finset Point) (hKV : ↑K = (convexHull ℝ) ↑V) (o : Point) :

∑ t ∈ ⋯.toFinset, dist (edgeVertices K t).1 (edgeVertices K t).2 * inner ℝ o (normalVector t) = 0

The proper-edge lengths of a polygon weight its normal directions to zero.

source

theorem MovingSofa.convexBody_area_support_integral_of_convexHull_interior (K : ConvexBody Point) (V : Finset Point) (hKV : ↑K = (convexHull ℝ) ↑V) (hint : (interior ↑K).Nonempty) :

ClassicalResults.area ↑K = 1 / 2 * ∫ (t : Real.Angle), supportValue (↑K) t ∂surfaceAreaMeasure K

The support-area identity for a polygon with interior, by fan triangulation.

source

theorem MovingSofa.convexBody_area_support_integral_of_convexHull (K : ConvexBody Point) (V : Finset Point) (hKV : ↑K = (convexHull ℝ) ↑V) :

ClassicalResults.area ↑K = 1 / 2 * ∫ (t : Real.Angle), supportValue (↑K) t ∂surfaceAreaMeasure K

The support-area identity for every finite convex hull.

Symmetry of the mixed support integral #

The mixed integral ∫ h_P dσ_Q of two finite convex hulls is computed by lifting the circle to (0, 2π] and indexing by the finite set F of lifts carrying a proper edge of P or of Q. The positive-vertex increment formula turns h_P into a partial sum along F, so the integral becomes a lower-triangular double sum ∑_{t ∈ F} ∑_{u ≤ t} α_u β_t sin (t - u), whose symmetry in (α, β) is Finset.sum_filter_le_add_sum_filter_le_swap together with the vanishing of the first trigonometric moments of the edge lengths. Polygon approximation transfers the identity to arbitrary convex bodies.

source

theorem MovingSofa.supportIntegral_symm_of_convexHull (P Q : ConvexBody Point) (VP VQ : Finset Point) (hP : ↑P = (convexHull ℝ) ↑VP) (hQ : ↑Q = (convexHull ℝ) ↑VQ) :

∫ (t : Real.Angle), supportValue (↑P) t ∂surfaceAreaMeasure Q = ∫ (t : Real.Angle), supportValue (↑Q) t ∂surfaceAreaMeasure P

Symmetry of the mixed support integral for finite convex hulls, including the degenerate point and segment cases.

source

theorem MovingSofa.supportIntegral_symm (K L : ConvexBody Point) :

∫ (t : Real.Angle), supportValue (↑K) t ∂surfaceAreaMeasure L = ∫ (t : Real.Angle), supportValue (↑L) t ∂surfaceAreaMeasure K

Symmetry of the mixed support integral for arbitrary planar convex bodies: ∫ h_K dσ_L = ∫ h_L dσ_K.

Convex / Linearity #

source

theorem MovingSofa.convexBody_maps_linear (t : ↑unitInterval) (K L : ConvexBody Point) :

(∀ (a : Real.Angle), supportValue (↑(convexBodyCombination t K L)) a = (1 - ↑t) * supportValue (↑K) a + ↑t * supportValue (↑L) a) ∧ (∀ (a : Real.Angle), (edgeVertices (convexBodyCombination t K L) a).1 = (1 - ↑t) • (edgeVertices K a).1 + ↑t • (edgeVertices L a).1 ∧ (edgeVertices (convexBodyCombination 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 (convexBodyCombination t K L) ↑a ↑b = (1 - ↑t) • supportingIntersection K ↑a ↑b + ↑t • supportingIntersection L ↑a ↑b) ∧ surfaceAreaMeasure (convexBodyCombination t K L) = ENNReal.ofReal (1 - ↑t) • surfaceAreaMeasure K + ENNReal.ofReal ↑t • surfaceAreaMeasure L

source

theorem MovingSofa.convexBody_area_support_integral :

(∀ (K : ConvexBody Point), ClassicalResults.area ↑K = 1 / 2 * ∫ (a : Real.Angle), supportValue (↑K) a ∂surfaceAreaMeasure K) ∧ (IsConvexBilinear convexBodyCombination convexBodyCombination realCombination fun (K L : ConvexBody Point) => 1 / 2 * ∫ (a : Real.Angle), supportValue (↑K) a ∂surfaceAreaMeasure L) ∧ IsQuadraticFunctional convexBodyCombination fun (K : ConvexBody Point) => ClassicalResults.area ↑K

The mixed area of two planar convex bodies #

The symmetry itself is MovingSofa.supportIntegral_symm in MovingSofa.Convex.SupportArea.

source

theorem MovingSofa.supportMeasure_mixedArea_symmetry (K L : ConvexBody Point) :

∫ (t : Real.Angle), supportValue (↑K) t ∂surfaceAreaMeasure L = ∫ (t : Real.Angle), supportValue (↑L) t ∂surfaceAreaMeasure K ∧ HasDerivWithinAt (segmentFunctional convexBodyCombination (fun (M : ConvexBody Point) => ClassicalResults.area ↑M) K L) (∫ (t : Real.Angle), supportValue (↑L) t - supportValue (↑K) t ∂surfaceAreaMeasure K) (Set.Icc 0 1) 0

Symmetry of the mixed support integral, together with the right derivative at 0 of the area along the Minkowski segment from K to L.

Convex / Tangent Line Path #

source

noncomputable def MovingSofa.tangentLinePath (K : ConvexBody Point) (t : ℝ) (s : ↑(Set.Ioc (t - Real.pi) t)) :

Point

Trace intersections with a fixed supporting line, ending at its exposed-edge endpoint.

Equations

MovingSofa.tangentLinePath K t s = if ↑s < t then MovingSofa.supportingIntersection K ↑↑s ↑t else (MovingSofa.edgeVertices K ↑t).2

Instances For

source

noncomputable def MovingSofa.tangentLineRestriction (K : ConvexBody Point) (t a b : ℝ) (ha : a ∈ Set.Ioc (t - Real.pi) t) (hb : b ∈ Set.Ioc (t - Real.pi) t) (s : ↑(Set.Icc a b)) :

Point

Restrict the tangent-line path to a closed interval of supporting directions.

Equations

MovingSofa.tangentLineRestriction K t a b ha hb s = MovingSofa.tangentLinePath K t ⟨↑s, ⋯⟩

Instances For

source

theorem MovingSofa.tangentLinePath_mem_supportingLine (K : ConvexBody Point) (t : ℝ) (s : ↑(Set.Ioc (t - Real.pi) t)) :

tangentLinePath K t s ∈ (supportingLineHalfPlane ↑K ↑↑s).1

Every value of a tangent-line path lies on the supporting line at its own path parameter.

source

theorem MovingSofa.tangentLinePath_segment_area (K : ConvexBody Point) (t a b : ℝ) (ha : a ∈ Set.Ioc (t - Real.pi) t) (hb : b ∈ Set.Ioc (t - Real.pi) t) (hab : a ≤ b) :

∃ (γ : ContinuousBVPaths a b), ↑γ = tangentLineRestriction K t a b ha hb ∧ Set.range ↑γ = segment ℝ (tangentLinePath K t ⟨a, ha⟩) (tangentLinePath K t ⟨b, hb⟩) ∧ Set.range ↑γ ⊆ (supportingLineHalfPlane ↑K ↑t).1 ∧ curveAreaFunctional γ = segmentArea (tangentLinePath K t ⟨a, ha⟩) (tangentLinePath K t ⟨b, hb⟩)

source

theorem MovingSofa.tangentLinePath_convexLinear (t a b : ℝ) (ha : a ∈ Set.Ioc (t - Real.pi) t) (hb : b ∈ Set.Ioc (t - Real.pi) t) (hab : a ≤ b) :

∃ (F : ConvexBody Point → ContinuousBVPaths a b), (∀ (K : ConvexBody Point), ↑(F K) = tangentLineRestriction K t a b ha hb) ∧ IsConvexLinear convexBodyCombination (fun (r : ↑unitInterval) (x y : ContinuousBVPaths a b) => (1 - ↑r) • x + ↑r • y) F

Convex.ArcCutBoundary.
Convex.ArcArea.
Convex.ArcBilinear.
Convex.ArcJordan.
Convex.ArcRegionArea.

Convex / Arc Cut Boundary #

source

theorem MovingSofa.frontier_eq_convexBoundaryArc_union_segment_of_cut (K K' : ConvexBody Point) (a b t : ℝ) (P Q : Point) (hat : a < t) (htb : t < b) (hba : b < a + Real.pi) (hP : P = (edgeVertices K ↑a).1) (hQ : Q = (edgeVertices K ↑b).2) (hleft : ∀ s ∈ Set.Ioc (t - Real.pi) a, exposedEdge K' ↑s = {P}) (hmiddle : ∀ s ∈ Set.Ioo a b, exposedEdge K' ↑s = exposedEdge K ↑s) (hright : ∀ s ∈ Set.Ico b (t + Real.pi), exposedEdge K' ↑s = {Q}) (hterminal : exposedEdge K' (↑t + ↑Real.pi) = segment ℝ Q P) (hInt : (interior ↑K').Nonempty) :

frontier ↑K' = convexBoundaryArc K a b ∪ segment ℝ P Q

The frontier of a cut body is the retained convex boundary arc together with its chord.

source

theorem MovingSofa.convexBoundaryArc_inter_segment_eq_endpoints_of_cut (K K' : ConvexBody Point) (a b t c : ℝ) (P Q : Point) (hat : a < t) (htb : t < b) (hba : b < a + Real.pi) (hPQ : P ≠ Q) (hPt : inner ℝ P (normalVector ↑t) = c) (hQt : inner ℝ Q (normalVector ↑t) = c) (hP : P = (edgeVertices K ↑a).1) (hQ : Q = (edgeVertices K ↑b).2) (hleft : ∀ s ∈ Set.Ioc (t - Real.pi) a, exposedEdge K' ↑s = {P}) (hmiddle : ∀ s ∈ Set.Ioo a b, exposedEdge K' ↑s = exposedEdge K ↑s) (hright : ∀ s ∈ Set.Ico b (t + Real.pi), exposedEdge K' ↑s = {Q}) (hterminal : exposedEdge K' (↑t + ↑Real.pi) = segment ℝ Q P) (hInt : (interior ↑K').Nonempty) :

convexBoundaryArc K a b ∩ segment ℝ P Q = {P, Q}

A retained convex boundary arc meets its cutting chord only at the endpoints.

source

theorem MovingSofa.exists_closedBVJordan_frontier_base_not_mem_chord (K : ConvexBody Point) (t : ℝ) (P Q : Point) (hInt : (interior ↑K).Nonempty) (hterminal : exposedEdge K (↑t + ↑Real.pi) = segment ℝ Q P) :

∃ (a : ℝ) (b : ℝ) (x : ContinuousBVPaths a b) (hab : a < b), IsOrientedJordanParametrization ⋯ (frontier ↑K) true ↑x ∧ ↑x ⟨a, ⋯⟩ ∉ segment ℝ P Q

A convex body admits a counterclockwise BV frontier parametrization based off a fixed face.

source

theorem MovingSofa.exists_rectifiableOrientedArc_convexBoundaryArc_of_cut (K K' : ConvexBody Point) (a b t c : ℝ) (P Q : Point) (hat : a < t) (htb : t < b) (hba : b < a + Real.pi) (hPQ : P ≠ Q) (hPt : inner ℝ P (normalVector ↑t) = c) (hQt : inner ℝ Q (normalVector ↑t) = c) (hP : P = (edgeVertices K ↑a).1) (hQ : Q = (edgeVertices K ↑b).2) (hleft : ∀ s ∈ Set.Ioc (t - Real.pi) a, exposedEdge K' ↑s = {P}) (hmiddle : ∀ s ∈ Set.Ioo a b, exposedEdge K' ↑s = exposedEdge K ↑s) (hright : ∀ s ∈ Set.Ico b (t + Real.pi), exposedEdge K' ↑s = {Q}) (hterminal : exposedEdge K' (↑t + ↑Real.pi) = segment ℝ Q P) (hInt : (interior ↑K').Nonempty) :

∃ (A : RectifiableOrientedArc), (↑A).carrier = convexBoundaryArc K a b ∧ (↑A).startPoint = P ∧ (↑A).endPoint = Q

The nonterminal boundary of a convex cut body realizes the corresponding convex boundary arc.

source

theorem MovingSofa.endpoint_of_exposedEdge_eq_singleton_of_eq_segment (K : ConvexBody Point) (x y P : Point) (s : Real.Angle) (hK : ↑K = segment ℝ x y) (hface : exposedEdge K s = {P}) :

x = P ∨ y = P

A singleton exposed face of a segment is one of its endpoints.

source

theorem MovingSofa.convexBoundaryArc_eq_segment_of_cut_interior_empty (K K' : ConvexBody Point) (a b t c : ℝ) (P Q : Point) (hat : a < t) (htb : t < b) (hba : b < a + Real.pi) (hPQ : P ≠ Q) (hPt : inner ℝ P (normalVector ↑t) = c) (hQt : inner ℝ Q (normalVector ↑t) = c) (hP : P = (edgeVertices K ↑a).1) (hQ : Q = (edgeVertices K ↑b).2) (hleft : ∀ s ∈ Set.Ioc (t - Real.pi) a, exposedEdge K' ↑s = {P}) (hmiddle : ∀ s ∈ Set.Ioo a b, exposedEdge K' ↑s = exposedEdge K ↑s) (hright : ∀ s ∈ Set.Ico b (t + Real.pi), exposedEdge K' ↑s = {Q}) (hInt : interior ↑K' = ∅) :

convexBoundaryArc K a b = segment ℝ P Q

A cut body with empty interior has its selected boundary arc equal to the endpoint segment.

Convex / Arc Area #

source

def MovingSofa.RealizesConvexArc (K : ConvexBody Point) (a b : ℝ) (Γ : RectifiableOrientedArc) :

Prop

An oriented rectifiable arc agrees with the prescribed convex boundary arc and its endpoints.

Equations

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

Instances For

source

noncomputable def MovingSofa.convexArcArea (K : ConvexBody Point) (a b : ℝ) :

ℝ

The signed area of a realization of the convex boundary arc, or zero if none exists.

Equations

MovingSofa.convexArcArea K a b = if h : ∃ (Γ : MovingSofa.RectifiableOrientedArc), MovingSofa.RealizesConvexArc K a b Γ then MovingSofa.jordanArcArea h.choose else 0

Instances For

source

theorem MovingSofa.convexArcArea_eq_jordanArcArea_of_realizes {K : ConvexBody Point} {a b : ℝ} {Γ : RectifiableOrientedArc} (hΓ : RealizesConvexArc K a b Γ) :

convexArcArea K a b = jordanArcArea Γ

Every realization of a convex boundary arc computes that arc's signed area.

source

theorem MovingSofa.convexArcArea_eq_curveAreaFunctional_of_realizes {K : ConvexBody Point} {a b : ℝ} {Γ : OrientedJordanArc} (p : ArcBVParametrization Γ) (hΓ : RealizesConvexArc K a b ⟨Γ, ⋯⟩) :

convexArcArea K a b = curveAreaFunctional p.path

Any bounded-variation parametrization of a convex boundary arc computes that arc's signed area.

source

theorem MovingSofa.convexArcArea_eq_curveAreaFunctional_of_injOn {K : ConvexBody Point} {α β a b : ℝ} {f : ℝ → Point} (x : ContinuousBVPaths a b) (hab : a < b) (hx : ∀ (t : ↑(Set.Icc a b)), ↑x t = f ↑t) (hinj : Set.InjOn f (Set.Icc a b)) (himage : f '' Set.Icc a b = convexBoundaryArc K α β) (hstart : f a = (edgeVertices K ↑α).1) (hend : f b = (edgeVertices K ↑β).2) :

convexArcArea K α β = curveAreaFunctional x

A continuous bounded-variation path on [a, b] that traces a convex boundary arc injectively, from the arc's first vertex to its last, computes that arc's signed area.

source

theorem MovingSofa.convexArcIntegral_bilinear (a b : ℝ) :

IsConvexBilinear convexBodyCombination convexBodyCombination realCombination fun (K L : ConvexBody Point) => 1 / 2 * ∫ (t : Real.Angle) in (fun (s : ℝ) => ↑s) '' Set.Ioo a b, supportValue (↑K) t ∂surfaceAreaMeasure L

The half support integral against a surface measure is convex-bilinear in the pair of bodies, by convex-linearity of support functions and surface measures.

source

theorem MovingSofa.convexArc_area (a b : ℝ) (hab : a < b) (hba : b < a + Real.pi) :

(∀ (K : ConvexBody Point), ∃ (Γ : RectifiableOrientedArc), RealizesConvexArc K a b Γ ∧ convexArcArea K a b = jordanArcArea Γ ∧ ((↑Γ).startPoint = (↑Γ).endPoint → (↑Γ).carrier = {(↑Γ).startPoint})) ∧ (∀ (K : ConvexBody Point), convexArcArea K a b = (∫ (t : Real.Angle) in (fun (s : ℝ) => ↑s) '' Set.Ioo a b, supportValue (↑K) t ∂surfaceAreaMeasure K) / 2) ∧ IsQuadraticFunctional convexBodyCombination fun (K : ConvexBody Point) => convexArcArea K a b

Convex / Arc Bilinear #

source

noncomputable def MovingSofa.openIntervalCrossIntegral {a b : ℝ} (f : Fin 2 → RightContinuousIntervalBV a b) (g : ↑(Set.Icc a b) → Point) :

ℝ

Half the coordinate cross Stieltjes integral over the open parameter interval.

Equations

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

Instances For

source

theorem MovingSofa.convexArc_bilinear_computation (a b : ℝ) (hab : a < b) (hba : b < a + Real.pi) :

(IsConvexBilinear convexBodyCombination convexBodyCombination realCombination fun (K L : ConvexBody Point) => 1 / 2 * ∫ (t : Real.Angle) in (fun (s : ℝ) => ↑s) '' Set.Ioo a b, supportValue (↑K) t ∂surfaceAreaMeasure L) ∧ ∃ (F : ConvexBody Point → Fin 2 → RightContinuousIntervalBV a b), (∀ (K : ConvexBody Point) (i : Fin 2) (t : ↑(Set.Icc a b)), (F K i).toFun t = (edgeVertices K ↑↑t).1.ofLp i) ∧ (∀ (K L : ConvexBody Point), (1 / 2 * ∫ (t : Real.Angle) in (fun (s : ℝ) => ↑s) '' Set.Ioo a b, supportValue (↑K) t ∂surfaceAreaMeasure L = openIntervalCrossIntegral (F L) fun (t : ↑(Set.Icc a b)) => (edgeVertices K ↑↑t).1) ∧ 1 / 2 * ∫ (t : Real.Angle) in (fun (s : ℝ) => ↑s) '' Set.Ioo a b, supportValue (↑K) t ∂surfaceAreaMeasure L = openIntervalCrossIntegral (F L) fun (t : ↑(Set.Icc a b)) => (edgeVertices K ↑↑t).2) ∧ ∀ (K : ConvexBody Point), convexArcArea K a b = openIntervalCrossIntegral (F K) fun (t : ↑(Set.Icc a b)) => (edgeVertices K ↑↑t).1

source

theorem MovingSofa.openIntervalCrossIntegral_antisymm {a b : ℝ} (hab : a < b) (K L : ConvexBody Point) (FK FL : Fin 2 → RightContinuousIntervalBV a b) (hFK : ∀ (i : Fin 2) (t : ↑(Set.Icc a b)), (FK i).toFun t = (edgeVertices K ↑↑t).1.ofLp i) (hFL : ∀ (i : Fin 2) (t : ↑(Set.Icc a b)), (FL i).toFun t = (edgeVertices L ↑↑t).1.ofLp i) :

((openIntervalCrossIntegral FL fun (t : ↑(Set.Icc a b)) => (edgeVertices K ↑↑t).2) - openIntervalCrossIntegral FK fun (t : ↑(Set.Icc a b)) => (edgeVertices L ↑↑t).1) = segmentArea (edgeVertices K ↑b).2 (edgeVertices L ↑b).2 - segmentArea (edgeVertices K ↑a).1 (edgeVertices L ↑a).1

Antisymmetry of the vertex cross Stieltjes integral over the open interval, up to the two endpoint corrections: the negative vertices at b and the positive vertices at a.

Convex / Arc Jordan #

source

def MovingSofa.IsSegmentTraversal (γ : RectifiablePathData) (P Q : Point) :

Prop

A rectifiable path traverses a segment with monotone surjective reparametrizations.

Equations

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

Instances For

source

def MovingSofa.IsReverseArcTraversal (γ : RectifiablePathData) {A : OrientedJordanArc} (p : ArcBVParametrization A) :

Prop

A rectifiable path traverses an oriented Jordan arc in reverse.

Equations

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

Instances For

source

theorem MovingSofa.IsSegmentTraversal.curveAreaFunctional_eq {γ : RectifiablePathData} {P Q : Point} (h : IsSegmentTraversal γ P Q) :

curveAreaFunctional γ.path = segmentArea P Q

A path traversing an oriented segment has the segment's signed area.

source

theorem MovingSofa.IsReverseArcTraversal.curveAreaFunctional_eq {γ : RectifiablePathData} {A : OrientedJordanArc} {p : ArcBVParametrization A} (h : IsReverseArcTraversal γ p) :

curveAreaFunctional γ.path = -curveAreaFunctional p.path

A path traversing an oriented Jordan arc backwards has the opposite signed area.

source

theorem MovingSofa.convexBoundaryArc_subset_body (K : ConvexBody Point) (a b : ℝ) :

convexBoundaryArc K a b ⊆ ↑K

A convex boundary arc lies in its convex body.

source

theorem MovingSofa.jordanInterior_subset_of_subset_closed_convex {Γ C : Set Point} (hΓ : Γ.Nonempty) (hsub : Γ ⊆ C) (hconv : Convex ℝ C) (hclosed : IsClosed C) :

jordanInterior Γ ⊆ C

The region enclosed by a loop inside a closed convex set stays inside that set.

source

theorem MovingSofa.convexBoundaryArc_jordan (K : ConvexBody Point) (a b : ℝ) (hab : a < b) (hba : b < a + Real.pi) (hne : (edgeVertices K ↑a).1 ≠ (edgeVertices K ↑b).2) :

∃ (A : RectifiableOrientedArc) (p : ArcBVParametrization ↑A) (γ : RectifiablePathData) (pieces : Fin 3 → RectifiablePathData), RealizesConvexArc K a b A ∧ IsSegmentTraversal (pieces 0) (edgeVertices K ↑a).1 (supportingIntersection K ↑a ↑b) ∧ IsSegmentTraversal (pieces 1) (supportingIntersection K ↑a ↑b) (edgeVertices K ↑b).2 ∧ IsReverseArcTraversal (pieces 2) p ∧ IsPathConcatenation γ pieces ∧ IsOrientedJordanParametrization ⋯ (Set.range ↑γ.path) true ↑γ.path ∧ jordanInterior (Set.range ↑γ.path) ⊆ interior ((supportingLineHalfPlane ↑K ↑a).2 ∩ (supportingLineHalfPlane ↑K ↑b).2) ∧ Disjoint (jordanInterior (Set.range ↑γ.path)) (⋂ t ∈ Set.Icc a b, (supportingLineHalfPlane ↑K ↑t).2)

The supporting segments and reversed convex boundary arc form a counterclockwise Jordan curve.

Area of the region between a convex arc and its supporting tangents #

The loop built from a convex boundary arc and the two tangent segments meeting at the intersection of the arc's endpoint supporting lines bounds the "Mamikon region" cut off by those tangents. The single result here bounds that region's signed area by the measure of any set that receives it.

source

theorem MovingSofa.convexArc_tangentRegion_area_le (B : ConvexBody Point) (a b : ℝ) (hab : a < b) (hba : b < a + Real.pi) {C : Set Point} (hconv : Convex ℝ C) (hclosed : IsClosed C) (hBC : ↑B ⊆ C) (hOC : supportingIntersection B ↑a ↑b ∈ C) {E : Set Point} (hE : MeasureTheory.volume E ≠ ⊤) (hsubE : ∀ q ∈ interior ((supportingLineHalfPlane ↑B ↑a).2 ∩ (supportingLineHalfPlane ↑B ↑b).2), q ∈ C → q ∉ ↑B → q ∈ E) :

segmentArea (edgeVertices B ↑a).1 (supportingIntersection B ↑a ↑b) + segmentArea (supportingIntersection B ↑a ↑b) (edgeVertices B ↑b).2 - convexArcArea B a b ≤ ClassicalResults.area E

The region between a convex boundary arc and its two supporting tangent segments has area at most that of any finite-measure set that receives every point of a closed convex carrier of the body which lies inside both endpoint supporting half-planes but outside the body.

Area.Mamikon.Basic.
Area.Variation.

Area / Mamikon / Basic #

source

noncomputable def MovingSofa.mamikonFunctional (K : ConvexBody Point) (a b : ℝ) (hab : a < b) (_hba : b < a + Real.pi) (z : ContinuousBVPaths a b) (_hz : ∀ (t : ↑(Set.Icc a b)), ↑z t ∈ (supportingLineHalfPlane ↑K ↑↑t).1) :

ℝ

The signed area between the convex boundary arc and a path on its supporting lines.

Equations

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

Instances For

Area / Variation #

source

def MovingSofa.pointPairCombination (t : ↑unitInterval) (x y : Point × Point) :

Point × Point

Coordinatewise convex combination of two pairs of planar points.

Equations

MovingSofa.pointPairCombination t x y = ((1 - ↑t) • x.1 + ↑t • y.1, (1 - ↑t) • x.2 + ↑t • y.2)

Instances For

source

theorem MovingSofa.segmentArea_variation :

(IsQuadraticFunctional pointPairCombination fun (x : Point × Point) => segmentArea x.1 x.2) ∧ ∀ (p q p' q' : Point), convexDirectionalDerivative pointPairCombination (fun (x : Point × Point) => segmentArea x.1 x.2) (p, q) (p', q') = (planeCrossProduct (p' + q') (q - p) - 2 * planeCrossProduct p q) / 2 + (segmentArea q q' - segmentArea p p')

source

def MovingSofa.bvPathCombination {a b : ℝ} (t : ↑unitInterval) (x y : ContinuousBVPaths a b) :

ContinuousBVPaths a b

The pointwise convex combination of two continuous BV paths.

Equations

MovingSofa.bvPathCombination t x y = (1 - ↑t) • x + ↑t • y

Instances For

source

theorem MovingSofa.curveArea_variation (a b : ℝ) (hab : a ≤ b) :

IsQuadraticFunctional bvPathCombination curveAreaFunctional ∧ ∀ (x y : ContinuousBVPaths a b), convexDirectionalDerivative bvPathCombination curveAreaFunctional x y = intervalStieltjesIntegral (continuousBVCoordinate x 1) (fun (t : ↑(Set.Icc a b)) => (↑y t).ofLp 0 - (↑x t).ofLp 0) Set.univ - intervalStieltjesIntegral (continuousBVCoordinate x 0) (fun (t : ↑(Set.Icc a b)) => (↑y t).ofLp 1 - (↑x t).ofLp 1) Set.univ + (segmentArea (↑x ⟨b, ⋯⟩) (↑y ⟨b, ⋯⟩) - segmentArea (↑x ⟨a, ⋯⟩) (↑y ⟨a, ⋯⟩))

source

theorem MovingSofa.curveArea_translation_convexLinear {a b : ℝ} (c : ContinuousBVPaths a b) :

IsConvexLinear bvPathCombination realCombination fun (x : ContinuousBVPaths a b) => curveAreaFunctional (x + c) - curveAreaFunctional x

Translating a continuous BV path by a fixed one changes its signed area by a convex-linear functional of the path: the two mixed Stieltjes cross integrals are separately linear and the translating path's own area is constant.

source

theorem MovingSofa.convexArcArea_variation (a b : ℝ) (hab : a < b) (hba : b < a + Real.pi) :

(IsQuadraticFunctional convexBodyCombination fun (K : ConvexBody Point) => convexArcArea K a b) ∧ ∀ (K L : ConvexBody Point), convexDirectionalDerivative convexBodyCombination (fun (M : ConvexBody Point) => convexArcArea M a b) K L = ∫ (t : Real.Angle) in (fun (s : ℝ) => ↑s) '' Set.Ioo a b, supportValue (↑L) t - supportValue (↑K) t ∂surfaceAreaMeasure K + (segmentArea (edgeVertices K ↑b).2 (edgeVertices L ↑b).2 - segmentArea (edgeVertices K ↑a).1 (edgeVertices L ↑a).1)

Optimality from the area upper bound #

AreaUpperBound says that no moving sofa has larger area than Gerver's sofa. Since Gerver's sofa is itself a moving sofa, the bound gives sofaConstant = volume gerversSofa.

source

def MovingSofa.AreaUpperBound :

Prop

Every moving sofa has area at most that of Gerver's sofa. This is the upper bound proved in Baek's paper; together with the fact that Gerver's sofa is a moving sofa it gives optimality.

Equations