Documentation

LeanPool.NandakumarRamanaRao.NRR.Multivalued.PerimeterObservable

NRR.Multivalued.PerimeterObservable — normalized perimeter as a nice multivalued function #

This module builds the concrete nice multivalued function representing perimeter on the lower-area convex-body hyperspace BodySpace K A (with A > 0).

The planar Cauchy perimeter of the solid bridge C.toGeometryConvexBody hA is normalized by the strictly positive constant 1 + K.perimeter. Since the underlying body of every element is contained in the parent body K, perimeter monotonicity under inclusion bounds the normalized value strictly below 1; nonnegativity of the perimeter bounds it below by 0. The normalized perimeter is therefore a continuous map into [0, 1), so |normalizedPerimeter C| < 1 and the canonical observable constructor NiceMV.ofObservable applies.

The resulting nice multivalued function perimeterNiceMV evaluates by (t : ℝ) - normalizedPerimeter C, following the fixed sign convention (negative at -1, positive at 1); its zero relation is exactly (t : ℝ) = normalizedPerimeter C.

source
noncomputable def NRR.normalizedPerimeter (K : Geometry.ConvexBody Geometry.Plane) (A : ℝ) (hA : 0 < A) :
C(BodySpace K A, ℝ)

The normalized perimeter observable on BodySpace K A (A > 0): the planar perimeter of the solid bridge divided by the strictly positive constant 1 + K.perimeter. It is continuous, as the perimeter of the solid bridge is continuous and the denominator is a positive constant.

Equations
Instances For
    source
    @[simp]
    theorem NRR.normalizedPerimeter_apply {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (hA : 0 < A) (C : BodySpace K A) :
    (normalizedPerimeter K A hA) C = (C.toGeometryConvexBody hA).perimeter / (1 + K.perimeter)
    source
    theorem NRR.one_add_perimeter_pos (K : Geometry.ConvexBody Geometry.Plane) :
    0 < 1 + K.perimeter

    The denominator 1 + K.perimeter is strictly positive.

    source
    theorem NRR.normalizedPerimeter_nonneg {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (hA : 0 < A) (C : BodySpace K A) :
    0 ≤ (normalizedPerimeter K A hA) C
    source
    theorem NRR.normalizedPerimeter_lt_one {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (hA : 0 < A) (C : BodySpace K A) :
    (normalizedPerimeter K A hA) C < 1
    source
    theorem NRR.abs_normalizedPerimeter_lt_one {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (hA : 0 < A) (C : BodySpace K A) :
    |(normalizedPerimeter K A hA) C| < 1
    source
    noncomputable def NRR.perimeterNiceMV (K : Geometry.ConvexBody Geometry.Plane) (A : ℝ) (hA : 0 < A) :
    NiceMV (BodySpace K A)

    The nice multivalued function representing perimeter on BodySpace K A, obtained from the normalized perimeter observable via the canonical constructor. It evaluates by (t : ℝ) - normalizedPerimeter C, so its zero set is the graph (t : ℝ) = normalizedPerimeter C.

    Equations
    Instances For
      source
      theorem NRR.perimeterNiceMV_eval {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (hA : 0 < A) (C : BodySpace K A) (t : ↑SignedInterval) :
      (perimeterNiceMV K A hA).eval C t = ↑t - (normalizedPerimeter K A hA) C
      source
      theorem NRR.perimeterNiceMV_zero_iff {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} (hA : 0 < A) (C : BodySpace K A) (t : ↑SignedInterval) :
      (perimeterNiceMV K A hA).Zero C t ↔ ↑t = (normalizedPerimeter K A hA) C