OAI/Analysis/KadisonSimilarity/Tensor/EndpointPairings.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.KadisonSimilarity.MatchingRepresentatives line 23

   Source documentation

   Choose the lower-ranked vertex in each pair.

   abbrev MatchingRepresentatives (rank : ι → ℕ) (P : PerfectMatching ι) :=
   …

   Mentions: OAI.KadisonSimilarity.PerfectMatching

2. instance OAI.KadisonSimilarity.matchingRepresentativesFintype line 26
3. theorem OAI.KadisonSimilarity.matching_rank_ne line 30
4. def OAI.KadisonSimilarity.matchingSplitEquiv line 35

   Source documentation

   The vertices split into a representative and its partner, once per pair.

   def matchingSplitEquiv (rank : ι → ℕ) (hrank : Function.Injective rank)
       (P : PerfectMatching ι) :
       MatchingRepresentatives rank P ⊕ MatchingRepresentatives rank P ≃ ι :=
   …

   Mentions: OAI.KadisonSimilarity.PerfectMatching, OAI.KadisonSimilarity.MatchingRepresentatives

5. theorem OAI.KadisonSimilarity.matchingSplitEquiv_inl line 68
6. theorem OAI.KadisonSimilarity.matchingSplitEquiv_inr line 73
7. def OAI.KadisonSimilarity.matchingClassEquiv line 78

   Source documentation

   Each matching orbit has exactly one lower-ranked representative.

   def matchingClassEquiv (rank : ι → ℕ) (hrank : Function.Injective rank)
       (P : PerfectMatching ι) : MatchingRepresentatives rank P ≃ PermutationCycles P.1 :=
   …

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

8. theorem OAI.KadisonSimilarity.permutationCycleCount_matching line 100
9. theorem OAI.KadisonSimilarity.permutationContraction_matching line 108

   Source documentation

   The unnormalized coordinate contraction of a matching is a product of ordinary matrix traces, one for each pair.

   theorem permutationContraction_matching (rank : ι → ℕ) (hrank : Function.Injective rank)
       (P : PerfectMatching ι) (v : ι → Matrix α α ℂ) :
       permutationContraction P.1 v =
         ∏ i : MatchingRepresentatives rank P, Matrix.trace (v i * v (P.1 i)) := by
   …

   Mentions: OAI.KadisonSimilarity.PerfectMatching, OAI.KadisonSimilarity.permutationContraction, OAI.KadisonSimilarity.MatchingRepresentatives

10. theorem OAI.KadisonSimilarity.normalizedPermutationContraction_matching line 143

    Source documentation

    The normalized contraction uses one normalized trace for each pair.

    theorem normalizedPermutationContraction_matching
        (rank : ι → ℕ) (hrank : Function.Injective rank)
        (P : PerfectMatching ι) (v : ι → Matrix α α ℂ) :
        normalizedPermutationContraction P.1 v =
          ∏ i : MatchingRepresentatives rank P,
            (Fintype.card α : ℂ)⁻¹ * Matrix.trace (v i * v (P.1 i)) := by
    …

    Mentions: OAI.KadisonSimilarity.PerfectMatching, OAI.KadisonSimilarity.normalizedPermutationContraction, OAI.KadisonSimilarity.MatchingRepresentatives

11. theorem OAI.KadisonSimilarity.sameCycle_involutive_iff line 156

    Source documentation

    The orbit of an involution consists of the point and its partner, allowing also the fixed-point case used for the endpoint.

    theorem sameCycle_involutive_iff (π : Equiv.Perm ι) (hπ : Function.Involutive π)
        (i j : ι) : π.SameCycle i j ↔ j = i ∨ j = π i := by
    …

12. def OAI.KadisonSimilarity.endpointMatching line 174

    Source documentation

    Add a fixed distinguished endpoint to a tail matching.

    def endpointMatching (P : PerfectMatching ι) : Equiv.Perm (Option ι) :=
    …

    Mentions: OAI.KadisonSimilarity.PerfectMatching

13. theorem OAI.KadisonSimilarity.endpointMatching_none line 178
14. theorem OAI.KadisonSimilarity.endpointMatching_some line 182
15. theorem OAI.KadisonSimilarity.endpointMatching_involutive line 186
16. theorem OAI.KadisonSimilarity.endpointMatching_isEndpointPairing line 194
17. def OAI.KadisonSimilarity.endpointMatchingClassEquiv line 203

    Source documentation

    The endpoint supplies one additional singleton orbit.

    def endpointMatchingClassEquiv (rank : ι → ℕ) (hrank : Function.Injective rank)
        (P : PerfectMatching ι) :
        Option (MatchingRepresentatives rank P) ≃ PermutationCycles (endpointMatching P) :=
    …

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

18. theorem OAI.KadisonSimilarity.permutationCycleCount_endpointMatching line 245
19. theorem OAI.KadisonSimilarity.permutationContraction_endpointMatching line 253

    Source documentation

    Splitting the endpoint coordinate leaves precisely the tail contraction.

    theorem permutationContraction_endpointMatching (P : PerfectMatching ι)
        (v : Option ι → Matrix α α ℂ) :
        permutationContraction (endpointMatching P) v =
          Matrix.trace (v none) * permutationContraction P.1 (fun i => v (some i)) := by
    …

    Mentions: OAI.KadisonSimilarity.PerfectMatching, OAI.KadisonSimilarity.permutationContraction, OAI.KadisonSimilarity.endpointMatching

20. theorem OAI.KadisonSimilarity.normalizedPermutationContraction_endpointMatching line 271

    Source documentation

    Each surviving finite-stage cycle form is the endpoint trace times the product of normalized pair traces.

    theorem normalizedPermutationContraction_endpointMatching
        (rank : ι → ℕ) (hrank : Function.Injective rank)
        (P : PerfectMatching ι) (v : Option ι → Matrix α α ℂ) :
        normalizedPermutationContraction (endpointMatching P) v =
          ((Fintype.card α : ℂ)⁻¹ * Matrix.trace (v none)) *
            ∏ i : MatchingRepresentatives rank P,
              (Fintype.card α : ℂ)⁻¹ * Matrix.trace (v (some i) * v (some (P.1 i))) := by
    …

    Mentions: OAI.KadisonSimilarity.PerfectMatching, OAI.KadisonSimilarity.normalizedPermutationContraction, OAI.KadisonSimilarity.endpointMatching, OAI.KadisonSimilarity.MatchingRepresentatives

21. theorem OAI.KadisonSimilarity.optionPerm_some line 285
22. def OAI.KadisonSimilarity.endpointTailMatching line 292

    Source documentation

    Remove the distinguished fixed endpoint from a surviving permutation.

    def endpointTailMatching (π : Equiv.Perm (Option ι)) (hπ : EndpointPairing π none) :
        PerfectMatching ι :=
    …

    Mentions: OAI.KadisonSimilarity.EndpointPairing, OAI.KadisonSimilarity.PerfectMatching

23. theorem OAI.KadisonSimilarity.endpointMatching_tail line 309
24. def OAI.KadisonSimilarity.endpointMatchingEquiv line 318

    Source documentation

    Surviving permutations are in bijection with tail matchings.

    def endpointMatchingEquiv : PerfectMatching ι ≃
        {π : Equiv.Perm (Option ι) // EndpointPairing π none} :=
    …

    Mentions: OAI.KadisonSimilarity.PerfectMatching, OAI.KadisonSimilarity.EndpointPairing

25. theorem OAI.KadisonSimilarity.endpointMatchingEquiv_apply line 331
26. theorem OAI.KadisonSimilarity.invariant_expansion_tail_pairings line 336

    Source documentation

    Combining the cycle threshold, centered singleton deletion, and explicit matrix factorization yields exactly the finite-stage pairing expansion.

    theorem invariant_expansion_tail_pairings
        (rank : ι → ℕ) (hrank : Function.Injective rank)
        (v : Option ι → Matrix α α ℂ) (hcenter : ∀ i, Matrix.trace (v (some i)) = 0)
        (c : Equiv.Perm (Option ι) → ℂ)
        (hsmall : ∀ π, 2 * permutationCycleCount π < Fintype.card (Option ι) + 1 → c π = 0) :
        (∑ π, c π * normalizedPermutationContraction π v) =
          ((Fintype.card α : ℂ)⁻¹ * Matrix.trace (v none)) *
            ∑ P : PerfectMatching ι, c (endpointMatching P) *
              ∏ i : MatchingRepresentatives rank P,
                (Fintype.card α : ℂ)⁻¹ * Matrix.trace (v (some i) * v (some (P.1 i))) := by
    …

    Mentions: OAI.KadisonSimilarity.permutationCycleCount, OAI.KadisonSimilarity.normalizedPermutationContraction, OAI.KadisonSimilarity.PerfectMatching, OAI.KadisonSimilarity.endpointMatching, OAI.KadisonSimilarity.MatchingRepresentatives

27. theorem OAI.KadisonSimilarity.normalizedPermutationContraction_endpointMatching_eq_pairingPolynomial line 369

    Source documentation

    In a tracial Hilbert-stage realization, the matrix factorization is the same continuous bilinear pairing polynomial used after taking density.

    theorem normalizedPermutationContraction_endpointMatching_eq_pairingPolynomial
        (rank : ι → ℕ) (hrank : Function.Injective rank)
        (P : PerfectMatching ι) (v : Option ι → Matrix α α ℂ)
        (embed : Matrix α α ℂ → E) (B : E →L[ℂ] E →L[ℂ] ℂ)
        (hB : ∀ a b, B (embed a) (embed b) =
          (Fintype.card α : ℂ)⁻¹ * Matrix.trace (a * b)) :
        normalizedPermutationContraction (endpointMatching P) v =
          ((Fintype.card α : ℂ)⁻¹ * Matrix.trace (v none)) *
            pairingPolynomial rank B P (fun i => embed (v (some i))) := by
    …

    Mentions: OAI.KadisonSimilarity.PerfectMatching, OAI.KadisonSimilarity.normalizedPermutationContraction, OAI.KadisonSimilarity.endpointMatching, OAI.KadisonSimilarity.pairingPolynomial