Radial boundary points of a planar convex body

For a compact convex body K in the plane containing the origin in its interior we define

• rad K θ, the largest t ≥ 0 with t • circleVec θ ∈ K;
• radPt K θ = rad K θ • circleVec θ, the corresponding boundary point.

The main tool of the whole development is the blocking lemma blocking: if two points of K lie on rays whose directions span at most a half turn, the radial boundary point in any intermediate direction dominates the corresponding convex combination of linear values.

We also record the planar cross product and the trigonometric identity expressing a direction lying between two others as a nonnegative combination of them.

Planar cross product

def HumanVerification.CauchyCrofton.cross (x y : Point2) : ℝ

The planar cross product.

Equations

• HumanVerification.CauchyCrofton.cross x y = x.ofLp 0 * y.ofLp 1 - x.ofLp 1 * y.ofLp 0

def HumanVerification.CauchyCrofton.rot (x : Point2) : Point2

Rotation by a quarter turn.

Equations

• HumanVerification.CauchyCrofton.rot x = !₂[-x.ofLp 1, x.ofLp 0]

@[simp]

theorem HumanVerification.CauchyCrofton.inner_rot (x y : Point2) : inner ℝ y (rot x) = cross x y

theorem HumanVerification.CauchyCrofton.cross_smul_left (a : ℝ) (x y : Point2) : cross (a • x) y = a * cross x y

theorem HumanVerification.CauchyCrofton.cross_smul_right (a : ℝ) (x y : Point2) : cross x (a • y) = a * cross x y

theorem HumanVerification.CauchyCrofton.cross_add_right (x y z : Point2) : cross x (y + z) = cross x y + cross x z

theorem HumanVerification.CauchyCrofton.cross_add_left (x y z : Point2) : cross (x + y) z = cross x z + cross y z

theorem HumanVerification.CauchyCrofton.cross_self (x : Point2) : cross x x = 0

theorem HumanVerification.CauchyCrofton.cross_circleVec (α β : ℝ) : cross (NRR.Geometry.circleVec α) (NRR.Geometry.circleVec β) = Real.sin (β - α)

theorem HumanVerification.CauchyCrofton.rot_ne_zero {x : Point2} (hx : x ≠ 0) : rot x ≠ 0

Elementary planar trigonometry

theorem HumanVerification.CauchyCrofton.circleVec_cone_identity (α β γ : ℝ) : Real.sin (γ - β) • NRR.Geometry.circleVec α + Real.sin (β - α) • NRR.Geometry.circleVec γ = Real.sin (γ - α) • NRR.Geometry.circleVec β

The fundamental cone identity: sin (γ-β) • u α + sin (β-α) • u γ = sin (γ-α) • u β.

theorem HumanVerification.CauchyCrofton.inner_circleVec_circleVec (α β : ℝ) : inner ℝ (NRR.Geometry.circleVec α) (NRR.Geometry.circleVec β) = Real.cos (β - α)

Inner product of two circle vectors.

theorem HumanVerification.CauchyCrofton.exists_angle (x : Point2) (c : ℝ) : ∃ θ ∈ Set.Ico c (c + 2 * Real.pi), x = ‖x‖ • NRR.Geometry.circleVec θ

Every nonzero planar vector is a positive multiple of some circleVec θ, and the angle can be chosen in any half-open period window.

theorem HumanVerification.CauchyCrofton.exists_angle_mem_Icc_of_nonneg_combination {α γ : ℝ} (hαγ : α < γ) (hlt : γ - α < Real.pi) {A B : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) (hne : A • NRR.Geometry.circleVec α + B • NRR.Geometry.circleVec γ ≠ 0) : ∃ β ∈ Set.Icc α γ, A • NRR.Geometry.circleVec α + B • NRR.Geometry.circleVec γ = ‖A • NRR.Geometry.circleVec α + B • NRR.Geometry.circleVec γ‖ • NRR.Geometry.circleVec β

A nonnegative combination of two circle vectors spanning less than a half-turn is a nonnegative multiple of a circle vector with intermediate angle.

theorem HumanVerification.CauchyCrofton.circleVec_eq_iff_exists {t s : ℝ} (h : NRR.Geometry.circleVec t = NRR.Geometry.circleVec s) : ∃ (q : ℤ), s = t + ↑q * (2 * Real.pi)

Two angles with the same circle vector differ by a multiple of a full turn.

theorem HumanVerification.CauchyCrofton.norm_circleVec_sub_le (a b : ℝ) : ‖NRR.Geometry.circleVec a - NRR.Geometry.circleVec b‖ ≤ |a - b|

The circle parametrization is 1-Lipschitz.

The radial function

def HumanVerification.CauchyCrofton.radSet (K : Body) (θ : ℝ) : Set ℝ

The set of admissible radii in direction circleVec θ.

Equations

• HumanVerification.CauchyCrofton.radSet K θ = {t : ℝ | 0 ≤ t ∧ t • NRR.Geometry.circleVec θ ∈ K.carrier}

noncomputable def HumanVerification.CauchyCrofton.rad (K : Body) (θ : ℝ) : ℝ

The radial function of K: the largest t ≥ 0 with t • circleVec θ ∈ K.

Equations

• HumanVerification.CauchyCrofton.rad K θ = sSup (HumanVerification.CauchyCrofton.radSet K θ)

noncomputable def HumanVerification.CauchyCrofton.radPt (K : Body) (θ : ℝ) : Point2

The radial boundary point of K in direction circleVec θ.

Equations

• HumanVerification.CauchyCrofton.radPt K θ = HumanVerification.CauchyCrofton.rad K θ • NRR.Geometry.circleVec θ

theorem HumanVerification.CauchyCrofton.radPt_eq (K : Body) (θ : ℝ) : radPt K θ = rad K θ • NRR.Geometry.circleVec θ

theorem HumanVerification.CauchyCrofton.radSet_nonempty {K : Body} (h0 : 0 ∈ K.carrier) (θ : ℝ) : (radSet K θ).Nonempty

theorem HumanVerification.CauchyCrofton.bddAbove_radSet {K : Body} (θ : ℝ) : BddAbove (radSet K θ)

theorem HumanVerification.CauchyCrofton.isClosed_radSet {K : Body} (θ : ℝ) : IsClosed (radSet K θ)

theorem HumanVerification.CauchyCrofton.rad_mem_radSet {K : Body} (h0 : 0 ∈ K.carrier) (θ : ℝ) : rad K θ ∈ radSet K θ

theorem HumanVerification.CauchyCrofton.rad_nonneg {K : Body} (h0 : 0 ∈ K.carrier) (θ : ℝ) : 0 ≤ rad K θ

theorem HumanVerification.CauchyCrofton.radPt_mem {K : Body} (h0 : 0 ∈ K.carrier) (θ : ℝ) : radPt K θ ∈ K.carrier

theorem HumanVerification.CauchyCrofton.le_rad {K : Body} {t θ : ℝ} (ht : 0 ≤ t) (htK : t • NRR.Geometry.circleVec θ ∈ K.carrier) : t ≤ rad K θ

Maximality of the radial function.

theorem HumanVerification.CauchyCrofton.rad_pos {K : Body} (h0 : 0 ∈ interior K.carrier) (θ : ℝ) : 0 < rad K θ

theorem HumanVerification.CauchyCrofton.norm_radPt {K : Body} (h0 : 0 ∈ K.carrier) (θ : ℝ) : ‖radPt K θ‖ = rad K θ

theorem HumanVerification.CauchyCrofton.radPt_ne_zero {K : Body} (h0 : 0 ∈ interior K.carrier) (θ : ℝ) : radPt K θ ≠ 0

theorem HumanVerification.CauchyCrofton.radPt_mem_frontier {K : Body} (h0 : 0 ∈ interior K.carrier) (θ : ℝ) : radPt K θ ∈ frontier K.carrier

The radial boundary point really is a boundary point.

theorem HumanVerification.CauchyCrofton.rad_periodic {K : Body} (θ : ℝ) : rad K (θ + 2 * Real.pi) = rad K θ

2π-periodicity of the radial function.

theorem HumanVerification.CauchyCrofton.radPt_periodic {K : Body} (θ : ℝ) : radPt K (θ + 2 * Real.pi) = radPt K θ

The blocking lemma

theorem HumanVerification.CauchyCrofton.inner_le_inner_radPt {K : Body} {β μ : ℝ} (hμ : 0 < μ) (hx : μ • NRR.Geometry.circleVec β ∈ K.carrier) {n : Point2} (hn : 0 ≤ inner ℝ (μ • NRR.Geometry.circleVec β) n) : inner ℝ (μ • NRR.Geometry.circleVec β) n ≤ inner ℝ (radPt K β) n

Blocking lemma, basic form. If a point x of K lies on the ray with direction circleVec β at positive distance and has nonnegative inner product with n, then the radial boundary point in direction β has at least as large an inner product with n.

theorem HumanVerification.CauchyCrofton.blocking {K : Body} {α β γ : ℝ} (hαβ : α < β) (hβγ : β < γ) (hlt : γ - α ≤ Real.pi) {a c : ℝ} (ha : 0 < a) (hc : 0 < c) (hx : a • NRR.Geometry.circleVec α ∈ K.carrier) (hy : c • NRR.Geometry.circleVec γ ∈ K.carrier) {n : Point2} (hxn : 0 < inner ℝ (a • NRR.Geometry.circleVec α) n) (hyn : 0 < inner ℝ (c • NRR.Geometry.circleVec γ) n) : ∃ (lam : ℝ), 0 < lam ∧ lam < 1 ∧ (1 - lam) * inner ℝ (a • NRR.Geometry.circleVec α) n + lam * inner ℝ (c • NRR.Geometry.circleVec γ) n ≤ inner ℝ (radPt K β) n

Blocking lemma. Let α < β < γ with γ - α ≤ π, and let a • circleVec α and c • circleVec γ be points of K (with a, c > 0) whose inner products with n are both positive. Then the radial boundary point in the intermediate direction β dominates a strict convex combination of the two inner products.

theorem HumanVerification.CauchyCrofton.lt_inner_radPt_of_blocking {K : Body} {α β γ : ℝ} (hαβ : α < β) (hβγ : β < γ) (hlt : γ - α ≤ Real.pi) {a c : ℝ} (ha : 0 < a) (hc : 0 < c) (hx : a • NRR.Geometry.circleVec α ∈ K.carrier) (hy : c • NRR.Geometry.circleVec γ ∈ K.carrier) {n : Point2} {d : ℝ} (hd : 0 < d) (hxn : d ≤ inner ℝ (a • NRR.Geometry.circleVec α) n) (hyn : d < inner ℝ (c • NRR.Geometry.circleVec γ) n) : d < inner ℝ (radPt K β) n

Convenient corollary of blocking: the radial point in an intermediate direction strictly exceeds the smaller of two positive values, when the larger one is strict.

theorem HumanVerification.CauchyCrofton.lt_inner_radPt_of_blocking' {K : Body} {α β γ : ℝ} (hαβ : α < β) (hβγ : β < γ) (hlt : γ - α ≤ Real.pi) {a c : ℝ} (ha : 0 < a) (hc : 0 < c) (hx : a • NRR.Geometry.circleVec α ∈ K.carrier) (hy : c • NRR.Geometry.circleVec γ ∈ K.carrier) {n : Point2} {d : ℝ} (hd : 0 < d) (hxn : d < inner ℝ (a • NRR.Geometry.circleVec α) n) (hyn : d ≤ inner ℝ (c • NRR.Geometry.circleVec γ) n) : d < inner ℝ (radPt K β) n

Variant of lt_inner_radPt_of_blocking with the strict bound on the left.

theorem HumanVerification.CauchyCrofton.le_inner_radPt_of_blocking {K : Body} {α β γ : ℝ} (hαβ : α < β) (hβγ : β < γ) (hlt : γ - α ≤ Real.pi) {a c : ℝ} (ha : 0 < a) (hc : 0 < c) (hx : a • NRR.Geometry.circleVec α ∈ K.carrier) (hy : c • NRR.Geometry.circleVec γ ∈ K.carrier) {n : Point2} {d : ℝ} (hd : 0 < d) (hxn : d ≤ inner ℝ (a • NRR.Geometry.circleVec α) n) (hyn : d ≤ inner ℝ (c • NRR.Geometry.circleVec γ) n) : d ≤ inner ℝ (radPt K β) n

Weak version of lt_inner_radPt_of_blocking.