Hausdorff perimeter of an inscribed cyclic polygon

The boundary of the polygon polySet K A is the union of its m edges, distinct edges meet in at most one point (a set of vanishing one-dimensional Hausdorff measure), and the measure of a segment is the distance between its endpoints. Hence the Hausdorff perimeter of the polygon is the sum of its edge lengths.

noncomputable def HumanVerification.CauchyCrofton.edgeLengthSum (K : Body) (A : AngleSystem) : ℝ

The cyclic sum of edge lengths of the inscribed polygon.

Equations

• HumanVerification.CauchyCrofton.edgeLengthSum K A = ∑ j ∈ Finset.range A.m, dist (HumanVerification.CauchyCrofton.vtx K A ↑j) (HumanVerification.CauchyCrofton.vtx K A (↑j + 1))

theorem HumanVerification.CauchyCrofton.edgeLengthSum_nonneg (K : Body) (A : AngleSystem) : 0 ≤ edgeLengthSum K A

theorem HumanVerification.CauchyCrofton.hausdorffMeasure_edge {K : Body} {A : AngleSystem} (j : ℤ) : (MeasureTheory.Measure.hausdorffMeasure 1) (edge K A j) = edist (vtx K A j) (vtx K A (j + 1))

One-dimensional Hausdorff measure of an edge.

theorem HumanVerification.CauchyCrofton.isClosed_edge {K : Body} {A : AngleSystem} (j : ℤ) : IsClosed (edge K A j)

Every edge is a closed set.

theorem HumanVerification.CauchyCrofton.aedisjoint_edge {K : Body} {A : AngleSystem} (h0 : 0 ∈ interior K.carrier) {j k : Fin A.m} (hjk : j ≠ k) : MeasureTheory.AEDisjoint (MeasureTheory.Measure.hausdorffMeasure 1) (edge K A ↑↑j) (edge K A ↑↑k)

Distinct edges are almost everywhere disjoint.

theorem HumanVerification.CauchyCrofton.hPerimeter_polyBody {K : Body} {A : AngleSystem} (h0 : 0 ∈ interior K.carrier) : hPerimeter (polyBody K A h0) = ENNReal.ofReal (edgeLengthSum K A)

Hausdorff perimeter of the inscribed polygon.