OAI/Analysis/LpDimension/RetractionIntegrals.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SubpolynomialLp.controlled_retraction_integrals line 12
2. lemma OAI.SubpolynomialLp.retraction_fixes line 33
3. lemma OAI.SubpolynomialLp.retraction_range line 39
4. lemma OAI.SubpolynomialLp.matrix_mulVec_bound line 45
5. lemma OAI.SubpolynomialLp.matrix_memLp line 54
6. lemma OAI.SubpolynomialLp.matrix_integral_sq_bound line 61
7. lemma OAI.SubpolynomialLp.ramp_error_le_cut_errors line 80
8. lemma OAI.SubpolynomialLp.cut_error_eq_neg_tail_error line 103