OAI/Computability/DirectedFeedback/RankGraph/FailureEvent.lean

GitHub source file

88 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DirectedFeedback.Construction.bigFunction_properties line 68
  2. theorem OAI.DirectedFeedback.Construction.smallFunction_properties line 77
  3. theorem OAI.DirectedFeedback.Construction.family_costs line 86
  4. theorem OAI.DirectedFeedback.Construction.big_budget line 105
  5. theorem OAI.DirectedFeedback.Construction.small_budget line 126
  6. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.uniform_single_le line 154
  7. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.fixed_choice_charge line 163
  8. theorem OAI.DirectedFeedback.SourceProbability.FiniteDistribution.probability_good_restrict line 176
  9. def OAI.DirectedFeedback.Construction.failureEvent line 199
  10. def OAI.DirectedFeedback.Construction.scaleDeletion line 206
  11. theorem OAI.DirectedFeedback.Construction.scaleDeletion_nonneg line 211
  12. theorem OAI.DirectedFeedback.Construction.comparison_probability_decomposition line 214
  13. theorem OAI.DirectedFeedback.Construction.single_scale_cost line 220
  14. theorem OAI.DirectedFeedback.Construction.good_failure_charge line 229
  15. theorem OAI.DirectedFeedback.Construction.comparison_charge line 282
  16. abbrev OAI.DirectedFeedback.JuntaSupport.Cube line 330
  17. def OAI.DirectedFeedback.JuntaSupport.bitSign line 332
  18. theorem OAI.DirectedFeedback.JuntaSupport.bitSign_sq line 334
  19. theorem OAI.DirectedFeedback.JuntaSupport.bitSign_xor line 337
  20. def OAI.DirectedFeedback.JuntaSupport.cubeXor line 341
  21. def OAI.DirectedFeedback.JuntaSupport.walsh line 343
  22. theorem OAI.DirectedFeedback.JuntaSupport.walsh_symm line 346
  23. theorem OAI.DirectedFeedback.JuntaSupport.walsh_sq line 350
  24. theorem OAI.DirectedFeedback.JuntaSupport.walsh_xor line 354
  25. theorem OAI.DirectedFeedback.JuntaSupport.coordinate_orthogonality line 362
  26. theorem OAI.DirectedFeedback.JuntaSupport.walsh_sum_orthogonality line 367
  27. theorem OAI.DirectedFeedback.JuntaSupport.walsh_orthogonality line 384
  28. def OAI.DirectedFeedback.JuntaSupport.coefficient line 391
  29. theorem OAI.DirectedFeedback.JuntaSupport.walsh_inversion line 394
  30. theorem OAI.DirectedFeedback.JuntaSupport.walsh_inner line 411
  31. theorem OAI.DirectedFeedback.JuntaSupport.walsh_parseval line 428
  32. theorem OAI.DirectedFeedback.JuntaSupport.sign_parseval line 432
  33. def OAI.DFVSMaxCut.Analytic.degree line 441
  34. theorem OAI.DFVSMaxCut.BooleanFourthMoment.sum_cube_succ line 449
  35. theorem OAI.DFVSMaxCut.BooleanFourthMoment.expect_cube_succ line 454
  36. theorem OAI.DFVSMaxCut.BooleanFourthMoment.expect_bool line 461
  37. def OAI.DFVSMaxCut.BooleanFourthMoment.polynomial line 465
  38. def OAI.DFVSMaxCut.BooleanFourthMoment.energy line 468
  39. theorem OAI.DFVSMaxCut.BooleanFourthMoment.energy_nonneg line 472
  40. theorem OAI.DFVSMaxCut.BooleanFourthMoment.walsh_cons line 481
  41. theorem OAI.DFVSMaxCut.BooleanFourthMoment.polynomial_cons line 485
  42. theorem OAI.DFVSMaxCut.BooleanFourthMoment.energy_cons line 497
  43. theorem OAI.DFVSMaxCut.BooleanFourthMoment.fourth_moment_cons line 507
  44. theorem OAI.DFVSMaxCut.BooleanFourthMoment.fourth_moment_bound line 520
  45. theorem OAI.DFVSMaxCut.BooleanFourthMoment.weight_eq_degree line 549
  46. theorem OAI.DFVSMaxCut.BooleanFourthMoment.energy_truncated line 553
  47. theorem OAI.DFVSMaxCut.BooleanFourthMoment.coefficient_polynomial line 565
  48. theorem OAI.DFVSMaxCut.BooleanFourthMoment.polynomial_second_moment line 573
  49. theorem OAI.DFVSMaxCut.BooleanFourthMoment.degree_fourth_moment_bound line 578
  50. theorem OAI.DFVSMaxCut.BooleanFourthMoment.degree_third_moment_bound line 585
  51. theorem OAI.DFVSMaxCut.BooleanFourthMoment.walsh_flip line 607
  52. def OAI.DFVSMaxCut.BooleanFourthMoment.discreteDiff line 619
  53. theorem OAI.DFVSMaxCut.BooleanFourthMoment.polynomial_diff line 622
  54. theorem OAI.DFVSMaxCut.BooleanFourthMoment.total_diff_second line 631
  55. theorem OAI.DFVSMaxCut.BooleanFourthMoment.total_diff_second_truncated line 643
  56. theorem OAI.DFVSMaxCut.BooleanFourthMoment.total_diff_third_truncated line 654
  57. def OAI.DirectedFeedback.Junta.influence line 679
  58. def OAI.DirectedFeedback.Junta.totalInfluence line 682
  59. def OAI.DirectedFeedback.Junta.IsBoolean line 684
  60. def OAI.DirectedFeedback.Junta.OnCoordinates line 686
  61. def OAI.DirectedFeedback.Junta.error line 689
  62. theorem OAI.DirectedFeedback.Junta.polynomial_coefficients line 692
  63. theorem OAI.DirectedFeedback.Junta.influence_nonneg line 697
  64. theorem OAI.DirectedFeedback.Junta.influence_eq_diff line 700
  65. theorem OAI.DirectedFeedback.Junta.totalInfluence_spectral line 708
  66. theorem OAI.DirectedFeedback.Junta.spectral_tail line 716
  67. def OAI.DirectedFeedback.Junta.pivotal line 733
  68. theorem OAI.DirectedFeedback.Junta.pivotal_sq line 736
  69. theorem OAI.DirectedFeedback.Junta.diff_mul_pivotal line 741
  70. theorem OAI.DirectedFeedback.Junta.pivotal_eq_difference_sq line 748
  71. theorem OAI.DirectedFeedback.Junta.expect_pivotal line 755
  72. def OAI.DirectedFeedback.Junta.lowDiffCoeff line 760
  73. def OAI.DirectedFeedback.Junta.lowDiff line 763
  74. theorem OAI.DirectedFeedback.Junta.coefficient_discreteDiff line 766
  75. theorem OAI.DirectedFeedback.Junta.inner_lowDiff line 772
  76. theorem OAI.DirectedFeedback.Junta.lowDiff_fourth line 783
  77. theorem OAI.DirectedFeedback.Junta.lowDiff_energy_le line 790
  78. def OAI.DirectedFeedback.Junta.support line 847
  79. def OAI.DirectedFeedback.Junta.projectCoeff line 850
  80. def OAI.DirectedFeedback.Junta.project line 853
  81. theorem OAI.DirectedFeedback.Junta.walsh_eq_on_support line 856
  82. theorem OAI.DirectedFeedback.Junta.project_onCoordinates line 864
  83. theorem OAI.DirectedFeedback.Junta.coefficient_sub line 873
  84. theorem OAI.DirectedFeedback.Junta.project_squared_error line 878
  85. theorem OAI.DirectedFeedback.Junta.project_squared_error_le line 888
  86. def OAI.DirectedFeedback.Junta.highInfluences line 914
  87. theorem OAI.DirectedFeedback.Junta.highInfluences_card_bound line 917
  88. theorem OAI.DirectedFeedback.Junta.lowDiff_sum_outside line 928