OAI/NumberTheory/SiegelZeros/Structure/AffineAssembly.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W01.affine_of_factorization_circle_data line 17
  2. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W01.tendsto_dyadic_logSquare_bound line 78
  3. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W01.affine_of_factorization_dyadic_minimum line 97
  4. theorem OAI.SiegelZeros.SiegelZerosAwei.W51.zeroSubproduct_univ line 131
  5. theorem OAI.SiegelZeros.SiegelZerosAwei.W51.differentiable_canonicalProduct line 136
  6. theorem OAI.SiegelZeros.SiegelZerosAwei.W51.canonicalProduct_ne_zero_of_normalizedCompletion_ne_zero line 142
  7. theorem OAI.SiegelZeros.SiegelZerosAwei.W51.analyticOrderAt_canonicalProduct line 152
  8. theorem OAI.SiegelZeros.SiegelZerosAwei.W51.actual_normalizedQuotient_entire_ne_zero line 173
  9. theorem OAI.SiegelZeros.SiegelZerosAwei.W51.exists_entire_canonicalFactorization line 181
  10. theorem OAI.SiegelZeros.SiegelZerosAwei.W03.actual_zero_norm_lower_bound line 202
  11. theorem OAI.SiegelZeros.SiegelZerosAwei.W03.actual_dyadic_count_bound line 218
  12. theorem OAI.SiegelZeros.SiegelZerosAwei.W03.actual_far_inverse_square_le line 231
  13. theorem OAI.SiegelZeros.SiegelZerosAwei.W03.dyadic_minimum_arithmetic line 253
  14. theorem OAI.SiegelZeros.SiegelZerosAwei.W03.dyadic_log_separation_lower line 287
  15. theorem OAI.SiegelZeros.SiegelZerosAwei.W03.actual_canonicalProduct_dyadic_minimum line 311
  16. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W01.normalizedCompletion_affine_factorization line 385