OAI/Computability/DirectedFeedback/Games/KMSBasisComparisonRetention.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Inverse.KMSBasisComparison.fullStepRetention line 11
  2. def OAI.DFVSGames.Inverse.KMSBasisComparison.liftRetention line 16
  3. def OAI.DFVSGames.Inverse.KMSBasisComparison.goodParametersEquiv line 19
  4. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.goodParameters_expect line 28
  5. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.fullStepRetention_compare line 40
  6. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.liftRange_retention_expect line 52
  7. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.liftRetention_compare line 65
  8. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.liftRetention_compare_kms line 79
  9. def OAI.DFVSGames.Inverse.KMSBasisComparison.liftDensity line 86
  10. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.liftDensity_eq_card line 89
  11. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.liftDensity_pos line 94
  12. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.liftDensity_mul_retention line 101
  13. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.fullStepRetention_eq_noise line 110
  14. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.liftRetention_le_of_correlation_le line 119
  15. def OAI.DFVSGames.Inverse.KMSBasisComparison.LiftExpansionPrinciple line 136
  16. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.exists_binary_ratio_threshold line 144
  17. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.nonempty_of_relativeDensity_pos line 155
  18. theorem OAI.DFVSGames.Inverse.KMSBasisComparison.expansion_of_liftExpansion line 161
  19. theorem OAI.DFVSGames.Inverse.KMSMomentToExpansion.liftExpansion_of_upperMoments line 202
  20. theorem OAI.DFVSGames.Inverse.KMSMomentToExpansion.expansion_of_upperMoments line 241
  21. theorem OAI.DFVSGames.Inverse.KMSExpansion.kms_expansion line 258
  22. def OAI.DFVSGames.Inverse.ShortcodeFromGrassmann.matrixFiber line 275
  23. def OAI.DFVSGames.Inverse.ShortcodeFromGrassmann.liftedFiber line 278
  24. theorem OAI.DFVSGames.Inverse.ShortcodeFromGrassmann.liftedFiber_subset_chart line 281
  25. theorem OAI.DFVSGames.Inverse.ShortcodeFromGrassmann.matrixVertex_mem_liftedFiber line 288
  26. theorem OAI.DFVSGames.Inverse.ShortcodeFromGrassmann.image_slice_points line 300
  27. theorem OAI.DFVSGames.Inverse.ShortcodeFromGrassmann.image_slice_fiber line 316
  28. theorem OAI.DFVSGames.Inverse.ShortcodeFromGrassmann.constantAgreement_eq_chart_density line 337
  29. theorem OAI.DFVSGames.Inverse.ShortcodeFromGrassmann.hasAffineSlice_of_dense_interval line 348
  30. theorem OAI.DFVSGames.Inverse.MatrixChart.span_basis_values line 374
  31. theorem OAI.DFVSGames.Inverse.MatrixChart.lowerRows_basis line 381
  32. theorem OAI.DFVSGames.Inverse.MatrixChart.mem_iff_annihilator_basis line 386
  33. theorem OAI.DFVSGames.Inverse.MatrixChart.functional_coordinate_decomposition line 400
  34. theorem OAI.DFVSGames.Inverse.MatrixChart.upperColumns_annihilator_basis line 405
  35. theorem OAI.DFVSGames.Inverse.MatrixChart.exists_interval_coordinates line 426
  36. theorem OAI.DFVSGames.Inverse.MatrixChart.dotFunctional_surjective line 456
  37. theorem OAI.DFVSGames.Inverse.MatrixChart.exists_matrix_interval_slice line 467
  38. theorem OAI.DFVSGames.Inverse.MatrixChart.exists_bounded_matrix_interval_slice line 487
  39. theorem OAI.DFVSGames.Inverse.MatrixChart.exists_shortcode_slice line 506
  40. def OAI.DFVSGames.Inverse.ShortcodeFromGrassmann.zeroFactorMass line 560
  41. theorem OAI.DFVSGames.Inverse.ShortcodeFromGrassmann.exists_zeroFactorMass_threshold line 563
  42. def OAI.DFVSGames.Inverse.ShortcodeFromGrassmann.ChartFiberRetention line 579
  43. theorem OAI.DFVSGames.Inverse.ShortcodeFromGrassmann.inversePrinciple_of_expansion_and_chart line 586
  44. theorem OAI.DFVSGames.Inverse.MatrixChart.dotFunctional_zero_binary line 630
  45. theorem OAI.DFVSGames.Inverse.MatrixChart.dotFunctional_ne_zero line 637
  46. theorem OAI.DFVSGames.Inverse.MatrixChart.vecMulLinear_rankOne line 642
  47. theorem OAI.DFVSGames.Inverse.MatrixChart.vecMulLinear_add_rankOne line 649
  48. theorem OAI.DFVSGames.Inverse.MatrixChart.adjacent_matrixVertex_add_rankOne line 659
  49. abbrev OAI.DFVSGames.Inverse.MatrixChart.NonzeroVectorFactors line 668
  50. abbrev OAI.DFVSGames.Inverse.MatrixChart.MatrixVertexChartNeighbors line 671
  51. def OAI.DFVSGames.Inverse.MatrixChart.vectorFactorMatrixNeighbor line 675
  52. theorem OAI.DFVSGames.Inverse.MatrixChart.vectorFactorMatrixNeighbor_injective line 681
  53. theorem OAI.DFVSGames.Inverse.MatrixChart.vectorFactorMatrixNeighbor_surjective line 692
  54. def OAI.DFVSGames.Inverse.MatrixChart.vectorFactorsEquivMatrixVertexChartNeighbors line 719
  55. theorem OAI.DFVSGames.Inverse.MatrixChart.vectorFactorsEquivMatrixVertexChartNeighbors_apply line 724
  56. theorem OAI.DFVSGames.Inverse.MatrixChart.card_matrixVertexChartNeighbors line 729