OAI/Analysis/PureInfiniteness/ConjugateGeneratedCone.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The concrete closed positive cone generated by a family of functionals and their coefficient conjugates, as used in KR02 Lemma 7.18.

  1. def OAI.WeakPureInfiniteness.positiveFunctionalReal line 15
  2. lemma OAI.WeakPureInfiniteness.positiveFunctionalReal_apply line 29
  3. lemma OAI.WeakPureInfiniteness.positiveFunctionalReal_nonneg line 32
  4. def OAI.WeakPureInfiniteness.weakConjugation line 35
  5. lemma OAI.WeakPureInfiniteness.conjugateRealFunctional_comp line 46
  6. def OAI.WeakPureInfiniteness.positiveRealDualCone line 57
  7. lemma OAI.WeakPureInfiniteness.positiveRealDualCone_closed line 67
  8. def OAI.WeakPureInfiniteness.conjugateGenerators line 77
  9. def OAI.WeakPureInfiniteness.conjugateGeneratedCone line 81
  10. lemma OAI.WeakPureInfiniteness.conjugateGenerators_nonneg line 84
  11. lemma OAI.WeakPureInfiniteness.conjugateGeneratedCone_nonneg line 91
  12. lemma OAI.WeakPureInfiniteness.conjugateGeneratedCone_zero line 96
  13. lemma OAI.WeakPureInfiniteness.conjugateGeneratedCone_base line 100
  14. lemma OAI.WeakPureInfiniteness.conjugateGeneratedCone_conjugate line 104