OAI/NumberTheory/Jacobsthal/Siegel/NormSqReal.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.WeightedTorusJets.norm_of_sq_eq_real line 27
  2. theorem OAI.Erdos970.WeightedTorusJets.norm_biquadratic_box_le line 31
  3. theorem OAI.Erdos970.WeightedTorusJets.norm_embedding_biquadratic_box_le line 58
  4. theorem OAI.Erdos970.WeightedTorusJets.norm_three_powers_le line 71
  5. theorem OAI.Erdos970.WeightedTorusJets.norm_embedding_basis_sum_le line 78
  6. theorem OAI.Erdos970.WeightedTorusJets.norm_embedding_derivative_entry_le line 88
  7. theorem OAI.Erdos970.WeightedTorusJets.abs_field_norm_eq_prod_embeddings line 111
  8. theorem OAI.Erdos970.WeightedTorusJets.log_abs_field_norm_eq_sum_embeddings line 116
  9. theorem OAI.Erdos970.WeightedTorusJets.quarter_log_field_norm_le_of_embeddings line 122
  10. theorem OAI.Erdos970.WeightedTorusJets.archimedean_jet_determinant_bound line 135
  11. theorem OAI.Erdos970.WeightedTorusJets.archimedean_bound_of_integral_jet_determinant line 165
  12. theorem OAI.Erdos970.WeightedTorusJets.quarter_log_field_norm_lower line 198
  13. theorem OAI.Erdos970.WeightedTorusJets.prime_floor_sum_lower_raw line 225
  14. theorem OAI.Erdos970.WeightedTorusJets.finite_place_raw_norm_bounds line 249
  15. theorem OAI.Erdos970.WeightedTorusJets.prime_floor_sum_lower line 265
  16. theorem OAI.Erdos970.WeightedTorusJets.finite_place_bounds_of_source_determinant line 284
  17. theorem OAI.Erdos970.WeightedTorusJets.source_character_global_greedy_determinant_local_bounds line 327
  18. theorem OAI.Erdos970.WeightedTorusJets.finite_place_lower_of_source_determinant line 422
  19. theorem OAI.Erdos970.WeightedTorusJets.three_le_level_of_nonprincipal line 443
  20. theorem OAI.Erdos970.WeightedTorusJets.source_given_determinant_finite_lower_of_real_zero line 462