OAI/Probability/SKRatio/Matrices/AugmentedBounds.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKRatio.Planted.shiftedDisorder_hasLaw line 14
2. lemma OAI.SKRatio.Planted.coupling_shift line 25
3. lemma OAI.SKRatio.Planted.meanMatrix_opNorm_bound line 32
4. lemma OAI.SKRatio.Planted.shifted_opNorm_bound line 46
5. lemma OAI.SKRatio.Planted.original_norm_rare line 55
6. lemma OAI.SKRatio.Planted.planted_norm_rare line 79
7. lemma OAI.SKRatio.Planted.continuous_augmentedDisorder line 92
8. lemma OAI.SKRatio.Planted.augmented_norm_rare line 96
9. lemma OAI.SKRatio.Planted.centered_augmentedDiagonal_hasLaw line 106
10. lemma OAI.SKRatio.Planted.augmented_diagonal_rare line 122