OAI/Computability/DirectedFeedback/Games/PartnerFullSampling.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Soundness.PartnerFullSampling.restrictIndices line 14
  2. def OAI.DFVSGames.Soundness.PartnerFullSampling.restrictionProductEquiv line 17
  3. theorem OAI.DFVSGames.Soundness.PartnerFullSampling.expect_restrictIndices line 32
  4. def OAI.DFVSGames.Soundness.PartnerFullSampling.fromFullIndices line 46
  5. theorem OAI.DFVSGames.Soundness.PartnerFullSampling.fixed_active_expect_fullIndices line 49
  6. theorem OAI.DFVSGames.Soundness.PartnerFullSampling.partner_expect_active_slots line 55
  7. theorem OAI.DFVSGames.Soundness.PartnerFullSampling.partner_expect_fullIndices line 65
  8. theorem OAI.DFVSGames.Soundness.PartnerFullSampling.projection_eq_of_slots_eq_on_active line 74
  9. theorem OAI.DFVSGames.Soundness.PartnerFullSampling.projection_fromFullIndices line 91
  10. def OAI.DFVSGames.Soundness.PartnerFullSampling.drawProductEquiv line 104
  11. theorem OAI.DFVSGames.Soundness.PartnerFullSampling.fixed_active_rawDraw_expect line 112
  12. theorem OAI.DFVSGames.Soundness.PartnerFullSampling.occurrence_partner_expect_eq_rawDraw line 139
  13. def OAI.DFVSGames.Clean.CoefficientSampling.selectCoefficients line 177
  14. def OAI.DFVSGames.Clean.CoefficientSampling.coefficientProductEquiv line 184
  15. theorem OAI.DFVSGames.Clean.CoefficientSampling.expect_outside line 205
  16. theorem OAI.DFVSGames.Clean.CoefficientSampling.expect_rawCoefficients line 217
  17. theorem OAI.DFVSGames.Clean.CoefficientSampling.expect_selectCoefficients line 232
  18. theorem OAI.DFVSGames.Clean.CoefficientSampling.uniform_expectation_eq_expect_inline_CoefficientSampling line 259
  19. theorem OAI.DFVSGames.Clean.CoefficientSampling.uniform_selectCoefficients line 263
  20. theorem OAI.DFVSGames.Clean.CoefficientSampling.mask_average_selectCoefficients line 271
  21. theorem OAI.DFVSGames.Clean.NativeExperiment.expectation_transport_inline_NativeExperiment line 297
  22. theorem OAI.DFVSGames.Clean.NativeExperiment.iid_product_split line 303
  23. theorem OAI.DFVSGames.Clean.NativeExperiment.expectation_iid_product line 313
  24. def OAI.DFVSGames.Clean.NativeExperiment.maskSet line 327
  25. abbrev OAI.DFVSGames.Clean.NativeExperiment.MaskStrategy line 330
  26. def OAI.DFVSGames.Clean.NativeExperiment.liftStrategy line 334
  27. def OAI.DFVSGames.Clean.NativeExperiment.success line 338
  28. theorem OAI.DFVSGames.Clean.NativeExperiment.success_eq_flat line 348
  29. def OAI.DFVSGames.Clean.ActualAdviceBridge.indexSlot line 414
  30. theorem OAI.DFVSGames.Clean.ActualAdviceBridge.slotIndex_indexSlot line 417
  31. structure OAI.DFVSGames.Clean.ActualAdviceBridge.Policies line 421
  32. def OAI.DFVSGames.Clean.ActualAdviceBridge.projection line 428
  33. def OAI.DFVSGames.Clean.ActualAdviceBridge.displayedQuestion line 433
  34. def OAI.DFVSGames.Clean.ActualAdviceBridge.agrees line 437
  35. def OAI.DFVSGames.Clean.ActualAdviceBridge.strategy line 443
  36. def OAI.DFVSGames.Clean.ActualAdviceBridge.encodedMapCoefficients line 449
  37. theorem OAI.DFVSGames.Clean.ActualAdviceBridge.sample_question line 454
  38. theorem OAI.DFVSGames.Clean.ActualAdviceBridge.agrees_implies_actualWin line 463
  39. def OAI.DFVSGames.Clean.ActualAdviceBridge.fixedMapSuccess line 502
  40. theorem OAI.DFVSGames.Clean.ActualAdviceBridge.fixedMapSuccess_le line 509
  41. def OAI.DFVSGames.Clean.ActualAdviceBridge.mapBitsEquiv line 521
  42. theorem OAI.DFVSGames.Clean.ActualAdviceBridge.uniform_maps_to_bits line 525
  43. def OAI.DFVSGames.Clean.ActualAdviceBridge.nativeStrategy line 533
  44. def OAI.DFVSGames.Clean.ActualAdviceBridge.success line 538
  45. theorem OAI.DFVSGames.Clean.ActualAdviceBridge.expectation_mono line 545
  46. theorem OAI.DFVSGames.Clean.ActualAdviceBridge.success_le_native line 552
  47. def OAI.DFVSGames.Clean.StochasticBound.actualGame line 590
  48. abbrev OAI.DFVSGames.Clean.StochasticBound.fixedAdviceGame line 599
  49. theorem OAI.DFVSGames.Clean.StochasticBound.success_eq_fixedAdviceSuccess line 603
  50. theorem OAI.DFVSGames.Clean.StochasticBound.exists_deterministic_ge_stochastic line 619
  51. theorem OAI.DFVSGames.Clean.StochasticBound.fixed_advice_stochastic_le_repeated_value line 638
  52. abbrev OAI.DFVSGames.Clean.StochasticBound.Responses line 653
  53. def OAI.DFVSGames.Clean.StochasticBound.nativeStochasticSuccess line 657
  54. theorem OAI.DFVSGames.Clean.StochasticBound.expectation_mono_inline_StochasticBound line 669
  55. theorem OAI.DFVSGames.Clean.StochasticBound.native_stochastic_le_deterministic line 677
  56. theorem OAI.DFVSGames.Clean.StochasticBound.native_stochastic_le_mask_moment line 700