OAI/NumberTheory/PiExponent/Approximation/FrameEquationFamily.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PiExponent.FrameEquationFamily.BoundedWords line 11
  2. def OAI.PiExponent.FrameEquationFamily.equations line 14
  3. theorem OAI.PiExponent.FrameEquationFamily.equations_mem line 18
  4. theorem OAI.PiExponent.FrameEquationFamily.span_equations line 23
  5. theorem OAI.PiExponent.FrameEquationFamily.monomialWeight_eq_weight line 36
  6. theorem OAI.PiExponent.FrameEquationFamily.hasWeightedDegreeLE_iff_supportBound line 41
  7. theorem OAI.PiExponent.FrameEquationFamily.equation_hasWeightedDegreeLE line 46
  8. theorem OAI.PiExponent.FrameEquationFamily.equation_supportBound line 53
  9. def OAI.PiExponent.FrameEquationFamily.sliceEquations line 63
  10. theorem OAI.PiExponent.FrameEquationFamily.span_sliceEquations line 68
  11. theorem OAI.PiExponent.FrameEquationFamily.sliceEquation_supportBound line 82
  12. theorem OAI.PiExponent.FrameEquationFamily.sliceEquation_weighted_sum_le line 92
  13. theorem OAI.PiExponent.FrameEquationFamily.sliceEquation_eval line 103