OAI/NumberTheory/CubicMoment/Transform/MetaplecticNegativeKernel.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The same actual critical kernel on the negative height dyad. Conjugating the coefficients supplies the required opposite-sign mean.

  1. theorem OAI.CubicFirstMoment.metaplectic_negative_kernel_mean line 14
  2. theorem OAI.CubicFirstMoment.metaplectic_actual_retained_negative_kernel line 42