Theorems · Definition · functional analysis

RKHS.coeCLM

(𝕜 : outParam (Type u_1)) →
  {H : Type u_2} →
    {X : outParam (Type u_3)} →
      {V : outParam (Type u_4)} →
        {inst : RCLike 𝕜} →
          {inst_1 : NormedAddCommGroup V} →
            {inst_2 : InnerProductSpace 𝕜 V} →
              {inst_3 : NormedAddCommGroup H} → {inst_4 : InnerProductSpace 𝕜 H} → [self : RKHS 𝕜 H X V] → H →L[𝕜] X → V

Continuous injection to functions from the reproducing kernel Hilbert space H to functions from the domain X to the Hilbert space V

Defined in

Mathlib.Analysis.InnerProductSpace.Reproducing

Cited by

13 results in Mathlib

Foundations

Depth 66 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RKHS