OAI/GroupTheory/PolycyclicRecognition/Geometry/IndependentWeightCone.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The closed cones used by the neighboring-offset argument

A ray and a cone on two independent weights are closed. We construct them as actual proper cones, so polar separation requires no closedness input.

  1. def OAI.PolycyclicRecognition.independentWeightCone line 23

    Source documentation

    The nonnegative span of an independent finite family is closed.

    def independentWeightCone (v : I → V) (hv : LinearIndependent ℝ v) : ProperCone ℝ V where
…
  2. theorem OAI.PolycyclicRecognition.mem_independentWeightCone line 31
  3. def OAI.PolycyclicRecognition.closedWeightRay line 36
  4. theorem OAI.PolycyclicRecognition.mem_closedWeightRay line 40
  5. theorem OAI.PolycyclicRecognition.closedWeightRay_eq_insert line 49
  6. def OAI.PolycyclicRecognition.closedTwoWeightCone line 63
  7. theorem OAI.PolycyclicRecognition.mem_closedTwoWeightCone line 66
  8. theorem OAI.PolycyclicRecognition.closedTwoWeightCone_eq_insert line 79