OAI/Computability/DirectedFeedback/Games/KMSBasisComparisonPseudorandom.lean

GitHub source file

77 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.prefixSpan line 14
  2. def OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.joinedTuple line 17
  3. abbrev OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.IndependentCompletion line 21
  4. def OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.completionVertex line 24
  5. theorem OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.prefix_le_completion line 29
  6. theorem OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.completion_le_sup line 36
  7. theorem OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.completion_mem_interval line 48
  8. theorem OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.prefix_independent line 54
  9. theorem OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.interval_complexity_le line 58
  10. def OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.GrassmannPseudorandom line 72
  11. def OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.completionEvent line 78
  12. def OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.restrictedLiftDensity line 82
  13. def OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.TuplePseudorandom line 87
  14. theorem OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.restrictedLiftDensity_eq_zero_of_dependent line 93
  15. abbrev OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.IntervalVertex line 103
  16. def OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.completionIntervalVertex line 106
  17. def OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.completionFiberEquiv line 110
  18. theorem OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.interval_completion_nonempty line 120
  19. def OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.completionEventEquiv line 129
  20. def OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.intervalEventEquiv line 138
  21. theorem OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.independent_density_eq_interval line 148
  22. theorem OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.restrictedLiftDensity_le_interval line 176
  23. theorem OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.grassmann_pseudorandom_restricted line 193
  24. theorem OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.grassmann_pseudorandom_lift line 205
  25. def OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.tupleBasis line 223
  26. def OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.tupleMapEquiv line 226
  27. def OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.tupleMap line 229
  28. theorem OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.tupleMap_range line 232
  29. theorem OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.tupleMap_basis line 236
  30. theorem OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.tupleMap_injective_iff line 240
  31. theorem OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.inLift_tupleMap_iff line 250
  32. theorem OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.restrictedLiftDensity_eq_expect line 265
  33. theorem OAI.DFVSGames.Inverse.KMSBasisComparisonPseudorandom.grassmann_pseudorandom_lift_expect line 274
  34. theorem OAI.DFVSGames.Inverse.KMSAffineRestriction.lifted_expect_in_basis line 292
  35. def OAI.DFVSGames.Inverse.KMSAffineRestriction.affineCoordinates line 308
  36. theorem OAI.DFVSGames.Inverse.KMSAffineRestriction.affineCoordinates_apply line 314
  37. theorem OAI.DFVSGames.Inverse.KMSAffineRestriction.lifted_expect_shifted_basis line 319
  38. theorem OAI.DFVSGames.Inverse.KMSAffineRestrictionComplement.exists_bounded_complement_of_linearMap line 347
  39. theorem OAI.DFVSGames.Inverse.KMSAffineRestrictionComplement.exists_bounded_complement line 366
  40. abbrev OAI.DFVSGames.Inverse.KMSAffineRestrictionSplit.localVanishing line 390
  41. def OAI.DFVSGames.Inverse.KMSAffineRestrictionSplit.splitLeft line 393
  42. theorem OAI.DFVSGames.Inverse.KMSAffineRestrictionSplit.splitLeft_apply line 402
  43. def OAI.DFVSGames.Inverse.KMSAffineRestrictionSplit.splitRight line 407
  44. theorem OAI.DFVSGames.Inverse.KMSAffineRestrictionSplit.splitRight_apply line 411
  45. def OAI.DFVSGames.Inverse.KMSAffineRestrictionSplit.joinMap line 415
  46. theorem OAI.DFVSGames.Inverse.KMSAffineRestrictionSplit.joinMap_apply_left line 421
  47. theorem OAI.DFVSGames.Inverse.KMSAffineRestrictionSplit.joinMap_apply_right line 427
  48. theorem OAI.DFVSGames.Inverse.KMSAffineRestrictionSplit.joinMap_vanishes line 433
  49. def OAI.DFVSGames.Inverse.KMSAffineRestrictionSplit.join line 445
  50. theorem OAI.DFVSGames.Inverse.KMSAffineRestrictionSplit.join_apply line 450
  51. theorem OAI.DFVSGames.Inverse.KMSAffineRestrictionSplit.join_embed_apply_left line 455
  52. theorem OAI.DFVSGames.Inverse.KMSAffineRestrictionSplit.join_embed_apply_right line 462
  53. theorem OAI.DFVSGames.Inverse.KMSAffineRestrictionSplit.splitLeft_join line 468
  54. theorem OAI.DFVSGames.Inverse.KMSAffineRestrictionSplit.splitRight_join line 477
  55. theorem OAI.DFVSGames.Inverse.KMSAffineRestrictionSplit.join_split line 485
  56. def OAI.DFVSGames.Inverse.KMSAffineRestrictionSplit.splitEquiv line 497
  57. theorem OAI.DFVSGames.Inverse.KMSAffineRestrictionSplit.splitEquiv_symm_apply line 521
  58. instance OAI.DFVSGames.Inverse.KMSAffineRestrictionSplit.freeFintype line 526
  59. theorem OAI.DFVSGames.Inverse.KMSAffineRestrictionSplit.expect_join line 534
  60. theorem OAI.DFVSGames.Inverse.KMSAffineRestrictionSplit.expect_restrict line 548
  61. def OAI.DFVSGames.Inverse.KMSAffineRestriction.complementBasis line 569
  62. theorem OAI.DFVSGames.Inverse.KMSAffineRestriction.complementBasis_inl line 574
  63. theorem OAI.DFVSGames.Inverse.KMSAffineRestriction.complementBasis_inr line 580
  64. def OAI.DFVSGames.Inverse.KMSAffineRestriction.freeCenter line 586
  65. theorem OAI.DFVSGames.Inverse.KMSAffineRestriction.freeCenter_coe line 591
  66. theorem OAI.DFVSGames.Inverse.KMSAffineRestriction.translate_join_eq_constr line 596
  67. theorem OAI.DFVSGames.Inverse.KMSAffineRestriction.affine_expect_of_complement line 621
  68. theorem OAI.DFVSGames.Inverse.KMSAffineRestriction.affine_expect_bound line 648
  69. theorem OAI.DFVSGames.Inverse.KMSAffineRestriction.affine_squared_expect_bound line 666
  70. def OAI.DFVSGames.Inverse.KMSAffineRestrictionPresentation.parameterEquiv line 696
  71. theorem OAI.DFVSGames.Inverse.KMSAffineRestrictionPresentation.parameterEquiv_apply_mk line 702
  72. theorem OAI.DFVSGames.Inverse.KMSAffineRestrictionPresentation.embed_parameterEquiv line 707
  73. theorem OAI.DFVSGames.Inverse.KMSAffineRestrictionPresentation.translate_parameterEquiv line 715
  74. theorem OAI.DFVSGames.Inverse.KMSAffineRestrictionPresentation.expect_presentation line 722
  75. theorem OAI.DFVSGames.Inverse.KMSAffineRestrictionPresentation.expect_presentation_sq line 732
  76. theorem OAI.DFVSGames.Inverse.KMSAffineRestrictionPresentation.order_add_dimensions line 740
  77. theorem OAI.DFVSGames.Inverse.KMSAffineRestrictionPresentation.order_le_of_dimensions line 752