OAI/Analysis/HardSphere/Cutoffs/Failure.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SineProduct.one_failure_le line 16
2. lemma OAI.SineProduct.coefficients_sq_le line 42
3. lemma OAI.SineProduct.contraction_sq line 56
4. lemma OAI.SineProduct.deriv_sq_le line 62
5. lemma OAI.SineProduct.fderiv_sq_le line 73