OAI/Computability/DirectedFeedback/Games/KMSBasisComparisonFibers.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Inverse.KMSBasisComparison.fiberProductEquiv line 15
  2. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.fiberProductEquiv_fst line 18
  3. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.expect_eq_of_uniform_fibers line 22
  4. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.density_eq_of_uniform_fibers line 34
  5. def OAI.DFVSGames.Inverse.KMSBasisComparison.RangeFiber line 50
  6. def OAI.DFVSGames.Inverse.KMSBasisComparison.rangeFiberEquiv line 53
  7. def OAI.DFVSGames.Inverse.KMSBasisComparison.rangeFiberEquivAut line 79
  8. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.rangeFiber_card line 87
  9. def OAI.DFVSGames.Inverse.KMSBasisComparison.vertexBasis line 93
  10. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.vertex_rangeFiber_card line 97
  11. abbrev OAI.DFVSGames.Inverse.KMSBasisComparison.InjectiveBasisMap line 102
  12. instance OAI.DFVSGames.Inverse.KMSBasisComparison.injectiveBasisMapFintype line 105
  13. instance OAI.DFVSGames.Inverse.KMSBasisComparison.basisAutomorphismFinite line 108
  14. instance OAI.DFVSGames.Inverse.KMSBasisComparison.basisAutomorphismFintype line 114
  15. def OAI.DFVSGames.Inverse.KMSBasisComparison.injectiveRange line 117
  16. def OAI.DFVSGames.Inverse.KMSBasisComparison.injectiveRangeFiberEquiv line 120
  17. def OAI.DFVSGames.Inverse.KMSBasisComparison.injectiveRangeFiberAut line 128
  18. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.injectiveRange_expect line 133
  19. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.injectiveRange_density line 140
  20. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.lift_nonempty_iff line 148
  21. def OAI.DFVSGames.Inverse.KMSBasisComparison.liftRange line 159
  22. def OAI.DFVSGames.Inverse.KMSBasisComparison.liftRangeFiberEquiv line 164
  23. def OAI.DFVSGames.Inverse.KMSBasisComparison.liftRangeFiberAut line 174
  24. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.lift_card line 179
  25. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.injectiveBasisMap_card line 185
  26. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.lift_density_factor line 192
  27. def OAI.DFVSGames.Inverse.KMSBasisComparison.outsideNeighborSample line 217
  28. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.outsideNeighborSample_val line 222
  29. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.card_outsideNeighborSample_fiber line 227
  30. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.expect_outsideNeighborSample line 243
  31. abbrev OAI.DFVSGames.Inverse.MatrixChart.BinaryChartNeighbors line 267
  32. abbrev OAI.DFVSGames.Inverse.MatrixChart.BinaryGraphChartNeighbors line 272
  33. def OAI.DFVSGames.Inverse.MatrixChart.rankOneEquivChartNeighbors line 278
  34. def OAI.DFVSGames.Inverse.MatrixChart.graphChartNeighbor line 295
  35. theorem OAI.DFVSGames.Inverse.MatrixChart.graphChartNeighbor_injective line 300
  36. theorem OAI.DFVSGames.Inverse.MatrixChart.graphChartNeighbor_surjective line 307
  37. def OAI.DFVSGames.Inverse.MatrixChart.chartNeighborsEquivGraphNeighbors line 318
  38. def OAI.DFVSGames.Inverse.MatrixChart.binaryFactorsEquivGraphNeighbors line 323
  39. theorem OAI.DFVSGames.Inverse.MatrixChart.binaryFactorsEquivGraphNeighbors_apply line 328
  40. theorem OAI.DFVSGames.Inverse.MatrixChart.binaryFactorsEquivGraphNeighbors_apply_add line 333
  41. theorem OAI.DFVSGames.Inverse.MatrixChart.graphChartNeighbor_finrank line 345
  42. theorem OAI.DFVSGames.Inverse.MatrixChart.graphChartNeighbor_ne_self line 352
  43. theorem OAI.DFVSGames.Inverse.MatrixChart.card_binaryGraphChartNeighbors line 359
  44. theorem OAI.DFVSGames.Inverse.MatrixChart.card_binaryGraphChartNeighbors_coordinates line 368
  45. abbrev OAI.DFVSGames.Inverse.MatrixChart.CoordinateMatrix line 383
  46. def OAI.DFVSGames.Inverse.MatrixChart.graphChartNeighborsEmbedding line 386
  47. theorem OAI.DFVSGames.Inverse.MatrixChart.card_grassmann_neighbors_graph line 395
  48. theorem OAI.DFVSGames.Inverse.MatrixChart.full_degree_eq_twice_chart_degree line 404
  49. theorem OAI.DFVSGames.Inverse.MatrixChart.chart_degree_ratio line 414
  50. abbrev OAI.DFVSGames.Inverse.MatrixChart.matrixGraph line 437
  51. theorem OAI.DFVSGames.Inverse.MatrixChart.mem_matrixGraph line 441
  52. theorem OAI.DFVSGames.Inverse.MatrixChart.matrixGraph_injective line 447
  53. abbrev OAI.DFVSGames.Inverse.MatrixChart.dotFunctional line 453
  54. theorem OAI.DFVSGames.Inverse.MatrixChart.dotFunctional_injective line 455
  55. theorem OAI.DFVSGames.Inverse.MatrixChart.dotFunctional_comp_vecMulLinear line 461
  56. theorem OAI.DFVSGames.Inverse.MatrixChart.column_equation_iff line 468
  57. theorem OAI.DFVSGames.Inverse.MatrixChart.matrix_interval_iff_slice line 473
  58. theorem OAI.DFVSGames.Inverse.MatrixChart.finrank_matrixGraph line 485
  59. def OAI.DFVSGames.Inverse.MatrixChart.coordinateJoin line 496
  60. def OAI.DFVSGames.Inverse.MatrixChart.matrixVertex line 501
  61. theorem OAI.DFVSGames.Inverse.MatrixChart.matrixVertex_injective line 506
  62. theorem OAI.DFVSGames.Inverse.MatrixChart.finrank_matrixVertex_intersection line 513
  63. theorem OAI.DFVSGames.Inverse.MatrixChart.adjacent_matrixVertex_iff line 526
  64. def OAI.DFVSGames.Inverse.MatrixChart.matrixChart line 551
  65. theorem OAI.DFVSGames.Inverse.MatrixChart.mem_matrixChart line 555
  66. theorem OAI.DFVSGames.Inverse.MatrixChart.card_matrixChart line 561
  67. def OAI.DFVSGames.Inverse.MatrixChart.grassmannNeighborsMapEquiv line 580
  68. def OAI.DFVSGames.Inverse.MatrixChart.kmsNeighborsEquiv line 596
  69. theorem OAI.DFVSGames.Inverse.MatrixChart.card_full_neighbors line 611
  70. theorem OAI.DFVSGames.Inverse.MatrixChart.card_full_neighbors_twice line 626
  71. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.relativeDensity_eq_expect_subtype_inline_KMSBasisComparisonNeighborsRetention line 643
  72. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.outsideNeighbor_retention line 659