OAI/Combinatorics/StripMass/ResidualEvaluation.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. lemma OAI.CriticalStrip.Diagram.torusEvaluation_rowNumerator line 14
  2. lemma OAI.CriticalStrip.Diagram.torusEvaluation_residual line 28
  3. lemma OAI.CriticalStrip.Diagram.torusEvaluation_residual_zero line 54
  4. lemma OAI.CriticalStrip.Diagram.permSpectral_rowDenominator line 72
  5. lemma OAI.CriticalStrip.Diagram.permSpectral_rowProduct line 77
  6. lemma OAI.CriticalStrip.Diagram.permSpectral_column_map line 82
  7. lemma OAI.CriticalStrip.Diagram.spectral_column_exchange line 89
  8. lemma OAI.CriticalStrip.Diagram.matrix_residual_covariance line 104
  9. theorem OAI.CriticalStrip.Diagram.rationalInterpolationResidual_covariance line 115
  10. lemma OAI.CriticalStrip.Diagram.torusEvaluation_permLaurent line 142
  11. lemma OAI.CriticalStrip.Diagram.rationalAt_localR line 164
  12. theorem OAI.CriticalStrip.Diagram.residual_zero_transport line 179
  13. lemma OAI.CriticalStrip.Diagram.firstZeroRaw_smul line 223
  14. lemma OAI.CriticalStrip.Diagram.rationalAt_firstFlat_weights line 232
  15. lemma OAI.CriticalStrip.Diagram.rationalAt_firstFlat_normalization line 252
  16. lemma OAI.CriticalStrip.Diagram.rationalAt_firstFlat_vacuum line 263
  17. lemma OAI.CriticalStrip.Diagram.deletionBeta_ne_const line 278
  18. lemma OAI.CriticalStrip.Diagram.firstFlatBeta_injective line 295
  19. lemma OAI.CriticalStrip.Diagram.firstFlatNode_sine_ne_zero line 308
  20. lemma OAI.CriticalStrip.Diagram.torus_firstZero_lastValue line 323
  21. lemma OAI.CriticalStrip.Diagram.rationalAt_last_normalization line 350
  22. lemma OAI.CriticalStrip.Diagram.rationalAt_last_vacuum line 367
  23. lemma OAI.CriticalStrip.Diagram.firstFlat_smaller_values line 381
  24. lemma OAI.CriticalStrip.Diagram.firstFlatNode_ne_zero line 418
  25. lemma OAI.CriticalStrip.Diagram.firstFlatNode_cosine line 424
  26. lemma OAI.CriticalStrip.Diagram.firstFlatNode_L line 433
  27. lemma OAI.CriticalStrip.Diagram.firstFlatNode_weights line 445
  28. lemma OAI.CriticalStrip.Diagram.firstZeroPolynomial_flatNode line 455
  29. theorem OAI.CriticalStrip.Diagram.rationalNodalPolynomial_firstFlat line 483