OAI/Analysis/BoundedHochschild/PositiveKernelActions.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Transport of finite kernel vectors and the corresponding bounded maps on their pre-Hilbert spaces.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.kernelForm_mapDomain_left line 16
  2. lemma OAI.BoundedHochschild.KadisonRingrose.kernelForm_mapDomain_right line 26
  3. lemma OAI.BoundedHochschild.KadisonRingrose.kernelForm_mapDomain line 38
  4. lemma OAI.BoundedHochschild.KadisonRingrose.kernelPre_norm_sq line 44
  5. def OAI.BoundedHochschild.KadisonRingrose.kernelPreMap line 50

    Source documentation

    A map of labels bounded for the kernel quadratic form induces a bounded linear map on the finite kernel vectors.

    def kernelPreMap (K : Matrix I I ℂ) (hK : K.PosSemidef) (f : I → I)
    (C : ℝ) (hC : 0 ≤ C)
    (hf : ∀ x : I →₀ ℂ, (kernelForm (fun i j => K (f i) (f j)) x x).re ≤
      C ^ 2 * (kernelForm K x x).re) :
    PositiveKernelPreSpace K hK →L[ℂ] PositiveKernelPreSpace K hK :=
…

    Mentions: OAI.BoundedHochschild.KadisonRingrose.kernelForm, OAI.BoundedHochschild.KadisonRingrose.PositiveKernelPreSpace

  6. lemma OAI.BoundedHochschild.KadisonRingrose.kernelPreMap_apply line 67