OAI/Analysis/MutuallyUnbiased/Tao/TaoFamily.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.commonRowTransform line 13
2. theorem OAI.MUB6.commonRowTransform_isHadamard line 16
3. theorem OAI.MUB6.g_commonRowTransform line 24
4. theorem OAI.MUB6.balanced_permute line 32
5. theorem OAI.MUB6.order_permute line 36
6. theorem OAI.MUB6.commonRowTransform_cross line 40
7. theorem OAI.MUB6.columnTransform_cross line 55
8. def OAI.MUB6.averageOtherFourier line 67
9. theorem OAI.MUB6.averageOtherFourier_order_two line 70
10. theorem OAI.MUB6.averageOtherFourier_positive line 82
11. theorem OAI.MUB6.different_matrices_conjugated line 107
12. theorem OAI.MUB6.averageOtherFourier_cross line 117
13. theorem OAI.MUB6.equivalent_tao_average line 140

    Source documentation

    A full-equivalence copy of Tao in six candidate Hadamards supplies exactly the three hypotheses of the checked Tao certificate.

    theorem equivalent_tao_average (H : Coord → CMatrix)
        (hH : ∀ t, IsHadamard (H t))
        (hcross : ∀ t s, t ≠ s → ∀ k l,
          Complex.normSq (∑ i, H t i k * conj (H s i l)) = 6)
        (horder : ∀ a, Balanced a → order a = 2 → ∑ t, g (H t) a = 0)
        (s : Coord) (heq : Equivalent (H s) tao) :
        ∃ f : Charge → ℂ,
          (∀ a c, Balanced a → Balanced c →
            offDiagSum (fun i j => f (a + difference i j) *
              star (g tao (c + difference i j))) = 0) ∧
          TaoArithmetic.OrderTwoValues f ∧
          0 ≤ 6 + offDiagSum (fun i j => (f ((3 : ℤ) • difference i j)).re) := by
    …

    Mentions: OAI.MUB6.Coord, OAI.MUB6.CMatrix, OAI.MUB6.IsHadamard, OAI.MUB6.Balanced, OAI.MUB6.order, OAI.MUB6.g, OAI.MUB6.Equivalent, OAI.MUB6.tao, OAI.MUB6.Charge, OAI.MUB6.offDiagSum, OAI.MUB6.difference, OAI.MUB6.TaoArithmetic.OrderTwoValues