OAI/Computability/MinUncut/PCP/Overlap.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MinUncutGames.Foundations.Repetition.min_half_formula line 12
  2. theorem OAI.MinUncutGames.Foundations.Repetition.sum_min_one_sub_tv line 20
  3. theorem OAI.MinUncutGames.Foundations.Repetition.discount_le_self line 29
  4. theorem OAI.MinUncutGames.Foundations.Repetition.discount_loss_le_mul line 34
  5. def OAI.MinUncutGames.Foundations.Repetition.discountedCommonMass line 44
  6. theorem OAI.MinUncutGames.Foundations.Repetition.discounted_common_mass_bounds line 48
  7. def OAI.MinUncutGames.Foundations.Repetition.diagonalWeights line 108
  8. theorem OAI.MinUncutGames.Foundations.Repetition.diagonalWeights_isProbability line 113
  9. theorem OAI.MinUncutGames.Foundations.Repetition.diagonal_overlap_identity line 124
  10. theorem OAI.MinUncutGames.Foundations.Repetition.diagonal_sampler_totalVariation_le line 149
  11. def OAI.MinUncutGames.Foundations.Repetition.TraceSeed line 214
  12. instance OAI.MinUncutGames.Foundations.Repetition.traceSeedFintype line 218
  13. instance OAI.MinUncutGames.Foundations.Repetition.traceSeedUniqueZero line 223
  14. def OAI.MinUncutGames.Foundations.Repetition.traceList line 226
  15. def OAI.MinUncutGames.Foundations.Repetition.traceSeedLaw line 230
  16. theorem OAI.MinUncutGames.Foundations.Repetition.traceSeedLaw_expectation line 236
  17. def OAI.MinUncutGames.Foundations.Repetition.sharedOutputLaw line 253
  18. theorem OAI.MinUncutGames.Foundations.Repetition.sharedOutputLaw_weight line 261
  19. def OAI.MinUncutGames.Foundations.Repetition.samplerLocal line 279
  20. def OAI.MinUncutGames.Foundations.Repetition.samplerOutputLaw line 285
  21. theorem OAI.MinUncutGames.Foundations.Repetition.probability_weight_le_one line 292
  22. theorem OAI.MinUncutGames.Foundations.Repetition.samplerOutputLaw_diagonal line 298
  23. theorem OAI.MinUncutGames.Foundations.Repetition.samplerOutputLaw_uniform_diagonal line 329
  24. theorem OAI.MinUncutGames.Foundations.Repetition.samplerOutputLaw_totalVariation line 349
  25. theorem OAI.MinUncutGames.Foundations.Repetition.samplerOutputLaw_arbitrarily_close line 371
  26. theorem OAI.MinUncutGames.Foundations.Repetition.finiteDistribution_nonempty line 387
  27. def OAI.MinUncutGames.Foundations.Repetition.selectedProfileFallback line 397
  28. def OAI.MinUncutGames.Foundations.Repetition.selectedLeftProfile line 405
  29. def OAI.MinUncutGames.Foundations.Repetition.selectedRightProfile line 418
  30. def OAI.MinUncutGames.Foundations.Repetition.selectedLeftProfileError line 431
  31. def OAI.MinUncutGames.Foundations.Repetition.selectedRightProfileError line 438
  32. theorem OAI.MinUncutGames.Foundations.Repetition.selectedLeftProfileError_le line 445
  33. theorem OAI.MinUncutGames.Foundations.Repetition.selectedRightProfileError_le line 459
  34. def OAI.MinUncutGames.Foundations.Repetition.selectedSamplingTarget line 473
  35. theorem OAI.MinUncutGames.Foundations.Repetition.selectedSamplingTarget_left_error line 481
  36. theorem OAI.MinUncutGames.Foundations.Repetition.selectedSamplingTarget_right_error line 494
  37. theorem OAI.MinUncutGames.Foundations.Repetition.pushforward_snd_weight_eq_secondMarginal line 507
  38. def OAI.MinUncutGames.Foundations.Repetition.revealDataSplitEquiv line 517
  39. theorem OAI.MinUncutGames.Foundations.Repetition.partialRevealMarginal_secondMarginal line 534
  40. def OAI.MinUncutGames.Foundations.Repetition.selectedObservationDataEquiv line 554
  41. theorem OAI.MinUncutGames.Foundations.Repetition.selectedFullReveal_secondMarginal line 563
  42. theorem OAI.MinUncutGames.Foundations.Repetition.selectedRawMarginal_secondMarginal line 577
  43. theorem OAI.MinUncutGames.Foundations.Repetition.selectedCommonLaw_secondMarginal line 599
  44. theorem OAI.MinUncutGames.Foundations.Repetition.selectedCommonLaw_questions_pushforward line 610
  45. theorem OAI.MinUncutGames.Foundations.Repetition.selectedQuestionRadius_le_informationRadius line 628
  46. theorem OAI.MinUncutGames.Foundations.Repetition.selectedQuestionMarginal_error_sum line 644
  47. def OAI.MinUncutGames.Foundations.Repetition.selectedEmbeddingError line 654
  48. theorem OAI.MinUncutGames.Foundations.Repetition.selectedEmbeddingError_nonnegative line 661
  49. theorem OAI.MinUncutGames.Foundations.Repetition.selectedLeftProfileError_sum line 670
  50. theorem OAI.MinUncutGames.Foundations.Repetition.selectedRightProfileError_sum line 688
  51. theorem OAI.MinUncutGames.Foundations.Repetition.selectedEmbeddingError_sum_le_fifteen line 706