OAI/GroupTheory/PolycyclicRecognition/Algebra/ValuedEigenlineCones.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Separated eigenline cones over a normed coefficient field

  1. def OAI.PolycyclicRecognition.ValuedLinearDynamics.cone line 12
  2. theorem OAI.PolycyclicRecognition.ValuedLinearDynamics.cone_functional_ne_zero line 15
  3. theorem OAI.PolycyclicRecognition.ValuedLinearDynamics.cone_norm_bound line 21
  4. theorem OAI.PolycyclicRecognition.ValuedLinearDynamics.cone_functional_lower line 31
  5. theorem OAI.PolycyclicRecognition.ValuedLinearDynamics.cone_functional_upper line 41
  6. theorem OAI.PolycyclicRecognition.ValuedLinearDynamics.cone_transverse_nonzero line 53
  7. theorem OAI.PolycyclicRecognition.ValuedLinearDynamics.cone_transverse_bound line 59
  8. theorem OAI.PolycyclicRecognition.ValuedLinearDynamics.cones_disjoint_of_separator line 72
  9. theorem OAI.PolycyclicRecognition.ValuedLinearDynamics.small_cones_disjoint line 95