Monotonicity of the Hausdorff perimeter

For compact convex bodies K ⊆ L in the plane, μH[1] (frontier K) ≤ μH[1] (frontier L).

The proof uses the nearest-point projection nearestPoint K, which is 1-Lipschitz: every boundary point of K is the image of a boundary point of L (push the boundary point of K outwards along a supporting direction until it hits the boundary of L), so frontier K ⊆ nearestPoint K '' frontier L, and Lipschitz maps do not increase the one-dimensional Hausdorff measure.

theorem HumanVerification.CauchyCrofton.exists_supporting_direction (K : Body) {x : Point2} (hx : x ∈ frontier K.carrier) : ∃ (n : Point2), n ≠ 0 ∧ ∀ y ∈ K.carrier, inner ℝ y n ≤ inner ℝ x n

A supporting direction at a boundary point of a convex body.

theorem HumanVerification.CauchyCrofton.exists_frontier_point_on_ray (K : Body) {a v : Point2} (ha : a ∈ K.carrier) (hv : v ≠ 0) : ∃ (t : ℝ), 0 ≤ t ∧ a + t • v ∈ frontier K.carrier ∧ ∀ (s : ℝ), 0 ≤ s → a + s • v ∈ K.carrier → s ≤ t

A ray from a point of a compact convex body leaves it through a boundary point.

theorem HumanVerification.CauchyCrofton.frontier_subset_nearestPoint_image {K L : Body} (hKL : K.carrier ⊆ L.carrier) : frontier K.carrier ⊆ nearestPoint K '' frontier L.carrier

Every boundary point of an inner convex body is the nearest-point image of a boundary point of an outer convex body.

theorem HumanVerification.CauchyCrofton.hPerimeter_mono {K L : Body} (hKL : K.carrier ⊆ L.carrier) : hPerimeter K ≤ hPerimeter L

Monotonicity of the Hausdorff perimeter.