OAI/InformationTheory/QuantumCircuit/Spectral.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.QAC.Count.flip_pattern line 11
  2. lemma OAI.QAC.Count.high_mul_pattern line 23
  3. lemma OAI.QAC.symmDiff_subset_of_subset line 38
  4. lemma OAI.QAC.card_le_add_symmDiff line 42
  5. lemma OAI.QAC.Count.high_flip_absorb line 51
  6. def OAI.QAC.Count.low line 67
  7. lemma OAI.QAC.Count.low_projection line 69
  8. lemma OAI.QAC.Count.low_eq_sum line 72
  9. lemma OAI.QAC.norm_mul_le_right line 84
  10. lemma OAI.QAC.norm_mul_le_left line 87
  11. lemma OAI.QAC.Count.high_flip_norm line 90
  12. lemma OAI.QAC.Count.generator_mul_pattern line 102
  13. lemma OAI.QAC.Count.operator_mul_pattern line 122
  14. def OAI.QAC.Count.spectral line 134
  15. lemma OAI.QAC.Count.operator_spectral line 137
  16. lemma OAI.QAC.Count.spectral_mul line 148
  17. lemma OAI.QAC.Count.operator_pow_spectral line 155
  18. lemma OAI.QAC.Count.operator_norm_le line 161
  19. def OAI.QAC.Count.polynomial line 166

    Source documentation

    Evaluate a real polynomial using the explicit integer spectral decomposition.

    def Count.polynomial {N : ℕ} (M : Count N) (p : Polynomial ℝ) : Operator N :=
…

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

  20. lemma OAI.QAC.Count.polynomial_eq_sum line 169
  21. lemma OAI.QAC.Count.generator_eq_restrict line 181
  22. def OAI.QAC.selectionSets line 195

    Source documentation

    Ordered monomials, retaining multiplicities, with repeated coordinates collapsed.

    def selectionSets {ι : Type*} [DecidableEq ι] (S : Finset ι) : ℕ → List (Finset ι)
  | 0 => [∅]
  | k+1 => S.toList.flatMap (fun i => (selectionSets S k).map (insert i))
  23. lemma OAI.QAC.selectionSets_card line 199
  24. lemma OAI.QAC.selectionSets_length line 209
  25. lemma OAI.QAC.list_sum_flatMap line 215
  26. lemma OAI.QAC.Count.selectionSets_sum line 221
  27. lemma OAI.QAC.Count.operator_monomials line 239
  28. lemma OAI.QAC.list_norm_sum_le line 249
  29. lemma OAI.QAC.list_norm_sum_le_const line 257
  30. lemma OAI.QAC.Count.zero_spectral line 269
  31. lemma OAI.QAC.Count.high_spectral line 279
  32. lemma OAI.QAC.Count.low_spectral line 286
  33. lemma OAI.QAC.Count.spectral_sub line 294
  34. lemma OAI.QAC.Count.polynomial_error_low line 298