OAI/NumberTheory/CubicMoment/Transform/MetaplecticRetainedMean.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The whole actual retained polynomial, with its fixed cutoff, is controlled by its canonical finite norm-dyad partition.

  1. lemma OAI.CubicFirstMoment.mean_norm_finset_sum_normalized line 14
  2. theorem OAI.CubicFirstMoment.metaplectic_actual_retained_mean line 25