UltrapowerExpectation.lean`

29 declarations, 0 contain sorry, 0 declared as axioms

The actual expectation onto the constant copy

Weak compactness constructs the expectation value inside the original von Neumann algebra. The finite-vector normal trace identifies it by trace pairings. This constructs, rather than assumes, the expectation used in the scalar-recovery weak limit.

def OAI.KadisonKastler.boundedSequenceConst line 24
Source documentation
Constant sequences as a unital star homomorphism.
```
def boundedSequenceConst : B →⋆ₐ[ℂ] BoundedSequence B where
…
```
Mentions: OAI.KadisonKastler.BoundedSequence
theorem OAI.KadisonKastler.boundedSequenceConst_apply line 34
theorem OAI.KadisonKastler.eq_of_trace_left_pairings line 37
Source documentation
A faithful tracial state separates elements by left pairings.
```
theorem eq_of_trace_left_pairings (τ : FaithfulTracialState B) {a b : B}
    (h : ∀ c, τ.toLinearMap (c * a) = τ.toLinearMap (c * b)) : a = b := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState

theorem OAI.KadisonKastler.injective_of_trace_preserving line 45

Source documentation

A trace-preserving star homomorphism out of a faithful tracial algebra is injective.

theorem injective_of_trace_preserving {C : Type*} [CStarAlgebra C]
    (τ : FaithfulTracialState B) (σ : FaithfulTracialState C) (φ : B →⋆ₐ[ℂ] C)
    (hφ : ∀ x, σ.toLinearMap (φ x) = τ.toLinearMap x) : Function.Injective φ := by
…

Mentions: OAI.KadisonKastler.FaithfulTracialState

theorem OAI.KadisonKastler.FiniteVectorTrace.exists_weak_limit_pairings line 60

Source documentation

Bounded sequences admit a concrete weak limit with all trace pairings, using the finite-vector formula.

theorem FiniteVectorTrace.exists_weak_limit_pairings
    {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
    {M : VonNeumannAlgebra H} {τ : FaithfulTracialState (Algebra M)}
    (hτ : FiniteVectorTrace τ) (ω : Ultrafilter ℕ) (s : BoundedSequence (Algebra M)) :
    ∃ a : Algebra M, ∀ b : Algebra M,
      Tendsto (fun j => τ.toLinearMap (b * s j)) (ω : Filter ℕ)
        (𝓝 (τ.toLinearMap (b * a))) := by
…

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

structure OAI.KadisonKastler.TraceQuotientMap line 81
Source documentation
The trace formula and quotient map furnished by a tracial ultrapower. The target trace is an explicit parameter so its construction stays separate from the elementary expectation proofs.
```
structure TraceQuotientMap {C : Type*} [CStarAlgebra C]
    (τ : FaithfulTracialState B) (σ : FaithfulTracialState C) (ω : Ultrafilter ℕ) where
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState

theorem OAI.KadisonKastler.TraceQuotientMap.traceTwoNorm_sq_limit line 89

Source documentation

The quotient trace formula passes to squared tracial two-norms.

theorem TraceQuotientMap.traceTwoNorm_sq_limit
    {A C : Type*} [CStarAlgebra A] [CStarAlgebra C]
    {τA : FaithfulTracialState A} {τC : FaithfulTracialState C} {ω : Ultrafilter ℕ}
    (Q : TraceQuotientMap τA τC ω) (x : BoundedSequence A) :
    Tendsto (fun j => traceTwoNorm τA (x j) ^ 2) (ω : Filter ℕ)
      (𝓝 (traceTwoNorm τC (Q.quotient x) ^ 2)) := by
…

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

theorem OAI.KadisonKastler.TraceQuotientMap.isTraceQuotient line 100

Source documentation

Faithfulness identifies the exact two-null kernel of any such quotient.

theorem TraceQuotientMap.isTraceQuotient
    {A C : Type*} [CStarAlgebra A] [CStarAlgebra C]
    {τA : FaithfulTracialState A} {τC : FaithfulTracialState C} {ω : Ultrafilter ℕ}
    (Q : TraceQuotientMap τA τC ω) : IsTraceQuotient τA (ω : Filter ℕ) Q.quotient := by
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.TraceQuotientMap, OAI.KadisonKastler.IsTraceQuotient

def OAI.KadisonKastler.TraceQuotientMap.constant line 133
Source documentation
The actual constant copy of the original factor.
```
def constant : Algebra M →⋆ₐ[ℂ] C := D.quotient.comp boundedSequenceConst
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.boundedSequenceConst
theorem OAI.KadisonKastler.TraceQuotientMap.trace_constant line 136
Source documentation
The constant copy preserves the constructed normalized trace.
```
theorem trace_constant (b : Algebra M) :
    σ.toLinearMap (D.constant (M := M) b) = τ.toLinearMap b := by
…
```
Mentions: OAI.KadisonKastler.Algebra
theorem OAI.KadisonKastler.TraceQuotientMap.constant_injective line 141
Source documentation
Faithfulness of the constant embedding follows from its trace formula.
```
theorem constant_injective : Function.Injective (D.constant (M := M)) :=
…
```
theorem OAI.KadisonKastler.TraceQuotientMap.trace_pairing_limit line 145
Source documentation
Coordinate left pairings have the expected ultrapower trace limit.
```
theorem trace_pairing_limit (s : BoundedSequence (Algebra M)) (b : Algebra M) :
    Tendsto (fun j => τ.toLinearMap (b * s j)) (ω : Filter ℕ)
      (𝓝 (σ.toLinearMap (D.constant (M := M) b * D.quotient s))) := by
…
```
Mentions: OAI.KadisonKastler.BoundedSequence, OAI.KadisonKastler.Algebra
theorem OAI.KadisonKastler.TraceQuotientMap.exists_expectation_value line 161
Source documentation
Every ultrapower element has a representative of its trace pairings in the original concrete factor.
```
theorem exists_expectation_value (x : C) :
    ∃ a : Algebra M, ∀ b : Algebra M,
      τ.toLinearMap (b * a) =
        σ.toLinearMap (D.constant (M := M) b * x) := by
…
```
Mentions: OAI.KadisonKastler.Algebra
def OAI.KadisonKastler.TraceQuotientMap.expectationValue line 173
theorem OAI.KadisonKastler.TraceQuotientMap.expectationValue_pairing line 176
def OAI.KadisonKastler.TraceQuotientMap.expectation line 182
Source documentation
The trace-preserving expectation, constructed by weak compactness.
```
def expectation : C →ₗ[ℂ] Algebra M where
…
```
Mentions: OAI.KadisonKastler.Algebra
theorem OAI.KadisonKastler.TraceQuotientMap.expectation_pairing line 210
Source documentation
The expectation's defining trace-pairing identity.
```
theorem expectation_pairing (x : C) (b : Algebra M) :
    τ.toLinearMap (b * D.expectation (M := M) hτ x) =
…
```
Mentions: OAI.KadisonKastler.Algebra
theorem OAI.KadisonKastler.TraceQuotientMap.expectation_constant line 216
Source documentation
The constructed expectation fixes the original algebra.
```
theorem expectation_constant (a : Algebra M) : D.expectation (M := M) hτ (D.constant (M := M) a) = a := by
…
```
Mentions: OAI.KadisonKastler.Algebra
theorem OAI.KadisonKastler.TraceQuotientMap.trace_expectation line 222
Source documentation
The expectation preserves the trace.
```
theorem trace_expectation (x : C) :
    τ.toLinearMap (D.expectation (M := M) hτ x) = σ.toLinearMap x := by
…
```
def OAI.KadisonKastler.TraceQuotientMap.baseExpectation line 228
Source documentation
In the ultrapower, the expectation is a linear projection onto the range of the constant embedding.
```
def baseExpectation : C →ₗ[ℂ] C :=
…
```
theorem OAI.KadisonKastler.TraceQuotientMap.baseExpectation_mem line 231
theorem OAI.KadisonKastler.TraceQuotientMap.baseExpectation_pairing line 234
theorem OAI.KadisonKastler.TraceQuotientMap.weak_limit_expectation line 243
Source documentation
Each bounded representative converges weakly to the constructed expectation in the original representation.
```
theorem weak_limit_expectation (s : BoundedSequence (Algebra M)) :
    ∀ ξ η : H, Tendsto (fun j => inner ℂ η ((s j : H →L[ℂ] H) ξ))
      (ω : Filter ℕ) (𝓝 (inner ℂ η ((D.expectation (M := M) hτ (D.quotient s) : H →L[ℂ] H) ξ))) := by
…
```
Mentions: OAI.KadisonKastler.BoundedSequence, OAI.KadisonKastler.Algebra
theorem OAI.KadisonKastler.TraceQuotientMap.expectation_bimodule line 256
Source documentation
The expectation respects multiplication by the original algebra on both sides.
```
theorem expectation_bimodule (a b : Algebra M) (x : C) :
    D.expectation (M := M) hτ (D.constant (M := M) a * x * D.constant (M := M) b) = a * D.expectation (M := M) hτ x * b := by
…
```
Mentions: OAI.KadisonKastler.Algebra
theorem OAI.KadisonKastler.TraceQuotientMap.norm_expectation_quotient_le line 273
Source documentation
Every coordinate bound passes to the expectation.
```
theorem norm_expectation_quotient_le (s : BoundedSequence (Algebra M))
    {C : ℝ} (hC : 0 ≤ C) (hs : ∀ j, ‖s j‖ ≤ C) :
    ‖D.expectation (M := M) hτ (D.quotient s)‖ ≤ C := by
…
```
Mentions: OAI.KadisonKastler.BoundedSequence, OAI.KadisonKastler.Algebra
theorem OAI.KadisonKastler.TraceQuotientMap.norm_expectation_le line 289
Source documentation
Quotient clipping upgrades the coordinate bound to contractivity in the actual quotient operator norm.
```
theorem norm_expectation_le (x : C) : ‖D.expectation (M := M) hτ x‖ ≤ ‖x‖ := by
…
```
def OAI.KadisonKastler.TraceQuotientMap.expectationCLM line 310
Source documentation
The constructed expectation is a bounded linear map.
```
def expectationCLM : C →L[ℂ] Algebra M :=
…
```
Mentions: OAI.KadisonKastler.Algebra
def OAI.KadisonKastler.TraceQuotientMap.baseExpectationCLM line 314
Source documentation
The projection onto the constant copy is norm continuous.
```
def baseExpectationCLM : C →L[ℂ] C :=
…
```
def OAI.KadisonKastler.TracialUltrapower.traceQuotient line 330
Source documentation
The published ultrapower supplies every premise of the constructed expectation, with its canonical trace.
```
def traceQuotient (Q : TracialUltrapower τ ω) : TraceQuotientMap τ Q.trace ω where
…
```
Mentions: OAI.KadisonKastler.TracialUltrapower, OAI.KadisonKastler.TraceQuotientMap