OAI/Combinatorics/CompleteCrossing/OrderPairing.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Order-detecting interpolation and its kernel.

  1. def OAI.Paper170.evenTriangleWeight line 15
  2. theorem OAI.Paper170.evenTriangleWeight_ne_zero line 19
  3. theorem OAI.Paper170.shifted_halfOrder line 31
  4. theorem OAI.Paper170.orderPairing_triangle line 46
  5. theorem OAI.Paper170.derivativeAtNode_equiv line 77
  6. theorem OAI.Paper170.weightedPairing_equiv line 86
  7. theorem OAI.Paper170.orderPairing_orderIso line 102
  8. theorem OAI.Paper170.order_pairing_nonsingular_fin line 123
  9. theorem OAI.Paper170.order_pairing_nonsingular line 159
  10. theorem OAI.Paper170.order_detector line 181