OAI/Probability/SKGap/Matrix/NormalizedInfluence.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGapCutoff.tanh_cubic_remainder line 37
2. lemma OAI.SKGapCutoff.normalized_tanh_difference line 54
3. lemma OAI.SKGapCutoff.rational_cubic_remainder line 67
4. lemma OAI.SKGapCutoff.normalized_tanh_cubic line 98
5. lemma OAI.SKGapCutoff.normalized_influence_cubic line 105
6. lemma OAI.SKGapCutoff.matrix_opNorm_le_schur line 129
7. lemma OAI.SKGapCutoff.matrix_diagonal_opNorm_le line 165
8. def OAI.SKGapCutoff.normalizedInfluence line 174
9. def OAI.SKGapCutoff.influenceCubicError line 177
10. lemma OAI.SKGapCutoff.influenceCubicError_norm_le line 180
11. def OAI.SKGapCutoff.normalizedInfluenceApprox line 203
12. lemma OAI.SKGapCutoff.normalizedInfluence_sub_approx line 206
13. lemma OAI.SKGapCutoff.normalizedInfluence_approx_norm_le line 217
14. lemma OAI.SKGapCutoff.normalizedInfluence_approx_tendsto line 250
15. def OAI.SKGapCutoff.influenceApprox line 303
16. lemma OAI.SKGapCutoff.influence_eq_normalized_mul line 306
17. lemma OAI.SKGapCutoff.influenceApprox_apply line 312
18. lemma OAI.SKGapCutoff.influence_approx_error_le line 318
19. lemma OAI.SKGapCutoff.influence_approx_tendsto line 329
20. lemma OAI.SKGapCutoff.normalizedInfluenceApprox_norm_le line 342
21. lemma OAI.SKGapCutoff.normalizedInfluence_opNorm_tight line 369