OAI/Computability/DirectedFeedback/Games/CompletedSampling.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DFVSGames.Foundations.Repetition.CompletedSampling.mixture_pushforward_base line 18
  2. theorem OAI.DFVSGames.Foundations.Repetition.CompletedSampling.product_pushforward_eq_mixture_right line 25
  3. theorem OAI.DFVSGames.Foundations.Repetition.CompletedSampling.product_product_pushforward_eq_mixture line 42
  4. theorem OAI.DFVSGames.Foundations.Repetition.CompletedSampling.mixture_totalVariation_le line 54
  5. def OAI.DFVSGames.Foundations.Repetition.CompletedSampling.diagonalLaw line 68
  6. theorem OAI.DFVSGames.Foundations.Repetition.CompletedSampling.diagonalLaw_eq_pushforward line 72
  7. theorem OAI.DFVSGames.Foundations.Repetition.CompletedSampling.diagonalLaw_mixture line 86
  8. abbrev OAI.DFVSGames.Foundations.Repetition.CompletedSampling.Seed line 99
  9. def OAI.DFVSGames.Foundations.Repetition.CompletedSampling.seedLaw line 102
  10. def OAI.DFVSGames.Foundations.Repetition.CompletedSampling.left line 107
  11. def OAI.DFVSGames.Foundations.Repetition.CompletedSampling.right line 110
  12. def OAI.DFVSGames.Foundations.Repetition.CompletedSampling.completionKernel line 113
  13. def OAI.DFVSGames.Foundations.Repetition.CompletedSampling.outputLaw line 118
  14. theorem OAI.DFVSGames.Foundations.Repetition.CompletedSampling.outputLaw_eq_product_pushforward line 125
  15. theorem OAI.DFVSGames.Foundations.Repetition.CompletedSampling.outputLaw_eq_mixture line 136
  16. theorem OAI.DFVSGames.Foundations.Repetition.CompletedSampling.diagonalLaw_completion_mixture line 165
  17. theorem OAI.DFVSGames.Foundations.Repetition.CompletedSampling.outputLaw_totalVariation_le line 172
  18. def OAI.DFVSGames.Foundations.Repetition.CompletedSampling.coordinateLeft line 189
  19. def OAI.DFVSGames.Foundations.Repetition.CompletedSampling.coordinateRight line 193
  20. theorem OAI.DFVSGames.Foundations.Repetition.CompletedSampling.coordinateLeft_preserves line 199
  21. theorem OAI.DFVSGames.Foundations.Repetition.CompletedSampling.coordinateRight_preserves line 206
  22. def OAI.DFVSGames.Foundations.Repetition.CompletedSampling.coordinateOutputLaw line 211
  23. theorem OAI.DFVSGames.Foundations.Repetition.CompletedSampling.coordinateOutputLaw_eq_mixture line 219
  24. theorem OAI.DFVSGames.Foundations.Repetition.CompletedSampling.coordinateOutputLaw_eq_outputLaw line 254
  25. theorem OAI.DFVSGames.Foundations.Repetition.CompletedSampling.coordinateOutputLaw_totalVariation_le line 264
  26. def OAI.DFVSGames.Foundations.Games.Game.localEmbeddingLaw line 291
  27. theorem OAI.DFVSGames.Foundations.Games.Game.success_le_value_add_embedding_distance line 298
  28. def OAI.DFVSGames.Foundations.Games.Game.coordinateGame line 327
  29. theorem OAI.DFVSGames.Foundations.Games.Game.coordinate_probability_le_value_add_embedding_distance line 333
  30. theorem OAI.DFVSGames.Foundations.Games.Game.coordinate_probability_le_value_of_approximate_embeddings line 348
  31. theorem OAI.DFVSGames.Foundations.Repetition.coordinate_probability_le_value_of_local_completion line 385
  32. theorem OAI.DFVSGames.Foundations.Repetition.selectedLabels_card line 453
  33. theorem OAI.DFVSGames.Foundations.Repetition.unusedCoordinates_card line 458
  34. theorem OAI.DFVSGames.Foundations.Repetition.unusedCoordinates_card_real line 463
  35. theorem OAI.DFVSGames.Foundations.Repetition.log_le_logTwo line 468
  36. theorem OAI.DFVSGames.Foundations.Repetition.selectedLabels_log_le line 477
  37. theorem OAI.DFVSGames.Foundations.Repetition.selectedInformationRadius_le line 490
  38. theorem OAI.DFVSGames.Foundations.Repetition.sqrt_budget_factor line 509
  39. theorem OAI.DFVSGames.Foundations.Repetition.exists_coordinate_le_information_budget line 517
  40. theorem OAI.DFVSGames.Foundations.Repetition.SelectionSequence.exists_unused_inline_SelectionSequence line 554
  41. def OAI.DFVSGames.Foundations.Repetition.SelectionSequence.nextSet line 570
  42. def OAI.DFVSGames.Foundations.Repetition.SelectionSequence.selectedSet line 576
  43. theorem OAI.DFVSGames.Foundations.Repetition.SelectionSequence.selectedSet_card line 582
  44. theorem OAI.DFVSGames.Foundations.Repetition.SelectionSequence.selectedSet_subset_succ line 605
  45. theorem OAI.DFVSGames.Foundations.Repetition.SelectionSequence.selectedSet_monotone line 615
  46. theorem OAI.DFVSGames.Foundations.Repetition.SelectionSequence.selectedSet_univ line 621
  47. theorem OAI.DFVSGames.Foundations.Repetition.SelectionSequence.selectedSet_step line 628
  48. def OAI.DFVSGames.Foundations.Repetition.SelectionSequence.SetStep line 643
  49. theorem OAI.DFVSGames.Foundations.Repetition.SelectionSequence.totalSetStep line 649
  50. theorem OAI.DFVSGames.Foundations.Repetition.SelectionSequence.exists_scalar_sequence line 664
  51. def OAI.DFVSGames.Foundations.Repetition.SelectionSequence.ConditionalCoordinateBound line 697
  52. theorem OAI.DFVSGames.Foundations.Repetition.SelectionSequence.repetition_success_le_of_conditionalCoordinateBound line 709
  53. theorem OAI.DFVSGames.Foundations.Repetition.selected_coordinate_probability_le_value_add_error line 746
  54. theorem OAI.DFVSGames.Foundations.Repetition.holenstein_conditionalCoordinateBound line 775
  55. theorem OAI.DFVSGames.Foundations.Repetition.holenstein_repetition_success line 789
  56. theorem OAI.DFVSGames.Foundations.Repetition.holenstein_repetition_value line 799