OAI/InformationTheory/QuantumCircuit/ApproximationBudget.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Asymptotic error budgets for low-degree approximations.

  1. lemma OAI.QAC.act_smul line 12
  2. lemma OAI.QAC.act_sub_state line 15
  3. lemma OAI.QAC.act_real_smul line 18
  4. def OAI.QAC.ApproxOn line 23
  5. lemma OAI.QAC.ApproxOn.exact line 26
  6. lemma OAI.QAC.ApproxOn.mono line 30
  7. lemma OAI.QAC.ApproxOn.congr_operator line 36
  8. lemma OAI.QAC.ApproxOn.add line 40
  9. lemma OAI.QAC.ApproxOn.smul line 49
  10. lemma OAI.QAC.ApproxOn.real_smul line 58
  11. lemma OAI.QAC.approx_list_sum line 71
  12. lemma OAI.QAC.approx_real_list_sum line 83
  13. lemma OAI.QAC.reflection_double_expansion line 95
  14. lemma OAI.QAC.sandwich_approximation line 117