OAI/Probability/SignedSweeps/WordEmbedding.lean
14 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SignedSweeps.euclideanEmbeddingLinearline 11 - lemma
OAI.SignedSweeps.euclideanEmbeddingLinear_applyline 17 - lemma
OAI.SignedSweeps.euclideanEmbeddingLinear_atline 29 - lemma
OAI.SignedSweeps.euclideanEmbeddingLinear_offline 35 - lemma
OAI.SignedSweeps.euclideanEmbeddingLinear_innerline 42 - def
OAI.SignedSweeps.euclideanEmbeddingline 53 - lemma
OAI.SignedSweeps.euclideanEmbedding_applyline 56 - lemma
OAI.SignedSweeps.euclideanEmbedding_singleline 59 - def
OAI.SignedSweeps.euclideanTensorEquivline 70 - lemma
OAI.SignedSweeps.euclideanTensorEquiv_tmulline 74 - def
OAI.SignedSweeps.pairColorWordline 87 - def
OAI.SignedSweeps.pairColorEmbeddingline 91 - def
OAI.SignedSweeps.pairWordEmbeddingline 106 - lemma
OAI.SignedSweeps.pairWordEmbedding_tmul_atline 111