Schur test

TheoremPer-row estimate in Schur's test#✓fully proved

The per-row estimate in Schur's test: the i-th coordinate of A x satisfies ‖(A x) i‖² ≤ R * ∑ j, ‖A i j‖ * ‖x j‖² when every row sum of ‖A i j‖ is at most R.

theorem schur_pointwise_sq_le (A : Matrix m n 𝕜) {R : ℝ}
    (hrow : ∀ i, ∑ j, ‖A i j‖ ≤ R) (x : EuclideanSpace 𝕜 n) (i : m) :
    ‖(Matrix.toLpLin 2 2 A x) i‖ ^ 2 ≤ R * ∑ j, ‖A i j‖ * ‖x j‖ ^ 2

Used by 1

Used bySquared-norm estimate in Schur's test

TheoremSquared-norm estimate in Schur's test#✓fully proved

The squared-norm estimate in Schur's test: ‖A x‖² ≤ R * C * ‖x‖² when every row sum of ‖A i j‖ is at most R and every column sum is at most C.

theorem schur_norm_sq_le (A : Matrix m n 𝕜) {R C : ℝ} (hR : 0 ≤ R)
    (hrow : ∀ i, ∑ j, ‖A i j‖ ≤ R) (hcol : ∀ j, ∑ i, ‖A i j‖ ≤ C)
    (x : EuclideanSpace 𝕜 n) :
    ‖Matrix.toLpLin 2 2 A x‖ ^ 2 ≤ R * C * ‖x‖ ^ 2

Uses 1 · Used by 1

Proof usesPer-row estimate in Schur's test

Used byNorm estimate in Schur's test

TheoremNorm estimate in Schur's test#✓fully proved

The unsquared estimate in Schur's test: ‖A x‖ ≤ √(R * C) * ‖x‖.

theorem schur_apply_le (A : Matrix m n 𝕜) {R C : ℝ} (hR : 0 ≤ R) (hC : 0 ≤ C)
    (hrow : ∀ i, ∑ j, ‖A i j‖ ≤ R) (hcol : ∀ j, ∑ i, ‖A i j‖ ≤ C)
    (x : EuclideanSpace 𝕜 n) :
    ‖Matrix.toLpLin 2 2 A x‖ ≤ Real.sqrt (R * C) * ‖x‖

Uses 1 · Used by 1

Proof usesSquared-norm estimate in Schur's test

Used bySchur's test for rectangular Euclidean matrix operators

TheoremSchur's test for rectangular Euclidean matrix operators#✓fully proved

Schur's test for the canonical rectangular Euclidean matrix operator.

theorem norm_toEuclideanLin_le (A : Matrix m n 𝕜) {R C : ℝ}
    (hR : 0 ≤ R) (hC : 0 ≤ C)
    (hrow : ∀ i, ∑ j, ‖A i j‖ ≤ R) (hcol : ∀ j, ∑ i, ‖A i j‖ ≤ C) :
    ‖(Matrix.toEuclideanLin A).toContinuousLinearMap‖ ≤ Real.sqrt (R * C)

Uses 1 · Used by 2

Proof usesNorm estimate in Schur's test

Used bySchur's test for the \(L^2\) operator norm of a matrix · Schur's test for square Euclidean continuous linear maps

TheoremSchur's test for square Euclidean continuous linear maps#✓fully proved

Schur's test for Mathlib's square Euclidean continuous linear map.

theorem norm_toEuclideanCLM_le (A : Matrix n n 𝕜) {R C : ℝ}
    (hR : 0 ≤ R) (hC : 0 ≤ C)
    (hrow : ∀ i, ∑ j, ‖A i j‖ ≤ R) (hcol : ∀ j, ∑ i, ‖A i j‖ ≤ C) :
    ‖Matrix.toEuclideanCLM (n := n) (𝕜 := 𝕜) A‖ ≤ Real.sqrt (R * C)

Uses 1

Proof usesSchur's test for rectangular Euclidean matrix operators

TheoremSchur's test for the \(L^2\) operator norm of a matrix#✓fully proved

Schur's test for the actual scoped L2 operator norm of a matrix.

theorem norm_matrix_l2_le (A : Matrix m n 𝕜) {R C : ℝ}
    (hR : 0 ≤ R) (hC : 0 ≤ C)
    (hrow : ∀ i, ∑ j, ‖A i j‖ ≤ R) (hcol : ∀ j, ∑ i, ‖A i j‖ ≤ C) :
    ‖A‖ ≤ Real.sqrt (R * C)

Uses 1

Proof usesSchur's test for rectangular Euclidean matrix operators

TheoremEntries of a Schur matrix are bounded by the row bound#✓fully proved

A single entry of a Schur matrix is bounded by the row bound.

theorem schurInf_single_le {a : ℕ → ℕ → 𝕜} {R : ℝ}
    (hrow : ∀ i, Summable fun j => ‖a i j‖)
    (hrow_le : ∀ i, ∑' j, ‖a i j‖ ≤ R) (i j : ℕ) : ‖a i j‖ ≤ R

Used by 2

Used byPartial sums of the weighted row series in Schur's test · Summability of the weighted row series in Schur's test

TheoremRow bound of a Schur matrix is nonnegative#✓fully proved

A single row bound: the row bound R is nonnegative.

theorem schurInf_nonneg_of_row {a : ℕ → ℕ → 𝕜} {R : ℝ}
    (hrow_le : ∀ i, ∑' j, ‖a i j‖ ≤ R) : 0 ≤ R

Used by 5

Used byNorm bound for the Schur linear map · Per-row estimate in Schur's test on \(\ell^2\) · Weighted partial sums grouped by the first index · Absolute summability of rows of a Schur matrix · Product summability for the Schur bilinear form

TheoremWeighted Cauchy–Schwarz for one row of a Schur matrix#✓fully proved

Finite weighted Cauchy–Schwarz for one row.

theorem schurInf_finset_cs {a : ℕ → ℕ → 𝕜} (s : Finset ℕ) (x : ℕ → 𝕜) (i : ℕ) :
    (∑ j ∈ s, ‖a i j‖ * ‖x j‖) ^ 2 ≤
      (∑ j ∈ s, ‖a i j‖) * (∑ j ∈ s, ‖a i j‖ * ‖x j‖ ^ 2)

Used by 2

Used byPer-row estimate in Schur's test on \(\ell^2\) · Absolute summability of rows of a Schur matrix

TheoremSummability of the weighted row series in Schur's test#✓fully proved

Weighted summability for one row: ∑' j, ‖a i j‖ * ‖x j‖² converges.

theorem summable_schurInf_weighted {a : ℕ → ℕ → 𝕜} {R : ℝ}
    (hrow : ∀ i, Summable fun j => ‖a i j‖)
    (hrow_le : ∀ i, ∑' j, ‖a i j‖ ≤ R) (x : ℓ²(ℕ, 𝕜)) (i : ℕ) :
    Summable fun j => ‖a i j‖ * ‖x j‖ ^ 2

Uses 2 · Used by 4

Proof usesEntries of a Schur matrix are bounded by the row bound · Square-summability of coordinates of an ℓ² vector

Used byPer-row estimate in Schur's test on \(\ell^2\) · Bound on the double weighted series in Schur's test · Partial sums of the weighted row series in Schur's test · Summability of the double weighted series in Schur's test

TheoremPartial sums of the weighted row series in Schur's test#✓fully proved

A finite partial sum of the weighted series is bounded by R * ‖x‖².

theorem sum_range_schurInf_weighted_le {a : ℕ → ℕ → 𝕜} {R : ℝ}
    (hrow : ∀ i, Summable fun j => ‖a i j‖)
    (hrow_le : ∀ i, ∑' j, ‖a i j‖ ≤ R) (x : ℓ²(ℕ, 𝕜)) (i : ℕ) (N : ℕ) :
    ∑ j ∈ Finset.range N, ‖a i j‖ * ‖x j‖ ^ 2 ≤ R * ‖x‖ ^ 2

Uses 4 · Used by 1

Proof usesEntries of a Schur matrix are bounded by the row bound · Summability of the weighted row series in Schur's test · Squared ℓ² norm as a sum of squared coordinates · Square-summability of coordinates of an ℓ² vector

Used byAbsolute summability of rows of a Schur matrix

TheoremAbsolute summability of rows of a Schur matrix#✓fully proved

Summability of the row series of absolute values.

theorem summable_schurInf_norm {a : ℕ → ℕ → 𝕜} {R : ℝ}
    (hrow : ∀ i, Summable fun j => ‖a i j‖)
    (hrow_le : ∀ i, ∑' j, ‖a i j‖ ≤ R) (x : ℓ²(ℕ, 𝕜)) (i : ℕ) :
    Summable fun j => ‖a i j‖ * ‖x j‖

Uses 3 · Used by 3

Proof usesWeighted Cauchy–Schwarz for one row of a Schur matrix · Row bound of a Schur matrix is nonnegative · Partial sums of the weighted row series in Schur's test

Used bySchur's test, adjoint form · Per-row estimate in Schur's test on \(\ell^2\) · Summability of the row series defining a Schur coordinate

TheoremSummability of the row series defining a Schur coordinate#✓fully proved

Summability of the row series defining one coordinate of the operator.

theorem summable_schurInf_coord {a : ℕ → ℕ → 𝕜} {R : ℝ}
    (hrow : ∀ i, Summable fun j => ‖a i j‖)
    (hrow_le : ∀ i, ∑' j, ‖a i j‖ ≤ R) (x : ℓ²(ℕ, 𝕜)) (i : ℕ) :
    Summable fun j => a i j * x j

Uses 1 · Used by 1

Proof usesAbsolute summability of rows of a Schur matrix

Used bySchur operator of an infinite matrix as a linear map

TheoremPer-row estimate in Schur's test on \(\ell^2\)#✓fully proved

The per-row estimate: ‖(T x) i‖² ≤ R * ∑' j, ‖a i j‖ * ‖x j‖².

theorem schurInf_pointwise_sq_le {a : ℕ → ℕ → 𝕜} {R : ℝ}
    (hrow : ∀ i, Summable fun j => ‖a i j‖)
    (hrow_le : ∀ i, ∑' j, ‖a i j‖ ≤ R) (x : ℓ²(ℕ, 𝕜)) (i : ℕ) :
    ‖∑' j, a i j * x j‖ ^ 2 ≤ R * ∑' j, ‖a i j‖ * ‖x j‖ ^ 2

Uses 4 · Used by 2

Proof usesWeighted Cauchy–Schwarz for one row of a Schur matrix · Row bound of a Schur matrix is nonnegative · Absolute summability of rows of a Schur matrix · Summability of the weighted row series in Schur's test

Used byNorm bound for the Schur linear map · Squared coordinates of a Schur image are summable

TheoremSummability of the double weighted series in Schur's test#✓fully proved

Summability of the double weighted series ∑' i, ∑' j, ‖a i j‖ * ‖x j‖².

theorem summable_schurInf_weighted_tsum {a : ℕ → ℕ → 𝕜} {R C : ℝ}
    (hrow : ∀ i, Summable fun j => ‖a i j‖)
    (hrow_le : ∀ i, ∑' j, ‖a i j‖ ≤ R)
    (hcol : ∀ j, Summable fun i => ‖a i j‖)
    (hcol_le : ∀ j, ∑' i, ‖a i j‖ ≤ C) (x : ℓ²(ℕ, 𝕜)) :
    Summable fun i => ∑' j, ‖a i j‖ * ‖x j‖ ^ 2

Uses 3 · Used by 3

Proof usesSummability of the weighted row series in Schur's test · Squared ℓ² norm as a sum of squared coordinates · Square-summability of coordinates of an ℓ² vector

Used byNorm bound for the Schur linear map · Bound on the double weighted series in Schur's test · Squared coordinates of a Schur image are summable

TheoremBound on the double weighted series in Schur's test#✓fully proved

The double weighted series is bounded by C * ‖x‖², via the tsum interchange.

theorem schurInf_tsum_weighted_le {a : ℕ → ℕ → 𝕜} {R C : ℝ}
    (hrow : ∀ i, Summable fun j => ‖a i j‖)
    (hrow_le : ∀ i, ∑' j, ‖a i j‖ ≤ R)
    (hcol : ∀ j, Summable fun i => ‖a i j‖)
    (hcol_le : ∀ j, ∑' i, ‖a i j‖ ≤ C) (x : ℓ²(ℕ, 𝕜)) :
    ∑' i, ∑' j, ‖a i j‖ * ‖x j‖ ^ 2 ≤ C * ‖x‖ ^ 2

Uses 4 · Used by 1

Proof usesSummability of the weighted row series in Schur's test · Summability of the double weighted series in Schur's test · Squared ℓ² norm as a sum of squared coordinates · Square-summability of coordinates of an ℓ² vector

Used byNorm bound for the Schur linear map

TheoremSquared coordinates of a Schur image are summable#✓fully proved

Summability of the squared coordinates of a Schur image.

theorem summable_schurInf_coordSq {a : ℕ → ℕ → 𝕜} {R C : ℝ}
    (hrow : ∀ i, Summable fun j => ‖a i j‖)
    (hrow_le : ∀ i, ∑' j, ‖a i j‖ ≤ R)
    (hcol : ∀ j, Summable fun i => ‖a i j‖)
    (hcol_le : ∀ j, ∑' i, ‖a i j‖ ≤ C) (x : ℓ²(ℕ, 𝕜)) :
    Summable fun i => ‖∑' j, a i j * x j‖ ^ 2

Uses 2 · Used by 2

Proof usesPer-row estimate in Schur's test on \(\ell^2\) · Summability of the double weighted series in Schur's test

Used byCoordinates of a Schur image lie in \(\ell^2\) · Norm bound for the Schur linear map

TheoremCoordinates of a Schur image lie in \(\ell^2\)#✓fully proved

The coordinates of a Schur image are in ℓ².

theorem memℓp_schurInfCoord {a : ℕ → ℕ → 𝕜} {R C : ℝ}
    (hrow : ∀ i, Summable fun j => ‖a i j‖)
    (hrow_le : ∀ i, ∑' j, ‖a i j‖ ≤ R)
    (hcol : ∀ j, Summable fun i => ‖a i j‖)
    (hcol_le : ∀ j, ∑' i, ‖a i j‖ ≤ C) (x : ℓ²(ℕ, 𝕜)) :
    Memℓp (fun i => ∑' j, a i j * x j) 2

Uses 2 · Used by 1

Proof usesSquared coordinates of a Schur image are summable · Square-summable sequences lie in ℓ²

Used bySchur operator of an infinite matrix as a linear map

DefinitionSchur operator of an infinite matrix as a linear map#✓fully proved

The Schur operator of a matrix, as a linear map.

MathlibExt.Analysis.FunctionalAnalysis.SchurTestInfinite.schurInfLinMap · 22 lines

noncomputable def schurInfLinMap (a : ℕ → ℕ → 𝕜) {R C : ℝ}
    (hrow : ∀ i, Summable fun j => ‖a i j‖)
    (hrow_le : ∀ i, ∑' j, ‖a i j‖ ≤ R)
    (hcol : ∀ j, Summable fun i => ‖a i j‖)
    (hcol_le : ∀ j, ∑' i, ‖a i j‖ ≤ C) :
    ℓ²(ℕ, 𝕜) →ₗ[𝕜] ℓ²(ℕ, 𝕜) where
  toFun x := ⟨fun i => ∑' j, a i j * x j, memℓp_schurInfCoord hrow hrow_le hcol hcol_le x⟩
  map_add' x y := by
    apply lp.ext
    funext i
    show (∑' j, a i j * (x + y) j) = (∑' j, a i j * x j) + (∑' j, a i j * y j)
    rw [← (summable_schurInf_coord hrow hrow_le x i).tsum_add
      (summable_schurInf_coord hrow hrow_le y i)]
    refine tsum_congr (fun j => ?_)
    simp only [lp.coeFn_add, Pi.add_apply, mul_add]
  map_smul' c x := by
    apply lp.ext
    funext i
    show (∑' j, a i j * (c • x) j) = c * (∑' j, a i j * x j)
    rw [← tsum_mul_left]
    refine tsum_congr (fun j => ?_)
    rw [lp.coeFn_smul, Pi.smul_apply, smul_eq_mul, mul_left_comm]

Uses 2 · Used by 3

Statement usesCoordinates of a Schur image lie in \(\ell^2\) · Summability of the row series defining a Schur coordinate

Used byNorm bound for the Schur linear map · Pointwise action of the Schur linear map · Schur operator on \(\ell^2(\mathbb{N})\)

TheoremPointwise action of the Schur linear map#✓fully proved

Pointwise action of the Schur linear map.

theorem schurInfLinMap_apply (a : ℕ → ℕ → 𝕜) {R C : ℝ}
    (hrow : ∀ i, Summable fun j => ‖a i j‖)
    (hrow_le : ∀ i, ∑' j, ‖a i j‖ ≤ R)
    (hcol : ∀ j, Summable fun i => ‖a i j‖)
    (hcol_le : ∀ j, ∑' i, ‖a i j‖ ≤ C) (x : ℓ²(ℕ, 𝕜)) (i : ℕ) :
    schurInfLinMap a hrow hrow_le hcol hcol_le x i = ∑' j, a i j * x j

Uses 1

Statement usesSchur operator of an infinite matrix as a linear map

TheoremNorm bound for the Schur linear map#✓fully proved

The Schur operator is bounded by √(R * C).

theorem norm_schurInfLinMap_le (a : ℕ → ℕ → 𝕜) {R C : ℝ}
    (hrow : ∀ i, Summable fun j => ‖a i j‖)
    (hrow_le : ∀ i, ∑' j, ‖a i j‖ ≤ R)
    (hcol : ∀ j, Summable fun i => ‖a i j‖)
    (hcol_le : ∀ j, ∑' i, ‖a i j‖ ≤ C) (x : ℓ²(ℕ, 𝕜)) :
    ‖schurInfLinMap a hrow hrow_le hcol hcol_le x‖ ≤ Real.sqrt (R * C) * ‖x‖

Uses 7 · Used by 2

Statement usesSchur operator of an infinite matrix as a linear map

Proof usesRow bound of a Schur matrix is nonnegative · Per-row estimate in Schur's test on \(\ell^2\) · Bound on the double weighted series in Schur's test · Squared coordinates of a Schur image are summable · Summability of the double weighted series in Schur's test · Squared ℓ² norm as a sum of squared coordinates

Used bySchur's test · Schur operator on \(\ell^2(\mathbb{N})\)

DefinitionSchur operator on \(\ell^2(\mathbb{N})\)#✓fully proved

The Schur operator of a matrix, as a bounded operator on ℓ²(ℕ, 𝕜).

noncomputable def schurInfOperator (a : ℕ → ℕ → 𝕜) {R C : ℝ}
    (hrow : ∀ i, Summable fun j => ‖a i j‖)
    (hrow_le : ∀ i, ∑' j, ‖a i j‖ ≤ R)
    (hcol : ∀ j, Summable fun i => ‖a i j‖)
    (hcol_le : ∀ j, ∑' i, ‖a i j‖ ≤ C) :
    ℓ²(ℕ, 𝕜) →L[𝕜] ℓ²(ℕ, 𝕜) :=
  (schurInfLinMap a hrow hrow_le hcol hcol_le).mkContinuous
    (Real.sqrt (R * C)) (norm_schurInfLinMap_le a hrow hrow_le hcol hcol_le)

Uses 2 · Used by 5

Statement usesNorm bound for the Schur linear map · Schur operator of an infinite matrix as a linear map

Used bySchur's test, adjoint form · Schur's test · Schur's test with a single row and column bound · Pointwise action of the Schur operator · Schur operator depends only on the matrix

TheoremPointwise action of the Schur operator#✓fully proved

Pointwise action of the Schur operator.

theorem schurInfOperator_apply (a : ℕ → ℕ → 𝕜) {R C : ℝ}
    (hrow : ∀ i, Summable fun j => ‖a i j‖)
    (hrow_le : ∀ i, ∑' j, ‖a i j‖ ≤ R)
    (hcol : ∀ j, Summable fun i => ‖a i j‖)
    (hcol_le : ∀ j, ∑' i, ‖a i j‖ ≤ C) (x : ℓ²(ℕ, 𝕜)) (i : ℕ) :
    schurInfOperator a hrow hrow_le hcol hcol_le x i = ∑' j, a i j * x j

Uses 1 · Used by 1

Statement usesSchur operator on \(\ell^2(\mathbb{N})\)

Used bySchur's test, adjoint form

TheoremSchur's test#✓fully proved

The operator norm is at most √(R * C).

theorem norm_schurInfOperator_le (a : ℕ → ℕ → 𝕜) {R C : ℝ}
    (hrow : ∀ i, Summable fun j => ‖a i j‖)
    (hrow_le : ∀ i, ∑' j, ‖a i j‖ ≤ R)
    (hcol : ∀ j, Summable fun i => ‖a i j‖)
    (hcol_le : ∀ j, ∑' i, ‖a i j‖ ≤ C) :
    ‖schurInfOperator a hrow hrow_le hcol hcol_le‖ ≤ Real.sqrt (R * C)

Uses 2 · Used by 1

Statement usesSchur operator on \(\ell^2(\mathbb{N})\)

Proof usesNorm bound for the Schur linear map

Used bySchur's test with a single row and column bound

TheoremSchur's test with a single row and column bound#✓fully proved

The single-bound form: if all row and column sums are at most B, then the operator norm is at most B.

theorem norm_schurInfOperator_le_of_le (a : ℕ → ℕ → 𝕜) {B : ℝ} (hB : 0 ≤ B)
    (hrow : ∀ i, Summable fun j => ‖a i j‖)
    (hrow_le : ∀ i, ∑' j, ‖a i j‖ ≤ B)
    (hcol : ∀ j, Summable fun i => ‖a i j‖)
    (hcol_le : ∀ j, ∑' i, ‖a i j‖ ≤ B) :
    ‖schurInfOperator a hrow hrow_le hcol hcol_le‖ ≤ B

Uses 2

Statement usesSchur operator on \(\ell^2(\mathbb{N})\)

Proof usesSchur's test

TheoremSchur operator depends only on the matrix#✓fully proved

The Schur operator depends only on the matrix, not on the bounds or proofs.

theorem schurInfOperator_congr {a b : ℕ → ℕ → 𝕜} {R C R' C' : ℝ} (h : a = b)
    (hrow : ∀ i, Summable fun j => ‖a i j‖)
    (hrow_le : ∀ i, ∑' j, ‖a i j‖ ≤ R)
    (hcol : ∀ j, Summable fun i => ‖a i j‖)
    (hcol_le : ∀ j, ∑' i, ‖a i j‖ ≤ C)
    (hrow' : ∀ i, Summable fun j => ‖b i j‖)
    (hrow_le' : ∀ i, ∑' j, ‖b i j‖ ≤ R')
    (hcol' : ∀ j, Summable fun i => ‖b i j‖)
    (hcol_le' : ∀ j, ∑' i, ‖b i j‖ ≤ C') :
    schurInfOperator a hrow hrow_le hcol hcol_le =
      schurInfOperator b hrow' hrow_le' hcol' hcol_le'

Uses 1

Statement usesSchur operator on \(\ell^2(\mathbb{N})\)

TheoremWeighted partial sums grouped by the first index#✓fully proved

A finite partial sum of the weighted series, grouped by the first index.

theorem sum_finset_schurInf_weighted_fst_le {a : ℕ → ℕ → 𝕜} {R : ℝ}
    (hrow : ∀ i, Summable fun j => ‖a i j‖)
    (hrow_le : ∀ i, ∑' j, ‖a i j‖ ≤ R) (x : ℓ²(ℕ, 𝕜)) (S : Finset (ℕ × ℕ)) :
    ∑ p ∈ S, ‖a p.1 p.2‖ * ‖x p.1‖ ^ 2 ≤ R * ‖x‖ ^ 2

Uses 3 · Used by 2

Proof usesRow bound of a Schur matrix is nonnegative · Squared ℓ² norm as a sum of squared coordinates · Square-summability of coordinates of an ℓ² vector

Used byWeighted partial sums grouped by the second index · Product summability for the Schur bilinear form

TheoremWeighted partial sums grouped by the second index#✓fully proved

A finite partial sum of the weighted series, grouped by the second index.

theorem sum_finset_schurInf_weighted_snd_le {a : ℕ → ℕ → 𝕜} {C : ℝ}
    (hcol : ∀ j, Summable fun i => ‖a i j‖)
    (hcol_le : ∀ j, ∑' i, ‖a i j‖ ≤ C) (v : ℓ²(ℕ, 𝕜)) (S : Finset (ℕ × ℕ)) :
    ∑ p ∈ S, ‖a p.1 p.2‖ * ‖v p.2‖ ^ 2 ≤ C * ‖v‖ ^ 2

Uses 1 · Used by 1

Proof usesWeighted partial sums grouped by the first index

Used byProduct summability for the Schur bilinear form

TheoremProduct summability for the Schur bilinear form#✓fully proved

Product summability for the bilinear form of a Schur matrix.

theorem summable_schurInf_prod {a : ℕ → ℕ → 𝕜} {R C : ℝ}
    (hrow : ∀ i, Summable fun j => ‖a i j‖)
    (hrow_le : ∀ i, ∑' j, ‖a i j‖ ≤ R)
    (hcol : ∀ j, Summable fun i => ‖a i j‖)
    (hcol_le : ∀ j, ∑' i, ‖a i j‖ ≤ C) (x v : ℓ²(ℕ, 𝕜)) :
    Summable fun p : ℕ × ℕ => ‖a p.1 p.2‖ * ‖x p.1‖ * ‖v p.2‖

Uses 3 · Used by 1

Proof usesRow bound of a Schur matrix is nonnegative · Weighted partial sums grouped by the first index · Weighted partial sums grouped by the second index

Used bySchur's test, adjoint form

TheoremRow summability of the conjugate-transpose Schur matrix#✓fully proved

Row summability for the conjugate-transpose matrix.

theorem summable_schurInf_transposeStar_row {a : ℕ → ℕ → 𝕜}
    (hcol : ∀ j, Summable fun i => ‖a i j‖) (i : ℕ) :
    Summable fun j => ‖star (a j i)‖

Used by 1

Used bySchur's test, adjoint form

TheoremRow bounds for the conjugate-transpose Schur matrix#✓fully proved

Row bounds for the conjugate-transpose matrix.

theorem schurInf_transposeStar_row_le {a : ℕ → ℕ → 𝕜} {C : ℝ}
    (hcol_le : ∀ j, ∑' i, ‖a i j‖ ≤ C) (i : ℕ) :
    ∑' j, ‖star (a j i)‖ ≤ C

Used by 1

Used bySchur's test, adjoint form

TheoremColumn summability for the conjugate-transpose matrix in Schur's test#✓fully proved

Column summability for the conjugate-transpose matrix.

theorem summable_schurInf_transposeStar_col {a : ℕ → ℕ → 𝕜}
    (hrow : ∀ i, Summable fun j => ‖a i j‖) (j : ℕ) :
    Summable fun i => ‖star (a j i)‖

Used by 1

Used bySchur's test, adjoint form

TheoremColumn bounds for the conjugate-transpose matrix in Schur's test#✓fully proved

Column bounds for the conjugate-transpose matrix.

theorem schurInf_transposeStar_col_le {a : ℕ → ℕ → 𝕜} {R : ℝ}
    (hrow_le : ∀ i, ∑' j, ‖a i j‖ ≤ R) (j : ℕ) :
    ∑' i, ‖star (a j i)‖ ≤ R

Used by 1

Used bySchur's test, adjoint form

TheoremSchur's test, adjoint form#✓fully proved

The adjoint of a Schur operator is the Schur operator of the conjugate-transpose matrix.

theorem adjoint_schurInfOperator (a : ℕ → ℕ → 𝕜) {R C : ℝ}
    (hrow : ∀ i, Summable fun j => ‖a i j‖)
    (hrow_le : ∀ i, ∑' j, ‖a i j‖ ≤ R)
    (hcol : ∀ j, Summable fun i => ‖a i j‖)
    (hcol_le : ∀ j, ∑' i, ‖a i j‖ ≤ C) :
    (schurInfOperator a hrow hrow_le hcol hcol_le)† =
      schurInfOperator (fun i j => star (a j i))
        (summable_schurInf_transposeStar_row hcol)
        (schurInf_transposeStar_row_le hcol_le)
        (summable_schurInf_transposeStar_col hrow)
        (schurInf_transposeStar_col_le hrow_le)

Uses 8

Statement usesSchur operator on \(\ell^2(\mathbb{N})\) · Column bounds for the conjugate-transpose matrix in Schur's test · Row bounds for the conjugate-transpose Schur matrix · Column summability for the conjugate-transpose matrix in Schur's test · Row summability of the conjugate-transpose Schur matrix

Proof usesPointwise action of the Schur operator · Absolute summability of rows of a Schur matrix · Product summability for the Schur bilinear form

34 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.