OAI/InformationTheory/QuantumCircuit/DepthZero.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.QAC.rankOne_sandwich line 11
2. lemma OAI.QAC.rankOne_markov_le line 21
3. lemma OAI.QAC.tensorMatrix_pattern_scale line 50
4. lemma OAI.QAC.Count.spectral_power_tensor line 69

   Source documentation

   The generating function of the mismatch spectral partition.

   lemma Count.spectral_power_tensor {N : ℕ} (M : Count N) (z : ℝ) :
       (∑ F ∈ M.support.powerset, z ^ F.card • M.pattern F) =
         tensorMatrix (fun i => if i ∈ M.support then
           z • (1 - rankOne (M.vector i)) + rankOne (M.vector i) else 1) := by
   …

   Mentions: OAI.QAC.Count, OAI.QAC.tensorMatrix, OAI.QAC.rankOne

5. lemma OAI.QAC.Count.high_le_generating line 80
6. def OAI.QAC.Count.site line 100

   Source documentation

   Single-site factor of a product projection.

   def Count.site {N : ℕ} (M : Count N) (i : Fin N) : QubitOperator :=
   …

   Mentions: OAI.QAC.Count, OAI.QAC.QubitOperator

7. lemma OAI.QAC.Count.site_projection line 103
8. lemma OAI.QAC.projection_markov_nonneg line 111
9. lemma OAI.QAC.projection_markov_self line 120
10. lemma OAI.QAC.Count.markov_site_le line 126
11. lemma OAI.QAC.Count.generating_eq_sites line 142
12. lemma OAI.QAC.Count.markov_sandwich_le line 152
13. lemma OAI.QAC.Count.depth_zero_square line 165
14. lemma OAI.QAC.Count.depth_zero_bound line 186