OAI/Geometry/ProjectionBody/UnitSupport.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ProjectionCounterexample.unit_support_halfspaces_eq line 14

   Source documentation

   For a positively homogeneous support bound, unit directions determine all directions. This connects the unit-sphere definition with an explicit zonotope's halfspace description.

   theorem unit_support_halfspaces_eq
       {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V]
       (f : V → ℝ) (hzero : 0 ≤ f 0)
       (hscale : ∀ (a : ℝ), 0 ≤ a → ∀ u, f (a • u) = a * f u) :
       {x : V | ∀ u, ‖u‖ = 1 → ⟪u, x⟫ ≤ f u} =
         {x : V | ∀ u, ⟪u, x⟫ ≤ f u} := by
   …