OAI/Computability/UniqueGames/Reduction/AddressOutputSize.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniqueGamesTheorem.Reduction.AddressOutputSize.vertexBound line 16
  2. def OAI.UniqueGamesTheorem.Reduction.AddressOutputSize.edgeBound line 20
  3. def OAI.UniqueGamesTheorem.Reduction.AddressOutputSize.bitsBound line 23
  4. theorem OAI.UniqueGamesTheorem.Reduction.AddressOutputSize.bitsBound_mono line 27
  5. def OAI.UniqueGamesTheorem.Reduction.AddressOutputSize.sizeBound line 35
  6. theorem OAI.UniqueGamesTheorem.Reduction.AddressOutputSize.table_constraints_eq line 38
  7. theorem OAI.UniqueGamesTheorem.Reduction.AddressOutputSize.scaled_sum_le line 46
  8. theorem OAI.UniqueGamesTheorem.Reduction.AddressOutputSize.collect_edge_coefficient line 53
  9. theorem OAI.UniqueGamesTheorem.Reduction.AddressOutputSize.output_constraints_eq line 59
  10. theorem OAI.UniqueGamesTheorem.Reduction.AddressOutputSize.output_vertices_le_input line 67
  11. theorem OAI.UniqueGamesTheorem.Reduction.AddressOutputSize.output_constraints_le_input line 86
  12. theorem OAI.UniqueGamesTheorem.Reduction.AddressOutputSize.output_bits_length_le line 95
  13. def OAI.UniqueGamesTheorem.Reduction.AddressOutputSize.outputPolynomial line 105

    Source documentation

    One fixed polynomial includes every declared address and every edge table.

    noncomputable def outputPolynomial (k : Nat) (T : NoiseTables.Table s d) : Polynomial Nat :=
…
  14. theorem OAI.UniqueGamesTheorem.Reduction.AddressOutputSize.outputPolynomial_eval line 113
  15. theorem OAI.UniqueGamesTheorem.Reduction.AddressOutputSize.output_bits_polynomial_in_input line 119
  16. theorem OAI.UniqueGamesTheorem.Reduction.AddressOutputSize.fixed_parameters_output_size line 127
  17. def OAI.UniqueGamesTheorem.Reduction.AddressOutputSize.directVertexBound line 134
  18. def OAI.UniqueGamesTheorem.Reduction.AddressOutputSize.directEdgeCoefficient line 137
  19. def OAI.UniqueGamesTheorem.Reduction.AddressOutputSize.directSizeBound line 140
  20. theorem OAI.UniqueGamesTheorem.Reduction.AddressOutputSize.direct_vertices_le_input line 144
  21. theorem OAI.UniqueGamesTheorem.Reduction.AddressOutputSize.direct_constraints_eq line 160
  22. theorem OAI.UniqueGamesTheorem.Reduction.AddressOutputSize.direct_constraints_le_input line 168
  23. theorem OAI.UniqueGamesTheorem.Reduction.AddressOutputSize.direct_bits_length_le line 176
  24. def OAI.UniqueGamesTheorem.Reduction.AddressOutputSize.directOutputPolynomial line 185
  25. theorem OAI.UniqueGamesTheorem.Reduction.AddressOutputSize.directOutputPolynomial_eval line 192
  26. theorem OAI.UniqueGamesTheorem.Reduction.AddressOutputSize.direct_bits_polynomial_in_input line 198
  27. theorem OAI.UniqueGamesTheorem.Reduction.AddressOutputSize.fixed_parameters_direct_output_size line 206