Documentation

TauCeti.Topology.ContinuousMap.ZeroAtInfty.Diagonal

Diagonal operators on the model space C₀(I, R) #

Let R be a seminormed ring and I a discrete index type. A bounded family d : I →ᵇ R acts on C₀(I, R) coordinatewise, x ↦ (x i * d i)ᵢ: the product of a family tending to zero with a bounded family tends to zero. This is the diagonal operator ZeroAtInftyContinuousMap.diagonalCLM d, a continuous linear map of norm at most ‖d‖, with equality over Tate scalars. The scalar d i multiplies on the right, so that the map is linear over a noncommutative R; its matrix is Matrix.diagonal d (ZeroAtInftyContinuousMap.matrixCoeff_diagonalCLM).

Diagonal operators are the basic test cases for compactness of operators between model spaces: the identity is the diagonal operator of the constant family 1, while in orthonormal bases of rescaled monomials the inclusion of power series restricted at a larger radius into those restricted at a smaller one is a diagonal operator with geometrically decaying entries. Their row compactness is treated in TauCeti.Analysis.Normed.Operator.RowCompact.Diagonal.

Main definitions #

Main results #

References #

source
noncomputable def ZeroAtInftyContinuousMap.diagonalCLM {I : Type u_1} {R : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [SeminormedRing R] (d : BoundedContinuousFunction I R) :
ZeroAtInftyContinuousMap I R →L[R] ZeroAtInftyContinuousMap I R

The diagonal operator of a bounded family d : I →ᵇ R: the continuous linear map of C₀(I, R) multiplying the i-th coordinate on the right by d i. Its matrix is Matrix.diagonal d (ZeroAtInftyContinuousMap.matrixCoeff_diagonalCLM).

Instances For
    source
    @[simp]
    theorem ZeroAtInftyContinuousMap.diagonalCLM_apply {I : Type u_1} {R : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [SeminormedRing R] (d : BoundedContinuousFunction I R) (x : ZeroAtInftyContinuousMap I R) (i : I) :
    ((diagonalCLM d) x) i = x i * d i
    source
    theorem ZeroAtInftyContinuousMap.norm_diagonalCLM_apply_le {I : Type u_1} {R : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [SeminormedRing R] (d : BoundedContinuousFunction I R) (x : ZeroAtInftyContinuousMap I R) :
    ‖(diagonalCLM d) x‖ ≤ ‖d‖ * ‖x‖

    The diagonal operator of d multiplies norms by at most ‖d‖.

    source
    theorem ZeroAtInftyContinuousMap.ringOpNorm_diagonalCLM_le {I : Type u_1} {R : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [SeminormedRing R] (d : BoundedContinuousFunction I R) :
    ‖diagonalCLM d‖ ≤ ‖d‖

    The diagonal operator of d has operator norm at most ‖d‖.

    source
    @[simp]
    theorem ZeroAtInftyContinuousMap.diagonalCLM_single {I : Type u_1} {R : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [SeminormedRing R] [DecidableEq I] (d : BoundedContinuousFunction I R) (i : I) (b : R) :
    (diagonalCLM d) (single i b) = single i (b * d i)
    source
    @[simp]
    theorem ZeroAtInftyContinuousMap.matrixCoeff_diagonalCLM {I : Type u_1} {R : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [SeminormedRing R] [DecidableEq I] (d : BoundedContinuousFunction I R) :
    (diagonalCLM d).matrixCoeff = Matrix.diagonal ⇑d
    source
    @[simp]
    theorem ZeroAtInftyContinuousMap.ringOpNorm_diagonalCLM {I : Type u_1} {R : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [SeminormedRing R] [TauCeti.NormedRing.IsTate R] (d : BoundedContinuousFunction I R) :
    ‖diagonalCLM d‖ = ‖d‖

    Over Tate scalars, the diagonal operator of d has operator norm exactly ‖d‖.

    source
    @[simp]
    theorem ZeroAtInftyContinuousMap.diagonalCLM_zero {I : Type u_1} {R : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [SeminormedRing R] :
    diagonalCLM 0 = 0
    source
    @[simp]
    theorem ZeroAtInftyContinuousMap.diagonalCLM_one {I : Type u_1} {R : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [SeminormedRing R] :
    diagonalCLM 1 = 1
    source
    @[simp]
    theorem ZeroAtInftyContinuousMap.diagonalCLM_add {I : Type u_1} {R : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [SeminormedRing R] (d e : BoundedContinuousFunction I R) :
    diagonalCLM (d + e) = diagonalCLM d + diagonalCLM e
    source
    @[simp]
    theorem ZeroAtInftyContinuousMap.diagonalCLM_neg {I : Type u_1} {R : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [SeminormedRing R] (d : BoundedContinuousFunction I R) :
    diagonalCLM (-d) = -diagonalCLM d
    source
    @[simp]
    theorem ZeroAtInftyContinuousMap.diagonalCLM_sub {I : Type u_1} {R : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [SeminormedRing R] (d e : BoundedContinuousFunction I R) :
    diagonalCLM (d - e) = diagonalCLM d - diagonalCLM e
    source
    @[simp]
    theorem ZeroAtInftyContinuousMap.diagonalCLM_mul {I : Type u_1} {R : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [SeminormedRing R] (d e : BoundedContinuousFunction I R) :
    diagonalCLM (d * e) = diagonalCLM e * diagonalCLM d

    The diagonal operator of a product is the composite of the diagonal operators, in the order dictated by multiplication on the right.

    source
    theorem ZeroAtInftyContinuousMap.not_isFiniteRank_diagonalCLM {I : Type u_1} {R : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [SeminormedRing R] [StrongRankCondition R] {d : BoundedContinuousFunction I R} (hd : {i : I | IsUnit (d i)}.Infinite) :
    ¬(↑(diagonalCLM d)).IsFiniteRank

    Diagonal operators of infinite rank: over a ring with the strong rank condition, a diagonal operator whose entries are units at infinitely many indices does not have finite rank.