OAI/Combinatorics/StripMass/SpectralComponents.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. lemma OAI.StripComplexification.component_comp line 14
  2. lemma OAI.StripComplexification.component_projection line 26
  3. lemma OAI.StripComplexification.component_degree_le line 36
  4. lemma OAI.StripComplexification.component_natDegree_le line 42
  5. lemma OAI.StripComplexification.component_zero_iff line 48
  6. lemma OAI.StripPfaffian.map_harmonic line 63
  7. lemma OAI.StripPfaffian.map_perturbedRoot line 66
  8. def OAI.StripPfaffian.rootPolynomialC line 72
  9. def OAI.StripPfaffian.homogeneousQC line 75
  10. def OAI.StripPfaffian.PerturbedMonicProblemC line 77
  11. def OAI.StripPfaffian.MonicProblemC line 80
  12. lemma OAI.StripPfaffian.perturbedRoot_homogeneous line 83
  13. lemma OAI.StripPfaffian.homogeneous_projection_zero_complex line 88
  14. theorem OAI.StripPfaffian.harmonic_natDegree line 113
  15. theorem OAI.StripPfaffian.degree_lt_natDegree_le_pred line 117
  16. theorem OAI.StripPfaffian.projection_natDegree_le line 125
  17. abbrev OAI.StripPfaffian.ProjectionSpace line 143
  18. def OAI.StripPfaffian.projectionMap line 146
  19. theorem OAI.StripPfaffian.natDegree_le_of_mem_degreeLT line 156
  20. theorem OAI.StripPfaffian.Epoly_natDegree_le line 162
  21. theorem OAI.StripPfaffian.perturbedRootC_natDegree_le line 172
  22. abbrev OAI.StripPfaffian.SystemSpace line 187
  23. abbrev OAI.StripPfaffian.SystemIndex line 188
  24. def OAI.StripPfaffian.systemBasis line 189
  25. def OAI.StripPfaffian.systemIndexEquiv line 192
  26. def OAI.StripPfaffian.targetBasis line 194
  27. def OAI.StripPfaffian.perturbedSystem line 197
  28. theorem OAI.StripPfaffian.homogeneous_system_injective line 223
  29. def OAI.StripPfaffian.CoeffContinuous line 239
  30. theorem OAI.StripPfaffian.CoeffContinuous.const line 241
  31. theorem OAI.StripPfaffian.CoeffContinuous.C line 243
  32. theorem OAI.StripPfaffian.CoeffContinuous.add line 248
  33. theorem OAI.StripPfaffian.CoeffContinuous.sub line 253
  34. theorem OAI.StripPfaffian.CoeffContinuous.mul line 258
  35. theorem OAI.StripPfaffian.CoeffContinuous.prod line 263
  36. theorem OAI.StripPfaffian.perturbedRootC_continuous line 272
  37. def OAI.StripPfaffian.systemMatrix line 281
  38. theorem OAI.StripPfaffian.target_repr line 283
  39. theorem OAI.StripPfaffian.systemMatrix_continuous line 286
  40. theorem OAI.StripPfaffian.systemMatrix_homogeneous_unit line 295
  41. def OAI.StripPfaffian.systemRHS line 312
  42. def OAI.StripPfaffian.rhsVector line 321
  43. theorem OAI.StripPfaffian.rhsVector_continuous line 323
  44. def OAI.StripPfaffian.solutionVector line 328
  45. def OAI.StripPfaffian.solutionTuple line 330
  46. def OAI.StripPfaffian.confluentPolynomial line 332
  47. theorem OAI.StripPfaffian.solutionVector_continuousAt line 335
  48. theorem OAI.StripPfaffian.confluentPolynomial_continuousAt line 350
  49. theorem OAI.StripPfaffian.solutionTuple_spec line 359
  50. theorem OAI.StripPfaffian.confluentPolynomial_spec line 369
  51. theorem OAI.StripPfaffian.perturbed_unique line 385
  52. lemma OAI.StripPfaffian.real_monic_problem_map line 414