OAI/Analysis/KadisonKastler/TraceUnitaryImages.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.exists_unitary_vector_image_of_traceDense line 18

   Source documentation

   Closedness of the unitary trace vectors extends the boundary image formula from a trace-dense family to every unitary.

   theorem exists_unitary_vector_image_of_traceDense
       (τM : FaithfulTracialState (Algebra M)) (τN : FaithfulTracialState (Algebra N))
       (J : Algebra M →ₗ[ℂ] E) (K : Algebra N →ₗ[ℂ] E)
       (hJ : ∀ a, ‖J a‖ = traceTwoNorm τM a)
       (hK : ∀ a, ‖K a‖ = traceTwoNorm τN a) (hτN : FiniteVectorTrace τN)
       (ρ : I → unitary (Algebra M))
       (hρ : ∀ u : unitary (Algebra M), ∀ ε : ℝ, 0 < ε →
         ∃ i, traceTwoNorm τM ((u : Algebra M) - ρ i) < ε)
       (S : unitary (E →L[ℂ] E))
       (himages : ∀ i, ∃ v : unitary (Algebra N), K v = (S : E →L[ℂ] E) (J (ρ i)))
       (u : unitary (Algebra M)) :
       ∃ v : unitary (Algebra N), K v = (S : E →L[ℂ] E) (J u) := by
   …

   Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.traceTwoNorm, OAI.KadisonKastler.FiniteVectorTrace

2. theorem OAI.KadisonKastler.exists_unital_linear_transfer_of_traceDense line 46

   Source documentation

   The normalized boundary unitary defines a unital linear map into the neighboring algebra and sends every unitary to a unitary.

   theorem exists_unital_linear_transfer_of_traceDense
       (τM : FaithfulTracialState (Algebra M)) (τN : FaithfulTracialState (Algebra N))
       (J : Algebra M →ₗ[ℂ] E) (K : Algebra N →ₗ[ℂ] E)
       (hJ : ∀ a, ‖J a‖ = traceTwoNorm τM a)
       (hK : ∀ a, ‖K a‖ = traceTwoNorm τN a) (hτN : FiniteVectorTrace τN)
       (ρ : I → unitary (Algebra M))
       (hρ : ∀ u : unitary (Algebra M), ∀ ε : ℝ, 0 < ε →
         ∃ i, traceTwoNorm τM ((u : Algebra M) - ρ i) < ε)
       (S : unitary (E →L[ℂ] E)) (hS1 : (S : E →L[ℂ] E) (J 1) = K 1)
       (himages : ∀ i, ∃ v : unitary (Algebra N), K v = (S : E →L[ℂ] E) (J (ρ i))) :
       ∃ θ : Algebra M →ₗ[ℂ] Algebra N,
         θ 1 = 1 ∧ (∀ a, K (θ a) = (S : E →L[ℂ] E) (J a)) ∧
   …

   Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.traceTwoNorm, OAI.KadisonKastler.FiniteVectorTrace

3. theorem OAI.KadisonKastler.exists_continuous_unital_transfer_of_traceDense line 68

   Source documentation

   The algebra transfer constructed from the boundary images is also continuous in the operator norm, as needed for spectral approximation.

   theorem exists_continuous_unital_transfer_of_traceDense
       (τM : FaithfulTracialState (Algebra M)) (τN : FaithfulTracialState (Algebra N))
       (J : Algebra M →ₗ[ℂ] E) (K : Algebra N →ₗ[ℂ] E)
       (hJ : ∀ a, ‖J a‖ = traceTwoNorm τM a)
       (hK : ∀ a, ‖K a‖ = traceTwoNorm τN a) (hτN : FiniteVectorTrace τN)
       (ρ : I → unitary (Algebra M))
       (hρ : ∀ u : unitary (Algebra M), ∀ ε : ℝ, 0 < ε →
         ∃ i, traceTwoNorm τM ((u : Algebra M) - ρ i) < ε)
       (S : unitary (E →L[ℂ] E)) (hS1 : (S : E →L[ℂ] E) (J 1) = K 1)
       (himages : ∀ i, ∃ v : unitary (Algebra N), K v = (S : E →L[ℂ] E) (J (ρ i))) :
       ∃ θ : Algebra M →L[ℂ] Algebra N,
         θ 1 = 1 ∧ (∀ a, K (θ a) = (S : E →L[ℂ] E) (J a)) ∧
   …

   Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.traceTwoNorm, OAI.KadisonKastler.FiniteVectorTrace