OAI/NumberTheory/PrimePackets/IdealNorms.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PrimeDegreePackets.finite_nonzeroIdeals_norm_le line 42
  2. def OAI.PrimeDegreePackets.normBoundedIdeals line 51
  3. lemma OAI.PrimeDegreePackets.mem_normBoundedIdeals line 54
  4. lemma OAI.PrimeDegreePackets.nonzeroIdeal_absNorm_one_le line 59
  5. lemma OAI.PrimeDegreePackets.normBoundedIdeals_weight_sum_le line 63
  6. theorem OAI.PrimeDegreePackets.packetMeasure_cube_moment_le_log_sum line 78
  7. theorem OAI.PrimeDegreePackets.weightedIdeal_log_sum_cutoff line 141
  8. lemma OAI.PrimeDegreePackets.cutoff_ratio_rpow line 178
  9. theorem OAI.PrimeDegreePackets.packetMeasure_cube_moment_of_count line 187
  10. theorem OAI.PrimeDegreePackets.packet_cube_moment_bounded_discr line 257
  11. theorem OAI.PrimeDegreePackets.packet_tight_bounded_discr line 301
  12. theorem OAI.PrimeDegreePackets.packet_limit_diagonal_invariant line 356
  13. def OAI.PrimeDegreePackets.diagonalOneParameter line 374
  14. def OAI.PrimeDegreePackets.twoSidedTube line 382
  15. lemma OAI.PrimeDegreePackets.conjugation_entry line 387
  16. lemma OAI.PrimeDegreePackets.tube_entries line 398
  17. lemma OAI.PrimeDegreePackets.tube_entries_uniform line 427
  18. lemma OAI.PrimeDegreePackets.exists_two_moved line 443
  19. lemma OAI.PrimeDegreePackets.product_two_small line 455
  20. lemma OAI.PrimeDegreePackets.determinant_diagonal_error line 481
  21. lemma OAI.PrimeDegreePackets.diagonalFlow_neg_log_val line 528
  22. lemma OAI.PrimeDegreePackets.normalizing_scalars_le line 541
  23. lemma OAI.PrimeDegreePackets.normalized_matrix_entry_bound line 565
  24. lemma OAI.PrimeDegreePackets.diagonal_log_mem_compact_box line 608
  25. theorem OAI.PrimeDegreePackets.cube_grid_cover line 621
  26. lemma OAI.PrimeDegreePackets.exp_sub_one_abs_le line 680
  27. lemma OAI.PrimeDegreePackets.diagonalFlow_small_entries line 689
  28. lemma OAI.PrimeDegreePackets.matrix_product_entry_error line 721
  29. theorem OAI.PrimeDegreePackets.near_diagonal_cover line 747
  30. theorem OAI.PrimeDegreePackets.tube_cover line 813
  31. lemma OAI.PrimeDegreePackets.continuous_rightAction_uncurry line 840
  32. def OAI.PrimeDegreePackets.diagonalLogBox line 849
  33. lemma OAI.PrimeDegreePackets.diagonalLogBox_isCompact line 852
  34. lemma OAI.PrimeDegreePackets.compact_diagonal_thickening line 857
  35. def OAI.PrimeDegreePackets.OrdinaryBallBound line 866
  36. lemma OAI.PrimeDegreePackets.ordinaryBallBound_of_le line 871
  37. theorem OAI.PrimeDegreePackets.tube_mass_of_ordinary_balls line 886