OAI/Computability/DirectedFeedback/Games/ActualAdviceStochasticBridge.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.DFVSGames.Clean.ActualAdviceStochasticBridge.sourceAnswerNonempty line 20
2. instance OAI.DFVSGames.Clean.ActualAdviceStochasticBridge.targetAnswerNonempty line 21
3. structure OAI.DFVSGames.Clean.ActualAdviceStochasticBridge.Policies line 24
4. def OAI.DFVSGames.Clean.ActualAdviceStochasticBridge.extendTargetKernel line 31
5. theorem OAI.DFVSGames.Clean.ActualAdviceStochasticBridge.extendTargetKernel_apply line 41
6. def OAI.DFVSGames.Clean.ActualAdviceStochasticBridge.firstResponse line 50
7. def OAI.DFVSGames.Clean.ActualAdviceStochasticBridge.secondResponse line 58
8. theorem OAI.DFVSGames.Clean.ActualAdviceStochasticBridge.decodeFirstMap_actual line 68
9. theorem OAI.DFVSGames.Clean.ActualAdviceStochasticBridge.decodeSecondMap_actual line 88
10. theorem OAI.DFVSGames.Clean.ActualAdviceStochasticBridge.firstResponse_actual line 99
11. theorem OAI.DFVSGames.Clean.ActualAdviceStochasticBridge.secondResponse_actual line 111
12. def OAI.DFVSGames.Clean.ActualAdviceStochasticBridge.fixedMapSuccess line 122
13. theorem OAI.DFVSGames.Clean.ActualAdviceStochasticBridge.fixedMapSuccess_le line 131
14. def OAI.DFVSGames.Clean.ActualAdviceStochasticBridge.responses line 175
15. def OAI.DFVSGames.Clean.ActualAdviceStochasticBridge.success line 183
16. theorem OAI.DFVSGames.Clean.ActualAdviceStochasticBridge.success_le_native_stochastic line 191
17. theorem OAI.DFVSGames.Clean.ActualAdviceStochasticBridge.success_le_some_native line 215
18. def OAI.DFVSGames.Soundness.LinearMapDensity.uniformMean line 238
19. theorem OAI.DFVSGames.Soundness.LinearMapDensity.uniformMean_eq_sum_div_card line 241
20. theorem OAI.DFVSGames.Soundness.LinearMapDensity.uniformMean_comm line 245
21. theorem OAI.DFVSGames.Soundness.LinearMapDensity.uniformMean_const_mul line 251
22. theorem OAI.DFVSGames.Soundness.LinearMapDensity.uniformMean_const line 255
23. theorem OAI.DFVSGames.Soundness.LinearMapDensity.restriction_surjective line 260
24. theorem OAI.DFVSGames.Soundness.LinearMapDensity.restriction_zero_iff line 267
25. def OAI.DFVSGames.Soundness.LinearMapDensity.pullbackMap line 277
26. theorem OAI.DFVSGames.Soundness.LinearMapDensity.pullbackMap_bijective line 288
27. theorem OAI.DFVSGames.Soundness.LinearMapDensity.annihilator_count line 311
28. def OAI.DFVSGames.Soundness.LinearMapDensity.kernelDensity line 326
29. theorem OAI.DFVSGames.Soundness.LinearMapDensity.kernelDensity_mean line 332
30. theorem OAI.DFVSGames.Soundness.LinearMapDensity.kernelDensity_product line 350
31. theorem OAI.DFVSGames.Soundness.LinearMapDensity.kernelDensity_pair_mean line 373
32. def OAI.DFVSGames.Soundness.LinearMapDensity.mixtureDensity line 380
33. theorem OAI.DFVSGames.Soundness.LinearMapDensity.mixtureDensity_mean line 384
34. theorem OAI.DFVSGames.Soundness.LinearMapDensity.mixtureDensity_second_moment line 392
35. theorem OAI.DFVSGames.Soundness.LinearMapDensity.kernelDensity_weighted_mean line 411
36. theorem OAI.DFVSGames.Soundness.LinearMapDensity.pullback_uniformMean line 442
37. theorem OAI.DFVSGames.Soundness.LinearMapDensity.mixture_pullback_uniformMean line 453
38. theorem OAI.DFVSGames.Soundness.ExpectationComparison.density_variance_identity line 478
39. theorem OAI.DFVSGames.Soundness.ExpectationComparison.density_variance_le line 492
40. theorem OAI.DFVSGames.Soundness.ExpectationComparison.bounded_test_second_moment line 499
41. theorem OAI.DFVSGames.Soundness.ExpectationComparison.bounded_test_centered_square line 506
42. theorem OAI.DFVSGames.Soundness.ExpectationComparison.bounded_test_expectation_comparison line 519
43. theorem OAI.DFVSGames.Soundness.ExpectationComparison.comparison_error_le_quarter line 533
44. theorem OAI.DFVSGames.Soundness.ExpectationComparison.parameter_error_le_quarter line 537
45. theorem OAI.DFVSGames.Soundness.ExpectationComparison.map_law_parameter_error line 547
46. theorem OAI.DFVSGames.Soundness.ExpectationComparison.bounded_test_expectation_quarter line 554
47. theorem OAI.DFVSGames.Soundness.ExpectationComparison.transferred_signal_lower line 563
48. def OAI.DFVSGames.Soundness.ExpectationComparison.wholeMapTest line 573
49. theorem OAI.DFVSGames.Soundness.ExpectationComparison.wholeMapTest_abs_le_one line 578
50. theorem OAI.DFVSGames.Soundness.ExpectationComparison.wholeMapTest_comparison line 595
51. theorem OAI.DFVSGames.Soundness.ExpectationComparison.averaged_expectation_comparison line 612
52. theorem OAI.DFVSGames.Soundness.ExpectationComparison.averaged_transferred_signal_lower line 632
53. theorem OAI.DFVSGames.Soundness.ExpectationComparison.uniform_expect_eq_sum_div_card line 648
54. def OAI.DFVSGames.Soundness.RepetitionUpper.bernoulliAverage line 656
55. theorem OAI.DFVSGames.Soundness.RepetitionUpper.bernoulliAverage_scale line 662
56. theorem OAI.DFVSGames.Soundness.RepetitionUpper.bernoulliAverage_geometric line 670
57. theorem OAI.DFVSGames.Soundness.RepetitionUpper.bernoulliAverage_mono line 682
58. theorem OAI.DFVSGames.Soundness.RepetitionUpper.success_le_geometric line 697
59. theorem OAI.DFVSGames.Soundness.RepetitionUpper.pow_mono_nonneg line 708
60. def OAI.DFVSGames.Soundness.RepetitionUpper.zeroProbability line 720
61. theorem OAI.DFVSGames.Soundness.RepetitionUpper.zeroProbability_nonneg line 722
62. theorem OAI.DFVSGames.Soundness.RepetitionUpper.zeroProbability_le_one line 725
63. theorem OAI.DFVSGames.Soundness.RepetitionUpper.zeroProbability_antitone line 733
64. theorem OAI.DFVSGames.Soundness.RepetitionUpper.geometric_le_dimension_bound line 752
65. theorem OAI.DFVSGames.Soundness.RepetitionUpper.projection_upper_bound line 766
66. def OAI.DFVSGames.Soundness.RepetitionUpper.decoderThreshold line 777
67. theorem OAI.DFVSGames.Soundness.RepetitionUpper.decoderThreshold_pos line 779
68. theorem OAI.DFVSGames.Soundness.RepetitionUpper.exists_pos_nat_gt line 788
69. theorem OAI.DFVSGames.Soundness.RepetitionUpper.power_mul_growth_le_one line 797
70. theorem OAI.DFVSGames.Soundness.RepetitionUpper.exists_power_lt line 813
71. theorem OAI.DFVSGames.Soundness.RepetitionUpper.zeroProbability_pos line 830
72. theorem OAI.DFVSGames.Soundness.RepetitionUpper.exists_repetition_length line 833
73. theorem OAI.DFVSGames.Soundness.RepetitionUpper.soundness_of_bounds line 847
74. theorem OAI.DFVSGames.Soundness.RepetitionUpper.soundness_from_repetition line 862