OAI/NumberTheory/CubicMoment/Transform/MetaplecticCubeFiberSum.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite collection of actual primary cube fibers. Compact norm weights remove the output cutoff without adding any support assumption on the arithmetic coefficients.

  1. lemma OAI.CubicFirstMoment.sum_primary_fin_two line 13
  2. theorem OAI.CubicFirstMoment.primary_cube_fiber_weighted_sum line 35