OAI/Computability/DirectedFeedback/Games/SharedSampling.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Foundations.Repetition.TraceSeed line 15
  2. instance OAI.DFVSGames.Foundations.Repetition.traceSeedFintype line 19
  3. instance OAI.DFVSGames.Foundations.Repetition.traceSeedUniqueZero line 24
  4. def OAI.DFVSGames.Foundations.Repetition.traceList line 27
  5. def OAI.DFVSGames.Foundations.Repetition.traceSeedLaw line 31
  6. theorem OAI.DFVSGames.Foundations.Repetition.traceSeedLaw_expectation line 37
  7. def OAI.DFVSGames.Foundations.Repetition.sharedOutputLaw line 54
  8. theorem OAI.DFVSGames.Foundations.Repetition.sharedOutputLaw_weight line 62
  9. def OAI.DFVSGames.Foundations.Repetition.samplerLocal line 81
  10. def OAI.DFVSGames.Foundations.Repetition.samplerOutputLaw line 87
  11. theorem OAI.DFVSGames.Foundations.Repetition.probability_weight_le_one line 94
  12. theorem OAI.DFVSGames.Foundations.Repetition.samplerOutputLaw_diagonal line 100
  13. theorem OAI.DFVSGames.Foundations.Repetition.samplerOutputLaw_uniform_diagonal line 131
  14. theorem OAI.DFVSGames.Foundations.Repetition.samplerOutputLaw_totalVariation line 151
  15. theorem OAI.DFVSGames.Foundations.Repetition.samplerOutputLaw_arbitrarily_close line 173
  16. def OAI.DFVSGames.Repetition.partialPairMass line 202
  17. def OAI.DFVSGames.Repetition.partialEdgeMass line 206
  18. def OAI.DFVSGames.Repetition.partialLabelScore line 211
  19. def OAI.DFVSGames.Repetition.partialSample line 215
  20. theorem OAI.DFVSGames.Repetition.expectation_mono_inline_RoundingSampling' line 219
  21. theorem OAI.DFVSGames.Repetition.expectation_const_inline_RoundingSampling' line 226
  22. theorem OAI.DFVSGames.Repetition.first_good_relation_le_inline_RoundingSampling line 231
  23. theorem OAI.DFVSGames.Repetition.partial_mass_bounds_inline_RoundingSampling line 254
  24. theorem OAI.DFVSGames.Repetition.partial_ratio_bound_inline_RoundingSampling line 283
  25. theorem OAI.DFVSGames.Repetition.partialSample_pair_lower line 306
  26. theorem OAI.DFVSGames.Repetition.expectation_partial_lower_inline_RoundingSampling line 345
  27. theorem OAI.DFVSGames.Repetition.exists_labeling_ge_partial line 359
  28. def OAI.DFVSGames.Repetition.thresholdLevels line 429
  29. theorem OAI.DFVSGames.Repetition.square_mem_thresholdLevels line 433
  30. abbrev OAI.DFVSGames.Repetition.ThresholdSeed line 439
  31. def OAI.DFVSGames.Repetition.thresholdDistribution line 441
  32. theorem OAI.DFVSGames.Repetition.thresholdSeed_nonempty line 444
  33. def OAI.DFVSGames.Repetition.thresholdAccept line 452
  34. def OAI.DFVSGames.Repetition.thresholdLabel line 455
  35. def OAI.DFVSGames.Repetition.thresholdRate line 458
  36. theorem OAI.DFVSGames.Repetition.thresholdRate_positive line 460
  37. theorem OAI.DFVSGames.Repetition.square_le_one_of_row_norm line 465
  38. theorem OAI.DFVSGames.Repetition.threshold_acceptance_mass line 472
  39. theorem OAI.DFVSGames.Repetition.threshold_good_pair_mass line 482
  40. theorem OAI.DFVSGames.Repetition.threshold_good_pair_mass_bool line 523
  41. theorem OAI.DFVSGames.Repetition.threshold_average_good_mass line 550
  42. theorem OAI.DFVSGames.Repetition.exists_labeling_high_value line 564
  43. theorem OAI.DFVSGames.Repetition.exists_labeling_high_value_of_rows_le_one line 583
  44. theorem OAI.DFVSGames.Repetition.pairEnergy_le_of_labeling_gap line 607
  45. def OAI.DFVSGames.Repetition.rowMass line 641
  46. def OAI.DFVSGames.Repetition.deterministicVector line 643
  47. theorem OAI.DFVSGames.Repetition.deterministicVector_rowMass line 648
  48. theorem OAI.DFVSGames.Repetition.rowMass_nonnegative line 654
  49. theorem OAI.DFVSGames.Repetition.deterministicVector_nonnegative line 659
  50. theorem OAI.DFVSGames.Repetition.deterministicVector_linear_image line 667
  51. theorem OAI.DFVSGames.Repetition.entry_eq_zero_of_rowMass_eq_zero line 674
  52. def OAI.DFVSGames.Repetition.rowLaw line 681
  53. theorem OAI.DFVSGames.Repetition.rowLaw_expectation_mul_mass line 697
  54. theorem OAI.DFVSGames.Repetition.square_expectation_le line 710
  55. theorem OAI.DFVSGames.Repetition.exists_expectation_le line 737
  56. theorem OAI.DFVSGames.Repetition.exists_deterministic_preserving_mass line 754
  57. theorem OAI.DFVSGames.Repetition.exists_deterministic_vector line 800