OAI/Analysis/KadisonSimilarity/Tensor/TensorPairings.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KadisonSimilarity.LabelPairingExpansion line 24

   Source documentation

   The restriction of a pairing expansion to an orthonormal alphabet. This is the concrete finite-expansion data used by the test, not an invariant classification hypothesis.

   def LabelPairingExpansion {J : Type*} [DecidableEq J]
       (Y : CompletedTensorWord E k →L[ℂ] CompletedTensorWord E l)
       (h : J → E) (c : PerfectMatching (Fin k ⊕ Fin l) → ℂ) : Prop :=
   …

   Mentions: OAI.KadisonSimilarity.CompletedTensorWord, OAI.KadisonSimilarity.PerfectMatching

2. theorem OAI.KadisonSimilarity.LabelPairingExpansion.comp line 33

   Source documentation

   Relabeling an orthonormal alphabet by an injection preserves the formula.

   theorem LabelPairingExpansion.comp {I J : Type*} [DecidableEq I] [DecidableEq J]
       {Y : CompletedTensorWord E k →L[ℂ] CompletedTensorWord E l}
       {h : J → E} {c : PerfectMatching (Fin k ⊕ Fin l) → ℂ}
       (hexp : LabelPairingExpansion Y h c) (f : I → J) (hf : Function.Injective f) :
       LabelPairingExpansion Y (h ∘ f) c := by
   …

   Mentions: OAI.KadisonSimilarity.CompletedTensorWord, OAI.KadisonSimilarity.PerfectMatching, OAI.KadisonSimilarity.LabelPairingExpansion

3. def OAI.KadisonSimilarity.sourcePairingTest line 53

   Source documentation

   Independent label choices on source-source pairs.

   def sourcePairingTest (P : PerfectMatching (Fin k ⊕ Fin l))
       (h : PermutationCycles P.1 × ℕ → E) (M : ℕ) : CompletedTensorWord E k := by
   …

   Mentions: OAI.KadisonSimilarity.PerfectMatching, OAI.KadisonSimilarity.PermutationCycles, OAI.KadisonSimilarity.CompletedTensorWord

4. def OAI.KadisonSimilarity.testPairingTest line 60

   Source documentation

   Independent label choices on test-test pairs.

   def testPairingTest (P : PerfectMatching (Fin k ⊕ Fin l))
       (h : PermutationCycles P.1 × ℕ → E) (M : ℕ) : CompletedTensorWord E l := by
   …

   Mentions: OAI.KadisonSimilarity.PerfectMatching, OAI.KadisonSimilarity.PermutationCycles, OAI.KadisonSimilarity.CompletedTensorWord

5. theorem OAI.KadisonSimilarity.norm_sourcePairingTest line 66
6. theorem OAI.KadisonSimilarity.norm_testPairingTest line 73
7. theorem OAI.KadisonSimilarity.pairingExpansion_label_test line 80
8. theorem OAI.KadisonSimilarity.inner_pairingTests line 90

   Source documentation

   Every summand contributes the same isolated coefficient.

   theorem inner_pairingTests
       (Y : CompletedTensorWord E k →L[ℂ] CompletedTensorWord E l)
       (P : PerfectMatching (Fin k ⊕ Fin l)) (h : PermutationCycles P.1 × ℕ → E)
       (c : PerfectMatching (Fin k ⊕ Fin l) → ℂ)
       (hexp : LabelPairingExpansion Y h c) (M : ℕ) :
       inner ℂ (testPairingTest P h M) (Y (sourcePairingTest P h M)) =
         c P * (M : ℂ) ^ (Fintype.card (SourcePairClasses P) + Fintype.card (TestPairClasses P)) := by
   …

   Mentions: OAI.KadisonSimilarity.CompletedTensorWord, OAI.KadisonSimilarity.PerfectMatching, OAI.KadisonSimilarity.PermutationCycles, OAI.KadisonSimilarity.LabelPairingExpansion, OAI.KadisonSimilarity.testPairingTest, OAI.KadisonSimilarity.sourcePairingTest, OAI.KadisonSimilarity.SourcePairClasses, OAI.KadisonSimilarity.TestPairClasses

9. theorem OAI.KadisonSimilarity.sqrt_power_product line 106
10. theorem OAI.KadisonSimilarity.pairing_coefficient_growth_bound line 116

    Source documentation

    The isolated coefficient grows as M^(rS+rT), while the two actual tensor norms grow as M^((rS+rT)/2).

    theorem pairing_coefficient_growth_bound
        (Y : CompletedTensorWord E k →L[ℂ] CompletedTensorWord E l)
        (P : PerfectMatching (Fin k ⊕ Fin l)) (h : PermutationCycles P.1 × ℕ → E)
        (hh : Orthonormal ℂ h) (c : PerfectMatching (Fin k ⊕ Fin l) → ℂ)
        (hexp : LabelPairingExpansion Y h c) (M : ℕ) :
        ‖c P‖ * (M : ℝ) ^ ((Fintype.card (SourcePairClasses P) +
          Fintype.card (TestPairClasses P) : ℕ) : ℝ) ≤
          ‖Y‖ * (M : ℝ) ^ (((Fintype.card (SourcePairClasses P) +
            Fintype.card (TestPairClasses P) : ℕ) : ℝ) / 2) := by
    …

    Mentions: OAI.KadisonSimilarity.CompletedTensorWord, OAI.KadisonSimilarity.PerfectMatching, OAI.KadisonSimilarity.PermutationCycles, OAI.KadisonSimilarity.LabelPairingExpansion, OAI.KadisonSimilarity.SourcePairClasses, OAI.KadisonSimilarity.TestPairClasses

11. theorem OAI.KadisonSimilarity.same_side_pairing_coefficient_eq_zero line 138

    Source documentation

    Boundedness excludes any coefficient with a same-side pair.

    theorem same_side_pairing_coefficient_eq_zero
        (Y : CompletedTensorWord E k →L[ℂ] CompletedTensorWord E l)
        (P : PerfectMatching (Fin k ⊕ Fin l)) (h : PermutationCycles P.1 × ℕ → E)
        (hh : Orthonormal ℂ h) (c : PerfectMatching (Fin k ⊕ Fin l) → ℂ)
        (hexp : LabelPairingExpansion Y h c)
        (hpair : 0 < Fintype.card (SourcePairClasses P) + Fintype.card (TestPairClasses P)) :
        c P = 0 := by
    …

    Mentions: OAI.KadisonSimilarity.CompletedTensorWord, OAI.KadisonSimilarity.PerfectMatching, OAI.KadisonSimilarity.PermutationCycles, OAI.KadisonSimilarity.LabelPairingExpansion, OAI.KadisonSimilarity.SourcePairClasses, OAI.KadisonSimilarity.TestPairClasses

12. def OAI.KadisonSimilarity.cyclePoolIndex line 151

    Source documentation

    Disjoint countable pools can be selected from one orthonormal sequence.

    def cyclePoolIndex (P : PerfectMatching (Fin k ⊕ Fin l)) : PermutationCycles P.1 × ℕ → ℕ :=
    …

    Mentions: OAI.KadisonSimilarity.PerfectMatching, OAI.KadisonSimilarity.PermutationCycles

13. theorem OAI.KadisonSimilarity.cyclePoolIndex_injective line 154
14. theorem OAI.KadisonSimilarity.same_side_pairing_coefficient_eq_zero_of_sequence line 162

    Source documentation

    A single infinite orthonormal family suffices for all matching tests.

    theorem same_side_pairing_coefficient_eq_zero_of_sequence
        (Y : CompletedTensorWord E k →L[ℂ] CompletedTensorWord E l)
        (h : ℕ → E) (hh : Orthonormal ℂ h)
        (c : PerfectMatching (Fin k ⊕ Fin l) → ℂ)
        (hexp : LabelPairingExpansion Y h c) (P : PerfectMatching (Fin k ⊕ Fin l))
        (hpair : 0 < Fintype.card (SourcePairClasses P) + Fintype.card (TestPairClasses P)) :
        c P = 0 :=
    …

    Mentions: OAI.KadisonSimilarity.CompletedTensorWord, OAI.KadisonSimilarity.PerfectMatching, OAI.KadisonSimilarity.LabelPairingExpansion, OAI.KadisonSimilarity.SourcePairClasses, OAI.KadisonSimilarity.TestPairClasses

15. theorem OAI.KadisonSimilarity.nonzero_pairing_coefficient_isCrossPairing line 174

    Source documentation

    Every nonzero coefficient must join source slots to test slots.

    theorem nonzero_pairing_coefficient_isCrossPairing
        (Y : CompletedTensorWord E k →L[ℂ] CompletedTensorWord E l)
        (h : ℕ → E) (hh : Orthonormal ℂ h)
        (c : PerfectMatching (Fin k ⊕ Fin l) → ℂ)
        (hexp : LabelPairingExpansion Y h c) (P : PerfectMatching (Fin k ⊕ Fin l))
        (hc : c P ≠ 0) : IsCrossPairing P.1 := by
    …

    Mentions: OAI.KadisonSimilarity.CompletedTensorWord, OAI.KadisonSimilarity.PerfectMatching, OAI.KadisonSimilarity.LabelPairingExpansion, OAI.KadisonSimilarity.IsCrossPairing

16. theorem OAI.KadisonSimilarity.pairing_coefficients_zero_of_degrees_ne line 187

    Source documentation

    In unequal degrees every pairing coefficient vanishes.

    theorem pairing_coefficients_zero_of_degrees_ne
        (Y : CompletedTensorWord E k →L[ℂ] CompletedTensorWord E l)
        (h : ℕ → E) (hh : Orthonormal ℂ h)
        (c : PerfectMatching (Fin k ⊕ Fin l) → ℂ)
        (hexp : LabelPairingExpansion Y h c) (hkl : k ≠ l) : c = 0 := by
    …

    Mentions: OAI.KadisonSimilarity.CompletedTensorWord, OAI.KadisonSimilarity.PerfectMatching, OAI.KadisonSimilarity.LabelPairingExpansion

17. def OAI.KadisonSimilarity.crossPairings line 198

    Source documentation

    The finite family of matchings which join source slots to test slots.

    def crossPairings (k l : ℕ) : Finset (PerfectMatching (Fin k ⊕ Fin l)) := by
    …

    Mentions: OAI.KadisonSimilarity.PerfectMatching

18. theorem OAI.KadisonSimilarity.label_pairing_expansion_restrict_cross line 203

    Source documentation

    The surviving expansion contains precisely cross pairings.

    theorem label_pairing_expansion_restrict_cross
        (Y : CompletedTensorWord E k →L[ℂ] CompletedTensorWord E l)
        (h : ℕ → E) (hh : Orthonormal ℂ h)
        (c : PerfectMatching (Fin k ⊕ Fin l) → ℂ)
        (hexp : LabelPairingExpansion Y h c) (s : Fin k → ℕ) (t : Fin l → ℕ) :
        inner ℂ (completedTensorWord (fun i => h (t i)))
          (Y (completedTensorWord (fun i => h (s i)))) =
          ∑ P ∈ crossPairings k l, c P * pairingLabelKernel P (Sum.elim s t) := by
    …

    Mentions: OAI.KadisonSimilarity.CompletedTensorWord, OAI.KadisonSimilarity.PerfectMatching, OAI.KadisonSimilarity.LabelPairingExpansion, OAI.KadisonSimilarity.completedTensorWord, OAI.KadisonSimilarity.crossPairings, OAI.KadisonSimilarity.pairingLabelKernel