OAI/Computability/DirectedFeedback/Probability/Enlargement.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Gadget.Enlargement.probability line 12
  2. theorem OAI.DFVSGames.Gadget.Enlargement.probability_exists_le_sum line 15
  3. theorem OAI.DFVSGames.Gadget.Enlargement.probability_preimage_of_fibers line 30
  4. theorem OAI.DFVSGames.Gadget.Enlargement.exists_equiv_map_nonzero line 65
  5. abbrev OAI.DFVSGames.Gadget.Enlargement.LinearInjection line 76
  6. theorem OAI.DFVSGames.Gadget.Enlargement.linearInjection_nonempty_of_finrank_le line 80
  7. def OAI.DFVSGames.Gadget.Enlargement.postcompose line 88
  8. theorem OAI.DFVSGames.Gadget.Enlargement.injection_eval_ne_zero line 102
  9. theorem OAI.DFVSGames.Gadget.Enlargement.exists_injection_hitting_nonzero line 110
  10. def OAI.DFVSGames.Gadget.Enlargement.productShift line 121
  11. theorem OAI.DFVSGames.Gadget.Enlargement.productShift_surjective line 128
  12. def OAI.DFVSGames.Gadget.Enlargement.enlargedOutput line 143
  13. theorem OAI.DFVSGames.Gadget.Enlargement.enlargedOutput_shift line 148
  14. theorem OAI.DFVSGames.Gadget.Enlargement.enlargedOutput_update line 158
  15. theorem OAI.DFVSGames.Gadget.Enlargement.enlargedOutput_update_ne_iff line 178
  16. theorem OAI.DFVSGames.Gadget.Enlargement.injection_eval_uniform line 186
  17. theorem OAI.DFVSGames.Gadget.Enlargement.pullback_ne_top_iff line 217
  18. theorem OAI.DFVSGames.Gadget.Enlargement.nonzero_density_le line 251
  19. theorem OAI.DFVSGames.Gadget.Enlargement.card_nonzero_binary line 259
  20. theorem OAI.DFVSGames.Gadget.Enlargement.probability_nonzero_subspace line 266
  21. theorem OAI.DFVSGames.Gadget.Enlargement.probability_annihilator_le line 290
  22. theorem OAI.DFVSGames.Gadget.Enlargement.union_bound_le_quarter line 302
  23. theorem OAI.DFVSGames.Gadget.Enlargement.pullback_failure_probability_le line 311
  24. theorem OAI.DFVSGames.Gadget.Enlargement.pullback_failure_probability_le_quarter line 350
  25. theorem OAI.DFVSGames.Gadget.Enlargement.probability_not line 365
  26. theorem OAI.DFVSGames.Gadget.Enlargement.average_detection_lower_bound line 379
  27. theorem OAI.DFVSGames.Gadget.Enlargement.detection_constants line 404
  28. theorem OAI.DFVSGames.Gadget.Enlargement.enlarged_detection line 409
  29. theorem OAI.DFVSGames.Gadget.EnlargementConstruction.probability_equiv line 439
  30. theorem OAI.DFVSGames.Gadget.EnlargementConstruction.probability_eq_sum_indicator line 446
  31. theorem OAI.DFVSGames.Gadget.EnlargementConstruction.probability_prod_average line 455
  32. theorem OAI.DFVSGames.Gadget.EnlargementConstruction.probability_prod_average_right line 466
  33. theorem OAI.DFVSGames.Gadget.EnlargementConstruction.probability_coordinate line 476
  34. theorem OAI.DFVSGames.Gadget.EnlargementConstruction.probability_coordinate_prod line 504
  35. theorem OAI.DFVSGames.Gadget.EnlargementConstruction.probability_prod_reorder line 515
  36. theorem OAI.DFVSGames.Gadget.EnlargementConstruction.probability_prod_eq_of_const line 526
  37. theorem OAI.DFVSGames.Gadget.EnlargementConstruction.enlarged_single_copy_probability line 537
  38. theorem OAI.DFVSGames.Gadget.EnlargementConstruction.enlarged_random_copy_probability line 554
  39. abbrev OAI.DFVSGames.Gadget.EnlargementConstruction.Copies line 582
  40. def OAI.DFVSGames.Gadget.EnlargementConstruction.copiesFintype line 586
  41. def OAI.DFVSGames.Gadget.EnlargementConstruction.productEmbed line 594
  42. theorem OAI.DFVSGames.Gadget.EnlargementConstruction.productEmbed_injective line 601
  43. def OAI.DFVSGames.Gadget.EnlargementConstruction.productStage line 608
  44. def OAI.DFVSGames.Gadget.EnlargementConstruction.build line 625
  45. theorem OAI.DFVSGames.Gadget.EnlargementConstruction.update_canonical line 631
  46. theorem OAI.DFVSGames.Gadget.EnlargementConstruction.probability_pointwise line 637
  47. theorem OAI.DFVSGames.Gadget.EnlargementConstruction.add_single_eq_update line 644
  48. theorem OAI.DFVSGames.Gadget.EnlargementConstruction.change_iff line 652
  49. def OAI.DFVSGames.Gadget.EnlargementConstruction.copyObserver line 669
  50. theorem OAI.DFVSGames.Gadget.EnlargementConstruction.copyObserver_shift line 679
  51. theorem OAI.DFVSGames.Gadget.EnlargementConstruction.dual_pullback_eq_top_iff line 706
  52. theorem OAI.DFVSGames.Gadget.EnlargementConstruction.detection_average line 712
  53. theorem OAI.DFVSGames.Gadget.EnlargementConstruction.probability_projection line 741
  54. theorem OAI.DFVSGames.Gadget.EnlargementConstruction.probability_projection_prod line 752
  55. theorem OAI.DFVSGames.Gadget.EnlargementConstruction.change_probability line 764
  56. theorem OAI.DFVSGames.Gadget.EnlargementConstruction.detection_probability line 801