OAI/Computability/DirectedFeedback/Games/GenericPolynomial.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DFVSGames.Quadratic.zmodTwo_sq line 14
  2. theorem OAI.DFVSGames.Quadratic.expand_two_eq_sq line 24
  3. theorem OAI.DFVSGames.Quadratic.exists_coordinate_separator line 29
  4. def OAI.DFVSGames.Quadratic.universalLinearForm line 50
  5. def OAI.DFVSGames.Quadratic.universalAlignmentColumn line 54
  6. theorem OAI.DFVSGames.Quadratic.universalLinearForm_prod line 58
  7. def OAI.DFVSGames.Quadratic.cubicPairing line 68
  8. def OAI.DFVSGames.Quadratic.alignmentObstruction line 73
  9. theorem OAI.DFVSGames.Quadratic.alignmentObstruction_parity_expansion line 78
  10. theorem OAI.DFVSGames.Quadratic.alignmentObstruction_ne_zero line 94
  11. theorem OAI.DFVSGames.Quadratic.eq_top_of_binary_coordinates line 111
  12. def OAI.DFVSGames.Quadratic.quadraticEvaluationSpan line 170
  13. def OAI.DFVSGames.Quadratic.cubicEvaluationSpan line 174
  14. theorem OAI.DFVSGames.Quadratic.eq_top_of_cubic_le_of_le_quadratic line 179
  15. theorem OAI.DFVSGames.Quadratic.quadraticEvaluationSpan_eq_top_of_cubic_le line 228
  16. theorem OAI.DFVSGames.Quadratic.binary_eq_zero_or_one line 238
  17. theorem OAI.DFVSGames.Quadratic.eq_top_of_binary_evaluation_stable line 243
  18. theorem OAI.DFVSGames.Quadratic.exists_cubic_not_mem_of_finrank_lt line 285
  19. theorem OAI.DFVSGames.Quadratic.exists_polynomial_alignment_annihilator line 313
  20. theorem OAI.DFVSGames.Quadratic.alignmentObstruction_eval_eq_zero line 413
  21. theorem OAI.DFVSGames.Quadratic.exists_nonzero_alignment_obstruction line 446
  22. def OAI.DFVSGames.Quadratic.parameterMap line 473
  23. theorem OAI.DFVSGames.Quadratic.parameterMap_apply line 477
  24. theorem OAI.DFVSGames.Quadratic.parameterMap_basis line 483
  25. theorem OAI.DFVSGames.Quadratic.eval_universalLinearForm line 490
  26. theorem OAI.DFVSGames.Quadratic.dot_parameter_lift line 497
  27. theorem OAI.DFVSGames.Quadratic.alignmentRightHandSide_sq line 511
  28. theorem OAI.DFVSGames.Quadratic.exists_all_lifts_alignment_polynomial line 527
  29. theorem OAI.DFVSGames.Quadratic.exists_binary_coordinate_one line 593
  30. theorem OAI.DFVSGames.Quadratic.exists_binary_minor_one line 598
  31. def OAI.DFVSGames.Quadratic.selectorAssignment line 617
  32. theorem OAI.DFVSGames.Quadratic.eval_universalLinearForm_selector_zero line 622
  33. theorem OAI.DFVSGames.Quadratic.eval_universalLinearForm_selector_one line 627
  34. theorem OAI.DFVSGames.Quadratic.universalLinearForm_zero_ne_zero line 632
  35. def OAI.DFVSGames.Quadratic.universalPairMinor line 640
  36. theorem OAI.DFVSGames.Quadratic.universalPairMinor_ne_zero line 645
  37. theorem OAI.DFVSGames.Quadratic.universalPairMinor_eq_zero_of_proportional line 657
  38. def OAI.DFVSGames.Quadratic.nonzeroBinaryInputs line 679
  39. def OAI.DFVSGames.Quadratic.distinctNonzeroBinaryPairs line 683
  40. def OAI.DFVSGames.Quadratic.separationPolynomial line 687
  41. theorem OAI.DFVSGames.Quadratic.separationPolynomial_ne_zero line 691
  42. theorem OAI.DFVSGames.Quadratic.parameterMap_separated_of_eval_ne_zero line 705