The Schäffer unitary power dilation

This file proves the Schäffer dilation through a repeated-interaction model on the bilateral Hilbert sum ℓ²(ℤ, E ⊕₂ E). A Halmos unitary acts independently at every site, after which the environment output moves one site to the right. The negative sites stay zero, so the system component at site zero evolves as Tⁿ. The boundary theorem packages this unitary, its isometric embedding, and the resulting power-compression identity.

@[reducible, inline]

abbrev SchaefferSpace (E : Type u) [NormedAddCommGroup E] : AddSubgroup (PreLp fun (x : ℤ) => E)

The Hilbert sum used for the Schäffer dilation.

Equations

• SchaefferSpace E = lp (fun (x : ℤ) => E) 2

noncomputable def schaefferEmbedding {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] : E →L[ℂ] ↥(SchaefferSpace E)

Embed E isometrically as coordinate zero of its bilateral Hilbert sum.

Equations

• schaefferEmbedding = lp.singleContinuousLinearMap ℂ (fun (x : ℤ) => E) 2 0

@[simp]

theorem schaefferEmbedding_apply {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (x : E) : schaefferEmbedding x = lp.single 2 0 x

theorem inner_schaefferEmbedding {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (x y : E) : inner ℂ (schaefferEmbedding x) (schaefferEmbedding y) = inner ℂ x y

The coordinate-zero embedding preserves the inner product.

theorem adjoint_schaefferEmbedding_apply {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (f : ↥(SchaefferSpace E)) : (ContinuousLinearMap.adjoint schaefferEmbedding) f = ↑f 0

The adjoint of the coordinate-zero embedding extracts coordinate zero.

noncomputable def lpReindexForward {E : Type u} [NormedAddCommGroup E] {ι : Type u_1} {ι' : Type u_2} (e : ι ≃ ι') (f : ↥(lp (fun (x : ι) => E) 2)) : ↥(lp (fun (x : ι') => E) 2)

Reindex a square-summable family along an equivalence.

Equations

• lpReindexForward e f = ⟨fun (j : ι') => ↑f (e.symm j), ⋯⟩

noncomputable def lpReindex {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {ι : Type u_1} {ι' : Type u_2} (e : ι ≃ ι') : ↥(lp (fun (x : ι) => E) 2) ≃ₗᵢ[ℂ] ↥(lp (fun (x : ι') => E) 2)

Reindexing a square-summable family along an equivalence is a linear isometry equivalence.

Equations

• lpReindex e = { toFun := lpReindexForward e, map_add' := ⋯, map_smul' := ⋯, invFun := lpReindexForward e.symm, left_inv := ⋯, right_inv := ⋯, norm_map' := ⋯ }

noncomputable def schaefferBilateralShiftEquiv {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] : ↥(SchaefferSpace E) ≃ₗᵢ[ℂ] ↥(SchaefferSpace E)

The right bilateral shift, as a linear isometry equivalence of the dilation space.

Equations

• schaefferBilateralShiftEquiv = lpReindex (Equiv.addRight 1)

@[simp]

theorem schaefferBilateralShiftEquiv_apply {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (f : ↥(SchaefferSpace E)) (j : ℤ) : ↑(schaefferBilateralShiftEquiv f) j = ↑f (j - 1)

noncomputable def schaefferBilateralShiftUnitary {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] : ↥(unitary (↥(SchaefferSpace E) →L[ℂ] ↥(SchaefferSpace E)))

The bilateral shift as an element of the unitary group.

Equations

• schaefferBilateralShiftUnitary = Unitary.linearIsometryEquiv.symm schaefferBilateralShiftEquiv

noncomputable def schaefferBilateralShift {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] : ↥(SchaefferSpace E) →L[ℂ] ↥(SchaefferSpace E)

The right bilateral shift, bundled as a continuous linear map.

Equations

• schaefferBilateralShift = ↑schaefferBilateralShiftUnitary

theorem schaefferBilateralShift_mem_unitary {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] : schaefferBilateralShift ∈ unitary (↥(SchaefferSpace E) →L[ℂ] ↥(SchaefferSpace E))

The bilateral shift is unitary.

@[simp]

theorem schaefferBilateralShift_apply {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (f : ↥(SchaefferSpace E)) (j : ℤ) : ↑(schaefferBilateralShift f) j = ↑f (j - 1)

@[reducible, inline]

abbrev SchaefferNetworkFiber (E : Type u) : Type u

One site in the repeated-interaction model: a system and one environment copy.

Equations

• SchaefferNetworkFiber E = WithLp 2 (E × E)

@[reducible, inline]

noncomputable abbrev SchaefferNetworkSpace (E : Type u) [NormedAddCommGroup E] : AddSubgroup (PreLp fun (x : ℤ) => SchaefferNetworkFiber E)

The bilateral Hilbert sum of system-environment sites.

Equations

• SchaefferNetworkSpace E = lp (fun (x : ℤ) => SchaefferNetworkFiber E) 2

noncomputable def schaefferFiberEmbedding {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] : E →L[ℂ] SchaefferNetworkFiber E

Insert the system space into the system component of one network site.

Equations

• schaefferFiberEmbedding = ↑(WithLp.prodContinuousLinearEquiv 2 ℂ E E).symm ∘SL ContinuousLinearMap.inl ℂ E E

noncomputable def schaefferNetworkEmbedding {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] : E →L[ℂ] ↥(SchaefferNetworkSpace E)

Embed the original space at the system component of site zero.

Equations

• schaefferNetworkEmbedding = lp.singleContinuousLinearMap ℂ (fun (x : ℤ) => SchaefferNetworkFiber E) 2 0 ∘SL schaefferFiberEmbedding

@[simp]

theorem schaefferNetworkEmbedding_apply {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (x : E) : schaefferNetworkEmbedding x = lp.single 2 0 (WithLp.toLp 2 (x, 0))

theorem inner_schaefferNetworkEmbedding {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (x y : E) : inner ℂ (schaefferNetworkEmbedding x) (schaefferNetworkEmbedding y) = inner ℂ x y

The network embedding preserves inner products.

theorem adjoint_schaefferNetworkEmbedding_apply {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (f : ↥(SchaefferNetworkSpace E)) : (ContinuousLinearMap.adjoint schaefferNetworkEmbedding) f = WithLp.fst (↑f 0)

The adjoint of the network embedding extracts the system component at site zero.

theorem exists_unitary_power_dilation {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (T : E →L[ℂ] E) (hT : ‖T‖ ≤ 1) : ∃ (H : Type u) (x : NormedAddCommGroup H) (x_1 : InnerProductSpace ℂ H) (x_2 : CompleteSpace H) (V : E →L[ℂ] H) (U : H →L[ℂ] H), (∀ (x_3 y : E), inner ℂ (V x_3) (V y) = inner ℂ x_3 y) ∧ U ∈ unitary (H →L[ℂ] H) ∧ ∀ (n : ℕ) (x_3 : E), (ContinuousLinearMap.adjoint V) ((U ^ n) (V x_3)) = (T ^ n) x_3

Every contraction has a unitary power dilation on a larger Hilbert space.