OAI/InformationTheory/QuantumCircuit/Reflection.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.QAC.reflect line 12

   Source documentation

   The real scalar spelling makes the coefficient budget transparent.

   def reflect {N : ℕ} (D : Count N) : Operator N := 1 - (2:ℝ) • D.zero

   Mentions: OAI.QAC.Count, OAI.QAC.Operator

2. def OAI.QAC.reflectList line 14
3. lemma OAI.QAC.reflectionMatrix_eq line 16
4. lemma OAI.QAC.reflect_unitary line 20
5. lemma OAI.QAC.reflect_disjoint_commute line 23
6. lemma OAI.QAC.reflect_disjoint_zero_commute line 28
7. def OAI.QAC.ReflectionLayer.active line 32
8. lemma OAI.QAC.ReflectionLayer.active_length line 36
9. lemma OAI.QAC.ReflectionLayer.active_conjugate line 44
10. def OAI.QAC.reflectionTerms line 57

    Source documentation

    Expansion of a disjoint reflection product. The real coefficients carry all multiplicities; no commutation of the middle projection is required.

    def reflectionTerms {N : ℕ} : List (Count N) → List (ℝ × Count N)
      | [] => [(1,Count.empty)]
      | A::l => reflectionTerms l ++ (reflectionTerms l).map (fun p => (-2*p.1,A.join p.2))

    Mentions: OAI.QAC.Count, OAI.QAC.Count.empty

11. lemma OAI.QAC.reflectionTerms_support line 61
12. lemma OAI.QAC.reflectionTerms_disjoint line 76
13. lemma OAI.QAC.reflectionTerms_sum line 84
14. lemma OAI.QAC.reflectionTerms_weight line 103
15. lemma OAI.QAC.star_list_sum line 116
16. lemma OAI.QAC.reflectList_selfAdjoint line 122
17. lemma OAI.QAC.list_sum_sandwich line 135
18. lemma OAI.QAC.bilinear_list_bound line 140
19. lemma OAI.QAC.reflection_conjugate_expansion line 160
20. lemma OAI.QAC.reflection_transition_bound line 167
21. lemma OAI.QAC.small_support_layer_bound line 186