OAI/Analysis/KadisonKastler/BoundaryPolarMeasurable.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.aestronglyMeasurable_polar_trace line 29

   Source documentation

   A uniformly near-identity field has measurable unitary polar factors whenever the original field is measurable in its tracial Hilbert space.

   theorem aestronglyMeasurable_polar_trace
       (τ : FaithfulTracialState B) (J : B →ₗ[ℂ] E)
       (hJ : ∀ x, ‖J x‖ = traceTwoNorm τ x) {μ : Measure P}
       (c : P → B) (a : P → unitary B) {r : ℝ} (hr : r < 1)
       (hnear : ∀ p, ‖c p - 1‖ ≤ r)
       (hpolar : ∀ p, (a p : B) * CFC.abs (c p) = c p)
       (hmeas : AEStronglyMeasurable (fun p => J (c p)) μ) :
       AEStronglyMeasurable (fun p => J (a p : B)) μ := by
   …

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

2. theorem OAI.KadisonKastler.exists_measurable_diagonal_unitary_comparison line 83

   Source documentation

   The diagonal comparison unitary is itself measurable in the trace Hilbert realization, in addition to its exact covariance and norm bound.

   theorem exists_measurable_diagonal_unitary_comparison
       (J : Algebra M →ₗ[ℂ] E) (hJ : ∀ x, ‖J x‖ = traceTwoNorm τ x)
       (hτ : FiniteVectorTrace τ)
       {G D : Type*} [Group G] [Countable G] [MeasurableSpace D] {μ : Measure (D × D)}
       (shift : G → D → D) (W : G → D → unitary (Algebra M))
       (hW : ∀ g t x, (W (g * t) x : Algebra M) =
         (W g x : Algebra M) * (W t (shift g x) : Algebra M))
       (hWmeas : ∀ t, AEStronglyMeasurable
         (fun p : D × D => J ((W t p.1 : Algebra M) * star (W t p.2 : Algebra M))) μ)
       {r : ℝ} (hr0 : 0 ≤ r) (hr : r < 1)
       (hnear : ∀ t x y, ‖(W t x : Algebra M) * star (W t y : Algebra M) - 1‖ ≤ r) :
       ∃ a : D → D → unitary (Algebra M),
   …

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

3. theorem OAI.KadisonKastler.exists_concrete_measurable_diagonal_unitary_comparison line 111

   Source documentation

   In a separably acting finite factor the diagonal comparison field is measurable after evaluation on every vector of the original Hilbert space.

   theorem exists_concrete_measurable_diagonal_unitary_comparison
       {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
       [SeparableSpace H] {M : VonNeumannAlgebra H}
       (hM : Generator.IsII1Factor M.toStarSubalgebra)
       {G D : Type*} [Group G] [Countable G] [MeasurableSpace D] {μ : Measure (D × D)}
       (shift : G → D → D) (W : G → D → unitary (Algebra M))
       (hW : ∀ g t x, (W (g * t) x : Algebra M) =
         (W g x : Algebra M) * (W t (shift g x) : Algebra M))
       (hWmeas : ∀ t, AEStronglyMeasurable (fun p : D × D =>
         concreteTraceEmbedding hM ((W t p.1 : Algebra M) * star (W t p.2 : Algebra M))) μ)
       {r : ℝ} (hr0 : 0 ≤ r) (hr : r < 1)
       (hnear : ∀ t x y, ‖(W t x : Algebra M) * star (W t y : Algebra M) - 1‖ ≤ r) :
   …

   Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.concreteTraceEmbedding