OAI/GroupTheory/PolycyclicRecognition/Algebra/PolynomialFamilies.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Fixed-degree polynomial formulas in the independent amplitudes

  1. def OAI.PolycyclicRecognition.HasPolynomialFormula line 16

    Source documentation

    The external parameter changes coefficients, but not the degree bound.

    def HasPolynomialFormula {P : Type*} {m : ℕ} (f : P → (Fin m → ℝ) → ℝ) : Prop :=
…
  2. theorem OAI.PolycyclicRecognition.hasPolynomialFormula_const line 20
  3. theorem OAI.PolycyclicRecognition.hasPolynomialFormula_coordinate line 24
  4. theorem OAI.PolycyclicRecognition.HasPolynomialFormula.add line 28
  5. theorem OAI.PolycyclicRecognition.HasPolynomialFormula.mul line 39
  6. theorem OAI.PolycyclicRecognition.hasPolynomialFormula_sum line 50
  7. def OAI.PolycyclicRecognition.HasPolynomialCoordinates line 62
  8. theorem OAI.PolycyclicRecognition.HasPolynomialCoordinates.exists_uniform_polynomials line 66
  9. theorem OAI.PolycyclicRecognition.hasPolynomialCoordinates_const line 79
  10. theorem OAI.PolycyclicRecognition.HasPolynomialCoordinates.smul line 83
  11. theorem OAI.PolycyclicRecognition.bilinear_pi_expansion line 89
  12. theorem OAI.PolycyclicRecognition.HasPolynomialCoordinates.bilinear line 102