OAI/Probability/SKGap/Stability/ImplicitCoefficient.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGapCutoff.Recipe.vectorNorm_const line 17
2. lemma OAI.SKGapCutoff.Recipe.vectorNorm_neg line 22
3. lemma OAI.SKGapCutoff.Recipe.vectorNorm_sub line 24
4. lemma OAI.SKGapCutoff.Recipe.vectorNorm_tanh line 26
5. lemma OAI.SKGapCutoff.Recipe.vectorNorm_tanh_diff line 30
6. lemma OAI.SKGapCutoff.Recipe.abs_logSlope_le_two line 34
7. lemma OAI.SKGapCutoff.Recipe.vectorNorm_logSlope line 38
8. lemma OAI.SKGapCutoff.Recipe.vectorNorm_logSlope_near line 44
9. lemma OAI.SKGapCutoff.Recipe.phi_near_current line 53
10. lemma OAI.SKGapCutoff.Recipe.vectorNorm_phi_near_current line 63
11. lemma OAI.SKGapCutoff.Recipe.normalized_mean_bound line 78
12. theorem OAI.SKGapCutoff.Recipe.implicit_coefficient_bounds line 88
13. lemma OAI.SKGap.ImplicitSystem.eliminated_rhs_bound line 137
14. lemma OAI.SKGap.ImplicitSystem.implicit_scalar_size line 147
15. lemma OAI.SKGap.ImplicitSystem.implicit_field_size line 155
16. theorem OAI.SKGap.ImplicitSystem.implicit_size_bounds line 166