OAI/InformationTheory/QuantumCircuit/RetainedMean.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Mean excitation counts of retained reflection layers.

  1. lemma OAI.QAC.eventually_exp_le_negative_power line 13
  2. theorem OAI.QAC.retained_test_mean line 22