OAI/NumberTheory/CubicMoment/Transform/MetaplecticRadialSelected.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Summing the actual radial lattice-to-residue error over an arbitrary level selector. All constants precede the selector and its coefficient family.

  1. theorem OAI.CubicFirstMoment.LogarithmicWeightFamily.radial_selected_error line 13