OAI/Analysis/PureInfiniteness/ConjugateCoefficientTest.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The separating-functional step of KR02 7.18: nonnegativity on the actual coefficient cone passes to every conjugate of an abelian compression and to the closed positive cone they generate.

  1. theorem OAI.WeakPureInfiniteness.polynomial_conjugate_nonneg_of_coefficient_test line 29
  2. theorem OAI.WeakPureInfiniteness.conjugate_nonneg_of_coefficient_test line 69
  3. theorem OAI.WeakPureInfiniteness.base_nonneg_of_coefficient_test line 105
  4. theorem OAI.WeakPureInfiniteness.abelianTensorCone_nonneg_of_coefficient_test line 129