OAI/Computability/DirectedFeedback/Probability/PolynomialProbability.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DFVSGames.Quadratic.isGeneric_range_of_injective line 15
  2. theorem OAI.DFVSGames.Quadratic.finrank_range_binary_parameters line 84
  3. def OAI.DFVSGames.Quadratic.assignmentProbability line 101
  4. theorem OAI.DFVSGames.Quadratic.assignmentProbability_mono line 106
  5. theorem OAI.DFVSGames.Quadratic.assignmentProbability_eval_zero_le line 116
  6. theorem OAI.DFVSGames.Quadratic.totalDegree_map_eq_of_injective line 126
  7. theorem OAI.DFVSGames.Quadratic.assignmentProbability_eval₂_zero_le line 133
  8. theorem OAI.DFVSGames.Quadratic.assignmentProbability_le_of_polynomial line 147
  9. theorem OAI.DFVSGames.Quadratic.assignmentProbability_union_le line 156
  10. def OAI.DFVSGames.Quadratic.reindexAssignments line 189
  11. def OAI.DFVSGames.Quadratic.finiteAssignmentProbability line 195
  12. theorem OAI.DFVSGames.Quadratic.finiteAssignmentProbability_reindex line 201
  13. theorem OAI.DFVSGames.Quadratic.finiteAssignmentProbability_le_of_polynomial line 217
  14. theorem OAI.DFVSGames.Quadratic.finiteAssignmentProbability_eval₂_zero_le line 240
  15. theorem OAI.DFVSGames.Quadratic.finiteAssignmentProbability_union_le line 247
  16. theorem OAI.DFVSGames.Quadratic.exists_genericity_polynomial line 280
  17. theorem OAI.DFVSGames.Quadratic.exists_genericity_error_numerator line 297
  18. def OAI.DFVSGames.Quadratic.parameterMapEquiv line 329
  19. theorem OAI.DFVSGames.Quadratic.parameterMap_event_card line 343
  20. theorem OAI.DFVSGames.Quadratic.parameterMap_event_probability line 353
  21. def OAI.DFVSGames.Quadratic.UniformSubspaces.Injection line 381
  22. instance OAI.DFVSGames.Quadratic.UniformSubspaces.injectionAction line 385
  23. theorem OAI.DFVSGames.Quadratic.UniformSubspaces.injection_transitive line 398
  24. def OAI.DFVSGames.Quadratic.UniformSubspaces.image line 412
  25. theorem OAI.DFVSGames.Quadratic.UniformSubspaces.image_action line 416
  26. theorem OAI.DFVSGames.Quadratic.UniformSubspaces.mean_image line 424
  27. theorem OAI.DFVSGames.Quadratic.UniformSubspaces.bad_image_count_ratio line 432
  28. theorem OAI.DFVSGames.Quadratic.UniformSubspaces.bad_subspace_bound line 442
  29. theorem OAI.DFVSGames.Quadratic.conditioning_counts_inline_GenericSubspaceProbability line 472
  30. theorem OAI.DFVSGames.Quadratic.generic_subspace_and_probability_of_parameter_error line 517
  31. theorem OAI.DFVSGames.Quadratic.exists_generic_subspace_error_numerator line 559
  32. theorem OAI.DFVSGames.Quadratic.conditional_error_le_of_small line 573
  33. abbrev OAI.DFVSGames.Quadratic.BinaryField line 586
  34. theorem OAI.DFVSGames.Quadratic.card_binaryField line 588
  35. theorem OAI.DFVSGames.Quadratic.finrank_binaryField line 592
  36. theorem OAI.DFVSGames.Quadratic.finrank_binaryField_triple line 596
  37. def OAI.DFVSGames.Quadratic.fieldDegree line 601
  38. theorem OAI.DFVSGames.Quadratic.fieldDegree_pos line 604
  39. theorem OAI.DFVSGames.Quadratic.threshold_lt_two_pow_fieldDegree line 607
  40. theorem OAI.DFVSGames.Quadratic.rankThreshold_le_triple_fieldDegree line 611
  41. theorem OAI.DFVSGames.Quadratic.exists_binary_field_degree line 615
  42. theorem OAI.DFVSGames.Quadratic.chosen_binaryField_thresholds line 620
  43. instance OAI.DFVSGames.Quadratic.binaryFieldFintype line 636
  44. theorem OAI.DFVSGames.Quadratic.exists_uniform_generic_field line 639
  45. theorem OAI.DFVSGames.Gadget.BaseConstruction.theta_le_one line 711
  46. theorem OAI.DFVSGames.Gadget.BaseConstruction.rate_eq_one_sub_theta line 717
  47. theorem OAI.DFVSGames.Gadget.BaseConstruction.quotient_detection line 720
  48. theorem OAI.DFVSGames.Gadget.BaseConstruction.quotient_error_le line 753
  49. theorem OAI.DFVSGames.Gadget.BaseConstruction.exists_base line 764