OAI/RepresentationTheory/FoulkesHowe/PermanentPairing.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem346.permanentPairing line 14

   Source documentation

   The normalized permanent of a pairing on two indexed families.

   def permanentPairing {X : Type u} {Y : Type v} (n : ℕ)
       (B : X → Y → ℂ) (x : Fin n → X) (y : Fin n → Y) : ℂ :=
   …

2. theorem OAI.Problem346.permanentPairing_perm_right line 18
3. theorem OAI.Problem346.permanentPairing_perm_left line 29
4. theorem OAI.Problem346.permanentPairing_flip line 49

   Source documentation

   Transposing the underlying pairing transposes the two families.

   theorem permanentPairing_flip {X : Type u} {Y : Type v} (n : ℕ)
       (B : X → Y → ℂ) (x : Fin n → X) (y : Fin n → Y) :
       permanentPairing n (fun y x => B x y) y x = permanentPairing n B x y := by
   …

   Mentions: OAI.Problem346.permanentPairing

5. theorem OAI.Problem346.permanentPairing_const_right line 66
6. theorem OAI.Problem346.permanentPairing_const_left line 73
7. theorem OAI.Problem346.permanentPairing_natural line 80

   Source documentation

   Moving a map across each scalar pairing moves it across the normalized permanent.

   theorem permanentPairing_natural {X : Type u} {Y : Type v}
       {X' : Type w} {Y' : Type z} (n : ℕ)
       (B : X → Y → ℂ) (B' : X' → Y' → ℂ)
       (f : X → X') (g : Y' → Y)
       (h : ∀ x y, B' (f x) y = B x (g y))
       (x : Fin n → X) (y : Fin n → Y') :
       permanentPairing n B' (fun i => f (x i)) y =
         permanentPairing n B x (fun i => g (y i)) := by
   …

   Mentions: OAI.Problem346.permanentPairing

8. def OAI.Problem346.permanentPairingRight line 97

   Source documentation

   The permanent pairing as a multilinear map in its right family.

   def permanentPairingRight (n : ℕ) (B : X →ₗ[ℂ] Y →ₗ[ℂ] ℂ)
       (x : Fin n → X) : MultilinearMap ℂ (fun _ : Fin n => Y) ℂ :=
   …

9. theorem OAI.Problem346.permanentPairingRight_apply line 103
10. def OAI.Problem346.permanentPairingLeft line 110

    Source documentation

    The permanent pairing as a multilinear map in its left family.

    def permanentPairingLeft (n : ℕ) (B : X →ₗ[ℂ] Y →ₗ[ℂ] ℂ)
        (y : Fin n → Y) : MultilinearMap ℂ (fun _ : Fin n => X) ℂ :=
    …

11. theorem OAI.Problem346.permanentPairingLeft_apply line 117
12. def OAI.Problem346.permanentPairingMultilinear line 124

    Source documentation

    Both families of the permanent pairing are multilinear.

    def permanentPairingMultilinear (n : ℕ) (B : X →ₗ[ℂ] Y →ₗ[ℂ] ℂ) :
        MultilinearMap ℂ (fun _ : Fin n => X)
          (MultilinearMap ℂ (fun _ : Fin n => Y) ℂ) where
    …

13. theorem OAI.Problem346.permanentPairingMultilinear_apply line 139
14. theorem OAI.Problem346.permanentPairingMultilinear_perm_left line 145
15. theorem OAI.Problem346.permanentPairingMultilinear_perm_right line 153