NRR.Geometry.ConvexBody — basic scalar properties of the planar perimeter

This module records basic scalar properties of the planar Cauchy perimeter planarPerimeter (defined in PlanarPerimeter.lean):

• Nonnegativity — already available as planarPerimeter_nonneg from PlanarPerimeter.lean (reused, not restated, to avoid a duplicate declaration in the same namespace).
• Extensionality (planarPerimeter_ext) — the perimeter depends only on the underlying set of the convex body, stated in the pointwise-membership form.
• Upper bound from a width bound (planarPerimeter_le_of_width_bound) — if the width along every direction circleVec θ, θ ∈ [0, 2π], is bounded by C, then the perimeter is at most π · C. This is (1/2) · ((2π − 0) · C) = π · C.

Import policy

Only PlanarPerimeter.lean is imported; it transitively provides all of Mathlib together with the planarPerimeter, widthFunction, and circleVec APIs. No extra imports are required.

theorem NRR.Geometry.planarPerimeter_ext {K L : ConvexBody Plane} (h : ∀ (x : Plane), x ∈ K.carrier ↔ x ∈ L.carrier) : planarPerimeter K = planarPerimeter L

Extensionality. The planar perimeter depends only on the underlying set of the convex body, here in pointwise-membership form.

theorem NRR.Geometry.planarPerimeter_le_of_width_bound (K : ConvexBody Plane) {C : ℝ} (hC : ∀ θ ∈ Set.Icc 0 (2 * Real.pi), K.widthFunction (circleVec θ) ≤ C) : planarPerimeter K ≤ Real.pi * C

Upper bound from a width bound. If the width along every direction circleVec θ, θ ∈ [0, 2π], is bounded by C, then the planar perimeter is at most π · C.

theorem NRR.Geometry.ConvexBody.widthFunction_pos {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : ConvexBody E) {u : E} (hu : u ≠ 0) : 0 < K.widthFunction u

Positive width. A convex body (which has nonempty interior) has strictly positive width in every nonzero direction.

theorem NRR.Geometry.planarPerimeter_pos (K : ConvexBody Plane) : 0 < planarPerimeter K

Strict positivity. The planar perimeter of a convex body is strictly positive.