OAI/Geometry/Kahler/BaseMeans.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.PinchedHartogs.BaseConstruction.(instance at line 20) line 20
2. lemma OAI.PinchedHartogs.BaseConstruction.sphere_norm line 22
3. def OAI.PinchedHartogs.BaseConstruction.Represents line 25
4. lemma OAI.PinchedHartogs.BaseConstruction.base_eq_sum_single line 29
5. lemma OAI.PinchedHartogs.BaseConstruction.multilinear_diagonal_polynomial line 33
6. lemma OAI.PinchedHartogs.BaseConstruction.continuous_integrable line 53
7. lemma OAI.PinchedHartogs.BaseConstruction.Represents.multilinear_moment line 57
8. lemma OAI.PinchedHartogs.BaseConstruction.Represents.partialSum_moment line 63
9. lemma OAI.PinchedHartogs.BaseConstruction.Represents.local_analytic_mean line 81
10. lemma OAI.PinchedHartogs.BaseConstruction.radial_mem_ball line 124
11. lemma OAI.PinchedHartogs.BaseConstruction.radial_continuous line 127
12. lemma OAI.PinchedHartogs.BaseConstruction.analytic_radial_integral line 133
13. lemma OAI.PinchedHartogs.BaseConstruction.Represents.analytic_mean line 173
14. theorem OAI.PinchedHartogs.BaseConstruction.representing_mean_criterion line 182