OAI/Probability/SKGap/Matrix/MatrixWordIncrement.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SKGap.word_opNorm_addline 14 - lemma
OAI.SKGap.real_product_four_pointline 20 - structure
OAI.SKGap.MatrixFactorPairBoundsline 38 - def
OAI.SKGap.wordParameterCoeffline 46 - def
OAI.SKGap.wordMixedCoeffline 50 - theorem
OAI.SKGap.matrixWord_pair_incrementsline 54