OAI/Computability/DirectedFeedback/Games/BlockOrientations.lean

GitHub source file

78 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DFVSGames.Quadratic.BlockOrientation line 10
  2. instance OAI.DFVSGames.Quadratic.fieldLineFintype line 13
  3. instance OAI.DFVSGames.Quadratic.finiteBlockOrientation line 15
  4. instance OAI.DFVSGames.Quadratic.blockOrientationFintype line 18
  5. def OAI.DFVSGames.Quadratic.chosenBlockOrientation line 21
  6. def OAI.DFVSGames.Quadratic.blockOrientationEquiv line 25
  7. theorem OAI.DFVSGames.Quadratic.card_blockOrientation line 38
  8. theorem OAI.DFVSGames.Quadratic.card_blockOrientation_eq line 42
  9. theorem OAI.DFVSGames.Quadratic.card_blockOrientation_pos line 46
  10. abbrev OAI.DFVSGames.Quadratic.BlockOrientationIndex line 51
  11. def OAI.DFVSGames.Quadratic.blockOrientationIndexEquiv line 54
  12. theorem OAI.DFVSGames.Quadratic.card_blockOrientationIndex line 65
  13. def OAI.DFVSGames.Quadratic.blockObservable line 76
  14. theorem OAI.DFVSGames.Quadratic.blockObservable_difference line 79
  15. theorem OAI.DFVSGames.Quadratic.blockObservable_difference_parametrized line 90
  16. def OAI.DFVSGames.Quadratic.hyperplaneNoiseShift line 97
  17. def OAI.DFVSGames.Quadratic.noiseParameterShift line 112
  18. def OAI.DFVSGames.Quadratic.blockNoiseCoordinates line 129
  19. theorem OAI.DFVSGames.Quadratic.blockObservable_difference_eq_noiseCoordinate line 132
  20. theorem OAI.DFVSGames.Quadratic.vec_add_eq_zero_iff_inline_BlockNoise line 139
  21. theorem OAI.DFVSGames.Quadratic.blockObservable_changes_iff line 147
  22. theorem OAI.DFVSGames.Quadratic.blockObservable_change_ne_zero line 158
  23. def OAI.DFVSGames.Quadratic.changedCoordinatesEquiv line 164
  24. theorem OAI.DFVSGames.Quadratic.natCard_ne_zero_inline_BlockNoise line 177
  25. theorem OAI.DFVSGames.Quadratic.natCard_line line 184
  26. theorem OAI.DFVSGames.Quadratic.natCard_hyperplane line 188
  27. theorem OAI.DFVSGames.Quadratic.natCard_U line 192
  28. theorem OAI.DFVSGames.Quadratic.natCard_block_changes line 200
  29. theorem OAI.DFVSGames.Quadratic.natCard_nonzero_U line 207
  30. theorem OAI.DFVSGames.Quadratic.block_change_ratio line 211
  31. abbrev OAI.DFVSGames.Quadratic.NonzeroBlock line 234
  32. def OAI.DFVSGames.Quadratic.nonzeroBlockChangeProbability line 236
  33. def OAI.DFVSGames.Quadratic.conditionedChangedEquiv line 241
  34. theorem OAI.DFVSGames.Quadratic.nonzeroBlockChangeProbability_eq_count line 250
  35. theorem OAI.DFVSGames.Quadratic.nonzeroBlockChangeProbability_eq line 266
  36. def OAI.DFVSGames.Gadget.OrientedBlockKernel.orientedBlockLinear line 296
  37. def OAI.DFVSGames.Gadget.OrientedBlockKernel.orientedBlockChange line 300
  38. theorem OAI.DFVSGames.Gadget.OrientedBlockKernel.mean_orientations_change line 307
  39. theorem OAI.DFVSGames.Gadget.OrientedBlockKernel.mean_block_pairs line 325
  40. theorem OAI.DFVSGames.Gadget.OrientedBlockKernel.mean_oriented_block_change line 343
  41. theorem OAI.DFVSGames.Gadget.OrientedBlockKernel.mean_oriented_block_kernel line 353
  42. theorem OAI.DFVSGames.Quadratic.squareMap_injective line 369
  43. def OAI.DFVSGames.Quadratic.squareRoot line 377
  44. theorem OAI.DFVSGames.Quadratic.squareRoot_sq line 380
  45. theorem OAI.DFVSGames.Quadratic.squareRoot_of_sq line 383
  46. theorem OAI.DFVSGames.Quadratic.squareRoot_unique line 387
  47. abbrev OAI.DFVSGames.Quadratic.traceBinary line 398
  48. theorem OAI.DFVSGames.Quadratic.trace_square line 401
  49. theorem OAI.DFVSGames.Quadratic.trace_square_mul line 407
  50. theorem OAI.DFVSGames.Quadratic.trace_mul_vanish_iff line 416
  51. theorem OAI.DFVSGames.Quadratic.trace_quadratic_vanish_iff line 426
  52. theorem OAI.DFVSGames.Quadratic.dot_add_first_inline_TraceDual line 443
  53. def OAI.DFVSGames.Quadratic.traceDotForm line 448
  54. theorem OAI.DFVSGames.Quadratic.traceDotForm_apply line 477
  55. theorem OAI.DFVSGames.Quadratic.traceDotForm_nondegenerate line 482
  56. def OAI.DFVSGames.Quadratic.traceDualEquiv line 502
  57. theorem OAI.DFVSGames.Quadratic.traceDualEquiv_apply line 507
  58. theorem OAI.DFVSGames.Quadratic.traceDualEquiv_symm_apply line 510
  59. def OAI.DFVSGames.Quadratic.representTraceFamily line 518
  60. theorem OAI.DFVSGames.Quadratic.representTraceFamily_spec line 522
  61. theorem OAI.DFVSGames.Quadratic.dot_sub_right_inline_BlockTrace line 535
  62. theorem OAI.DFVSGames.Quadratic.dot_single_inline_BlockTrace line 540
  63. theorem OAI.DFVSGames.Quadratic.annihilator_hyperplane_iff_mem_line line 544
  64. theorem OAI.DFVSGames.Quadratic.trace_annihilator_hyperplane_iff_mem_line line 574
  65. theorem OAI.DFVSGames.Quadratic.trace_annihilator_hyperplane line 587
  66. theorem OAI.DFVSGames.Quadratic.dot_Q_smul line 601
  67. def OAI.DFVSGames.Quadratic.blockCharacter line 612
  68. def OAI.DFVSGames.Quadratic.BlockAnnihilates line 615
  69. theorem OAI.DFVSGames.Quadratic.blockCharacter_on_quadratic line 619
  70. theorem OAI.DFVSGames.Quadratic.blockAnnihilates_self_iff line 624
  71. theorem OAI.DFVSGames.Quadratic.U_smul_ne_zero line 644
  72. theorem OAI.DFVSGames.Quadratic.U_eq_of_nonzero_mem_line line 651
  73. theorem OAI.DFVSGames.Quadratic.mem_line_of_blockAnnihilates line 660
  74. theorem OAI.DFVSGames.Quadratic.blockAnnihilates_iff line 669
  75. def OAI.DFVSGames.Quadratic.alignmentMatrix line 695
  76. theorem OAI.DFVSGames.Quadratic.dot_lift_eq_alignment_mulVec line 699
  77. theorem OAI.DFVSGames.Quadratic.exists_lift_alignment_iff_mem_range line 719
  78. theorem OAI.DFVSGames.Quadratic.finrank_alignment_range_le line 742