OAI/Combinatorics/CompleteCrossing/VertexEvaluation.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Vertex specialization, local interpolation tests, and kernel vanishing.

  1. theorem OAI.Paper170.evalFour_swapFirst line 15
  2. theorem OAI.Paper170.evalFour_swapSecond line 28
  3. theorem OAI.Paper170.vertexSpecialization_monomial line 41
  4. theorem OAI.Paper170.vertexSpecialization_rectangle line 51
  5. theorem OAI.Paper170.neighbor_nodePolynomial line 72
  6. theorem OAI.Paper170.neighbor_nodeWeight line 80
  7. theorem OAI.Paper170.sum_away line 89
  8. theorem OAI.Paper170.kernel_ordered_eval_zero line 106
  9. theorem OAI.Paper170.kernel_independent_eval_zero line 117
  10. theorem OAI.Paper170.evalFour_liftUnivariate line 158
  11. theorem OAI.Paper170.evalFour_liftBivariate13 line 164
  12. theorem OAI.Paper170.evalFour_localTestPolynomial line 173
  13. def OAI.Paper170.vertexTestSummand line 183
  14. theorem OAI.Paper170.vertexTestSummand_offDiagonal line 188
  15. theorem OAI.Paper170.orderPairing_weight_form line 216
  16. theorem OAI.Paper170.vertexTestSummand_diagonal line 228
  17. theorem OAI.Paper170.polynomialTest_local_reduction line 245
  18. def OAI.Paper170.vertexPairingFunctional line 293
  19. theorem OAI.Paper170.vertexPairingFunctional_apply line 300
  20. theorem OAI.Paper170.vertexPairingFunctional_zero line 325
  21. theorem OAI.Paper170.kernel_local_pairing_zero line 348
  22. theorem OAI.Paper170.kernel_vertex_vanishing line 379