Documentation

LeanPool.NandakumarRamanaRao.NRR.AreaPerimeter

NRR.AreaPerimeter — planar Cauchy perimeter #

This module exposes the public perimeter of a planar convex body as the implemented Cauchy mean-width integral. It provides nonnegativity, the integral formula, monotonicity, and continuity for explicitly parameterized convex-body families with jointly continuous angle-width functions.

No topology on the type of all convex bodies is assumed.

source
noncomputable def NRR.Geometry.ConvexBody.perimeter (K : ConvexBody Plane) :
ℝ

Perimeter of a planar convex body, defined by Cauchy's mean-width formula: an alias of the implemented NRR.Geometry.planarPerimeter.

Equations
Instances For
    source
    theorem NRR.Geometry.ConvexBody.perimeter_def (K : ConvexBody Plane) :
    K.perimeter = planarPerimeter K

    Definitional unfolding of perimeter.

    source
    theorem NRR.Geometry.ConvexBody.perimeter_nonneg (K : ConvexBody Plane) :
    0 ≤ K.perimeter

    The perimeter is nonnegative.

    source
    theorem NRR.Geometry.ConvexBody.perimeter_eq_integral_width (K : ConvexBody Plane) :
    K.perimeter = 1 / 2 * ∫ (θ : ℝ) in 0..2 * Real.pi, K.width (circleVec θ)

    Cauchy's formula: perimeter K = ½ ∫₀^{2π} width_K(circleVec θ) dθ, integrating over unit directions parametrized by angle.

    source
    theorem NRR.Geometry.ConvexBody.perimeter_mono {K L : ConvexBody Plane} (h : K.carrier ⊆ L.carrier) :
    K.perimeter ≤ L.perimeter

    Monotonicity of perimeter under inclusion of convex bodies.

    source
    theorem NRR.Geometry.ConvexBody.continuous_perimeter_of_angleWidth {α : Type u_1} [TopologicalSpace α] (K : α → ConvexBody Plane) (hK : AngleWidthContinuousFamily K) :
    Continuous fun (a : α) => (K a).perimeter

    Continuity of perimeter for a family of convex bodies whose angle-width integrand is jointly continuous. There is no metric topology on Geometry.ConvexBody; continuity is therefore stated for an explicit family with a jointly continuous angle-width integrand.

    source
    theorem NRR.SolidConvexBody.perimeter_pos (K : SolidConvexBody) :
    0 < K.toConvexBody.perimeter

    A solid convex body has strictly positive perimeter, wrapping the implemented planarPerimeter_pos.