OAI/Analysis/MutuallyUnbiased/Fourier/ChargeDecomposition.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.weightMultiset line 13
2. theorem OAI.MUB6.weightMultiset_card line 16
3. theorem OAI.MUB6.weightMultiset_count line 24
4. def OAI.MUB6.positivePositions line 33
5. def OAI.MUB6.negativePositions line 34
6. theorem OAI.MUB6.positivePositions_card line 36
7. theorem OAI.MUB6.negativePositions_card line 39
8. theorem OAI.MUB6.charge_eq_counts line 47
9. theorem OAI.MUB6.positive_negative_ne line 52
10. theorem OAI.MUB6.order_one_decomposition line 63

    Source documentation

    A balanced charge of order one is one positive and one negative coordinate.

    theorem order_one_decomposition {a : Charge} (ha : Balanced a) (ho : order a = 1) :
        ∃ i j, i ≠ j ∧ a = difference i j := by
    …

    Mentions: OAI.MUB6.Charge, OAI.MUB6.Balanced, OAI.MUB6.order, OAI.MUB6.difference

11. theorem OAI.MUB6.order_two_decomposition line 74

    Source documentation

    An order-two charge has two positive and two negative positions, allowing repetitions on either side but no cancellation between the sides.

    theorem order_two_decomposition {a : Charge} (ha : Balanced a) (ho : order a = 2) :
        ∃ i l j k, i ≠ j ∧ i ≠ k ∧ l ≠ j ∧ l ≠ k ∧
          a = difference i j + difference l k := by
    …

    Mentions: OAI.MUB6.Charge, OAI.MUB6.Balanced, OAI.MUB6.order, OAI.MUB6.difference

12. theorem OAI.MUB6.g_order_one line 92