OAI/Probability/SKGap/Localization/Operation.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGapCutoff.Recipe.vectorNorm line 15
2. lemma OAI.SKGapCutoff.Recipe.vectorNorm_sq line 17
3. lemma OAI.SKGapCutoff.Recipe.vectorNorm_nonneg line 20
4. lemma OAI.SKGapCutoff.Recipe.vectorNorm_mul line 22
5. lemma OAI.SKGapCutoff.Recipe.row_scaled_frobenius line 30
6. lemma OAI.SKGapCutoff.Recipe.row_entry_bound line 41
7. lemma OAI.SKGapCutoff.Recipe.multiplier_frobenius line 47
8. lemma OAI.SKGapCutoff.Recipe.product_remainder_frobenius line 57
9. lemma OAI.SKGapCutoff.Recipe.source_derivative_product line 70
10. lemma OAI.SKGapCutoff.Recipe.source_frobenius line 78
11. lemma OAI.SKGapCutoff.Recipe.source_sum_frobenius line 88
12. lemma OAI.SKGapCutoff.Recipe.vectorNorm_add line 113
13. lemma OAI.SKGapCutoff.Recipe.vectorNorm_smul line 117
14. lemma OAI.SKGapCutoff.Recipe.vectorNorm_sum line 121
15. lemma OAI.SKGapCutoff.Recipe.vectorNorm_mono line 129
16. lemma OAI.SKGapCutoff.Recipe.vectorNorm_abs line 135
17. lemma OAI.SKGapCutoff.Recipe.vectorNorm_matrix_mul line 139
18. lemma OAI.SKGapCutoff.Recipe.siteMean_square line 143
19. lemma OAI.SKGapCutoff.Recipe.primary_mean_size line 154
20. lemma OAI.SKGapCutoff.Recipe.scaled_frobenius_by_rows line 168
21. lemma OAI.SKGapCutoff.Recipe.primary_mean_frobenius line 181
22. lemma OAI.SKGapCutoff.Recipe.coefficient_mean_value line 198
23. lemma OAI.SKGapCutoff.Recipe.coefficient_mean_difference line 210