OAI/NumberTheory/SiegelZeros/Determinants/DeterminantComparison.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SiegelZeros.SiegelZerosAwei.W36.abs_norm_eq_prod_embeddings line 23
2. theorem OAI.SiegelZeros.SiegelZerosAwei.W36.log_abs_norm_eq_sum_embeddings line 28
3. theorem OAI.SiegelZeros.SiegelZerosAwei.W36.log_abs_norm_le_finrank_mul line 34
4. theorem OAI.SiegelZeros.SiegelZerosAwei.W36.quarter_log_abs_norm_le line 42
5. theorem OAI.SiegelZeros.SiegelZerosAwei.W36.quarter_log_abs_norm_det_le line 51
6. def OAI.SiegelZeros.SiegelZerosAwei.W36.thetaRowMatrix line 74
7. theorem OAI.SiegelZeros.SiegelZerosAwei.W36.map_thetaRowMatrix line 81
8. theorem OAI.SiegelZeros.SiegelZerosAwei.W36.archimedean_norm_bound line 91
9. theorem OAI.SiegelZeros.SiegelZerosAwei.W46.cutoff_first_sum_pos line 124
10. theorem OAI.SiegelZeros.SiegelZerosAwei.W46.cutoff_normalization_pos line 135
11. theorem OAI.SiegelZeros.SiegelZerosAwei.W46.integral_field_log_norm line 149
12. theorem OAI.SiegelZeros.SiegelZerosAwei.W46.master_actual_determinant line 155