OAI/NumberTheory/CubicMoment/Estimates/BalancedFullRows.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Collection over the second conductor variable, with literal row fibers.

  1. def OAI.CubicFirstMoment.pairFirstFiber line 12
  2. lemma OAI.CubicFirstMoment.mem_pairFirstFiber line 15
  3. lemma OAI.CubicFirstMoment.pair_sum_fibers line 28
  4. lemma OAI.CubicFirstMoment.balanced_pair_moment_collection line 44
  5. theorem OAI.CubicFirstMoment.balanced_smalltwist_log_pair_power line 66
  6. theorem OAI.CubicFirstMoment.balanced_smalltwist_pair_power line 103