QuotientRepresentation.lean`

57 declarations, 0 contain sorry, 0 declared as axioms

Complete operator-norm bounded sequences and their contractive map to the actual quotient trace Hilbert space. This map is not asserted injective.

abbrev OAI.Generator.Tracial.Sequences line 23
instance OAI.Generator.Tracial.sequencesIsTopologicalRing line 25
def OAI.Generator.Tracial.boundedMap line 29
Source documentation
Forget continuity (automatic on the discrete index set) and retain boundedness.
```
def boundedMap : Sequences M →⋆ₐ[ℂ] Bounded M where
…
```
Mentions: OAI.Generator.Tracial.Sequences
theorem OAI.Generator.Tracial.boundedMap_surjective line 38
def OAI.Generator.Tracial.sequenceQuotient line 47
Source documentation
The actual star-algebra quotient map on complete bounded sequences.
```
def sequenceQuotient : Sequences M →⋆ₐ[ℂ] Q τ ω :=
…
```
Mentions: OAI.Generator.Tracial.Sequences, OAI.Generator.Tracial.Q
theorem OAI.Generator.Tracial.sequenceQuotient_surjective line 50
theorem OAI.Generator.Tracial.quotient_norm_tendsto line 56
theorem OAI.Generator.Tracial.sequence_norm_tendsto line 62
theorem OAI.Generator.Tracial.sequenceQuotient_norm_le line 67
def OAI.Generator.Tracial.sequenceInclusion line 73
Source documentation
The continuous Hilbert realization used by the analytic remainder theorem.
```
def sequenceInclusion : Sequences M →L[ℂ] L2 τ ω :=
…
```
Mentions: OAI.Generator.Tracial.Sequences, OAI.Generator.Tracial.L2
theorem OAI.Generator.Tracial.sequenceInclusion_apply line 84
theorem OAI.Generator.Tracial.sequenceInclusion_norm_le line 87
theorem OAI.Generator.Tracial.sequence_inner_tendsto line 92
Source documentation
Literal ultralimit inner product, including the complex orientation.
```
theorem sequence_inner_tendsto (a b : Sequences M) :
    Tendsto (fun n => τ.trace (star (a n)*b n)) (ω : Filter ℕ)
      (𝓝 (inner ℂ (sequenceInclusion τ ω a) (sequenceInclusion τ ω b))) := by
…
```
Mentions: OAI.Generator.Tracial.Sequences, OAI.Generator.Tracial.sequenceInclusion
theorem OAI.Generator.Tracial.sequenceInclusion_eq_zero_iff line 99
Source documentation
The kernel consists exactly of trace-null bounded sequences.
```
theorem sequenceInclusion_eq_zero_iff (a : Sequences M) :
    sequenceInclusion τ ω a = 0 ↔ Tendsto (fun n => τ.norm₂ (a n)) (ω : Filter ℕ) (𝓝 0) := by
…
```
Mentions: OAI.Generator.Tracial.Sequences, OAI.Generator.Tracial.sequenceInclusion
def OAI.Generator.Tracial.constantSequence line 118
def OAI.Generator.Tracial.constantQuotient line 127
theorem OAI.Generator.Tracial.constantQuotient_trace line 130
theorem OAI.Generator.Tracial.constantQuotient_norm line 135
theorem OAI.Generator.Tracial.constantQuotient_injective line 140
Source documentation
No nonzero constant element is killed by the tracial quotient ideal.
```
theorem constantQuotient_injective : Function.Injective (constantQuotient τ ω) := by
…
```
Mentions: OAI.Generator.Tracial.constantQuotient
theorem OAI.Generator.Tracial.constantQuotient_inner line 146
theorem OAI.Generator.Tracial.sequence_mul_norm_le line 163
def OAI.Generator.Tracial.leftOnQuotient line 174
theorem OAI.Generator.Tracial.leftOnQuotient_apply line 178
theorem OAI.Generator.Tracial.inclusion_denseRange line 181
def OAI.Generator.Tracial.leftAction line 185
Source documentation
Bounded left multiplication extended to the actual Hilbert completion.
```
def leftAction (a : Sequences M) : L2 τ ω →L[ℂ] L2 τ ω :=
…
```
Mentions: OAI.Generator.Tracial.Sequences, OAI.Generator.Tracial.L2
theorem OAI.Generator.Tracial.leftAction_inclusion line 189
theorem OAI.Generator.Tracial.leftAction_coe line 196
theorem OAI.Generator.Tracial.leftAction_norm_le line 200
theorem OAI.Generator.Tracial.leftAction_one line 207
theorem OAI.Generator.Tracial.leftAction_mul line 213
theorem OAI.Generator.Tracial.leftAction_add line 220
theorem OAI.Generator.Tracial.completionT2Space line 227
theorem OAI.Generator.Tracial.leftAction_smul line 230
theorem OAI.Generator.Tracial.leftAction_zero line 247
theorem OAI.Generator.Tracial.leftAction_star line 253
def OAI.Generator.Tracial.sequenceAction line 264
Source documentation
A concrete star-algebra action, constructed from the trace quotient.
```
def sequenceAction : Sequences M →⋆ₐ[ℂ] (L2 τ ω →L[ℂ] L2 τ ω) where
…
```
Mentions: OAI.Generator.Tracial.Sequences, OAI.Generator.Tracial.L2
theorem OAI.Generator.Tracial.leftAction_eq_iff line 281
Source documentation
Equality of operators is precisely equality in the tracial quotient.
```
theorem leftAction_eq_iff (a b : Sequences M) :
    leftAction τ ω a = leftAction τ ω b ↔ sequenceQuotient τ ω a = sequenceQuotient τ ω b := by
…
```
Mentions: OAI.Generator.Tracial.Sequences, OAI.Generator.Tracial.leftAction, OAI.Generator.Tracial.sequenceQuotient

def OAI.Generator.Tracial.descendStarAlgHom line 307

Source documentation

Descend a proved compatible map through a surjective star-algebra map.

def descendStarAlgHom (q : A →⋆ₐ[ℂ] B) (hq : Function.Surjective q)
    (f : A →⋆ₐ[ℂ] C) (g : B → C) (hg : ∀ a, g (q a) = f a) : B →⋆ₐ[ℂ] C where
…

def OAI.Generator.Tracial.quotientOperator line 332
theorem OAI.Generator.Tracial.quotientOperator_mk line 335
theorem OAI.Generator.Tracial.sequenceAction_apply line 340
def OAI.Generator.Tracial.quotientRepresentation line 345
Source documentation
The quotient itself, rather than a chosen representative algebra, acts faithfully by bounded Hilbert-space operators.
```
def quotientRepresentation : Q τ ω →⋆ₐ[ℂ] (L2 τ ω →L[ℂ] L2 τ ω) :=
…
```
Mentions: OAI.Generator.Tracial.Q, OAI.Generator.Tracial.L2
theorem OAI.Generator.Tracial.quotientRepresentation_inclusion line 351
theorem OAI.Generator.Tracial.quotientRepresentation_separating line 361
Source documentation
The identity vector separates all represented quotient elements.
```
theorem quotientRepresentation_separating (a : Q τ ω)
    (h : quotientRepresentation τ ω a (inclusion τ ω 1) = 0) : a = 0 := by
…
```
Mentions: OAI.Generator.Tracial.Q, OAI.Generator.Tracial.quotientRepresentation, OAI.Generator.Tracial.inclusion
theorem OAI.Generator.Tracial.quotientRepresentation_injective line 367
theorem OAI.Generator.Tracial.quotientRepresentation_trace line 374
Source documentation
The represented vector trace is precisely the original ultralimit trace.
```
theorem quotientRepresentation_trace (a : Q τ ω) :
    inner ℂ (inclusion τ ω 1) (quotientRepresentation τ ω a (inclusion τ ω 1)) =
      quotientTrace τ ω a := by
…
```
Mentions: OAI.Generator.Tracial.Q, OAI.Generator.Tracial.inclusion, OAI.Generator.Tracial.quotientRepresentation
def OAI.Generator.Tracial.quotientL2AddCommMonoid line 387
def OAI.Generator.Tracial.quotientL2AddCommGroup line 390
def OAI.Generator.Tracial.quotientOperatorSemiring line 395
def OAI.Generator.Tracial.quotientOperatorNonAssocSemiring line 398
def OAI.Generator.Tracial.quotientOperatorAlgebra line 403
theorem OAI.Generator.Tracial.quotientOperatorSemitopology line 408
def OAI.Generator.Tracial.sequenceEval line 420
theorem OAI.Generator.Tracial.sequence_exp_apply line 429
Source documentation
Operator-norm exponentials of bounded sequences evaluate coordinatewise.
```
theorem sequence_exp_apply (a : Sequences M) (n : ℕ) :
    (NormedSpace.exp a) n = NormedSpace.exp (a n) :=
…
```
Mentions: OAI.Generator.Tracial.Sequences
theorem OAI.Generator.Tracial.sequence_exp_product_apply line 434

theorem OAI.Generator.Tracial.select_coordinate line 445

Source documentation

Both limits hold at one coordinate, with the same positive tolerance.

theorem select_coordinate (a ξ b : Sequences M) (ε : ℝ) (hε : 0 < ε) :
    ∃ n : ℕ, τ.norm₂ (a n) < ‖sequenceQuotient τ ω a‖ + ε ∧
      ‖τ.trace (star (ξ n)*b n) -
        inner ℂ (sequenceInclusion τ ω ξ) (sequenceInclusion τ ω b)‖ < ε := by
…

Mentions: OAI.Generator.Tracial.Sequences, OAI.Generator.Tracial.sequenceQuotient, OAI.Generator.Tracial.sequenceInclusion

theorem OAI.Generator.Tracial.select_coordinate_with_bounds line 458

Source documentation

Source-facing error transfer: a common representative index preserves a quotient size bound and a complex trace-correlation bound, up to epsilon.

theorem select_coordinate_with_bounds (a ξ b : Sequences M)
    (d r ε : ℝ) (target : ℂ) (hε : 0 < ε)
    (ha : ‖sequenceQuotient τ ω a‖ ≤ d)
    (hb : ‖inner ℂ (sequenceInclusion τ ω ξ) (sequenceInclusion τ ω b) - target‖ ≤ r) :
    ∃ n : ℕ, τ.norm₂ (a n) < d + ε ∧ ‖τ.trace (star (ξ n)*b n)-target‖ < r+ε := by
…

Mentions: OAI.Generator.Tracial.Sequences, OAI.Generator.Tracial.sequenceQuotient, OAI.Generator.Tracial.sequenceInclusion