OAI/InformationTheory/QuantumCircuit/Parity.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.QAC.eventually_exp_neg_power_lt line 13
2. lemma OAI.QAC.polynomial_qubit_threshold line 20
3. lemma OAI.QAC.hadamard_high_entry_bound line 29
4. theorem OAI.QAC.parity_lower_bound line 45

   Source documentation

   The measured-output parity lower bound, allowing arbitrary final garbage and all polynomially many initially zero ancillas. No cleanliness assumption is used.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: OAI.QAC.ParityStatement

   Proof uses: Nat, Real, LE.le, OfNat.ofNat, LT.lt, HDiv.hDiv, lt_of_lt_of_le, zero_lt_one, HMul.hMul, id, div_pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Eq.refl, Bool, Nat.ble, mul_pos, Mathlib.Meta.NormNum.instAtLeastTwo, lt_of_not_ge and 168 more

   148 instances, coercions and auxiliary constants left out.

   Distinct definitions of this name: ComparatorChallenges/QACParity.lean:71 (different declaration text). Qualify references as OAI.QAC.parity_lower_bound@path.

   Tactic trace: 36 steps

   Open to load the checked before-and-after goal states.

   theorem parity_lower_bound : ParityStatement := by
   …

   Mentions: OAI.QAC.ParityStatement