Theorems · Inductive type · functional analysis

RKHS

(𝕜 : outParam (Type u_1)) →
  (H : Type u_2) →
    outParam (Type u_3) →
      (V : outParam (Type u_4)) →
        [inst : RCLike 𝕜] →
          [inst_1 : NormedAddCommGroup V] →
            [InnerProductSpace 𝕜 V] →
              [inst_3 : NormedAddCommGroup H] → [InnerProductSpace 𝕜 H] → Type (max (max u_2 u_3) u_4)

A reproducing kernel Hilbert space is a Hilbert space with an injection to functions mapping into another Hilbert space, such that point evaluation is continuous.

Defined in

Mathlib.Analysis.InnerProductSpace.Reproducing

Cited by

28 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms

Assumes

RCLikeNormedAddCommGroupInnerProductSpaceNormedAddCommGroupInnerProductSpace