OAI/NumberTheory/CubicGauss/CubeOperators.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Cube extraction for cubic operators and weighted sums over cube factors.

  1. lemma OAI.CubicFirstMoment.norm_pow_eq line 16
  2. def OAI.CubicFirstMoment.cubicRowEnergy line 21
  3. lemma OAI.CubicFirstMoment.cubicRowEnergy_nonneg line 24
  4. lemma OAI.CubicFirstMoment.cubic_cube_row_twist line 27
  5. lemma OAI.CubicFirstMoment.cubic_cube_row_twist_conj line 38
  6. lemma OAI.CubicFirstMoment.cubic_twist_energy_le line 53
  7. lemma OAI.CubicFirstMoment.cubic_cube_box_bound line 62
  8. abbrev OAI.CubicFirstMoment.CubeIndex line 78
  9. def OAI.CubicFirstMoment.cubeIndices line 80
  10. def OAI.CubicFirstMoment.cubeMap₁ line 86
  11. def OAI.CubicFirstMoment.cubeMap₂ line 87
  12. lemma OAI.CubicFirstMoment.cube_parameter_bounds line 89
  13. lemma OAI.CubicFirstMoment.nonzero_ball_subset_cube_images line 107
  14. lemma OAI.CubicFirstMoment.cubic_full_cube_sum_le line 155
  15. theorem OAI.CubicFirstMoment.cubic_full_cube_bound line 180
  16. def OAI.CubicFirstMoment.latticeZeta line 204
  17. lemma OAI.CubicFirstMoment.latticeZeta_nonneg line 206
  18. lemma OAI.CubicFirstMoment.latticeZeta_pos line 209
  19. lemma OAI.CubicFirstMoment.norm_rpow_finset_le line 216
  20. lemma OAI.CubicFirstMoment.quotient_norm_rpow line 221
  21. lemma OAI.CubicFirstMoment.cube_rpow_sum_bound line 234
  22. lemma OAI.CubicFirstMoment.squarefreePrimaryBall_card_le line 267
  23. lemma OAI.CubicFirstMoment.norm_reciprocal_sum_bound line 272
  24. lemma OAI.CubicFirstMoment.cube_pair_count_bound line 291