OAI/Probability/SKGap/Matrix/WordDiagUniform.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SKGap.zeroDiag_exact_word_uniform_prediction line 15
2. theorem OAI.SKGap.exactWord_uniform_opNorm line 59
3. lemma OAI.SKGap.wordRecursionAt_degree_budget line 110
4. lemma OAI.SKGap.wordRecursionTerms_degree_budget line 125
5. def OAI.SKGap.wordPredictionPolynomial line 137
6. lemma OAI.SKGap.polynomial_list_degree_le line 148
7. lemma OAI.SKGap.polynomial_eval_list_sum line 154
8. theorem OAI.SKGap.wordPredictionPolynomial_spec line 160