Wold decomposition

17 fully proved

Wandering subspaces

DefinitionWandering subspace of an isometry#✓fully proved

The wandering subspace of an isometry V: the orthogonal complement of its range. Vectors here are orthogonal to every vector in the range of V.

noncomputable def wanderingSub (V : H →ₗᵢ[𝕜] H) : Submodule 𝕜 H :=
  (LinearMap.range (V : H →ₗ[𝕜] H))ᗮ

Used by 8

Used byOne-step Wold splitting into wandering vector plus range · Finite Wold decomposition · Orthogonality of pushed-forward wandering vectors · Orthogonality of pushed-forward wandering vectors, symmetric form · Residual subspace is orthogonal to the wandering part · Wandering subspace and range are complementary · Uniqueness of the finite Wold decomposition · Pythagorean identity for the Wold decomposition

TheoremPowers of an isometry preserve inner products#✓fully proved

Pulling inner products back along powers of an isometry.

theorem inner_pow_pullback (V : H →ₗᵢ[𝕜] H) (k d : ℕ) (a b : H) :
    ⟪(V ^ k) a, (V ^ (k + d)) b⟫_𝕜 = ⟪a, (V ^ d) b⟫_𝕜

Used by 1

Used byOrthogonality of pushed-forward wandering vectors

TheoremPositive powers of an isometry land in its range#✓fully proved

A positive power of an isometry lands in the range of the isometry.

theorem pow_mem_range (V : H →ₗᵢ[𝕜] H) {d : ℕ} (hd : 0 < d) (b : H) :
    (V ^ d) b ∈ LinearMap.range (V : H →ₗ[𝕜] H)

Used by 1

Used byOrthogonality of pushed-forward wandering vectors

TheoremOrthogonality of pushed-forward wandering vectors#✓fully proved

A wandering vector, pushed forward k times, is orthogonal to any vector pushed forward strictly more times.

theorem inner_pow_wandering (V : H →ₗᵢ[𝕜] H) {k l : ℕ} (hkl : k < l) (a : H)
    (ha : a ∈ wanderingSub V) (b : H) :
    ⟪(V ^ k) a, (V ^ l) b⟫_𝕜 = 0

Uses 3 · Used by 2

Statement usesWandering subspace of an isometry

Proof usesPowers of an isometry preserve inner products · Positive powers of an isometry land in its range

Used byOrthogonality of pushed-forward wandering vectors, symmetric form · Uniqueness of the finite Wold decomposition

TheoremOrthogonality of pushed-forward wandering vectors, symmetric form#✓fully proved

The symmetric form of inner_pow_wandering.

theorem inner_pow_wandering' (V : H →ₗᵢ[𝕜] H) {k l : ℕ} (hkl : k < l) (a : H)
    (ha : a ∈ wanderingSub V) (b : H) :
    ⟪(V ^ l) b, (V ^ k) a⟫_𝕜 = 0

Uses 2 · Used by 1

Statement usesWandering subspace of an isometry

Proof usesOrthogonality of pushed-forward wandering vectors

Used byResidual subspace is orthogonal to the wandering part

Complete

TheoremWandering subspace and range are complementary#✓fully proved

The ambient space splits as the wandering subspace plus the range.

theorem isCompl_wandering (V : H →ₗᵢ[𝕜] H) :
    IsCompl (wanderingSub V) (LinearMap.range (V : H →ₗ[𝕜] H))

Uses 1 · Used by 1

Statement usesWandering subspace of an isometry

Used byOne-step Wold splitting into wandering vector plus range

TheoremOne-step Wold splitting into wandering vector plus range#✓fully proved

One step of the Wold decomposition: every vector splits as a wandering vector plus a vector in the range.

theorem exists_wandering_add_range (V : H →ₗᵢ[𝕜] H) (x : H) :
    ∃ w ∈ wanderingSub V, ∃ y : H, x = w + V y

Uses 2 · Used by 1

Statement usesWandering subspace of an isometry

Proof usesWandering subspace and range are complementary

Used byFinite Wold decomposition

TheoremFinite Wold decomposition#✓fully proved

Finite Wold decomposition: every vector is a finite sum of pushed-forward wandering vectors plus a remainder in the range of V ^ n. The wandering coefficients vanish at and beyond n.

theorem exists_wold_decomposition (V : H →ₗᵢ[𝕜] H) (x : H) (n : ℕ) :
    ∃ w : ℕ → H, ∃ y : H, (∀ k, w k ∈ wanderingSub V) ∧ (∀ k ≥ n, w k = 0) ∧
      x = (∑ k ∈ Finset.range n, (V ^ k) (w k)) + (V ^ n) y

Uses 2

Statement usesWandering subspace of an isometry

Proof usesOne-step Wold splitting into wandering vector plus range

TheoremPythagorean identity for the Wold decomposition#✓fully proved

Pythagoras for a Wold decomposition: the squared norm of a vector is the sum of the squared norms of its wandering coefficients plus the squared norm of the remainder.

theorem wold_norm_sq (V : H →ₗᵢ[𝕜] H) (n : ℕ) (w : ℕ → H)
    (hw : ∀ k, w k ∈ wanderingSub V) (y : H) (x : H)
    (hx : x = (∑ k ∈ Finset.range n, (V ^ k) (w k)) + (V ^ n) y) :
    ‖x‖ ^ 2 = (∑ k ∈ Finset.range n, ‖w k‖ ^ 2) + ‖y‖ ^ 2

Uses 1

Statement usesWandering subspace of an isometry

TheoremUniqueness of the finite Wold decomposition#✓fully proved

Uniqueness of the Wold decomposition at level n: the remainder and the finite wandering sum are uniquely determined.

theorem wold_decomposition_unique (V : H →ₗᵢ[𝕜] H) (n : ℕ) (w₁ w₂ : ℕ → H)
    (hw₁ : ∀ k, w₁ k ∈ wanderingSub V) (hw₂ : ∀ k, w₂ k ∈ wanderingSub V)
    (y₁ y₂ : H) (x : H)
    (hx₁ : x = (∑ k ∈ Finset.range n, (V ^ k) (w₁ k)) + (V ^ n) y₁)
    (hx₂ : x = (∑ k ∈ Finset.range n, (V ^ k) (w₂ k)) + (V ^ n) y₂) :
    y₁ = y₂ ∧
      (∑ k ∈ Finset.range n, (V ^ k) (w₁ k)) =
        ∑ k ∈ Finset.range n, (V ^ k) (w₂ k)

Uses 2

Statement usesWandering subspace of an isometry

Proof usesOrthogonality of pushed-forward wandering vectors

DefinitionResidual subspace of an isometry#✓fully proved

The residual subspace of an isometry: vectors in the range of every power of V.

noncomputable def residualSub (V : H →ₗᵢ[𝕜] H) : Submodule 𝕜 H :=
  ⨅ n, LinearMap.range ((V ^ n : H →ₗᵢ[𝕜] H) : H →ₗ[𝕜] H)

Used by 6

Used byResidual subspace is orthogonal to the wandering part · Isometry restricted to the residual subspace preserves inner products · An isometry maps its residual subspace into itself · Isometry restricted to the residual subspace is bijective · Unitary part of an isometry on its residual subspace · Action of the residual unitary of an isometry

TheoremAn isometry maps its residual subspace into itself#✓fully proved

The isometry maps its residual subspace into itself.

theorem mapsTo_residual (V : H →ₗᵢ[𝕜] H) :
    ∀ x ∈ residualSub V, V x ∈ residualSub V

Uses 1 · Used by 3

Statement usesResidual subspace of an isometry

Used byIsometry restricted to the residual subspace preserves inner products · Isometry restricted to the residual subspace is bijective · Unitary part of an isometry on its residual subspace

TheoremResidual subspace is orthogonal to the wandering part#✓fully proved

The residual subspace is orthogonal to every pushed-forward wandering vector: the wandering part and the residual part of Wold's decomposition are orthogonal.

theorem inner_residual_wandering (V : H →ₗᵢ[𝕜] H) (x : H) (hx : x ∈ residualSub V)
    (k : ℕ) (a : H) (ha : a ∈ wanderingSub V) :
    ⟪x, (V ^ k) a⟫_𝕜 = 0

Uses 3

Statement usesResidual subspace of an isometry · Wandering subspace of an isometry

Proof usesOrthogonality of pushed-forward wandering vectors, symmetric form

TheoremIsometry restricted to the residual subspace is bijective#✓fully proved

The restriction of an isometry to its residual subspace is bijective.

theorem restrict_residual_bijective (V : H →ₗᵢ[𝕜] H) :
    Function.Bijective (((V : H →ₗ[𝕜] H).restrict (mapsTo_residual V) :
      residualSub V →ₗ[𝕜] residualSub V))

Uses 2 · Used by 1

Statement usesAn isometry maps its residual subspace into itself · Residual subspace of an isometry

Used byUnitary part of an isometry on its residual subspace

TheoremIsometry restricted to the residual subspace preserves inner products#✓fully proved

The restriction of an isometry to its residual subspace preserves inner products.

theorem inner_restrict_residual (V : H →ₗᵢ[𝕜] H) (x y : residualSub V) :
    ⟪((V : H →ₗ[𝕜] H).restrict (mapsTo_residual V) x : H),
        ((V : H →ₗ[𝕜] H).restrict (mapsTo_residual V) y : H)⟫_𝕜 =
      ⟪(x : H), (y : H)⟫_𝕜

Uses 2 · Used by 1

Statement usesAn isometry maps its residual subspace into itself · Residual subspace of an isometry

Used byUnitary part of an isometry on its residual subspace

DefinitionUnitary part of an isometry on its residual subspace#✓fully proved

The isometry restricts to a unitary operator (a linear isometric equivalence) on its residual subspace.

noncomputable def woldResidualEquiv (V : H →ₗᵢ[𝕜] H) :
    residualSub V ≃ₗᵢ[𝕜] residualSub V :=
  LinearEquiv.isometryOfInner
    (LinearEquiv.ofBijective ((V : H →ₗ[𝕜] H).restrict (mapsTo_residual V))
      (restrict_residual_bijective V))
    (inner_restrict_residual V)

Uses 4 · Used by 1

Statement usesIsometry restricted to the residual subspace preserves inner products · An isometry maps its residual subspace into itself · Residual subspace of an isometry · Isometry restricted to the residual subspace is bijective

Used byAction of the residual unitary of an isometry

TheoremAction of the residual unitary of an isometry#✓fully proved

Applying the residual unitary is the same as applying V and viewing the result in the ambient space.

@[simp]
theorem woldResidualEquiv_apply_coe (V : H →ₗᵢ[𝕜] H) (x : residualSub V) :
    ((woldResidualEquiv V x : residualSub V) : H) = V (x : H)

Uses 2

Statement usesResidual subspace of an isometry · Unitary part of an isometry on its residual subspace

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.