OAI/InformationTheory/QuantumCircuit/Regularity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Low-degree propagation and pruning for regular quantum trajectories.

  1. theorem OAI.QAC.low_degree_propagation_unconditional line 16
  2. theorem OAI.QAC.regular_pruning_of_factors line 31