OAI/Computability/DirectedFeedback/Games/Genericity.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Quadratic.alignmentEvent line 20
  2. theorem OAI.DFVSGames.Quadratic.all_lifts_bound_iff_subsets line 25
  3. theorem OAI.DFVSGames.Quadratic.all_lifts_bound_of_card_le line 58
  4. def OAI.DFVSGames.Quadratic.alignmentRightHandSide line 72
  5. def OAI.DFVSGames.Quadratic.IsGeneric line 74
  6. theorem OAI.DFVSGames.Quadratic.finrank_le_one_of_nonzero_unique line 96
  7. theorem OAI.DFVSGames.Quadratic.finrank_ker_le_one_of_nonzero_unique line 114
  8. theorem OAI.DFVSGames.Quadratic.finrank_source_le_range_add_one line 130
  9. def OAI.DFVSGames.Quadratic.lossIndices line 140
  10. def OAI.DFVSGames.Quadratic.alignedCharacters line 144
  11. theorem OAI.DFVSGames.Quadratic.lossIndices_subset_image line 148
  12. theorem OAI.DFVSGames.Quadratic.card_lossIndices_le_card_aligned line 159
  13. theorem OAI.DFVSGames.Quadratic.card_lossIndices_le line 167
  14. theorem OAI.DFVSGames.Quadratic.card_lossIndices_le_nonzero line 174
  15. theorem OAI.DFVSGames.Quadratic.dot_add_first_inline_BlockRestriction line 194
  16. def OAI.DFVSGames.Quadratic.blockCharacterLinear line 199
  17. def OAI.DFVSGames.Quadratic.blockRestriction line 214
  18. theorem OAI.DFVSGames.Quadratic.blockRestriction_apply line 235
  19. theorem OAI.DFVSGames.Quadratic.blockRestriction_eq_zero_iff line 241
  20. theorem OAI.DFVSGames.Quadratic.mem_ker_blockRestriction_iff line 251
  21. theorem OAI.DFVSGames.Quadratic.blockRestriction_nonzero_kernel_unique line 260
  22. theorem OAI.DFVSGames.Quadratic.finrank_ker_blockRestriction_le_one line 281
  23. theorem OAI.DFVSGames.Quadratic.finrank_blockRestriction_source_le_range_add_one line 288
  24. def OAI.DFVSGames.Quadratic.orientedBlockRestriction line 307
  25. theorem OAI.DFVSGames.Quadratic.orientedBlockRestriction_apply line 313
  26. theorem OAI.DFVSGames.Quadratic.orientedBlockRestriction_eq_zero_iff line 319
  27. theorem OAI.DFVSGames.Quadratic.ker_orientedBlockRestriction line 332
  28. theorem OAI.DFVSGames.Quadratic.ker_orientedBlockRestriction_independent line 340
  29. theorem OAI.DFVSGames.Quadratic.mem_ker_orientedBlockRestriction_iff line 347
  30. theorem OAI.DFVSGames.Quadratic.finrank_ker_orientedBlockRestriction_le_one line 357
  31. abbrev OAI.DFVSGames.Gadget.BlockDescent.BinaryDual line 376
  32. def OAI.DFVSGames.Gadget.BlockDescent.traceSpace line 378
  33. def OAI.DFVSGames.Gadget.BlockDescent.traceSpaceEquiv line 381
  34. theorem OAI.DFVSGames.Gadget.BlockDescent.traceSpace_finrank line 387
  35. theorem OAI.DFVSGames.Gadget.BlockDescent.traceSpaceEquiv_apply_val line 392
  36. theorem OAI.DFVSGames.Gadget.BlockDescent.traceSpaceEquiv_symm_val line 397
  37. def OAI.DFVSGames.Gadget.BlockDescent.traceLift line 404
  38. theorem OAI.DFVSGames.Gadget.BlockDescent.childCharacter_comp_traceSpaceEquiv line 408
  39. theorem OAI.DFVSGames.Gadget.BlockDescent.childCharacter_range_eq line 426
  40. theorem OAI.DFVSGames.Gadget.BlockDescent.childCharacter_range_eq_dual_pullback line 435
  41. theorem OAI.DFVSGames.Gadget.BlockDescent.childCharacter_rank_independent line 444
  42. def OAI.DFVSGames.Gadget.Descent.commonGamma line 468
  43. theorem OAI.DFVSGames.Gadget.Descent.commonGamma_spec line 474
  44. def OAI.DFVSGames.Gadget.Descent.childDomain line 480
  45. def OAI.DFVSGames.Gadget.Descent.childLift line 484
  46. def OAI.DFVSGames.Gadget.Descent.childSection line 490
  47. theorem OAI.DFVSGames.Gadget.Descent.childSection_rightInverse line 497
  48. theorem OAI.DFVSGames.Gadget.Descent.childLift_spec line 506
  49. theorem OAI.DFVSGames.Gadget.Descent.child_detection line 515
  50. theorem OAI.DFVSGames.Gadget.Descent.child_rank_le line 523
  51. def OAI.DFVSGames.Gadget.Descent.leafRank line 528
  52. theorem OAI.DFVSGames.Gadget.Descent.leafRank_le line 537
  53. def OAI.DFVSGames.Quadratic.characterFieldLine line 558
  54. theorem OAI.DFVSGames.Quadratic.characterFieldLine_eq_of_mem line 563
  55. def OAI.DFVSGames.Quadratic.fieldLineRestrictions line 571
  56. theorem OAI.DFVSGames.Quadratic.alignedCharacters_eq_alignmentEvent line 576
  57. theorem OAI.DFVSGames.Quadratic.card_loss_fieldLineRestrictions_le line 587
  58. theorem OAI.DFVSGames.Quadratic.card_loss_fieldLineRestrictions_le_three_rank line 605