L2ScalarIntertwining.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Scalar multiplication is preserved by coordinate inclusions and the cyclic spectral maps. These are the intertwining identities for the common central Hilbert model.

theorem OAI.KadisonSimilarity.l2MapIsometry_scalar_intertwines line 21

def OAI.KadisonSimilarity.coordinateIntertwinerData line 35

Source documentation

Compose a scalar intertwiner with a fixed Hilbert coordinate and retain its intertwining identity without unfolding the scalar construction.

def coordinateIntertwinerData (ν : Measure X) (V : ℂ →ₗᵢ[ℂ] H)
    (d : {J : Lp ℂ 2 ν →ₗᵢ[ℂ] Lp ℂ 2 μ //
      ∀ (f : C(X, ℂ)) (ξ : Lp ℂ 2 ν),
        J (continuousL2Mul ν f ξ) = continuousL2Mul μ f (J ξ)}) :
    {J : Lp ℂ 2 ν →ₗᵢ[ℂ] Lp H 2 μ //
      ∀ (f : C(X, ℂ)) (ξ : Lp ℂ 2 ν),
        J (continuousL2Mul ν f ξ) = VectorL2.continuousL2Mul μ f (J ξ)} := by
…

Mentions: OAI.KadisonSimilarity.continuousL2Mul, OAI.KadisonSimilarity.VectorL2.continuousL2Mul

theorem OAI.KadisonSimilarity.spectralDensityIsometryOfEq_intertwines line 52
def OAI.KadisonSimilarity.spectralDensityIntertwinerData line 61
Source documentation
Retain the intertwining property with the chosen measure-change isometry, so later concrete instantiations do not unfold its extension construction.
```
def spectralDensityIntertwinerData (heq : squaredDensityMeasure μ u = ν) :
    {J : Lp ℂ 2 ν →ₗᵢ[ℂ] Lp ℂ 2 μ //
      ∀ (f : C(X, ℂ)) (ξ : Lp ℂ 2 ν),
        J (continuousL2Mul ν f ξ) = continuousL2Mul μ f (J ξ)} :=
…
```
Mentions: OAI.KadisonSimilarity.squaredDensityMeasure, OAI.KadisonSimilarity.continuousL2Mul
theorem OAI.KadisonSimilarity.commutativeCyclicIsometry_intertwines line 78