BoundaryDiagonal.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Pointwise diagonal comparison in a finite algebra

The least-norm argument is carried out in a supplied faithful tracial Hilbert realization. Bounded completeness of the concrete finite algebra keeps Hilbert limits in the operator algebra. No measurable selection or existence of a boundary space is asserted here.

theorem OAI.KadisonKastler.eq_of_convex_least_norm line 29

Source documentation

The least-norm vector of a convex set is unique.

theorem eq_of_convex_least_norm {K : Set E} (hK : Convex ℝ K)
    {x y : E} (hx : x ∈ K) (hy : y ∈ K)
    (hxm : ∀ z ∈ K, ‖x‖ ≤ ‖z‖) (hym : ∀ z ∈ K, ‖y‖ ≤ ‖z‖) : x = y := by
…

theorem OAI.KadisonKastler.exists_unique_least_norm line 46

Source documentation

Every nonempty closed convex subset of a Hilbert space has a unique least-norm vector.

theorem exists_unique_least_norm [CompleteSpace E] {K : Set E}
    (hne : K.Nonempty) (hclosed : IsClosed K) (hconvex : Convex ℝ K) :
    ∃! x : E, x ∈ K ∧ ∀ y ∈ K, ‖x‖ ≤ ‖y‖ := by
…

theorem OAI.KadisonKastler.traceHilbert_injective line 71
Source documentation
Faithfulness makes a tracial Hilbert realization injective.
```
theorem traceHilbert_injective : Function.Injective J := by
…
```
theorem OAI.KadisonKastler.FiniteVectorTrace.isClosed_traceHilbert_ball line 80
Source documentation
Operator closed balls have closed images in a faithful tracial Hilbert realization, by concrete bounded two-norm completeness.
```
theorem FiniteVectorTrace.isClosed_traceHilbert_ball (hτ : FiniteVectorTrace τ)
    (a : Algebra M) {r : ℝ} (hr : 0 ≤ r) :
    IsClosed (J '' Metric.closedBall a r) := by
…
```
Mentions: OAI.KadisonKastler.FiniteVectorTrace, OAI.KadisonKastler.Algebra
def OAI.KadisonKastler.diagonalTraceHull line 118
Source documentation
Closed convex hull in the supplied trace Hilbert space.
```
def diagonalTraceHull (s : Set (Algebra M)) : Set E :=
…
```
Mentions: OAI.KadisonKastler.Algebra
theorem OAI.KadisonKastler.diagonalTraceHull_eq line 122
Source documentation
The definition agrees with the ordinary Hilbert closed convex hull.
```
theorem diagonalTraceHull_eq (s : Set (Algebra M)) :
    diagonalTraceHull J s = closure (convexHull ℝ (J '' s)) := by
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.diagonalTraceHull
theorem OAI.KadisonKastler.diagonalTraceHull_convex line 129
Source documentation
The trace hull is convex.
```
theorem diagonalTraceHull_convex (s : Set (Algebra M)) :
    Convex ℝ (diagonalTraceHull J s) := by
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.diagonalTraceHull
theorem OAI.KadisonKastler.traceHull_mem_ball line 137
Source documentation
Bounds on every generator hold throughout the trace Hilbert hull, as actual operator-norm bounds on an element of the algebra.
```
theorem traceHull_mem_ball (hτ : FiniteVectorTrace τ) {s : Set (Algebra M)}
    (a : Algebra M) {r : ℝ} (hr : 0 ≤ r)
    (hs : ∀ x ∈ s, ‖x - a‖ ≤ r) {z : E} (hz : z ∈ diagonalTraceHull J s) :
    ∃ b : Algebra M, J b = z ∧ ‖b - a‖ ≤ r := by
…
```
Mentions: OAI.KadisonKastler.FiniteVectorTrace, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.diagonalTraceHull

theorem OAI.KadisonKastler.exists_unique_diagonal_least line 153

Source documentation

A nonempty family of contractions near one has an actual unique least-two-norm operator in its trace Hilbert closed convex hull.

theorem exists_unique_diagonal_least [CompleteSpace E]
    (hτ : FiniteVectorTrace τ) {s : Set (Algebra M)} (hsne : s.Nonempty)
    {r : ℝ} (hr : 0 ≤ r) (hs1 : ∀ x ∈ s, ‖x‖ ≤ 1)
    (hsr : ∀ x ∈ s, ‖x - 1‖ ≤ r) :
    ∃! b : Algebra M, J b ∈ diagonalTraceHull J s ∧ ‖b‖ ≤ 1 ∧ ‖b - 1‖ ≤ r ∧
      ∀ z ∈ diagonalTraceHull J s, ‖J b‖ ≤ ‖z‖ := by
…

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

theorem OAI.KadisonKastler.traceHull_map line 178
Source documentation
Trace-isometric linear maps carry trace convex hulls into the hull of any containing image of the generators.
```
theorem traceHull_map (F : Algebra M →ₗ[ℂ] Algebra M)
    (hF : ∀ x, traceTwoNorm τ (F x) = traceTwoNorm τ x)
    {s t : Set (Algebra M)} (himage : F '' s ⊆ t)
    {b : Algebra M} (hb : J b ∈ diagonalTraceHull J s) :
    J (F b) ∈ diagonalTraceHull J t := by
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.traceTwoNorm, OAI.KadisonKastler.diagonalTraceHull

theorem OAI.KadisonKastler.diagonal_least_covariance line 202

Source documentation

Least vectors transform exactly under left and right unitary actions, provided these actions identify the two generating sets.

theorem diagonal_least_covariance (u v : unitary (Algebra M))
    {s t : Set (Algebra M)}
    (hforward : ∀ x ∈ s, (u : Algebra M) * x * star (v : Algebra M) ∈ t)
    (hbackward : ∀ y ∈ t, star (u : Algebra M) * y * (v : Algebra M) ∈ s)
    {b c : Algebra M}
    (hb : J b ∈ diagonalTraceHull J s)
    (hc : J c ∈ diagonalTraceHull J t)
    (hbm : ∀ z ∈ diagonalTraceHull J s, ‖J b‖ ≤ ‖z‖)
    (hcm : ∀ z ∈ diagonalTraceHull J t, ‖J c‖ ≤ ‖z‖) :
    c = (u : Algebra M) * b * star (v : Algebra M) := by
…

Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.diagonalTraceHull

def OAI.KadisonKastler.diagonalGenerators line 231
Source documentation
The pointwise diagonal generating family from an exact cocycle.
```
def diagonalGenerators {G D : Type*} (W : G → D → unitary (Algebra M))
    (x y : D) : Set (Algebra M) :=
…
```
Mentions: OAI.KadisonKastler.Algebra

theorem OAI.KadisonKastler.exists_diagonal_least_field_full line 238

Source documentation

The least-norm diagonal field is an actual contraction and satisfies exact covariance under the cocycle. This is a pointwise result.

theorem exists_diagonal_least_field_full [CompleteSpace E]
    (hτ : FiniteVectorTrace τ) {G D : Type*} [Group G]
    (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))
    {r : ℝ} (hr : 0 ≤ r)
    (hnear : ∀ t x y, ‖(W t x : Algebra M) * star (W t y : Algebra M) - 1‖ ≤ r) :
    ∃ c : D → D → Algebra M,
      (∀ x y, J (c x y) ∈ diagonalTraceHull J (diagonalGenerators W x y) ∧
        ‖c x y‖ ≤ 1 ∧ ‖c x y - 1‖ ≤ r ∧
        ∀ z ∈ diagonalTraceHull J (diagonalGenerators W x y), ‖J (c x y)‖ ≤ ‖z‖) ∧
      (∀ g x y, c x y = (W g x : Algebra M) * c (shift g x) (shift g y) *
…

Mentions: OAI.KadisonKastler.FiniteVectorTrace, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.diagonalTraceHull, OAI.KadisonKastler.diagonalGenerators

theorem OAI.KadisonKastler.exists_diagonal_least_field line 298

Source documentation

The pointwise diagonal least field, with only its operator bounds and covariance exposed.

theorem exists_diagonal_least_field [CompleteSpace E]
    (hτ : FiniteVectorTrace τ) {G D : Type*} [Group G]
    (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))
    {r : ℝ} (hr : 0 ≤ r)
    (hnear : ∀ t x y, ‖(W t x : Algebra M) * star (W t y : Algebra M) - 1‖ ≤ r) :
    ∃ c : D → D → Algebra M,
      (∀ x y, ‖c x y‖ ≤ 1 ∧ ‖c x y - 1‖ ≤ r) ∧
      (∀ g x y, c x y = (W g x : Algebra M) * c (shift g x) (shift g y) *
        star (W g y : Algebra M)) := by
…

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

theorem OAI.KadisonKastler.polar_unitary_sandwich line 323

Source documentation

Polar normalization respects left and right multiplication by unitaries, for invertible elements.

theorem polar_unitary_sandwich {b c : B} (hbunit : IsUnit b)
    (u v a d : unitary B) (ha : (a : B) * CFC.abs b = b)
    (hd : (d : B) * CFC.abs c = c)
    (hbc : b = (u : B) * c * star (v : B)) :
    (a : B) = (u : B) * (d : B) * star (v : B) := by
…

theorem OAI.KadisonKastler.exists_diagonal_polar_field line 349

Source documentation

Pointwise polar normalization of a covariant near-identity field.

theorem exists_diagonal_polar_field {D G : Type*} (shift : G → D → D)
    (u : G → D → unitary B) (c : D → D → B)
    {r : ℝ} (hr : r < 1) (hnear : ∀ x y, ‖c x y - 1‖ ≤ r)
    (hcov : ∀ g x y, c x y = (u g x : B) * c (shift g x) (shift g y) *
      star (u g y : B)) :
    ∃ a : D → D → unitary B,
      (∀ x y, ‖(a x y : B) - 1‖ ≤ 2 * r) ∧
      (∀ g x y, (a x y : B) = (u g x : B) * (a (shift g x) (shift g y) : B) *
        star (u g y : B)) := by
…

theorem OAI.KadisonKastler.exists_pointwise_diagonal_comparison line 373

Source documentation

Pointwise diagonal comparison, including the actual least-norm construction and its unitary polar normalization.

theorem exists_pointwise_diagonal_comparison
    {H E : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
    [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E]
    {M : VonNeumannAlgebra H} {τ : FaithfulTracialState (Algebra M)}
    (J : Algebra M →ₗ[ℂ] E) (hJ : ∀ x, ‖J x‖ = traceTwoNorm τ x)
    (hτ : FiniteVectorTrace τ) {G D : Type*} [Group G]
    (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))
    {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.FaithfulTracialState, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.traceTwoNorm, OAI.KadisonKastler.FiniteVectorTrace