OAI/Analysis/SymmetricDomains/Vector.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Release061.Wiener.discContinuityWithin_pullback line 31
2. def OAI.Release061.Complexify.monomial line 62
3. lemma OAI.Release061.Complexify.monomial_apply line 66
4. lemma OAI.Release061.Complexify.monomial_norm_le line 70
5. def OAI.Release061.Complexify.coefficient line 77
6. lemma OAI.Release061.Complexify.coefficient_norm_le line 81
7. lemma OAI.Release061.Complexify.coordinate_expansion line 98
8. lemma OAI.Release061.Complexify.coefficient_real line 112
9. def OAI.Release061.Complexify.series line 121
10. lemma OAI.Release061.Complexify.radius_lower_bound line 124
11. lemma OAI.Release061.Complexify.radius_pos line 141
12. lemma OAI.Release061.Complexify.norm_real_vector line 147
13. lemma OAI.Release061.Complexify.series_real line 150
14. theorem OAI.Release061.Complexify.scalar line 170
15. theorem OAI.Release061.Complexify.vector line 180