OAI/Computability/DirectedFeedback/RankGraph/RoundBoolean.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectedFeedback.Junta.roundBoolean line 62
  2. theorem OAI.DirectedFeedback.Junta.roundBoolean_isBoolean line 65
  3. theorem OAI.DirectedFeedback.Junta.roundBoolean_onCoordinates line 71
  4. theorem OAI.DirectedFeedback.Junta.rounding_error_le line 77
  5. theorem OAI.DirectedFeedback.Junta.friedgut_uniform line 99
  6. def OAI.DirectedFeedback.Junta.cubeEquiv line 141
  7. theorem OAI.DirectedFeedback.Junta.cubeEquiv_update line 147
  8. def OAI.DirectedFeedback.Junta.DependsOn line 159
  9. def OAI.DirectedFeedback.Junta.cubeInfluence line 162
  10. def OAI.DirectedFeedback.Junta.cubeError line 166
  11. theorem OAI.DirectedFeedback.Junta.cubeInfluence_reindex line 169
  12. theorem OAI.DirectedFeedback.Junta.friedgut_finite line 177
  13. def OAI.DirectedFeedback.Junta.merge line 220
  14. def OAI.DirectedFeedback.Junta.swapOutside line 223
  15. theorem OAI.DirectedFeedback.Junta.expect_merge line 229
  16. def OAI.DirectedFeedback.Junta.disagree line 243
  17. theorem OAI.DirectedFeedback.Junta.disagree_triangle line 245
  18. theorem OAI.DirectedFeedback.Junta.restriction_approximation line 253
  19. def OAI.DirectedFeedback.Junta.flatAnd line 290
  20. theorem OAI.DirectedFeedback.Junta.flatAnd_expectation line 293
  21. def OAI.DirectedFeedback.Junta.biasedInfluence line 300
  22. theorem OAI.DirectedFeedback.Junta.flatAnd_update_other line 304
  23. theorem OAI.DirectedFeedback.Junta.flatAnd_update_cases line 314
  24. theorem OAI.DirectedFeedback.Junta.flatAnd_influence_le line 334
  25. theorem OAI.DirectedFeedback.Junta.flatAnd_totalInfluence_le line 346
  26. theorem OAI.DirectedFeedback.Junta.friedgut_dyadic line 356
  27. theorem OAI.DirectedFeedback.Pivotal.bitValue_boolean line 410
  28. theorem OAI.DirectedFeedback.Pivotal.dyadic_coin line 413
  29. theorem OAI.DirectedFeedback.Pivotal.dyadic_law line 422
  30. theorem OAI.DirectedFeedback.Pivotal.update_insertBit line 428
  31. theorem OAI.DirectedFeedback.Pivotal.prod_insertBit line 435
  32. theorem OAI.DirectedFeedback.Pivotal.flip_square line 442
  33. theorem OAI.DirectedFeedback.Pivotal.biasedInfluence_eq line 457
  34. theorem OAI.DirectedFeedback.Pivotal.dyadic_influences_le_budget line 472
  35. theorem OAI.DirectedFeedback.Pivotal.boolean_dyadic_junta line 477
  36. def OAI.DirectedFeedback.Pivotal.DyadicJuntaBound line 507
  37. theorem OAI.DirectedFeedback.Pivotal.uniform_dyadic_junta line 516
  38. theorem OAI.DirectedFeedback.Pivotal.family_dyadic_junta line 528
  39. theorem OAI.DirectedFeedback.Coupling.product_pattern_lipschitz line 561
  40. theorem OAI.DirectedFeedback.Coupling.comparison_juntas line 575
  41. theorem OAI.DirectedFeedback.Soundness.averaged_comparison line 633
  42. theorem OAI.DirectedFeedback.Construction.double_bias line 739
  43. def OAI.DirectedFeedback.Construction.bigAcceptance line 752
  44. def OAI.DirectedFeedback.Construction.smallAcceptance line 755
  45. def OAI.DirectedFeedback.Construction.bigBudget line 759
  46. def OAI.DirectedFeedback.Construction.smallBudget line 762
  47. theorem OAI.DirectedFeedback.Construction.independent_comparison line 765
  48. theorem OAI.DirectedFeedback.transGen_loop_walk line 816
  49. theorem OAI.DirectedFeedback.exists_topological_order line 837
  50. theorem OAI.DirectedFeedback.Prefix.prefixCell_congr line 885
  51. theorem OAI.DirectedFeedback.RankGraph.good_take_prefix line 900
  52. theorem OAI.DirectedFeedback.Construction.cell_takePrefix line 926