OAI/Probability/SKRatio/Certificates/CertifiedFunctionBounds.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKRatio.Certificate.abs_v_le line 12
2. lemma OAI.SKRatio.Certificate.abs_m_le line 13
3. lemma OAI.SKRatio.Certificate.abs_mv_le line 14
4. lemma OAI.SKRatio.Certificate.approx_coefficient_bound line 18
5. lemma OAI.SKRatio.Certificate.approxF_bound line 29
6. lemma OAI.SKRatio.Certificate.bounded_center_square line 74
7. lemma OAI.SKRatio.Certificate.scalarFunction_bound line 82