OAI/Computability/DirectedFeedback/Games/Collision.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.DFVSGames.Repetition.ProjectionKernel line 12
  2. def OAI.DFVSGames.Repetition.ProjectionKernel.toGame line 24
  3. theorem OAI.DFVSGames.Repetition.ProjectionKernel.toGame_isProjection line 34
  4. def OAI.DFVSGames.Repetition.ProjectionKernel.apply line 37
  5. def OAI.DFVSGames.Repetition.ProjectionKernel.energy line 41
  6. def OAI.DFVSGames.Repetition.ProjectionKernel.assignment line 44
  7. def OAI.DFVSGames.Repetition.ProjectionKernel.assignmentEnergy line 48
  8. def OAI.DFVSGames.Repetition.ProjectionKernel.collisionValue line 51
  9. def OAI.DFVSGames.Repetition.ProjectionKernel.vectorEnergy line 55
  10. def OAI.DFVSGames.Repetition.ProjectionKernel.vectorMass line 58
  11. theorem OAI.DFVSGames.Repetition.ProjectionKernel.energy_nonneg line 61
  12. theorem OAI.DFVSGames.Repetition.ProjectionKernel.assignmentEnergy_le_collisionValue line 66
  13. theorem OAI.DFVSGames.Repetition.ProjectionKernel.collisionValue_le_iff line 72
  14. theorem OAI.DFVSGames.Repetition.ProjectionKernel.exists_optimal_assignment line 78
  15. theorem OAI.DFVSGames.Repetition.ProjectionKernel.collisionValue_nonneg line 86
  16. theorem OAI.DFVSGames.Repetition.ProjectionKernel.apply_assignment line 92
  17. abbrev OAI.DFVSGames.Repetition.ProjectionKernel.SymmetricEdge line 132
  18. def OAI.DFVSGames.Repetition.ProjectionKernel.symmetricLeft line 134
  19. def OAI.DFVSGames.Repetition.ProjectionKernel.symmetricRight line 136
  20. def OAI.DFVSGames.Repetition.ProjectionKernel.symmetricDistribution line 138
  21. def OAI.DFVSGames.Repetition.ProjectionKernel.symmetricAccept line 162
  22. def OAI.DFVSGames.Repetition.ProjectionKernel.singleLabelVector line 168
  23. theorem OAI.DFVSGames.Repetition.ProjectionKernel.sum_projection_gates line 173
  24. theorem OAI.DFVSGames.Repetition.ProjectionKernel.apply_single_label line 203
  25. theorem OAI.DFVSGames.Repetition.ProjectionKernel.energy_single_label line 223
  26. theorem OAI.DFVSGames.Repetition.ProjectionKernel.vectorEnergy_singleLabelVector line 265
  27. theorem OAI.DFVSGames.Repetition.ProjectionKernel.symmetric_probability_eq_assignmentEnergy line 278
  28. def OAI.DFVSGames.Repetition.ProjectionKernel.linearCoefficient line 304
  29. theorem OAI.DFVSGames.Repetition.ProjectionKernel.apply_eq_linearCoefficient_sum line 308
  30. theorem OAI.DFVSGames.Repetition.ProjectionKernel.energy_eq_linearCoefficient_sum line 319
  31. theorem OAI.DFVSGames.Repetition.ProjectionKernel.exists_energy_le_deterministicVector line 327
  32. def OAI.DFVSGames.Repetition.ProjectionKernel.vectorAmplitude line 340
  33. theorem OAI.DFVSGames.Repetition.ProjectionKernel.vectorAmplitude_nonnegative line 345
  34. theorem OAI.DFVSGames.Repetition.ProjectionKernel.rowSquareMass_vectorAmplitude line 351
  35. theorem OAI.DFVSGames.Repetition.ProjectionKernel.exists_vectorEnergy_le_singleLabelVector line 354
  36. theorem OAI.DFVSGames.Repetition.ProjectionKernel.exists_mass_preserving_singleLabelVector line 375
  37. theorem OAI.DFVSGames.Repetition.ProjectionKernel.sq_expectation_le_expectation_sq line 401
  38. theorem OAI.DFVSGames.Repetition.ProjectionKernel.apply_assignment_nonneg line 413
  39. theorem OAI.DFVSGames.Repetition.ProjectionKernel.sum_apply_assignment_le_one line 419
  40. theorem OAI.DFVSGames.Repetition.ProjectionKernel.success_eq_outer_apply line 443
  41. theorem OAI.DFVSGames.Repetition.ProjectionKernel.success_sq_le_assignmentEnergy line 458
  42. theorem OAI.DFVSGames.Repetition.ProjectionKernel.value_sq_le_collisionValue line 472
  43. theorem OAI.DFVSGames.Repetition.ProjectionKernel.exists_best_response line 479
  44. theorem OAI.DFVSGames.Repetition.ProjectionKernel.assignmentEnergy_le_value line 495
  45. theorem OAI.DFVSGames.Repetition.ProjectionKernel.collisionValue_le_value line 521
  46. theorem OAI.DFVSGames.Repetition.ProjectionKernel.collisionValue_le_one line 526
  47. theorem OAI.DFVSGames.Repetition.ProjectionKernel.distribution_nonempty_inline_RoundingKernel line 545
  48. theorem OAI.DFVSGames.Repetition.ProjectionKernel.vectorEnergy_le_gap_rate line 552
  49. def OAI.DFVSGames.Repetition.kernelApply line 612
  50. def OAI.DFVSGames.Repetition.tensorKernel line 615
  51. theorem OAI.DFVSGames.Repetition.kernelApply_tensor line 619
  52. theorem OAI.DFVSGames.Repetition.kernelApply_nonnegative line 633
  53. theorem OAI.DFVSGames.Repetition.kernelApply_sum line 643
  54. theorem OAI.DFVSGames.Repetition.kernelApply_smul line 657
  55. theorem OAI.DFVSGames.Repetition.kernelApply_slice_mass line 669
  56. def OAI.DFVSGames.Repetition.ProjectionKernel.coefficients line 692
  57. theorem OAI.DFVSGames.Repetition.ProjectionKernel.apply_eq_kernelApply line 696
  58. theorem OAI.DFVSGames.Repetition.ProjectionKernel.apply_nonnegative line 708
  59. theorem OAI.DFVSGames.Repetition.ProjectionKernel.apply_sum line 720
  60. theorem OAI.DFVSGames.Repetition.ProjectionKernel.apply_smul line 726
  61. def OAI.DFVSGames.Repetition.ProjectionKernel.product line 732
  62. theorem OAI.DFVSGames.Repetition.ProjectionKernel.coefficients_product line 744
  63. theorem OAI.DFVSGames.Repetition.ProjectionKernel.apply_product line 752
  64. theorem OAI.DFVSGames.Repetition.ProjectionKernel.toGame_product line 762