OAI/Combinatorics/StripMass/PolynomialDegrees.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. theorem OAI.CriticalStrip.natDegree_le_of_mem_degreeLT line 13
  2. theorem OAI.CriticalStrip.homogeneous_exists_degree line 21
  3. theorem OAI.CriticalStrip.HasProjection.smul line 61
  4. theorem OAI.CriticalStrip.HasProjection.sub line 69
  5. theorem OAI.CriticalStrip.homogeneous_monic_unique line 81
  6. def OAI.CriticalStrip.perturbedRoot line 112
  7. def OAI.CriticalStrip.PerturbedMonicProblem line 115
  8. theorem OAI.CriticalStrip.paired_homogeneous line 118
  9. theorem OAI.CriticalStrip.perturbedRoot_homogeneous line 142
  10. theorem OAI.CriticalStrip.perturbedRoot_natDegree_le line 149
  11. abbrev OAI.CriticalStrip.SystemSpace line 172
  12. abbrev OAI.CriticalStrip.SystemIndex line 173
  13. def OAI.CriticalStrip.systemBasis line 174
  14. def OAI.CriticalStrip.systemIndexEquiv line 177
  15. def OAI.CriticalStrip.targetBasis line 179
  16. def OAI.CriticalStrip.perturbedSystem line 182
  17. theorem OAI.CriticalStrip.homogeneous_system_injective line 208
  18. def OAI.CriticalStrip.CoeffContinuous line 226
  19. theorem OAI.CriticalStrip.CoeffContinuous.const line 228
  20. theorem OAI.CriticalStrip.CoeffContinuous.C line 230
  21. theorem OAI.CriticalStrip.CoeffContinuous.add line 235
  22. theorem OAI.CriticalStrip.CoeffContinuous.sub line 240
  23. theorem OAI.CriticalStrip.CoeffContinuous.mul line 245
  24. theorem OAI.CriticalStrip.CoeffContinuous.prod line 250
  25. theorem OAI.CriticalStrip.perturbedRoot_continuous line 259
  26. def OAI.CriticalStrip.systemMatrix line 268
  27. theorem OAI.CriticalStrip.target_repr line 270
  28. theorem OAI.CriticalStrip.systemMatrix_continuous line 273
  29. theorem OAI.CriticalStrip.systemMatrix_homogeneous_unit line 282
  30. def OAI.CriticalStrip.systemRHS line 299
  31. def OAI.CriticalStrip.rhsVector line 308
  32. theorem OAI.CriticalStrip.rhsVector_continuous line 310
  33. def OAI.CriticalStrip.solutionVector line 315
  34. def OAI.CriticalStrip.solutionTuple line 317
  35. def OAI.CriticalStrip.confluentPolynomial line 319
  36. theorem OAI.CriticalStrip.solutionVector_continuousAt line 322
  37. theorem OAI.CriticalStrip.confluentPolynomial_continuousAt line 337
  38. theorem OAI.CriticalStrip.solutionTuple_spec line 346
  39. theorem OAI.CriticalStrip.confluentPolynomial_spec line 356
  40. theorem OAI.CriticalStrip.perturbed_unique line 372
  41. theorem OAI.CriticalStrip.perturbed_monic_continuity line 403