OAI/InformationTheory/QuantumCircuit/Transition.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.QAC.norm_unitary_conjugate line 14
  2. lemma OAI.QAC.conjugate_projection line 18
  3. lemma OAI.QAC.projection_transition_square line 28
  4. lemma OAI.QAC.norm_split_bound line 49
  5. lemma OAI.QAC.sum_powers_bound line 58
  6. lemma OAI.QAC.low_patterns_card line 69
  7. lemma OAI.QAC.list_disjoint_hits_length line 91
  8. lemma OAI.QAC.norm_list_smul_sum line 115

    Source documentation

    Scalar list estimates retain multiplicities, including the ordered monomials.

    lemma norm_list_smul_sum {ι A : Type*} [SeminormedAddCommGroup A] [NormedSpace ℝ A]
    (l : List ι) (c : ι → ℝ) (f : ι → A) (δ : ℝ) (hf : ∀ i ∈ l, ‖f i‖ ≤ δ) :
    ‖(l.map (fun i => c i • f i)).sum‖ ≤ (l.map (fun i => |c i|)).sum * δ := by
…
  9. lemma OAI.QAC.Count.low_propagation_bound line 129
  10. lemma OAI.QAC.norm_mul_le_one line 146
  11. lemma OAI.QAC.three_factor_transition line 153
  12. def OAI.QAC.conjugate line 179
  13. lemma OAI.QAC.conjugate_comp line 181
  14. lemma OAI.QAC.conjugate_mul line 184
  15. lemma OAI.QAC.conjugate_star line 188
  16. lemma OAI.QAC.conjugate_sub line 191
  17. lemma OAI.QAC.conjugate_one line 194
  18. lemma OAI.QAC.conjugate_smul line 197
  19. lemma OAI.QAC.conjugate_list_sum line 200
  20. lemma OAI.QAC.conjugate_fixed line 204
  21. lemma OAI.QAC.list_conjugate_filter line 208