OAI/Analysis/LpDimension/StableRetractions.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SubpolynomialLp.below_projection_moments line 12
2. lemma OAI.SubpolynomialLp.L2_norm_sq line 96
3. lemma OAI.SubpolynomialLp.Lp_coe_sum line 103
4. lemma OAI.SubpolynomialLp.L2_hilbertMul_energy line 117
5. lemma OAI.SubpolynomialLp.charFun_linear_sum line 136
6. lemma OAI.SubpolynomialLp.stable_linear_sum_identical line 159
7. lemma OAI.SubpolynomialLp.stable_joint_gradient line 176
8. lemma OAI.SubpolynomialLp.clip_sq line 191
9. lemma OAI.SubpolynomialLp.stable_retraction_moments line 200