OAI/Computability/DirectedFeedback/Games/ActualAdviceSampling.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DFVSGames.Decoder.ActualAdviceSampling.product_probability line 19
  2. theorem OAI.DFVSGames.Decoder.ActualAdviceSampling.fixedMapSuccess_eq_product line 28
  3. theorem OAI.DFVSGames.Decoder.ActualAdviceSampling.fixedMapSuccess_eq_observed line 49
  4. def OAI.DFVSGames.Decoder.ActualAdviceSampling.sampledAgreement line 70
  5. theorem OAI.DFVSGames.Decoder.ActualAdviceSampling.actualSuccess_eq_sampledAgreement line 86
  6. theorem OAI.DFVSGames.Decoder.ActualAdviceSampling.sampledAgreement_average_bound line 102
  7. theorem OAI.DFVSGames.Decoder.ActualSeedPointwise.rawProjection_congr_slots line 135
  8. theorem OAI.DFVSGames.Decoder.ActualSeedPointwise.supported_congr_slots line 155
  9. theorem OAI.DFVSGames.Decoder.ActualSeedPointwise.observedAgreement_changePositions line 169
  10. theorem OAI.DFVSGames.Decoder.ActualSeedPointwise.seedAgreement_pointwise line 188
  11. theorem OAI.DFVSGames.Decoder.ActualSeedPointwise.seedAgreement_repack_at_inline_ActualSeedPointwise line 208
  12. theorem OAI.DFVSGames.Decoder.ActualSeedPointwise.seedAgreement_repack line 235
  13. theorem OAI.DFVSGames.Decoder.ActualSeedSampling.uniform_occurrence_slots line 281
  14. def OAI.DFVSGames.Decoder.ActualSeedSampling.drawAgreement line 293
  15. theorem OAI.DFVSGames.Decoder.ActualSeedSampling.sampledAgreement_eq_separated line 306
  16. theorem OAI.DFVSGames.Decoder.ActualSeedSampling.fullSeedLaw_eq_sampledAgreement line 341
  17. theorem OAI.DFVSGames.Decoder.ActualSeedSampling.fullSeedLaw_upper line 379
  18. theorem OAI.DFVSGames.Decoder.ActualMatrixContradiction.univ_fintype_eq_inline_ActualMatrixContradiction line 412
  19. def OAI.DFVSGames.Decoder.ActualMatrixContradiction.expectationOf_inline_ActualMatrixContradiction line 416
  20. theorem OAI.DFVSGames.Decoder.ActualMatrixContradiction.card_to_natCard_inline_ActualMatrixContradiction line 420
  21. theorem OAI.DFVSGames.Decoder.ActualMatrixContradiction.law_expectation_eq line 424
  22. theorem OAI.DFVSGames.Decoder.ActualMatrixContradiction.contradiction line 433
  23. def OAI.DFVSGames.Gadget.aggregate line 476
  24. def OAI.DFVSGames.Gadget.shiftAggregate line 481
  25. def OAI.DFVSGames.Gadget.parentShifts line 487
  26. def OAI.DFVSGames.Gadget.parentLogical line 491
  27. def OAI.DFVSGames.Gadget.parentEmbed line 496
  28. theorem OAI.DFVSGames.Gadget.parentEmbed_injective line 502
  29. theorem OAI.DFVSGames.Gadget.shiftAggregate_surjective line 510
  30. theorem OAI.DFVSGames.Gadget.parentLogical_surjective line 522
  31. def OAI.DFVSGames.Gadget.parentOutput line 534
  32. theorem OAI.DFVSGames.Gadget.aggregate_output_shift line 539
  33. theorem OAI.DFVSGames.Gadget.parentOutput_equivariant line 549
  34. theorem OAI.DFVSGames.Gadget.output_difference_shift line 570
  35. structure OAI.DFVSGames.Gadget.Stage line 584
  36. def OAI.DFVSGames.Gadget.Stage.base line 613
  37. def OAI.DFVSGames.Gadget.Stage.next line 628
  38. def OAI.DFVSGames.Gadget.Stage.iterate line 642
  39. theorem OAI.DFVSGames.Gadget.Stage.iterate_zero line 647
  40. theorem OAI.DFVSGames.Gadget.Stage.iterate_succ line 651
  41. theorem OAI.DFVSGames.Gadget.family_factors_of_ker line 667
  42. theorem OAI.DFVSGames.Gadget.common_parent_factorization line 684
  43. theorem OAI.DFVSGames.Gadget.common_child_factorization line 703
  44. theorem OAI.DFVSGames.Gadget.aggregate_fst_surjective line 714