OAI/NumberTheory/SiegelZeros/Determinants/NormSqReal.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.WeightedTorusJets.norm_of_sq_eq_real line 25
  2. theorem OAI.SiegelZeros.WeightedTorusJets.norm_biquadratic_box_le line 29
  3. theorem OAI.SiegelZeros.WeightedTorusJets.norm_embedding_biquadratic_box_le line 56
  4. theorem OAI.SiegelZeros.WeightedTorusJets.norm_three_powers_le line 69
  5. theorem OAI.SiegelZeros.WeightedTorusJets.norm_embedding_basis_sum_le line 76
  6. theorem OAI.SiegelZeros.WeightedTorusJets.norm_embedding_derivative_entry_le line 86
  7. theorem OAI.SiegelZeros.WeightedTorusJets.abs_field_norm_eq_prod_embeddings line 109
  8. theorem OAI.SiegelZeros.WeightedTorusJets.log_abs_field_norm_eq_sum_embeddings line 114
  9. theorem OAI.SiegelZeros.WeightedTorusJets.quarter_log_field_norm_le_of_embeddings line 120
  10. theorem OAI.SiegelZeros.WeightedTorusJets.archimedean_jet_determinant_bound line 133
  11. theorem OAI.SiegelZeros.WeightedTorusJets.archimedean_bound_of_integral_jet_determinant line 163
  12. theorem OAI.SiegelZeros.WeightedTorusJets.quarter_log_field_norm_lower line 196
  13. theorem OAI.SiegelZeros.WeightedTorusJets.prime_floor_sum_lower_raw line 223
  14. theorem OAI.SiegelZeros.WeightedTorusJets.finite_place_raw_norm_bounds line 247
  15. theorem OAI.SiegelZeros.WeightedTorusJets.prime_floor_sum_lower line 263
  16. theorem OAI.SiegelZeros.WeightedTorusJets.finite_place_bounds_of_source_determinant line 282
  17. theorem OAI.SiegelZeros.WeightedTorusJets.source_character_global_greedy_determinant_local_bounds line 325
  18. theorem OAI.SiegelZeros.WeightedTorusJets.finite_place_lower_of_source_determinant line 420
  19. theorem OAI.SiegelZeros.WeightedTorusJets.three_le_level_of_nonprincipal line 441
  20. theorem OAI.SiegelZeros.WeightedTorusJets.source_given_determinant_finite_lower_of_real_zero line 460