OAI/Analysis/SymmetricDomains/VectorLift.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Release061.AnalyticLift.monomial line 15
2. lemma OAI.Release061.AnalyticLift.monomial_apply line 20
3. lemma OAI.Release061.AnalyticLift.monomial_norm_le line 24
4. def OAI.Release061.AnalyticLift.coefficient line 31
5. lemma OAI.Release061.AnalyticLift.coefficient_norm_le line 35
6. lemma OAI.Release061.AnalyticLift.coordinate_expansion line 52
7. lemma OAI.Release061.AnalyticLift.evaluation_coefficient line 67
8. def OAI.Release061.AnalyticLift.series line 76
9. lemma OAI.Release061.AnalyticLift.radius_lower_bound line 79
10. lemma OAI.Release061.AnalyticLift.radius_pos line 96
11. lemma OAI.Release061.AnalyticLift.analytic_series line 104
12. lemma OAI.Release061.AnalyticLift.evaluation_series line 110
13. theorem OAI.Release061.AnalyticLift.exists_scalar_lift line 138
14. theorem OAI.Release061.AnalyticLift.exists_vector_lift line 149