The Cauchy–Crofton bridge

Combining

• the polygon identity hPerimeter P = cPerimeter P for inscribed cyclic polygons,
• monotonicity of both perimeters,
• their common behaviour under dilations,
• and the inscribed approximation r⁻¹ • K ⊆ P ⊆ K,

a squeeze as r ↓ 1 gives the Cauchy–Crofton identity

μH[1] (frontier K) = ENNReal.ofReal (perimeter K)

for every planar compact convex body with nonempty interior.

theorem HumanVerification.CauchyCrofton.hausdorffPerimeter_eq_cauchyPerimeter_of_zero_mem (K : Body) (h0 : 0 ∈ interior K.carrier) : hPerimeter K = cPerimeter K

The bridge, for a body containing the origin in its interior.

theorem HumanVerification.CauchyCrofton.hPerimeter_eq_cPerimeter (K : Body) : hPerimeter K = cPerimeter K

Cauchy–Crofton, in terms of the two perimeter functionals.

theorem HumanVerification.CauchyCrofton.hausdorffPerimeter_eq_cauchyPerimeter (K : NRR.Geometry.ConvexBody Point2) : (MeasureTheory.Measure.hausdorffMeasure 1) (frontier K.carrier) = ENNReal.ofReal K.perimeter

Cauchy–Crofton. The one-dimensional Hausdorff measure of the boundary of a planar compact convex body with nonempty interior equals its Cauchy width-integral perimeter.

theorem HumanVerification.CauchyCrofton.cauchyCroftonStatement : CauchyCroftonStatement

Proposition-level form used by the human-verification transfer.