Cauchy perimeter of an inscribed cyclic polygon

For every direction u, the cyclic total variation of the linear functional ⟪·, u⟫ along the vertices of the inscribed polygon equals twice its width:

∑ j, |⟪v (j+1) - v j, u⟫| = 2 * width P u.

Integrating this identity over the circle and using ∫₀^{2π} |⟪e, circleVec θ⟫| dθ = 4 ‖e‖ identifies the Cauchy perimeter of the polygon with the sum of its edge lengths.

The elementary edge integral

theorem HumanVerification.CauchyCrofton.integral_abs_cos_full_period (φ : ℝ) : ∫ (θ : ℝ) in 0..2 * Real.pi, |Real.cos (θ - φ)| = 4

Full-period integral of the absolute cosine.

theorem HumanVerification.CauchyCrofton.integral_abs_inner_circleVec (e : Point2) : ∫ (θ : ℝ) in 0..2 * Real.pi, |inner ℝ e (NRR.Geometry.circleVec θ)| = 4 * ‖e‖

Integral of the absolute projection of one edge over the unit circle.

Width of the inscribed polygon

theorem HumanVerification.CauchyCrofton.exists_max_vtx (K : Body) (A : AngleSystem) (u : Point2) : ∃ (j : ℤ), ∀ (k : ℤ), inner ℝ (vtx K A k) u ≤ inner ℝ (vtx K A j) u

There is a vertex maximizing any linear functional.

theorem HumanVerification.CauchyCrofton.supportFunction_polyBody {K : Body} {A : AngleSystem} (h0 : 0 ∈ interior K.carrier) {w : Point2} (hw : w ≠ 0) {C : ℝ} (hle : ∀ (j : ℤ), inner ℝ (vtx K A j) w ≤ C) (hex : ∃ (j : ℤ), inner ℝ (vtx K A j) w = C) : NRR.Geometry.ConvexBody.supportFunction (polyBody K A h0) w = C

The support function of the polygon is the maximum of the vertex values.

theorem HumanVerification.CauchyCrofton.widthFunction_polyBody {K : Body} {A : AngleSystem} (h0 : 0 ∈ interior K.carrier) {u : Point2} (hu : u ≠ 0) {M N : ℝ} (hMle : ∀ (j : ℤ), inner ℝ (vtx K A j) u ≤ M) (hMex : ∃ (j : ℤ), inner ℝ (vtx K A j) u = M) (hNle : ∀ (j : ℤ), N ≤ inner ℝ (vtx K A j) u) (hNex : ∃ (j : ℤ), inner ℝ (vtx K A j) u = N) : NRR.Geometry.ConvexBody.widthFunction (polyBody K A h0) u = M - N

The width of the polygon is the range of the linear functional over its vertices.

Unimodality of the vertex values

theorem HumanVerification.CauchyCrofton.upcrossing_unique {K : Body} {A : AngleSystem} (h0 : 0 ∈ interior K.carrier) {u : Point2} {t : ℝ} (ht : t ≠ 0) {j k : ℤ} (hj : inner ℝ (vtx K A j) u ≤ t) (hj' : t < inner ℝ (vtx K A (j + 1)) u) (hk : inner ℝ (vtx K A k) u ≤ t) (hk' : t < inner ℝ (vtx K A (k + 1)) u) : ∃ (q : ℤ), k = j + q * ↑A.m

At most one up-crossing per period.

theorem HumanVerification.CauchyCrofton.sum_abs_inner_edge {K : Body} {A : AngleSystem} (h0 : 0 ∈ interior K.carrier) {u : Point2} (hu : u ≠ 0) : ∑ j ∈ Finset.range A.m, |inner ℝ (vtx K A (↑j + 1) - vtx K A ↑j) u| = 2 * NRR.Geometry.ConvexBody.widthFunction (polyBody K A h0) u

Projection-variation identity.

The Cauchy perimeter of the polygon

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

Cauchy perimeter of the inscribed polygon.

theorem HumanVerification.CauchyCrofton.polygon_hPerimeter_eq_cPerimeter {K : Body} {A : AngleSystem} (h0 : 0 ∈ interior K.carrier) : hPerimeter (polyBody K A h0) = cPerimeter (polyBody K A h0)

Cauchy–Crofton for the inscribed polygon.