OAI/Combinatorics/PolynomialVacuum/Algebra/SpectralEigenvector.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PolynomialVacuumAlgebra.AnalyticVacuum.four_ne_zero line 9
  2. theorem OAI.PolynomialVacuumAlgebra.AnalyticVacuum.physical_auxiliary line 20
  3. theorem OAI.PolynomialVacuumAlgebra.AnalyticVacuum.physical_fusion line 23
  4. theorem OAI.PolynomialVacuumAlgebra.AnalyticVacuum.physical_cup_denominator line 34
  5. def OAI.PolynomialVacuumAlgebra.AnalyticVacuum.spectralMatrix line 48
  6. def OAI.PolynomialVacuumAlgebra.AnalyticVacuum.rowDenominator line 50
  7. def OAI.PolynomialVacuumAlgebra.AnalyticVacuum.spectralPolynomial line 52
  8. theorem OAI.PolynomialVacuumAlgebra.AnalyticVacuum.rowDenominator_one line 55
  9. theorem OAI.PolynomialVacuumAlgebra.AnalyticVacuum.spectralMatrix_one line 57
  10. theorem OAI.PolynomialVacuumAlgebra.AnalyticVacuum.spectral_fusion_one line 60
  11. theorem OAI.PolynomialVacuumAlgebra.AnalyticVacuum.analytic_spectral_fusion line 63
  12. theorem OAI.PolynomialVacuumAlgebra.AnalyticVacuum.fusion_eventually_ne_zero line 73
  13. theorem OAI.PolynomialVacuumAlgebra.AnalyticVacuum.spectralPolynomial_eigen line 77