OAI/Analysis/WeakInfiniteness/States.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.WeakPureInfiniteness.norm_add_one_of_nonneg line 22
  2. def OAI.WeakPureInfiniteness.selfAdjointComplexification line 33
  3. lemma OAI.WeakPureInfiniteness.selfAdjointComplexification_apply line 42
  4. lemma OAI.WeakPureInfiniteness.real_functional_nonneg line 47
  5. def OAI.WeakPureInfiniteness.positiveComplexification line 70
  6. lemma OAI.WeakPureInfiniteness.positiveComplexification_apply line 82
  7. theorem OAI.WeakPureInfiniteness.exists_norming_positive_functional line 87
  8. def OAI.WeakPureInfiniteness.gnsCyclicVector line 110
  9. lemma OAI.WeakPureInfiniteness.norm_gnsCyclicVector line 113
  10. lemma OAI.WeakPureInfiniteness.norm_gns_action_sq line 119
  11. theorem OAI.WeakPureInfiniteness.exists_norming_gns line 128