OAI/InformationTheory/QuantumCircuit/PropagationAsymptotics.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Asymptotic estimates for propagation through reflection layers.

  1. lemma OAI.QAC.HasDegreeLE.floor line 13
  2. lemma OAI.QAC.propagationBudget_log_bound line 19
  3. lemma OAI.QAC.eventually_propagationBudget line 55
  4. def OAI.QAC.LayerRegular line 67
  5. def OAI.QAC.TransportOn line 74
  6. lemma OAI.QAC.ApproxOn.transport line 79