OAI/Analysis/WeakInfiniteness/VectorStates.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakPureInfiniteness.representationVectorFunctional line 31
2. lemma OAI.WeakPureInfiniteness.representationVectorFunctional_norm_le line 43
3. lemma OAI.WeakPureInfiniteness.representationVectorFunctional_one line 55
4. lemma OAI.WeakPureInfiniteness.representationVectorFunctional_square line 63
5. lemma OAI.WeakPureInfiniteness.normalized_vector_mem_realStateSpace line 73
6. lemma OAI.WeakPureInfiniteness.gns_vectorFunctional_eq line 88