OAI/Analysis/SymmetricDomains/PrimeZeroLocusMaximum.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Release061.coeff_pow_X_sub_C_pred line 15
2. theorem OAI.Release061.norm_finite_average_le_one line 21
3. theorem OAI.Release061.extended_fiber_average line 31
4. theorem OAI.Release061.holomorphic_maximum_subsequence_on_ball line 86
5. theorem OAI.Release061.unit_disc_finset_sum_eq_card line 112
6. theorem OAI.Release061.scalar_maximum_local_of_finite_analytic_map line 128
7. theorem OAI.Release061.prime_zeroLocus_maximum_local line 242