DenseEndpointIdentification.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A named normalized endpoint can be identified before instantiating the dense-word equality. This avoids unfolding its Hilbert-space construction.

theorem OAI.KadisonSimilarity.repeatedWordInclusion_eq_of_dense_endpoint line 21

Source documentation

Use a proved endpoint identity while keeping its normed-space data opaque.

theorem repeatedWordInclusion_eq_of_dense_endpoint
    (U : OrthogonalWordLevels (MultiplicityWordSpace J E F) H)
    (n : ℕ) (R : K →ₗᵢ[ℂ] J n) (d e : E) (r : F) (c : ℂ)
    (hd : ‖d‖ = 1) (hr : ‖r‖ = 1) (heq : d = c • e)
    (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 d r hd hr = L := by
…

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