OAI/NumberTheory/CubicGauss/FiniteOperators.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Finite Fourier orthogonality and row-column operator duality.

  1. lemma OAI.CubicFirstMoment.SieveFourier.finite_fourier_parseval line 15
  2. lemma OAI.CubicFirstMoment.SieveFourier.saturated_gauss_nonunit line 47
  3. lemma OAI.CubicFirstMoment.SieveFourier.saturated_gauss_mulShift line 73
  4. def OAI.CubicFirstMoment.SieveOperator.Bound line 85
  5. lemma OAI.CubicFirstMoment.SieveOperator.sum_mul_norm_sq line 88
  6. lemma OAI.CubicFirstMoment.SieveOperator.Bound.transpose line 97