Cyclic convex polygons inscribed in a planar convex body

Given a compact convex body K in the plane with the origin in its interior, and a cyclic angle system A (a strictly increasing family θ : ℤ → ℝ with θ (j + m) = θ j + 2π and all gaps smaller than π/2), the points

vtx K A j = radPt K (A.θ j)

are boundary points of K listed in cyclic angular order. Their convex hull (together with the origin) is a convex polygon polySet K A whose boundary is, by construction, the union of the m consecutive edges segment ℝ (vtx j) (vtx (j+1)).

The cyclic ordering of the vertices is therefore supplied by the construction; no combinatorial analysis of an arbitrary finite planar point set is needed.

Cyclic angle systems

structure HumanVerification.CauchyCrofton.AngleSystem : Type

A cyclic system of m sample angles: strictly increasing over ℤ, m-periodic modulo a full turn, with all gaps smaller than a quarter turn.

• m : ℕ

  Number of sample directions.

• θ : ℤ → ℝ

  The angles, indexed by ℤ and increasing by 2π after m steps.

• strictMono : StrictMono self.θ
• period (j : ℤ) : self.θ (j + ↑self.m) = self.θ j + 2 * Real.pi
• gap_lt (j : ℤ) : self.θ (j + 1) - self.θ j < Real.pi / 2

theorem HumanVerification.CauchyCrofton.AngleSystem.gap_pos (A : AngleSystem) (j : ℤ) : 0 < A.θ (j + 1) - A.θ j

theorem HumanVerification.CauchyCrofton.AngleSystem.m_pos (A : AngleSystem) : 0 < A.m

theorem HumanVerification.CauchyCrofton.AngleSystem.period_zsmul (A : AngleSystem) (j k : ℤ) : A.θ (j + k * ↑A.m) = A.θ j + ↑k * (2 * Real.pi)

Iterated periodicity.

theorem HumanVerification.CauchyCrofton.AngleSystem.exists_lt_angle (A : AngleSystem) (t : ℝ) : ∃ (j : ℤ), t < A.θ j

theorem HumanVerification.CauchyCrofton.AngleSystem.exists_angle_le (A : AngleSystem) (t : ℝ) : ∃ (j : ℤ), A.θ j ≤ t

theorem HumanVerification.CauchyCrofton.AngleSystem.exists_index (A : AngleSystem) (t : ℝ) : ∃ (j : ℤ), A.θ j ≤ t ∧ t < A.θ (j + 1)

Every real number lies in one of the sample intervals.

theorem HumanVerification.CauchyCrofton.AngleSystem.exists_index_mem_range (A : AngleSystem) (t : ℝ) (ht : t ∈ Set.Ico (A.θ 0) (A.θ 0 + 2 * Real.pi)) : ∃ (j : ℤ), 0 ≤ j ∧ j < ↑A.m ∧ A.θ j ≤ t ∧ t < A.θ (j + 1)

Every real number lies in one of the sample intervals with index in the base window.

The inscribed polygon

noncomputable def HumanVerification.CauchyCrofton.vtx (K : Body) (A : AngleSystem) (j : ℤ) : Point2

The j-th vertex: the radial boundary point of K at angle A.θ j.

Equations

• HumanVerification.CauchyCrofton.vtx K A j = HumanVerification.CauchyCrofton.radPt K (A.θ j)

def HumanVerification.CauchyCrofton.polyVerts (K : Body) (A : AngleSystem) : Set Point2

The vertex set of the polygon, together with the origin.

Equations

• HumanVerification.CauchyCrofton.polyVerts K A = insert 0 (Set.range fun (j : Fin A.m) => HumanVerification.CauchyCrofton.vtx K A ↑↑j)

def HumanVerification.CauchyCrofton.polySet (K : Body) (A : AngleSystem) : Set Point2

The inscribed polygon attached to K and the angle system A.

Equations

• HumanVerification.CauchyCrofton.polySet K A = (convexHull ℝ) (HumanVerification.CauchyCrofton.polyVerts K A)

def HumanVerification.CauchyCrofton.edge (K : Body) (A : AngleSystem) (j : ℤ) : Set Point2

The j-th edge.

Equations

• HumanVerification.CauchyCrofton.edge K A j = segment ℝ (HumanVerification.CauchyCrofton.vtx K A j) (HumanVerification.CauchyCrofton.vtx K A (j + 1))

noncomputable def HumanVerification.CauchyCrofton.nrm (K : Body) (A : AngleSystem) (j : ℤ) : Point2

Outward normal of the j-th edge.

Equations

• HumanVerification.CauchyCrofton.nrm K A j = HumanVerification.CauchyCrofton.rot (HumanVerification.CauchyCrofton.vtx K A j - HumanVerification.CauchyCrofton.vtx K A (j + 1))

noncomputable def HumanVerification.CauchyCrofton.dd (K : Body) (A : AngleSystem) (j : ℤ) : ℝ

Value of the j-th edge functional.

Equations

• HumanVerification.CauchyCrofton.dd K A j = HumanVerification.CauchyCrofton.cross (HumanVerification.CauchyCrofton.vtx K A j) (HumanVerification.CauchyCrofton.vtx K A (j + 1))

theorem HumanVerification.CauchyCrofton.vtx_periodic {K : Body} {A : AngleSystem} (j : ℤ) : vtx K A (j + ↑A.m) = vtx K A j

theorem HumanVerification.CauchyCrofton.vtx_periodic_zsmul {K : Body} {A : AngleSystem} (j k : ℤ) : vtx K A (j + k * ↑A.m) = vtx K A j

theorem HumanVerification.CauchyCrofton.vtx_mem_polyVerts {K : Body} {A : AngleSystem} (j : ℤ) : vtx K A j ∈ polyVerts K A

theorem HumanVerification.CauchyCrofton.exists_fin_vtx_eq {K : Body} {A : AngleSystem} (k : ℤ) : ∃ (i : Fin A.m), vtx K A ↑↑i = vtx K A k

Every vertex index is equivalent to one in the base window.

theorem HumanVerification.CauchyCrofton.finite_polyVerts {K : Body} {A : AngleSystem} : (polyVerts K A).Finite

theorem HumanVerification.CauchyCrofton.vtx_mem {K : Body} {A : AngleSystem} (h0 : 0 ∈ K.carrier) (j : ℤ) : vtx K A j ∈ K.carrier

theorem HumanVerification.CauchyCrofton.polySet_subset {K : Body} {A : AngleSystem} (h0 : 0 ∈ K.carrier) : polySet K A ⊆ K.carrier

theorem HumanVerification.CauchyCrofton.isCompact_polySet {K : Body} {A : AngleSystem} : IsCompact (polySet K A)

theorem HumanVerification.CauchyCrofton.convex_polySet {K : Body} {A : AngleSystem} : Convex ℝ (polySet K A)

theorem HumanVerification.CauchyCrofton.zero_mem_polySet {K : Body} {A : AngleSystem} : 0 ∈ polySet K A

theorem HumanVerification.CauchyCrofton.vtx_mem_polySet {K : Body} {A : AngleSystem} (j : ℤ) : vtx K A j ∈ polySet K A

theorem HumanVerification.CauchyCrofton.edge_subset_polySet {K : Body} {A : AngleSystem} (j : ℤ) : edge K A j ⊆ polySet K A

Edge functionals

theorem HumanVerification.CauchyCrofton.inner_vtx_nrm_left {K : Body} {A : AngleSystem} (j : ℤ) : inner ℝ (vtx K A j) (nrm K A j) = dd K A j

theorem HumanVerification.CauchyCrofton.inner_vtx_nrm_right {K : Body} {A : AngleSystem} (j : ℤ) : inner ℝ (vtx K A (j + 1)) (nrm K A j) = dd K A j

theorem HumanVerification.CauchyCrofton.dd_pos {K : Body} {A : AngleSystem} (h0 : 0 ∈ interior K.carrier) (j : ℤ) : 0 < dd K A j

theorem HumanVerification.CauchyCrofton.nrm_ne_zero {K : Body} {A : AngleSystem} (h0 : 0 ∈ interior K.carrier) (j : ℤ) : nrm K A j ≠ 0

theorem HumanVerification.CauchyCrofton.inner_nrm_of_mem_edge {K : Body} {A : AngleSystem} {j : ℤ} {x : Point2} (hx : x ∈ edge K A j) : inner ℝ x (nrm K A j) = dd K A j

Points of the j-th edge lie on the edge line.

theorem HumanVerification.CauchyCrofton.inner_vtx_ge_of_between {K : Body} {A : AngleSystem} (h0 : 0 ∈ interior K.carrier) {n : Point2} {s : ℝ} (hs : 0 < s) {j i k : ℤ} (hji : j < i) (hik : i < k) (hspread : A.θ k - A.θ j ≤ Real.pi) (hj : s ≤ inner ℝ (vtx K A j) n) (hk : s ≤ inner ℝ (vtx K A k) n) : s ≤ inner ℝ (vtx K A i) n

Blocking, in vertex form. A vertex lying (in index order) between two vertices whose functional value is at least s > 0 also has value at least s, provided the two directions span at most a half turn.

theorem HumanVerification.CauchyCrofton.inner_vtx_gt_of_between {K : Body} {A : AngleSystem} (h0 : 0 ∈ interior K.carrier) {n : Point2} {s : ℝ} (hs : 0 < s) {j i k : ℤ} (hji : j < i) (hik : i < k) (hspread : A.θ k - A.θ j ≤ Real.pi) (hj : s ≤ inner ℝ (vtx K A j) n) (hk : s < inner ℝ (vtx K A k) n) : s < inner ℝ (vtx K A i) n

Strict form of inner_vtx_ge_of_between.

theorem HumanVerification.CauchyCrofton.inner_vtx_gt_of_between' {K : Body} {A : AngleSystem} (h0 : 0 ∈ interior K.carrier) {n : Point2} {s : ℝ} (hs : 0 < s) {j i k : ℤ} (hji : j < i) (hik : i < k) (hspread : A.θ k - A.θ j ≤ Real.pi) (hj : s < inner ℝ (vtx K A j) n) (hk : s ≤ inner ℝ (vtx K A k) n) : s < inner ℝ (vtx K A i) n

Variant of inner_vtx_gt_of_between with the strict bound on the left.

The supporting-line property

This is the geometric heart of the construction: each edge line supports the whole vertex set.

theorem HumanVerification.CauchyCrofton.inner_vtx_le_of_consecutive_eq {K : Body} {A : AngleSystem} (h0 : 0 ∈ interior K.carrier) {j : ℤ} {n : Point2} {d : ℝ} (hd : 0 < d) (h1 : inner ℝ (vtx K A j) n = d) (h2 : inner ℝ (vtx K A (j + 1)) n = d) (k : ℤ) : inner ℝ (vtx K A k) n ≤ d

Supporting-line property (abstract form). If a linear functional takes the same positive value d at two consecutive vertices, then it is ≤ d on every vertex.

theorem HumanVerification.CauchyCrofton.inner_vtx_nrm_le {K : Body} {A : AngleSystem} (h0 : 0 ∈ interior K.carrier) (j k : ℤ) : inner ℝ (vtx K A k) (nrm K A j) ≤ dd K A j

Supporting-line property.

theorem HumanVerification.CauchyCrofton.polySet_subset_halfspace {K : Body} {A : AngleSystem} (h0 : 0 ∈ interior K.carrier) (j : ℤ) : polySet K A ⊆ {x : Point2 | inner ℝ x (nrm K A j) ≤ dd K A j}

The polygon lies in each edge half-plane.

Radial description of the polygon

theorem HumanVerification.CauchyCrofton.inner_circleVec_nrm_left {K : Body} {A : AngleSystem} (h0 : 0 ∈ interior K.carrier) (j : ℤ) : inner ℝ (NRR.Geometry.circleVec (A.θ j)) (nrm K A j) = dd K A j / rad K (A.θ j)

Inner product of the j-th vertex direction with the j-th normal.

theorem HumanVerification.CauchyCrofton.inner_circleVec_nrm_right {K : Body} {A : AngleSystem} (h0 : 0 ∈ interior K.carrier) (j : ℤ) : inner ℝ (NRR.Geometry.circleVec (A.θ (j + 1))) (nrm K A j) = dd K A j / rad K (A.θ (j + 1))

theorem HumanVerification.CauchyCrofton.circleVec_cone_sector {A : AngleSystem} (j : ℤ) (t : ℝ) : Real.sin (A.θ (j + 1) - t) • NRR.Geometry.circleVec (A.θ j) + Real.sin (t - A.θ j) • NRR.Geometry.circleVec (A.θ (j + 1)) = Real.sin (A.θ (j + 1) - A.θ j) • NRR.Geometry.circleVec t

A direction in the j-th sector, written in the cone of the two edge directions.

theorem HumanVerification.CauchyCrofton.inner_circleVec_nrm_pos {K : Body} {A : AngleSystem} (h0 : 0 ∈ interior K.carrier) {j : ℤ} {t : ℝ} (h1 : A.θ j ≤ t) (h2 : t ≤ A.θ (j + 1)) : 0 < inner ℝ (NRR.Geometry.circleVec t) (nrm K A j)

On a sector, the edge normal has positive inner product with every direction.

noncomputable def HumanVerification.CauchyCrofton.rayPt (K : Body) (A : AngleSystem) (j : ℤ) (t : ℝ) : Point2

The point where the ray of angle t meets the j-th edge line.

Equations

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

theorem HumanVerification.CauchyCrofton.rayPt_mem_edge {K : Body} {A : AngleSystem} (h0 : 0 ∈ interior K.carrier) {j : ℤ} {t : ℝ} (h1 : A.θ j ≤ t) (h2 : t ≤ A.θ (j + 1)) : rayPt K A j t ∈ edge K A j

The ray of an angle in the j-th sector meets the j-th edge.

theorem HumanVerification.CauchyCrofton.exists_ball_subset_polySet {K : Body} {A : AngleSystem} (h0 : 0 ∈ interior K.carrier) : ∃ ε > 0, Metric.ball 0 ε ⊆ polySet K A

A ball around the origin is contained in the polygon.

theorem HumanVerification.CauchyCrofton.zero_mem_interior_polySet {K : Body} {A : AngleSystem} (h0 : 0 ∈ interior K.carrier) : 0 ∈ interior (polySet K A)

def HumanVerification.CauchyCrofton.polyBody (K : Body) (A : AngleSystem) (h0 : 0 ∈ interior K.carrier) : Body

The polygon, as a convex body.

Equations

• HumanVerification.CauchyCrofton.polyBody K A h0 = { carrier := HumanVerification.CauchyCrofton.polySet K A, convex' := ⋯, isCompact' := ⋯, interior_nonempty' := ⋯ }

@[simp]

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

The boundary decomposition

theorem HumanVerification.CauchyCrofton.edge_subset_frontier {K : Body} {A : AngleSystem} (h0 : 0 ∈ interior K.carrier) (j : ℤ) : edge K A j ⊆ frontier (polySet K A)

Every edge is contained in the boundary of the polygon.

theorem HumanVerification.CauchyCrofton.frontier_polySet {K : Body} {A : AngleSystem} (h0 : 0 ∈ interior K.carrier) : frontier (polySet K A) = ⋃ (j : Fin A.m), edge K A ↑↑j

Boundary decomposition. The boundary of the polygon is the union of its m edges.

theorem HumanVerification.CauchyCrofton.ne_zero_of_mem_edge {K : Body} {A : AngleSystem} (h0 : 0 ∈ interior K.carrier) {j : ℤ} {x : Point2} (hx : x ∈ edge K A j) : x ≠ 0

Every point of an edge is nonzero.

theorem HumanVerification.CauchyCrofton.exists_angle_of_mem_edge {K : Body} {A : AngleSystem} (h0 : 0 ∈ interior K.carrier) {j : ℤ} {x : Point2} (hx : x ∈ edge K A j) : ∃ (t : ℝ), A.θ j ≤ t ∧ t ≤ A.θ (j + 1) ∧ x = ‖x‖ • NRR.Geometry.circleVec t

Every point of the j-th edge has an angle in the j-th sector.

theorem HumanVerification.CauchyCrofton.eq_vtx_left_of_mem_edge {K : Body} {A : AngleSystem} (h0 : 0 ∈ interior K.carrier) {j : ℤ} {x : Point2} (hx : x ∈ edge K A j) (hxt : x = ‖x‖ • NRR.Geometry.circleVec (A.θ j)) : x = vtx K A j

A point of the j-th edge whose angle is the left endpoint is the left vertex.

theorem HumanVerification.CauchyCrofton.eq_vtx_right_of_mem_edge {K : Body} {A : AngleSystem} (h0 : 0 ∈ interior K.carrier) {j : ℤ} {x : Point2} (hx : x ∈ edge K A j) (hxt : x = ‖x‖ • NRR.Geometry.circleVec (A.θ (j + 1))) : x = vtx K A (j + 1)

A point of the j-th edge whose angle is the right endpoint is the right vertex.

theorem HumanVerification.CauchyCrofton.edge_inter_subset_pair {K : Body} {A : AngleSystem} (h0 : 0 ∈ interior K.carrier) {j k : ℤ} (hj0 : 0 ≤ j) (hjm : j < ↑A.m) (hk0 : 0 ≤ k) (hkm : k < ↑A.m) (hjk : j ≠ k) : edge K A j ∩ edge K A k ⊆ {vtx K A j, vtx K A (j + 1)}

Distinct edges meet only in vertices.