Polygonal approximation from inside

For a planar convex body K with the origin in its interior and any r > 1, a sufficiently fine uniform angle system produces an inscribed polygon P with

r⁻¹ • K ⊆ P ⊆ K.

The construction uses the uniform angles θ j = j * (2π / M), so the cyclic order of the vertices is immediate. The inclusion r⁻¹ • K ⊆ P follows from two elementary facts:

• r⁻¹ • K is at distance at least (1 - r⁻¹) * ρ from the complement of K, where ball 0 ρ ⊆ K;
• a ray hitting a chord whose endpoints have radius at least L meets it at radius at least L * cos (δ / 2), where δ is the angle subtended by the chord.

noncomputable def HumanVerification.CauchyCrofton.uniformAngles (M : ℕ) (hM : 5 ≤ M) : AngleSystem

The uniform angle system with M directions.

Equations

• HumanVerification.CauchyCrofton.uniformAngles M hM = { m := M, θ := fun (j : ℤ) => ↑j * (2 * Real.pi / ↑M), strictMono := ⋯, period := ⋯, gap_lt := ⋯ }

@[simp]

theorem HumanVerification.CauchyCrofton.uniformAngles_m (M : ℕ) (hM : 5 ≤ M) : (uniformAngles M hM).m = M

@[simp]

theorem HumanVerification.CauchyCrofton.uniformAngles_θ (M : ℕ) (hM : 5 ≤ M) (j : ℤ) : (uniformAngles M hM).θ j = ↑j * (2 * Real.pi / ↑M)

theorem HumanVerification.CauchyCrofton.mem_convexHull_triangle_of_norm_le {α γ t : ℝ} (hαt : α ≤ t) (htγ : t ≤ γ) (hlt : γ - α < Real.pi) {a b L s : ℝ} (hL : 0 < L) (ha : L ≤ a) (hb : L ≤ b) (hs : 0 ≤ s) (hsle : s ≤ L * Real.cos ((γ - α) / 2)) : s • NRR.Geometry.circleVec t ∈ (convexHull ℝ) {0, a • NRR.Geometry.circleVec α, b • NRR.Geometry.circleVec γ}

Chord estimate. A point of the plane whose direction lies in the angular sector [α, γ] and whose norm is at most L * cos ((γ - α)/2) lies in the triangle spanned by the origin and two points of radius at least L in the directions α and γ.

theorem HumanVerification.CauchyCrofton.exists_inner_outer_radius (K : Body) (h0 : 0 ∈ interior K.carrier) : ∃ (ρ : ℝ) (R : ℝ), 0 < ρ ∧ 0 < R ∧ Metric.ball 0 ρ ⊆ K.carrier ∧ K.carrier ⊆ Metric.closedBall 0 R

Inner and outer radii of a convex body with the origin in its interior.

theorem HumanVerification.CauchyCrofton.add_ball_subset_of_smul {K : Body} {ρ : ℝ} (hball : Metric.ball 0 ρ ⊆ K.carrier) {r : ℝ} (hr : 1 < r) {x : Point2} (hx : x ∈ r⁻¹ • K.carrier) {y : Point2} (hy : ‖y - x‖ < (1 - r⁻¹) * ρ) : y ∈ K.carrier

A shrunken copy of K stays inside K together with a uniform ball.

theorem HumanVerification.CauchyCrofton.exists_polygon_sandwich (K : Body) (h0 : 0 ∈ interior K.carrier) {r : ℝ} (hr : 1 < r) : ∃ (A : AngleSystem), r⁻¹ • K.carrier ⊆ polySet K A

Inscribed polygonal approximation.