NRR.Geometry.ConvexBody — monotonicity of the planar perimeter

This module records the monotonicity of the planar (Cauchy) perimeter planarPerimeter with respect to set inclusion of convex bodies:

• planarPerimeter_mono — K ⊆ L ⇒ planarPerimeter K ≤ planarPerimeter L,
• planarPerimeter_eq_of_mutual_subset — mutual inclusion forces equality.

Design notes

The proof reduces to the pointwise width-function monotonicity widthFunction_mono from Width.lean: for every angle θ, the width of K along circleVec θ is at most the width of L. Applying intervalIntegral.integral_mono_on over the compact interval [0, 2π] (using the interval-integrability of both integrands, intervalIntegrable_planarPerimeter_integrand) yields the inequality of integrals, and multiplying by the nonnegative factor 1 / 2 gives the result.

Equality under mutual subset then follows from antisymmetry of ≤.

Import policy

Only PlanarPerimeter.lean and Width.lean are imported; they transitively provide all of Mathlib together with the perimeter and width APIs. No extra imports are required.

theorem NRR.Geometry.planarPerimeter_mono {K L : ConvexBody Plane} (hKL : K.carrier ⊆ L.carrier) : planarPerimeter K ≤ planarPerimeter L

Monotonicity of the planar perimeter. A larger convex body has a larger Cauchy perimeter.

theorem NRR.Geometry.planarPerimeter_eq_of_mutual_subset {K L : ConvexBody Plane} (hKL : K.carrier ⊆ L.carrier) (hLK : L.carrier ⊆ K.carrier) : planarPerimeter K = planarPerimeter L

Equality from mutual inclusion. If two convex bodies contain each other (as sets), their planar perimeters coincide.