BoundedSequence.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Bounded sequences, spectral clipping and trace-to-strong transfer

The sequence algebra is the ordinary C*-algebra of bounded functions on the discrete natural numbers. Evaluation commutes with the spectral cutoff. A trace quotient therefore kills the discarded part as soon as the quotient norm satisfies the desired cutoff bound.

abbrev OAI.KadisonKastler.BoundedSequence line 24
instance OAI.KadisonKastler.boundedSequenceCStarAlgebra line 26
def OAI.KadisonKastler.boundedSequenceEval line 29
theorem OAI.KadisonKastler.boundedSequenceEval_apply line 40
theorem OAI.KadisonKastler.spectralClip_sequence_apply line 53
Source documentation
The algebraic spectral clip evaluates to the clip of each coordinate.
```
theorem spectralClip_sequence_apply {β : ℝ} (hβ : 0 < β)
    (x : BoundedSequence B) (j : ℕ) :
    spectralClip β x j = spectralClip β (x j) :=
…
```
Mentions: OAI.KadisonKastler.BoundedSequence, OAI.KadisonKastler.spectralClip
theorem OAI.KadisonKastler.sequence_discard_quotient_zero line 61
Source documentation
Clipping a bounded sequence at a bound for its quotient norm changes it by an element of the quotient kernel.
```
theorem sequence_discard_quotient_zero (π : BoundedSequence B →⋆ₐ[ℂ] Q)
    {β : ℝ} (hβ : 0 < β) (x : BoundedSequence B) (hx : ‖π x‖ ≤ β) :
    π (x - spectralClip β x) = 0 :=
…
```
Mentions: OAI.KadisonKastler.BoundedSequence, OAI.KadisonKastler.spectralClip
def OAI.KadisonKastler.traceTwoNorm line 69
Source documentation
The tracial two-seminorm, on the faithful tracial algebra in use.
```
def traceTwoNorm {B : Type*} [CStarAlgebra B] (τ : FaithfulTracialState B) (x : B) : ℝ :=
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState
def OAI.KadisonKastler.TraceStrongContinuous line 75
Source documentation
Continuity from the tracial two-norm to the strong topology on each norm-bounded ball. This is the exact normal-representation property used by the clipping argument; no existence assertion is made here.
```
def TraceStrongContinuous {B H : Type*} [CStarAlgebra B]
    [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
    (τ : FaithfulTracialState B) (ρ : B →⋆ₐ[ℂ] (H →L[ℂ] H)) : Prop :=
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState

theorem OAI.KadisonKastler.TraceStrongContinuous.tendsto line 83

Source documentation

The continuity property transfers two-small bounded sequences to strongly small sequences in the given representation.

theorem TraceStrongContinuous.tendsto {B H J : Type*} [CStarAlgebra B]
    [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
    {τ : FaithfulTracialState B} {ρ : B →⋆ₐ[ℂ] (H →L[ℂ] H)}
    (hρ : TraceStrongContinuous τ ρ) (l : Filter J) (x : J → B)
    {C : ℝ} (hC : 0 ≤ C) (hx : ∀ j, ‖x j‖ ≤ C)
    (h2 : Tendsto (fun j => traceTwoNorm τ (x j)) l (𝓝 0)) (z : H) :
    Tendsto (fun j => ρ (x j) z) l (𝓝 0) := by
…

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

def OAI.KadisonKastler.IsTraceQuotient line 97
Source documentation
The precise quotient-kernel condition needed for discarded sequences.
```
def IsTraceQuotient {B Q : Type*} [CStarAlgebra B] [CStarAlgebra Q]
    (τ : FaithfulTracialState B) (l : Filter ℕ)
    (π : BoundedSequence B →⋆ₐ[ℂ] Q) : Prop :=
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.BoundedSequence

theorem OAI.KadisonKastler.IsTraceQuotient.strong_zero line 104

Source documentation

A zero quotient class acts strongly as zero in every representation with the trace continuity property.

theorem IsTraceQuotient.strong_zero {B Q H : Type*} [CStarAlgebra B] [CStarAlgebra Q]
    [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
    {τ : FaithfulTracialState B} {l : Filter ℕ}
    {π : BoundedSequence B →⋆ₐ[ℂ] Q} (hπ : IsTraceQuotient τ l π)
    {ρ : B →⋆ₐ[ℂ] (H →L[ℂ] H)} (hρ : TraceStrongContinuous τ ρ)
    (x : BoundedSequence B) (hx : π x = 0) (z : H) :
    Tendsto (fun j => ρ (x j) z) l (𝓝 0) :=
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.BoundedSequence, OAI.KadisonKastler.IsTraceQuotient, OAI.KadisonKastler.TraceStrongContinuous

theorem OAI.KadisonKastler.IsTraceQuotient.spectralDiscard_strong_zero line 125

Source documentation

Quotient clipping gives the actual strong error on every fixed vector.

theorem IsTraceQuotient.spectralDiscard_strong_zero
    {τ : FaithfulTracialState B} {l : Filter ℕ}
    {π : BoundedSequence B →⋆ₐ[ℂ] Q} (hπ : IsTraceQuotient τ l π)
    {ρ : B →⋆ₐ[ℂ] (H →L[ℂ] H)} (hρ : TraceStrongContinuous τ ρ)
    {β : ℝ} (hβ : 0 < β) (x : BoundedSequence B) (hx : ‖π x‖ ≤ β) (z : H) :
    Tendsto (fun j => ρ (x j - spectralClip β (x j)) z) l (𝓝 0) := by
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.BoundedSequence, OAI.KadisonKastler.IsTraceQuotient, OAI.KadisonKastler.TraceStrongContinuous, OAI.KadisonKastler.spectralClip

theorem OAI.KadisonKastler.IsTraceQuotient.spectralDiscard_mul_strong_zero line 138
Source documentation
Right multiplication by any bounded sequence keeps the discarded part in the kernel. This is the moving-vector transfer needed before estimating the remaining unitary commutator.
```
theorem IsTraceQuotient.spectralDiscard_mul_strong_zero
    {τ : FaithfulTracialState B} {l : Filter ℕ}
    {π : BoundedSequence B →⋆ₐ[ℂ] Q} (hπ : IsTraceQuotient τ l π)
    {ρ : B →⋆ₐ[ℂ] (H →L[ℂ] H)} (hρ : TraceStrongContinuous τ ρ)
    {β : ℝ} (hβ : 0 < β) (x v : BoundedSequence B) (hx : ‖π x‖ ≤ β) (z : H) :
    Tendsto (fun j => ρ (x j - spectralClip β (x j)) (ρ (v j) z)) l (𝓝 0) := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.BoundedSequence, OAI.KadisonKastler.IsTraceQuotient, OAI.KadisonKastler.TraceStrongContinuous, OAI.KadisonKastler.spectralClip