OAI/Analysis/KadisonKastler/FixedProductAbsorption.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Absorbing an extra family of lambda sites

The explicit even/odd bijection is applied to finite-site coordinates of the actual product representation. The published input contains only construction, sum and reindexing facts for pointed products.

  1. theorem OAI.KadisonKastler.TwoRatioProductModel.absorbs_powers line 23

    Source documentation

    The fixed two-ratio product absorbs the lambda-only Powers product, by an actual vector-preserving unitary between the Hilbert spaces.

    theorem TwoRatioProductModel.absorbs_powers (P : TwoRatioProductModel.{u})
    (hProduct : PublishedPointedMatrixOperations.{u}) :
    ∃ R : PointedMatrixProduct.{u} (fun _ : ℕ => fixedProductLambda),
    ∃ U : SpatialHilbert P.K R.K ≃ₗᵢ[ℂ] P.K,
      U (tensorVector R.vector P.stages.vector) = P.stages.vector ∧
      ∀ x : SpatialHilbert P.K R.K →L[ℂ] SpatialHilbert P.K R.K,
        x ∈ spatialProductAlgebra P.stages.algebra R.algebra ↔
          U.conjStarAlgEquiv x ∈ P.stages.algebra := by
…

    Mentions: OAI.KadisonKastler.fixedProductLambda, OAI.KadisonKastler.tensorVector, OAI.KadisonKastler.spatialProductAlgebra