OAI/Analysis/FactorGeneration/Coefficients.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Coefficientwise absolute-value product comparison, retaining all convolution terms contributing to the same group element.

  1. def OAI.Generator.normCoefficients line 17
  2. theorem OAI.Generator.normCoefficients_apply line 21
  3. theorem OAI.Generator.normCoefficients_support line 25
  4. theorem OAI.Generator.normCoefficients_nonnegative line 31
  5. theorem OAI.Generator.normCoefficients_mul_le line 36

    Source documentation

    Exact source inequality |fg|(w) ≤ (|f| |g|)(w), including cancellations.

    theorem normCoefficients_mul_le (f g : MonoidAlgebra ℂ G) (w : G) :
    (normCoefficients (f * g)).coeff w ≤
      (normCoefficients f * normCoefficients g).coeff w := by
…

    Mentions: OAI.Generator.normCoefficients

  6. theorem OAI.Generator.normCoefficients_add_le line 57

    Source documentation

    The corresponding additive coefficient comparison.

    theorem normCoefficients_add_le (f g : MonoidAlgebra ℂ G) (w : G) :
    (normCoefficients (f + g)).coeff w ≤
      (normCoefficients f + normCoefficients g).coeff w :=
…

    Mentions: OAI.Generator.normCoefficients

  7. instance OAI.Generator.CoefficientOrder.coefficientPartialOrder line 71
  8. theorem OAI.Generator.CoefficientOrder.le_iff line 75
  9. instance OAI.Generator.CoefficientOrder.coefficientOrderedAdd line 77
  10. instance OAI.Generator.CoefficientOrder.coefficientZeroLEOne line 80
  11. theorem OAI.Generator.CoefficientOrder.mul_nonnegative line 87
  12. theorem OAI.Generator.CoefficientOrder.mul_le_left line 100
  13. theorem OAI.Generator.CoefficientOrder.mul_le_right line 107
  14. instance OAI.Generator.CoefficientOrder.coefficientOrderedRing line 114