Cayley transform

26 fully proved

Scalar operators and the Cayley transform

TheoremNonzero scalar operators are units#✓fully proved

A nonzero scalar operator is a unit.

theorem isUnit_smul_one (z : ℂ) (hz : z ≠ 0) : IsUnit (z • (1 : H →L[ℂ] H))

Used by 3

Used bySpectral mapping for the Cayley transform, preimage direction · Spectral mapping for the Cayley transform, image direction · Inverse of a scalar operator

TheoremInverse of a scalar operator#✓fully proved

The ring inverse of a scalar operator is the scalar operator of the inverse scalar.

theorem ringInverse_smul_one (z : ℂ) :
    Ring.inverse (z • (1 : H →L[ℂ] H)) = z⁻¹ • (1 : H →L[ℂ] H)

Uses 1

Proof usesNonzero scalar operators are units

DefinitionCayley transform of an operator#✓fully proved

The Cayley transform of an operator A: (A - i) * (A + i)⁻¹. The factor A + i • 1 is a unit when A is self-adjoint on a complete Hilbert space (see isUnit_add_I_smul_one_of_isSelfAdjoint below), in which case the ring inverse here is the genuine operator inverse.

noncomputable def cayleyTransform : H →L[ℂ] H :=
  (A - Complex.I • (1 : H →L[ℂ] H)) * Ring.inverse (A + Complex.I • (1 : H →L[ℂ] H))

Used by 18

TheoremFactors of the Cayley transform commute#✓fully proved

The two factors of the Cayley transform commute.

theorem commute_sub_I_add_I :
    (A - Complex.I • (1 : H →L[ℂ] H)) * (A + Complex.I • (1 : H →L[ℂ] H))
      = (A + Complex.I • (1 : H →L[ℂ] H)) * (A - Complex.I • (1 : H →L[ℂ] H))

Used by 2

Used byAdjoint of the Cayley transform is a right inverse · Adjoint of the Cayley transform is a left inverse

Self Adjoint

TheoremSelf-adjoint operator minus a non-real scalar is invertible#✓fully proved

For a self-adjoint operator, A - w • 1 is a unit whenever w has nonzero imaginary part. The proof is the norm estimate ‖(A - w • 1) x‖ ≥ |w.im| * ‖x‖, read off from the imaginary part of ⟪(A - w • 1) x, x⟫.

theorem isUnit_sub_smul_one_of_isSelfAdjoint_of_im_ne_zero (hA : IsSelfAdjoint A)
    {w : ℂ} (hw : w.im ≠ 0) : IsUnit (A - w • (1 : H →L[ℂ] H))

Used by 2

Used bySelf-adjoint operator plus \(i\) is invertible · Self-adjoint operator minus \(i\) is invertible

TheoremSelf-adjoint operator plus \(i\) is invertible#✓fully proved

For a self-adjoint operator, A + i • 1 is a unit.

theorem isUnit_add_I_smul_one_of_isSelfAdjoint (hA : IsSelfAdjoint A) :
    IsUnit (A + Complex.I • (1 : H →L[ℂ] H))

Uses 1 · Used by 8

Proof usesSelf-adjoint operator minus a non-real scalar is invertible

Used byResolvent factorization for the Cayley transform · Eigenvalues of the Cayley transform · Inverse of a self-adjoint operator plus \(i\) is a unit · Spectral mapping for the Cayley transform, image direction · Adjoint of the Cayley transform is a right inverse · Formula for one plus the Cayley transform · Formula for one minus the Cayley transform · Adjoint of the Cayley transform is a left inverse

TheoremSelf-adjoint operator minus \(i\) is invertible#✓fully proved

For a self-adjoint operator, A - i • 1 is a unit.

theorem isUnit_sub_I_smul_one_of_isSelfAdjoint (hA : IsSelfAdjoint A) :
    IsUnit (A - Complex.I • (1 : H →L[ℂ] H))

Uses 1 · Used by 3

Proof usesSelf-adjoint operator minus a non-real scalar is invertible

Used byCayley transform of a self-adjoint operator is invertible · Adjoint of the Cayley transform is a right inverse · Adjoint of the Cayley transform is a left inverse

TheoremInverse of a self-adjoint operator plus \(i\) is a unit#✓fully proved

The inverse of A + i • 1 is a unit for self-adjoint A.

theorem isUnit_ringInverse_add_I_of_isSelfAdjoint (hA : IsSelfAdjoint A) :
    IsUnit (Ring.inverse (A + Complex.I • (1 : H →L[ℂ] H)))

Uses 1 · Used by 4

Proof usesSelf-adjoint operator plus \(i\) is invertible

Used bySpectral mapping for the Cayley transform, preimage direction · Cayley transform of a self-adjoint operator is invertible · One minus the Cayley transform is invertible · Spectral mapping for the Cayley transform, image direction

TheoremAdjoint of the Cayley transform#✓fully proved

The adjoint of the Cayley transform.

theorem star_cayleyTransform (hA : IsSelfAdjoint A) :
    star (cayleyTransform A)
      = Ring.inverse (A - Complex.I • (1 : H →L[ℂ] H))
          * (A + Complex.I • (1 : H →L[ℂ] H))

noncomputable def cayleyTransform : H →L[ℂ] H :=
  (A - Complex.I • (1 : H →L[ℂ] H)) * Ring.inverse (A + Complex.I • (1 : H →L[ℂ] H))

MathlibExt/Analysis/InnerProductSpace/CayleyTransform.lean:79

Uses 1 · Used by 2

Statement usesCayley transform of an operator

Used byAdjoint of the Cayley transform is a right inverse · Adjoint of the Cayley transform is a left inverse

TheoremAdjoint of the Cayley transform is a left inverse#✓fully proved

The Cayley transform of a self-adjoint operator satisfies U† * U = 1.

theorem star_mul_self_cayleyTransform (hA : IsSelfAdjoint A) :
    star (cayleyTransform A) * cayleyTransform A = 1

noncomputable def cayleyTransform : H →L[ℂ] H :=
  (A - Complex.I • (1 : H →L[ℂ] H)) * Ring.inverse (A + Complex.I • (1 : H →L[ℂ] H))

MathlibExt/Analysis/InnerProductSpace/CayleyTransform.lean:79

Uses 5 · Used by 1

Statement usesCayley transform of an operator

Proof usesFactors of the Cayley transform commute · Self-adjoint operator plus \(i\) is invertible · Self-adjoint operator minus \(i\) is invertible · Adjoint of the Cayley transform

Used byCayley transform of a self-adjoint operator is unitary

TheoremAdjoint of the Cayley transform is a right inverse#✓fully proved

The Cayley transform of a self-adjoint operator satisfies U * U† = 1.

theorem mul_star_self_cayleyTransform (hA : IsSelfAdjoint A) :
    cayleyTransform A * star (cayleyTransform A) = 1

noncomputable def cayleyTransform : H →L[ℂ] H :=
  (A - Complex.I • (1 : H →L[ℂ] H)) * Ring.inverse (A + Complex.I • (1 : H →L[ℂ] H))

MathlibExt/Analysis/InnerProductSpace/CayleyTransform.lean:79

Uses 5

Statement usesCayley transform of an operator

Proof usesFactors of the Cayley transform commute · Self-adjoint operator plus \(i\) is invertible · Self-adjoint operator minus \(i\) is invertible · Adjoint of the Cayley transform

TheoremCayley transform of a self-adjoint operator is invertible#✓fully proved

The Cayley transform of a self-adjoint operator is a unit.

theorem isUnit_cayleyTransform (hA : IsSelfAdjoint A) : IsUnit (cayleyTransform A)

noncomputable def cayleyTransform : H →L[ℂ] H :=
  (A - Complex.I • (1 : H →L[ℂ] H)) * Ring.inverse (A + Complex.I • (1 : H →L[ℂ] H))

MathlibExt/Analysis/InnerProductSpace/CayleyTransform.lean:79

Uses 3 · Used by 1

Statement usesCayley transform of an operator

Proof usesInverse of a self-adjoint operator plus \(i\) is a unit · Self-adjoint operator minus \(i\) is invertible

Used byCayley transform of a self-adjoint operator is unitary

TheoremCayley transform of a self-adjoint operator is unitary#✓fully proved

The Cayley transform of a self-adjoint operator is unitary.

theorem mem_unitary_cayleyTransform (hA : IsSelfAdjoint A) :
    cayleyTransform A ∈ unitary (H →L[ℂ] H)

noncomputable def cayleyTransform : H →L[ℂ] H :=
  (A - Complex.I • (1 : H →L[ℂ] H)) * Ring.inverse (A + Complex.I • (1 : H →L[ℂ] H))

MathlibExt/Analysis/InnerProductSpace/CayleyTransform.lean:79

Uses 3 · Used by 2

Statement usesCayley transform of an operator

Proof usesCayley transform of a self-adjoint operator is invertible · Adjoint of the Cayley transform is a left inverse

Used byCayley transform preserves norms of vectors · Spectrum of the Cayley transform lies on the unit circle

TheoremCayley transform preserves norms of vectors#✓fully proved

The Cayley transform of a self-adjoint operator is an isometry.

theorem norm_cayleyTransform_apply (hA : IsSelfAdjoint A) (x : H) :
    ‖cayleyTransform A x‖ = ‖x‖

noncomputable def cayleyTransform : H →L[ℂ] H :=
  (A - Complex.I • (1 : H →L[ℂ] H)) * Ring.inverse (A + Complex.I • (1 : H →L[ℂ] H))

MathlibExt/Analysis/InnerProductSpace/CayleyTransform.lean:79

Uses 2 · Used by 1

Statement usesCayley transform of an operator

Proof usesCayley transform of a self-adjoint operator is unitary

Used byOperator norm of the Cayley transform is one

TheoremOperator norm of the Cayley transform is one#✓fully proved

On a nontrivial space, the Cayley transform has operator norm 1.

theorem norm_cayleyTransform (hA : IsSelfAdjoint A) [Nontrivial H] :
    ‖cayleyTransform A‖ = 1

noncomputable def cayleyTransform : H →L[ℂ] H :=
  (A - Complex.I • (1 : H →L[ℂ] H)) * Ring.inverse (A + Complex.I • (1 : H →L[ℂ] H))

MathlibExt/Analysis/InnerProductSpace/CayleyTransform.lean:79

Uses 2

Statement usesCayley transform of an operator

Proof usesCayley transform preserves norms of vectors

TheoremFormula for one plus the Cayley transform#✓fully proved

1 + U is 2 • A times the inverse of A + i • 1.

theorem one_add_cayleyTransform (hA : IsSelfAdjoint A) :
    1 + cayleyTransform A
      = (2 : ℂ) • A * Ring.inverse (A + Complex.I • (1 : H →L[ℂ] H))

noncomputable def cayleyTransform : H →L[ℂ] H :=
  (A - Complex.I • (1 : H →L[ℂ] H)) * Ring.inverse (A + Complex.I • (1 : H →L[ℂ] H))

MathlibExt/Analysis/InnerProductSpace/CayleyTransform.lean:79

Uses 2 · Used by 1

Statement usesCayley transform of an operator

Proof usesSelf-adjoint operator plus \(i\) is invertible

Used byInverse Cayley formula

TheoremFormula for one minus the Cayley transform#✓fully proved

1 - U is 2 • (i • 1) times the inverse of A + i • 1.

theorem one_sub_cayleyTransform (hA : IsSelfAdjoint A) :
    1 - cayleyTransform A
      = (2 : ℂ) • (Complex.I • (1 : H →L[ℂ] H))
          * Ring.inverse (A + Complex.I • (1 : H →L[ℂ] H))

noncomputable def cayleyTransform : H →L[ℂ] H :=
  (A - Complex.I • (1 : H →L[ℂ] H)) * Ring.inverse (A + Complex.I • (1 : H →L[ℂ] H))

MathlibExt/Analysis/InnerProductSpace/CayleyTransform.lean:79

Uses 2 · Used by 2

Statement usesCayley transform of an operator

Proof usesSelf-adjoint operator plus \(i\) is invertible

Used byInverse Cayley formula · One minus the Cayley transform is invertible

TheoremOne minus the Cayley transform is invertible#✓fully proved

1 - U is a unit for the Cayley transform of a self-adjoint operator: 1 is never in the spectrum of U.

theorem isUnit_one_sub_cayleyTransform (hA : IsSelfAdjoint A) :
    IsUnit (1 - cayleyTransform A)

noncomputable def cayleyTransform : H →L[ℂ] H :=
  (A - Complex.I • (1 : H →L[ℂ] H)) * Ring.inverse (A + Complex.I • (1 : H →L[ℂ] H))

MathlibExt/Analysis/InnerProductSpace/CayleyTransform.lean:79

Uses 3 · Used by 2

Statement usesCayley transform of an operator

Proof usesInverse of a self-adjoint operator plus \(i\) is a unit · Formula for one minus the Cayley transform

Used byInverse Cayley formula · One is not in the spectrum of the Cayley transform

TheoremInverse Cayley formula#✓fully proved

The inverse Cayley formula: A = i • (1 + U) * (1 - U)⁻¹.

theorem eq_cayleyTransform_inv (hA : IsSelfAdjoint A) :
    A = Complex.I • (1 + cayleyTransform A) * Ring.inverse (1 - cayleyTransform A)

noncomputable def cayleyTransform : H →L[ℂ] H :=
  (A - Complex.I • (1 : H →L[ℂ] H)) * Ring.inverse (A + Complex.I • (1 : H →L[ℂ] H))

MathlibExt/Analysis/InnerProductSpace/CayleyTransform.lean:79

Uses 4

Statement usesCayley transform of an operator

Proof usesOne minus the Cayley transform is invertible · Formula for one plus the Cayley transform · Formula for one minus the Cayley transform

TheoremResolvent factorization for the Cayley transform#✓fully proved

The resolvent-type factorization behind the spectral mapping: for μ ≠ 1 and λ = i * (1 + μ) / (1 - μ), μ • 1 - U = ((μ - 1) • (A - λ • 1)) * (A + i • 1)⁻¹.

theorem algebraMap_sub_cayleyTransform (hA : IsSelfAdjoint A) {μ : ℂ} (hμ : μ ≠ 1) :
    algebraMap ℂ (H →L[ℂ] H) μ - cayleyTransform A
      = ((μ - 1) • (A - (Complex.I * (1 + μ) / (1 - μ)) • (1 : H →L[ℂ] H)))
          * Ring.inverse (A + Complex.I • (1 : H →L[ℂ] H))

noncomputable def cayleyTransform : H →L[ℂ] H :=
  (A - Complex.I • (1 : H →L[ℂ] H)) * Ring.inverse (A + Complex.I • (1 : H →L[ℂ] H))

MathlibExt/Analysis/InnerProductSpace/CayleyTransform.lean:79

Uses 2 · Used by 2

Statement usesCayley transform of an operator

Proof usesSelf-adjoint operator plus \(i\) is invertible

Used bySpectral mapping for the Cayley transform, preimage direction · Spectral mapping for the Cayley transform, image direction

TheoremOne is not in the spectrum of the Cayley transform#✓fully proved

1 is never in the spectrum of the Cayley transform.

theorem one_notMem_spectrum_cayleyTransform (hA : IsSelfAdjoint A) :
    (1 : ℂ) ∉ spectrum ℂ (cayleyTransform A)

noncomputable def cayleyTransform : H →L[ℂ] H :=
  (A - Complex.I • (1 : H →L[ℂ] H)) * Ring.inverse (A + Complex.I • (1 : H →L[ℂ] H))

MathlibExt/Analysis/InnerProductSpace/CayleyTransform.lean:79

Uses 2 · Used by 1

Statement usesCayley transform of an operator

Proof usesOne minus the Cayley transform is invertible

Used bySpectral mapping for the Cayley transform, preimage direction

TheoremSpectral mapping for the Cayley transform, image direction#✓fully proved

The image direction of the spectral mapping: if w is in the spectrum of A, then (w - i) / (w + i) is in the spectrum of U.

theorem mem_spectrum_cayleyTransform_of_mem_spectrum (hA : IsSelfAdjoint A)
    {w : ℂ} (hw : w ∈ spectrum ℂ A) :
    (w - Complex.I) / (w + Complex.I) ∈ spectrum ℂ (cayleyTransform A)

noncomputable def cayleyTransform : H →L[ℂ] H :=
  (A - Complex.I • (1 : H →L[ℂ] H)) * Ring.inverse (A + Complex.I • (1 : H →L[ℂ] H))

MathlibExt/Analysis/InnerProductSpace/CayleyTransform.lean:79

Uses 5 · Used by 1

Statement usesCayley transform of an operator

Proof usesResolvent factorization for the Cayley transform · Self-adjoint operator plus \(i\) is invertible · Inverse of a self-adjoint operator plus \(i\) is a unit · Nonzero scalar operators are units

Used bySpectrum of the Cayley transform

TheoremSpectral mapping for the Cayley transform, preimage direction#✓fully proved

The preimage direction of the spectral mapping: every point of the spectrum of U is (w - i) / (w + i) for some w in the spectrum of A.

theorem exists_mem_spectrum_of_mem_spectrum_cayleyTransform (hA : IsSelfAdjoint A)
    {μ : ℂ} (hμ : μ ∈ spectrum ℂ (cayleyTransform A)) :
    ∃ w ∈ spectrum ℂ A, (w - Complex.I) / (w + Complex.I) = μ

noncomputable def cayleyTransform : H →L[ℂ] H :=
  (A - Complex.I • (1 : H →L[ℂ] H)) * Ring.inverse (A + Complex.I • (1 : H →L[ℂ] H))

MathlibExt/Analysis/InnerProductSpace/CayleyTransform.lean:79

Uses 5 · Used by 1

Statement usesCayley transform of an operator

Proof usesResolvent factorization for the Cayley transform · Inverse of a self-adjoint operator plus \(i\) is a unit · Nonzero scalar operators are units · One is not in the spectrum of the Cayley transform

Used bySpectrum of the Cayley transform

TheoremSpectrum of the Cayley transform#✓fully proved

The spectrum of the Cayley transform is the image of the spectrum of A under the Möbius map λ ↦ (λ - i) / (λ + i).

theorem spectrum_cayleyTransform (hA : IsSelfAdjoint A) :
    spectrum ℂ (cayleyTransform A)
      = (fun w => (w - Complex.I) / (w + Complex.I)) '' spectrum ℂ A

noncomputable def cayleyTransform : H →L[ℂ] H :=
  (A - Complex.I • (1 : H →L[ℂ] H)) * Ring.inverse (A + Complex.I • (1 : H →L[ℂ] H))

MathlibExt/Analysis/InnerProductSpace/CayleyTransform.lean:79

Uses 3

Statement usesCayley transform of an operator

Proof usesSpectral mapping for the Cayley transform, preimage direction · Spectral mapping for the Cayley transform, image direction

TheoremSpectrum of the Cayley transform lies on the unit circle#✓fully proved

Points of the spectrum of the Cayley transform lie on the unit circle.

theorem norm_eq_one_of_mem_spectrum_cayleyTransform (hA : IsSelfAdjoint A)
    {μ : ℂ} (hμ : μ ∈ spectrum ℂ (cayleyTransform A)) : ‖μ‖ = 1

noncomputable def cayleyTransform : H →L[ℂ] H :=
  (A - Complex.I • (1 : H →L[ℂ] H)) * Ring.inverse (A + Complex.I • (1 : H →L[ℂ] H))

MathlibExt/Analysis/InnerProductSpace/CayleyTransform.lean:79

Uses 2

Statement usesCayley transform of an operator

Proof usesCayley transform of a self-adjoint operator is unitary

TheoremEigenvalues of the Cayley transform#✓fully proved

The eigenvalue correspondence: for μ ≠ 1, μ is an eigenvalue of the Cayley transform U iff i * (1 + μ) / (1 - μ) is an eigenvalue of A.

theorem hasEigenvalue_cayleyTransform_iff (hA : IsSelfAdjoint A) {μ : ℂ} (hμ : μ ≠ 1) :
    Module.End.HasEigenvalue ((cayleyTransform A : H →L[ℂ] H) : Module.End ℂ H) μ ↔
      Module.End.HasEigenvalue ((A : H →L[ℂ] H) : Module.End ℂ H)
        (Complex.I * (1 + μ) / (1 - μ))

noncomputable def cayleyTransform : H →L[ℂ] H :=
  (A - Complex.I • (1 : H →L[ℂ] H)) * Ring.inverse (A + Complex.I • (1 : H →L[ℂ] H))

MathlibExt/Analysis/InnerProductSpace/CayleyTransform.lean:79

Uses 2

Statement usesCayley transform of an operator

Proof usesSelf-adjoint operator plus \(i\) is invertible

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.