OAI/NumberTheory/Ostmann/Characters/PolynomialWeightPair.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The actual off-diagonal product of two polynomial weights

  1. def OAI.Ostmann.ClippedPolynomialFactor.conjugate line 11
  2. theorem OAI.Ostmann.ClippedPolynomialFactor.conjugate_value line 27
  3. def OAI.Ostmann.pairedPolynomialFactors line 30
  4. theorem OAI.Ostmann.pairedPolynomialFactors_weight line 34
  5. theorem OAI.Ostmann.pairedPolynomialFactors_budget line 41
  6. def OAI.Ostmann.polynomialAmplitude line 48
  7. def OAI.Ostmann.pairedPolynomialKeep line 52
  8. theorem OAI.Ostmann.pairedPolynomialAmplitude line 56
  9. theorem OAI.Ostmann.polynomialAmplitude_norm line 75
  10. def OAI.Ostmann.polynomialWeightComplexity line 83
  11. theorem OAI.Ostmann.polynomialWeightComplexity_pair line 87