OAI/Analysis/KadisonSimilarity/Tensor/TensorDensity.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonSimilarity.continuous_tensorWord line 18
2. theorem OAI.KadisonSimilarity.continuous_completedTensorWord line 31
3. theorem OAI.KadisonSimilarity.exists_common_stage line 37

   Source documentation

   Finitely many letters in the union of nested stages lie in a common stage.

   theorem exists_common_stage {ι : Type*} [Fintype ι]
       (S : ℕ → Set E) (hmono : Monotone S) (x : ι → E)
       (hx : ∀ i, x i ∈ ⋃ n, S n) : ∃ n, ∀ i, x i ∈ S n := by
   …

4. theorem OAI.KadisonSimilarity.continuous_eq_of_nested_stages line 49

   Source documentation

   Equality of continuous finite-letter functions on every common stage extends to all letters. No coefficient identity is assumed outside the stages.

   theorem continuous_eq_of_nested_stages {ι : Type*} [Fintype ι]
       (S : ℕ → Set E) (hmono : Monotone S) (hdense : Dense (⋃ n, S n))
       (F G : (ι → E) → ℂ) (hF : Continuous F) (hG : Continuous G)
       (hstage : ∀ n, ∀ x : ι → E, (∀ i, x i ∈ S n) → F x = G x) : F = G := by
   …

5. def OAI.KadisonSimilarity.pairingPolynomial line 65

   Source documentation

   The actual pairing polynomial, with one bilinear factor per pair. An injective rank function chooses a representative of each pair.

   def pairingPolynomial (rank : ι → ℕ) (B : E →L[ℂ] E →L[ℂ] ℂ)
       (P : PerfectMatching ι) (v : ι → E) : ℂ :=
   …

   Mentions: OAI.KadisonSimilarity.PerfectMatching

6. theorem OAI.KadisonSimilarity.continuous_pairingPolynomial line 70
7. theorem OAI.KadisonSimilarity.pairingPolynomial_labels line 78

   Source documentation

   On a bilinearly orthonormal alphabet, the pairing polynomial is exactly the equality-indicator kernel used by the Hilbert tensor tests.

   theorem pairingPolynomial_labels {J : Type*} [DecidableEq J]
       (rank : ι → ℕ) (hrank : Function.Injective rank)
       (B : E →L[ℂ] E →L[ℂ] ℂ) (h : J → E)
       (hB : ∀ a b, B (h a) (h b) = if a = b then 1 else 0)
       (P : PerfectMatching ι) (labels : ι → J) :
       pairingPolynomial rank B P (fun i => h (labels i)) = pairingLabelKernel P labels := by
   …

   Mentions: OAI.KadisonSimilarity.PerfectMatching, OAI.KadisonSimilarity.pairingPolynomial, OAI.KadisonSimilarity.pairingLabelKernel

8. def OAI.KadisonSimilarity.tracialWordCoefficient line 108

   Source documentation

   Coefficients with the test letters conjugated by the tracial involution.

   def tracialWordCoefficient (Y : CompletedTensorWord E k →L[ℂ] CompletedTensorWord E l)
       (J : E → E) (v : Fin k ⊕ Fin l → E) : ℂ :=
   …

   Mentions: OAI.KadisonSimilarity.CompletedTensorWord

9. theorem OAI.KadisonSimilarity.continuous_tracialWordCoefficient line 113
10. theorem OAI.KadisonSimilarity.tracial_pairing_identity_of_stages line 127

    Source documentation

    The finite-stage coefficient formula extends by density, with no bounded pairing operator presupposed. Each individual pairing polynomial is continuous as a function of its finitely many letters.

    theorem tracial_pairing_identity_of_stages
        (Y : CompletedTensorWord E k →L[ℂ] CompletedTensorWord E l)
        (J : E → E) (hJ : Continuous J)
        (B : E →L[ℂ] E →L[ℂ] ℂ) (rank : Fin k ⊕ Fin l → ℕ)
        (c : PerfectMatching (Fin k ⊕ Fin l) → ℂ)
        (S : ℕ → Set E) (hmono : Monotone S) (hdense : Dense (⋃ n, S n))
        (hstage : ∀ n, ∀ v : Fin k ⊕ Fin l → E, (∀ i, v i ∈ S n) →
          tracialWordCoefficient Y J v = ∑ P, c P * pairingPolynomial rank B P v) :
        ∀ v : Fin k ⊕ Fin l → E,
          tracialWordCoefficient Y J v = ∑ P, c P * pairingPolynomial rank B P v := by
    …

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

11. theorem OAI.KadisonSimilarity.labelPairingExpansion_of_tracial_identity line 147

    Source documentation

    Restricting the extended stage identity to self-adjoint orthonormal letters gives the precise input for the completed tensor label sums.

    theorem labelPairingExpansion_of_tracial_identity
        (Y : CompletedTensorWord E k →L[ℂ] CompletedTensorWord E l)
        (J : E → E) (B : E →L[ℂ] E →L[ℂ] ℂ)
        (rank : Fin k ⊕ Fin l → ℕ) (hrank : Function.Injective rank)
        (c : PerfectMatching (Fin k ⊕ Fin l) → ℂ) (h : ℕ → E)
        (hJ : ∀ n, J (h n) = h n)
        (hB : ∀ a b, B (h a) (h b) = if a = b then 1 else 0)
        (hfull : ∀ v, tracialWordCoefficient Y J v =
          ∑ P, c P * pairingPolynomial rank B P v) : LabelPairingExpansion Y h c := by
    …

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

12. theorem OAI.KadisonSimilarity.tensorOperator_eq_zero_of_tracial_stages line 169

    Source documentation

    In unequal degrees, the stage formula, density, and orthonormal label tests force the actual completed tensor operator to vanish.

    theorem tensorOperator_eq_zero_of_tracial_stages
        (Y : CompletedTensorWord E k →L[ℂ] CompletedTensorWord E l)
        (J : E → E) (hJ : Continuous J) (hJJ : Function.Involutive J)
        (B : E →L[ℂ] E →L[ℂ] ℂ)
        (rank : Fin k ⊕ Fin l → ℕ) (hrank : Function.Injective rank)
        (c : PerfectMatching (Fin k ⊕ Fin l) → ℂ)
        (h : ℕ → E) (hh : Orthonormal ℂ h) (hfix : ∀ n, J (h n) = h n)
        (hB : ∀ a b, B (h a) (h b) = if a = b then 1 else 0)
        (S : ℕ → Set E) (hmono : Monotone S) (hdense : Dense (⋃ n, S n))
        (hstage : ∀ n, ∀ v : Fin k ⊕ Fin l → E, (∀ i, v i ∈ S n) →
          tracialWordCoefficient Y J v = ∑ P, c P * pairingPolynomial rank B P v)
        (hkl : k ≠ l) : Y = 0 := by
    …

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