OAI/NumberTheory/CubicMoment/Transform/MetaplecticFreeBlock.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Fixed supported parameters only rescale the positive rational frequencies of the free primary polynomial.

  1. lemma OAI.CubicFirstMoment.metaplectic_scaled_free_norm line 13
  2. theorem OAI.CubicFirstMoment.metaplectic_scaled_free_meanAbsolute line 27