OAI/NumberTheory/PrimePackets/PacketMoments.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PrimeDegreePackets.saturationIndex_le_packetScale line 39
  2. lemma OAI.PrimeDegreePackets.nonzeroIdealWeight_eq_global line 45
  3. theorem OAI.PrimeDegreePackets.packetMeasure_box_moment_le_count line 51
  4. lemma OAI.PrimeDegreePackets.packet_moment_normalization line 116
  5. theorem OAI.PrimeDegreePackets.box_interval_parameters line 149
  6. lemma OAI.PrimeDegreePackets.packet_box_constant_identity line 215
  7. theorem OAI.PrimeDegreePackets.packetMeasure_box_moment_of_count line 228
  8. theorem OAI.PrimeDegreePackets.packet_box_moment_bounded_discr line 267
  9. def OAI.PrimeDegreePackets.rightActionHomeomorph line 312
  10. theorem OAI.PrimeDegreePackets.right_invariance_of_tendsto line 322
  11. theorem OAI.PrimeDegreePackets.tight_probability_subsequence line 338
  12. lemma OAI.PrimeDegreePackets.weakProbabilityConvergence_iff line 354
  13. theorem OAI.PrimeDegreePackets.tendsto_of_tight_of_unique_subsequential_limit line 364
  14. theorem OAI.PrimeDegreePackets.quotient_covering line 384
  15. def OAI.PrimeDegreePackets.matrixBall line 394
  16. lemma OAI.PrimeDegreePackets.matrixBall_isOpen line 397
  17. lemma OAI.PrimeDegreePackets.right_ball_isOpen line 407
  18. lemma OAI.PrimeDegreePackets.vecMul_sub_coordinate_le line 418
  19. theorem OAI.PrimeDegreePackets.exists_integer_row_no_zero_coordinate line 441
  20. def OAI.PrimeDegreePackets.vectorEnvelope line 475
  21. lemma OAI.PrimeDegreePackets.continuous_integer_row_coordinate line 481
  22. lemma OAI.PrimeDegreePackets.vectorEnvelope_isOpen line 490
  23. lemma OAI.PrimeDegreePackets.vectorEnvelope_mono line 514
  24. lemma OAI.PrimeDegreePackets.mem_vectorEnvelope line 522
  25. theorem OAI.PrimeDegreePackets.compact_uniform_vector_envelope line 545
  26. def OAI.PrimeDegreePackets.orthoBox line 563
  27. lemma OAI.PrimeDegreePackets.orthoBox_preimage line 568
  28. lemma OAI.PrimeDegreePackets.orthoBox_volume line 573
  29. lemma OAI.PrimeDegreePackets.orthoBox_convex line 586
  30. lemma OAI.PrimeDegreePackets.orthoBox_symmetric line 594
  31. lemma OAI.PrimeDegreePackets.orthoBox_norm_le line 601
  32. lemma OAI.PrimeDegreePackets.orthoBox_norm_le_of_zero_first line 611
  33. lemma OAI.PrimeDegreePackets.exists_orthonormal_first_perp line 626
  34. theorem OAI.PrimeDegreePackets.bounded_vector_outside_subspace line 649
  35. theorem OAI.PrimeDegreePackets.bounded_real_basis_in_lattice line 703
  36. def OAI.PrimeDegreePackets.rowBasis line 736
  37. lemma OAI.PrimeDegreePackets.rowBasis_apply line 739
  38. def OAI.PrimeDegreePackets.euclideanRowBasis line 745
  39. lemma OAI.PrimeDegreePackets.euclideanRowBasis_apply line 749
  40. lemma OAI.PrimeDegreePackets.euclideanRowBasis_volume line 753
  41. lemma OAI.PrimeDegreePackets.sum_euclideanRowBasis line 771
  42. theorem OAI.PrimeDegreePackets.bounded_independent_rows line 779
  43. def OAI.PrimeDegreePackets.coordinateMod line 825
  44. lemma OAI.PrimeDegreePackets.coordinateMod_ker line 830
  45. lemma OAI.PrimeDegreePackets.finite_integral_submodules_above_mod line 843
  46. def OAI.PrimeDegreePackets.columnModule line 859
  47. lemma OAI.PrimeDegreePackets.det_smul_mem_columnModule line 862
  48. lemma OAI.PrimeDegreePackets.coordinateMod_ker_le_columnModule line 868
  49. theorem OAI.PrimeDegreePackets.finite_bounded_column_modules line 881
  50. lemma OAI.PrimeDegreePackets.exists_int_matrix_of_columnModule_le line 888
  51. lemma OAI.PrimeDegreePackets.exists_SL_of_columnModule_eq line 905
  52. theorem OAI.PrimeDegreePackets.finite_bounded_matrix_representatives line 925
  53. lemma OAI.PrimeDegreePackets.exists_SL_of_signed_columnModule_eq line 947
  54. theorem OAI.PrimeDegreePackets.finite_bounded_nonsingular_matrix_representatives line 972
  55. theorem OAI.PrimeDegreePackets.bounded_SL_representatives line 1006
  56. def OAI.PrimeDegreePackets.thickLattices line 1063
  57. lemma OAI.PrimeDegreePackets.continuous_integer_row line 1067
  58. lemma OAI.PrimeDegreePackets.thickLattices_isClosed line 1075
  59. theorem OAI.PrimeDegreePackets.mahler_compact line 1094
  60. def OAI.PrimeDegreePackets.packetSupport line 1122
  61. lemma OAI.PrimeDegreePackets.packetSupport_isCompact line 1126
  62. lemma OAI.PrimeDegreePackets.orbitProbability_compl_range line 1133
  63. theorem OAI.PrimeDegreePackets.packetMeasure_compl_support line 1148