OAI/Combinatorics/CompleteCrossing/Polynomials.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

Coordinate symmetry, polynomial quotients, collision divisibility, and specialization.

  1. lemma OAI.Paper170.substitution_difference_dvd line 24
  2. def OAI.Paper170.reinsertDiagonal line 39
  3. theorem OAI.Paper170.diagonal_vanishing_iff_divisible line 42
  4. lemma OAI.Paper170.difference_coefficient line 68
  5. lemma OAI.Paper170.difference_degree line 72
  6. theorem OAI.Paper170.difference_prime line 97
  7. theorem OAI.Paper170.collision_factors_nonassociate line 109
  8. theorem OAI.Paper170.collision_factor_properties line 125
  9. abbrev OAI.Paper170.BoundedExponents line 157
  10. def OAI.Paper170.tupleExponent line 159
  11. lemma OAI.Paper170.tupleExponent_apply line 162
  12. def OAI.Paper170.boxExponentEquiv line 165
  13. lemma OAI.Paper170.box_eq_restrictSupport line 172
  14. def OAI.Paper170.boxBasis line 179
  15. lemma OAI.Paper170.box_finite line 183
  16. lemma OAI.Paper170.boxBasis_repr line 186
  17. theorem OAI.Paper170.symmetric_space_finite line 190
  18. lemma OAI.Paper170.swapFirstPair_mul line 207
  19. lemma OAI.Paper170.swapSecondPair_mul line 211
  20. theorem OAI.Paper170.collision_quotient line 215
  21. theorem OAI.Paper170.local_weight_degrees line 263

    Source documentation

    The three extra factors in the local test have the degree vector printed in the paper.

    theorem local_weight_degrees (i : Fin 4) :
    ((X 1 - X 3) * (X 1 - X 2) * (X 3 - X 0) : Poly4).degreeOf i =
      (![1, 2, 1, 2] : Fin 4 → ℕ) i := by
…

    Mentions: OAI.Paper170.Poly4

  22. theorem OAI.Paper170.difference_quotient_polynomial line 275

    Source documentation

    Identifying any two variables leaves a polynomial ring in the other three.

    theorem difference_quotient_polynomial (i j : Fin 4) (hij : i ≠ j) :
    Nonempty ((Poly4 ⧸ Ideal.span ({X i - X j} : Set Poly4)) ≃ₐ[ℝ]
      MvPolynomial (Fin 3) ℝ) := by
…

    Mentions: OAI.Paper170.Poly4

  23. def OAI.Paper170.diagonalUnivariate line 320
  24. lemma OAI.Paper170.diagonalUnivariate_monomial line 323
  25. lemma OAI.Paper170.diagonalUnivariate_bound line 334
  26. lemma OAI.Paper170.diagonalUnivariate_eval line 350
  27. lemma OAI.Paper170.diagonal_eval line 361
  28. lemma OAI.Paper170.vertex_eval line 372
  29. lemma OAI.Paper170.diagonal_zero_of_vertices line 385
  30. theorem OAI.Paper170.box_rename line 414
  31. theorem OAI.Paper170.coeff_rename_tuple line 422
  32. theorem OAI.Paper170.box_coeff_ext line 431
  33. theorem OAI.Paper170.tuple4_eta line 440
  34. abbrev OAI.Paper170.SymmetricCoordinate line 444
  35. def OAI.Paper170.tupleOrbit line 446
  36. theorem OAI.Paper170.tupleOrbit_swap_first line 449
  37. theorem OAI.Paper170.tupleOrbit_swap_second line 454
  38. theorem OAI.Paper170.symmetric_coeff_first line 459
  39. theorem OAI.Paper170.symmetric_coeff_second line 471
  40. def OAI.Paper170.symmetricCoefficients line 483
  41. theorem OAI.Paper170.symmetricCoefficients_orbit line 488
  42. def OAI.Paper170.realizeBox line 493
  43. theorem OAI.Paper170.realizeBox_coeff line 496
  44. theorem OAI.Paper170.realizeBox_symmetric line 502
  45. def OAI.Paper170.realizeSymmetric line 517
  46. def OAI.Paper170.symmetricCoordinatesEquiv line 520
  47. theorem OAI.Paper170.symmetric_space_dimension line 549
  48. lemma OAI.Paper170.collisionFactors_prime line 569
  49. lemma OAI.Paper170.collisionFactors_coprime line 572
  50. lemma OAI.Paper170.collision_divides_of_diagonal_vanishing line 579