OAI/Computability/MinUncut/PCP/CompletedSampling.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MinUncutGames.Foundations.Repetition.CompletedSampling.mixture_pushforward_base line 17
  2. theorem OAI.MinUncutGames.Foundations.Repetition.CompletedSampling.product_pushforward_eq_mixture_right line 24
  3. theorem OAI.MinUncutGames.Foundations.Repetition.CompletedSampling.product_product_pushforward_eq_mixture line 41
  4. theorem OAI.MinUncutGames.Foundations.Repetition.CompletedSampling.mixture_totalVariation_le line 53
  5. def OAI.MinUncutGames.Foundations.Repetition.CompletedSampling.diagonalLaw line 67
  6. theorem OAI.MinUncutGames.Foundations.Repetition.CompletedSampling.diagonalLaw_eq_pushforward line 71
  7. theorem OAI.MinUncutGames.Foundations.Repetition.CompletedSampling.diagonalLaw_mixture line 85
  8. abbrev OAI.MinUncutGames.Foundations.Repetition.CompletedSampling.Seed line 98
  9. def OAI.MinUncutGames.Foundations.Repetition.CompletedSampling.seedLaw line 101
  10. def OAI.MinUncutGames.Foundations.Repetition.CompletedSampling.left line 106
  11. def OAI.MinUncutGames.Foundations.Repetition.CompletedSampling.right line 109
  12. def OAI.MinUncutGames.Foundations.Repetition.CompletedSampling.completionKernel line 112
  13. def OAI.MinUncutGames.Foundations.Repetition.CompletedSampling.outputLaw line 117
  14. theorem OAI.MinUncutGames.Foundations.Repetition.CompletedSampling.outputLaw_eq_product_pushforward line 124
  15. theorem OAI.MinUncutGames.Foundations.Repetition.CompletedSampling.outputLaw_eq_mixture line 135
  16. theorem OAI.MinUncutGames.Foundations.Repetition.CompletedSampling.diagonalLaw_completion_mixture line 164
  17. theorem OAI.MinUncutGames.Foundations.Repetition.CompletedSampling.outputLaw_totalVariation_le line 171
  18. def OAI.MinUncutGames.Foundations.Repetition.CompletedSampling.coordinateLeft line 188
  19. def OAI.MinUncutGames.Foundations.Repetition.CompletedSampling.coordinateRight line 192
  20. theorem OAI.MinUncutGames.Foundations.Repetition.CompletedSampling.coordinateLeft_preserves line 198
  21. theorem OAI.MinUncutGames.Foundations.Repetition.CompletedSampling.coordinateRight_preserves line 205
  22. def OAI.MinUncutGames.Foundations.Repetition.CompletedSampling.coordinateOutputLaw line 210
  23. theorem OAI.MinUncutGames.Foundations.Repetition.CompletedSampling.coordinateOutputLaw_eq_mixture line 218
  24. theorem OAI.MinUncutGames.Foundations.Repetition.CompletedSampling.coordinateOutputLaw_eq_outputLaw line 253
  25. theorem OAI.MinUncutGames.Foundations.Repetition.CompletedSampling.coordinateOutputLaw_totalVariation_le line 263
  26. def OAI.MinUncutGames.Foundations.Games.Game.localEmbeddingLaw line 290
  27. theorem OAI.MinUncutGames.Foundations.Games.Game.success_le_value_add_embedding_distance line 297
  28. def OAI.MinUncutGames.Foundations.Games.Game.coordinateGame line 326
  29. theorem OAI.MinUncutGames.Foundations.Games.Game.coordinate_probability_le_value_add_embedding_distance line 332
  30. theorem OAI.MinUncutGames.Foundations.Games.Game.coordinate_probability_le_value_of_approximate_embeddings line 347
  31. theorem OAI.MinUncutGames.Foundations.Repetition.coordinate_probability_le_value_of_local_completion line 384
  32. def OAI.MinUncutGames.Foundations.Repetition.logTwo line 441
  33. theorem OAI.MinUncutGames.Foundations.Repetition.logTwo_one line 443
  34. theorem OAI.MinUncutGames.Foundations.Repetition.logTwo_inv_le_of_half_pow_le line 445
  35. theorem OAI.MinUncutGames.Foundations.Repetition.contraction_step line 457
  36. theorem OAI.MinUncutGames.Foundations.Repetition.initial_step line 496
  37. theorem OAI.MinUncutGames.Foundations.Repetition.cutoff_step line 501
  38. theorem OAI.MinUncutGames.Foundations.Repetition.cutoff_le_length line 513
  39. def OAI.MinUncutGames.Foundations.Repetition.ScalarRecurrence line 521
  40. theorem OAI.MinUncutGames.Foundations.Repetition.decay_to_cutoff line 525
  41. theorem OAI.MinUncutGames.Foundations.Repetition.block_contraction line 562
  42. theorem OAI.MinUncutGames.Foundations.Repetition.scalar_bound_6000 line 574
  43. def OAI.MinUncutGames.Foundations.Repetition.incidenceRate line 597
  44. theorem OAI.MinUncutGames.Foundations.Repetition.incidenceRate_pos line 599
  45. theorem OAI.MinUncutGames.Foundations.Repetition.incidenceRate_lt_one line 601
  46. theorem OAI.MinUncutGames.Foundations.Repetition.incidenceRate_fourth line 603
  47. theorem OAI.MinUncutGames.Foundations.Repetition.incidence_rate_comparison line 607
  48. theorem OAI.MinUncutGames.Foundations.Repetition.scalar_incidence_bound line 618