OAI/Computability/DirectedFeedback/Games/TensorDomination.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Repetition.ProjectionKernel.tensorSlice line 18
  2. theorem OAI.DFVSGames.Repetition.ProjectionKernel.tensorSlice_nonnegative line 25
  3. theorem OAI.DFVSGames.Repetition.ProjectionKernel.sum_assignment_product line 38
  4. theorem OAI.DFVSGames.Repetition.ProjectionKernel.tensorSlice_label_mass line 46
  5. theorem OAI.DFVSGames.Repetition.ProjectionKernel.vectorMass_tensorSlice line 57
  6. theorem OAI.DFVSGames.Repetition.ProjectionKernel.vectorMass_tensorSlice_le line 70
  7. theorem OAI.DFVSGames.Repetition.ProjectionKernel.vectorEnergy_tensorSlice line 77
  8. theorem OAI.DFVSGames.Repetition.ProjectionKernel.vectorMass_smul line 142
  9. theorem OAI.DFVSGames.Repetition.ProjectionKernel.energy_smul line 148
  10. theorem OAI.DFVSGames.Repetition.ProjectionKernel.vectorEnergy_smul line 159
  11. theorem OAI.DFVSGames.Repetition.ProjectionKernel.entry_eq_zero_of_vectorMass_nonpositive line 167
  12. theorem OAI.DFVSGames.Repetition.ProjectionKernel.vectorEnergy_eq_zero_of_mass_nonpositive line 181
  13. theorem OAI.DFVSGames.Repetition.ProjectionKernel.vectorEnergy_le_of_unit_bound line 191
  14. def OAI.DFVSGames.Repetition.ProjectionKernel.reindex line 231
  15. theorem OAI.DFVSGames.Repetition.ProjectionKernel.apply_reindex line 241
  16. theorem OAI.DFVSGames.Repetition.ProjectionKernel.energy_reindex line 260
  17. theorem OAI.DFVSGames.Repetition.ProjectionKernel.assignmentEnergy_reindex line 275
  18. theorem OAI.DFVSGames.Repetition.ProjectionKernel.collisionValue_reindex line 297
  19. def OAI.DFVSGames.Repetition.ProjectionKernel.repetition line 328
  20. theorem OAI.DFVSGames.Repetition.ProjectionKernel.repetition_accepts_iff line 341
  21. theorem OAI.DFVSGames.Repetition.ProjectionKernel.toGame_repetition line 348
  22. theorem OAI.DFVSGames.Repetition.ProjectionKernel.eq_of_data_eq line 366
  23. theorem OAI.DFVSGames.Repetition.ProjectionKernel.repetition_succ line 376
  24. theorem OAI.DFVSGames.Repetition.ProjectionKernel.collisionValue_repetition_succ line 409
  25. theorem OAI.DFVSGames.Repetition.ProjectionKernel.collisionValue_repetition_zero_le_one line 415
  26. def OAI.DFVSGames.Foundations.Repetition.revealedProductWeight line 432
  27. def OAI.DFVSGames.Foundations.Repetition.revealedLeftWeight line 438
  28. def OAI.DFVSGames.Foundations.Repetition.revealedRightWeight line 443
  29. theorem OAI.DFVSGames.Foundations.Repetition.revealedProductWeight_factorizes line 448
  30. theorem OAI.DFVSGames.Foundations.Repetition.revealedProductWeight_local_restrictions line 461
  31. theorem OAI.DFVSGames.Foundations.Repetition.productWeight_mass line 474
  32. def OAI.DFVSGames.Foundations.Repetition.normalizedWeight line 480
  33. theorem OAI.DFVSGames.Foundations.Repetition.normalizedWeight_isProbability line 483
  34. theorem OAI.DFVSGames.Foundations.Repetition.normalized_productWeight line 491
  35. theorem OAI.DFVSGames.Foundations.Repetition.normalized_rectangle_restriction line 499
  36. def OAI.DFVSGames.Foundations.Repetition.normalizeOr line 527
  37. theorem OAI.DFVSGames.Foundations.Repetition.sum_mul_normalizeOr line 535
  38. theorem OAI.DFVSGames.Foundations.Repetition.local_completion_recombination line 550
  39. theorem OAI.DFVSGames.Foundations.Repetition.factorized_completion_row line 563
  40. def OAI.DFVSGames.Repetition.leftQuestionMarginal line 592
  41. def OAI.DFVSGames.Repetition.rightQuestionMarginal line 599
  42. def OAI.DFVSGames.Repetition.leftGivenRight line 606
  43. theorem OAI.DFVSGames.Repetition.rightQuestionMarginal_mul_leftGivenRight line 611
  44. def OAI.DFVSGames.Repetition.kernelOfGame line 619
  45. theorem OAI.DFVSGames.Repetition.kernelOfGame_question_weight line 626
  46. theorem OAI.DFVSGames.Repetition.toGame_kernelOfGame line 631
  47. theorem OAI.DFVSGames.Repetition.kernelOfGame_success line 643
  48. theorem OAI.DFVSGames.Repetition.kernelOfGame_value line 649
  49. theorem OAI.DFVSGames.Repetition.sequence_le_power line 660
  50. theorem OAI.DFVSGames.Repetition.squared_rate_le_dsRate_sq line 672
  51. theorem OAI.DFVSGames.Repetition.rate_of_squared_collision_recurrence line 678
  52. theorem OAI.DFVSGames.Repetition.ProjectionKernel.collisionValue_product_le_gap_rate line 706
  53. theorem OAI.DFVSGames.Repetition.ProjectionKernel.repetition_value_le_dsRate line 720
  54. theorem OAI.DFVSGames.Repetition.projection_repetition_value line 743
  55. theorem OAI.DFVSGames.Repetition.projection_repetition_success line 752
  56. theorem OAI.DFVSGames.Repetition.clean_repetition_value line 761
  57. theorem OAI.DFVSGames.Repetition.final_repetition_value line 771