OAI/Combinatorics/CompleteCrossing/Interpolation.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

Bivariate interpolation degrees, spaces, pairings, and polynomial tests.

  1. theorem OAI.Paper170.rectangle_membership line 27
  2. theorem OAI.Paper170.box4_membership line 33
  3. theorem OAI.Paper170.symmetric_space_membership line 39
  4. theorem OAI.Paper170.derivative_product line 44
  5. theorem OAI.Paper170.weight_nonzero line 49
  6. theorem OAI.Paper170.interpolation_weights line 54
  7. theorem OAI.Paper170.omitted_node_weight line 61
  8. theorem OAI.Paper170.weighted_chain_boundary line 77
  9. theorem OAI.Paper170.degreeOf_mul_bound line 103
  10. theorem OAI.Paper170.degreeOf_liftUnivariate line 107
  11. theorem OAI.Paper170.liftBivariate_eq_rename line 124
  12. theorem OAI.Paper170.degreeOf_rename_zero line 132
  13. theorem OAI.Paper170.degreeOf_liftBivariate13 line 139
  14. theorem OAI.Paper170.degreeOf_difference_bound line 151
  15. theorem OAI.Paper170.local_test_degree line 157
  16. theorem OAI.Paper170.evalTwo_monomial line 192
  17. theorem OAI.Paper170.weighted_evalTwo_second_zero line 201
  18. theorem OAI.Paper170.weighted_evalTwo_first_zero line 224
  19. theorem OAI.Paper170.weightedPairing_add line 247
  20. theorem OAI.Paper170.evalTwo_difference_mul line 253
  21. theorem OAI.Paper170.pairing_row_column_invariant line 258
  22. def OAI.Paper170.exponentPair line 325
  23. theorem OAI.Paper170.exponentPair_symm_zero line 333
  24. theorem OAI.Paper170.exponentPair_symm_one line 334
  25. theorem OAI.Paper170.rectangle_eq_restrictSupport line 336
  26. def OAI.Paper170.rectangleExponentEquiv line 344
  27. def OAI.Paper170.rectangleBasis line 353
  28. theorem OAI.Paper170.rectangle_finite line 357
  29. theorem OAI.Paper170.rectangle_dimension line 360
  30. def OAI.Paper170.toBiPolynomial line 366

    Source documentation

    The coefficient-preserving bridge to the existing bivariate interpolation library.

    def toBiPolynomial : Poly2 ≃ₗ[ℝ] Zarankiewicz.BiPoly :=
…

    Mentions: OAI.Paper170.Poly2, OAI.Zarankiewicz.BiPoly

  31. theorem OAI.Paper170.toBiPolynomial_coeff line 370
  32. theorem OAI.Paper170.toBiPolynomial_monomial line 378
  33. theorem OAI.Paper170.toBiPolynomial_eval line 399
  34. theorem OAI.Paper170.toBiPolynomial_bounded line 415
  35. def OAI.Paper170.polynomialTestLinear line 449
  36. theorem OAI.Paper170.polynomialTestLinear_apply line 454
  37. theorem OAI.Paper170.evalFour_monomial line 458
  38. theorem OAI.Paper170.polynomialTest_monomial line 467
  39. theorem OAI.Paper170.polynomial_cycle_tests line 482
  40. theorem OAI.Paper170.products_span_degree line 498