OAI/InformationTheory/QuantumCircuit/ReflectionApproximation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Low-degree approximation of products of reflections.

  1. def OAI.QAC.propagationBudget line 13
  2. lemma OAI.QAC.propagationBudget_nonneg line 16
  3. lemma OAI.QAC.conjugate_complex_list_sum line 20
  4. lemma OAI.QAC.subcount_sandwich_approximation line 27
  5. lemma OAI.QAC.reflection_expansion_approximation line 45
  6. lemma OAI.QAC.tensor_reflection_approximation line 79
  7. theorem OAI.QAC.low_degree_reflection_approximation line 116