Documentation

LeanPool.NandakumarRamanaRao.NRR.SupportFunction

NRR.SupportFunction — public support-function and width API #

This compatibility module re-exports the implemented convex-body support function and width under stable public names. All substantive proofs live under NRR.Geometry.ConvexBody.

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

Support function (compatibility alias). supportFn K u = h_K(u) = ⨆ x ∈ K, ⟪x, u⟫.

Equations
Instances For
    source
    noncomputable def NRR.Geometry.ConvexBody.width (K : ConvexBody Plane) (u : Plane) :
    ℝ

    Width (compatibility alias). width K u = w_K(u) = h_K(u) + h_K(-u).

    Equations
    Instances For
      source
      theorem NRR.Geometry.ConvexBody.supportFn_eq (K : ConvexBody Plane) (u : Plane) :
      K.supportFn u = K.supportFunction u

      Unfolding lemma for the supportFn alias.

      source
      theorem NRR.Geometry.ConvexBody.width_eq (K : ConvexBody Plane) (u : Plane) :
      K.width u = K.widthFunction u

      Unfolding lemma for the width alias.

      source
      theorem NRR.Geometry.ConvexBody.exists_supportFn_eq (K : ConvexBody Plane) (u : Plane) :
      ∃ x ∈ K.carrier, K.supportFn u = inner ℝ x u

      The supremum defining supportFn is attained on the compact body.

      source
      theorem NRR.Geometry.ConvexBody.supportFn_smul (K : ConvexBody Plane) {c : ℝ} (hc : 0 ≤ c) (u : Plane) :
      K.supportFn (c • u) = c * K.supportFn u

      Positive homogeneity of the support function.

      source
      theorem NRR.Geometry.ConvexBody.supportFn_add_le (K : ConvexBody Plane) (u v : Plane) :
      K.supportFn (u + v) ≤ K.supportFn u + K.supportFn v

      Subadditivity of the support function.

      source
      theorem NRR.Geometry.ConvexBody.convexOn_supportFn (K : ConvexBody Plane) :
      ConvexOn ℝ Set.univ K.supportFn

      The support function is convex in the direction u (from positive homogeneity and subadditivity).

      source
      theorem NRR.Geometry.ConvexBody.continuous_supportFn (K : ConvexBody Plane) :
      Continuous K.supportFn

      The support function is continuous in the direction u.

      source
      theorem NRR.Geometry.ConvexBody.supportFn_mono {K L : ConvexBody Plane} (h : K.carrier ⊆ L.carrier) (u : Plane) :
      K.supportFn u ≤ L.supportFn u

      Monotonicity of the support function under inclusion of bodies.

      source
      theorem NRR.Geometry.ConvexBody.subset_iInter_support_halfspace (K : ConvexBody Plane) :
      K.carrier ⊆ ⋂ (u : Plane), {x : Plane | inner ℝ x u ≤ K.supportFn u}

      Half-space inclusion. K is contained in the intersection of all its supporting half-spaces. (The reverse inclusion, i.e. exact reconstruction, requires a separation theorem and is not claimed here.)

      source
      theorem NRR.Geometry.ConvexBody.continuous_width (K : ConvexBody Plane) :
      Continuous K.width

      The width functional is continuous in the direction.

      source
      theorem NRR.Geometry.ConvexBody.width_nonneg (K : ConvexBody Plane) (u : Plane) :
      0 ≤ K.width u

      The width is nonnegative.

      source
      theorem NRR.Geometry.ConvexBody.width_mono {K L : ConvexBody Plane} (h : K.carrier ⊆ L.carrier) (u : Plane) :
      K.width u ≤ L.width u

      Width is monotone under inclusion of bodies.