OAI/Analysis/KadisonSimilarity/Tensor/InvariantForms.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The finite-stage coefficient form

The coefficient function used by the invariant argument is proved multilinear from the linear source letters and conjugate-linear test letters. No finite or completed coefficient expansion is part of this construction.

  1. theorem OAI.KadisonSimilarity.completedTensorWord_update_add line 23

    Source documentation

    The elementary completed word retains multilinearity in every letter.

    theorem completedTensorWord_update_add {n : ℕ} (x : Fin n → F) (i : Fin n) (a b : F) :
    completedTensorWord (Function.update x i (a + b)) =
      completedTensorWord (Function.update x i a) + completedTensorWord (Function.update x i b) := by
…

    Mentions: OAI.KadisonSimilarity.completedTensorWord

  2. theorem OAI.KadisonSimilarity.completedTensorWord_update_smul line 31
  3. theorem OAI.KadisonSimilarity.endpointWord_add_endpoint line 39
  4. theorem OAI.KadisonSimilarity.endpointWord_smul_endpoint line 47
  5. theorem OAI.KadisonSimilarity.endpointWord_update_add line 55
  6. theorem OAI.KadisonSimilarity.endpointWord_update_smul line 60
  7. def OAI.KadisonSimilarity.pullLetters line 65
  8. theorem OAI.KadisonSimilarity.pullLetters_update line 68
  9. theorem OAI.KadisonSimilarity.pullLetters_update_miss line 76
  10. abbrev OAI.KadisonSimilarity.sourceIndex line 82
  11. abbrev OAI.KadisonSimilarity.testIndex line 83
  12. def OAI.KadisonSimilarity.invariantStageCoefficient line 88

    Source documentation

    The coefficient with distinguished endpoint and two groups of tail letters.

    def invariantStageCoefficient
    (Y : EndpointTensor E F k →L[ℂ] EndpointTensor E F l) (Ω : E)
    (testEndpoint : D →ₗ⋆[ℂ] E) (sourceLetter : D →ₗ[ℂ] F)
    (testLetter : D →ₗ⋆[ℂ] F) (v : Option (Fin k ⊕ Fin l) → D) : ℂ :=
…

    Mentions: OAI.KadisonSimilarity.EndpointTensor, OAI.KadisonSimilarity.testLetter

  13. def OAI.KadisonSimilarity.invariantStageForm line 96

    Source documentation

    Multilinearity of the actual finite-stage coefficient function.

    def invariantStageForm
    (Y : EndpointTensor E F k →L[ℂ] EndpointTensor E F l) (Ω : E)
    (testEndpoint : D →ₗ⋆[ℂ] E) (sourceLetter : D →ₗ[ℂ] F)
    (testLetter : D →ₗ⋆[ℂ] F) :
    MultilinearMap ℂ (fun _ : Option (Fin k ⊕ Fin l) => D) ℂ :=
…

    Mentions: OAI.KadisonSimilarity.EndpointTensor, OAI.KadisonSimilarity.testLetter

  14. theorem OAI.KadisonSimilarity.invariantStageForm_apply line 179