DenseWordIdentification.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Normalize a tensor-word endpoint and identify the completed column from dense vectors.

theorem OAI.KadisonSimilarity.repeatedWordInclusion_eq_of_dense line 23

Source documentation

Equality on the dense algebra vectors identifies a normalized word column. The unnormalized endpoint is the one occurring in the raw formula.

theorem repeatedWordInclusion_eq_of_dense
    (U : OrthogonalWordLevels (MultiplicityWordSpace J E F) H)
    (n : ℕ) (R : K →ₗᵢ[ℂ] J n) (e : E) (r : F) (c : ℂ)
    (he : ‖c • e‖ = 1) (hr : ‖r‖ = 1)
    (L : K →ₗᵢ[ℂ] H) (VA : B → K) (hdense : DenseRange VA)
    (hword : ∀ b, L (VA b) = c • U.inclusion n
      (hilbertTensorInsert (R (VA b)) (endpointWord e (fun _ : Fin n => r)))) :
    repeatedWordInclusion U n R (c • e) r he hr = L := by
…

Mentions: OAI.KadisonSimilarity.OrthogonalWordLevels, OAI.KadisonSimilarity.MultiplicityWordSpace, OAI.KadisonSimilarity.hilbertTensorInsert, OAI.KadisonSimilarity.endpointWord, OAI.KadisonSimilarity.repeatedWordInclusion