Operations on RKHS

This file implements the maps that show how RKHSs created from kernels formed by applying operations to a set of kernels relate to the RKHSs of the constituant kernels.

main definitions

• generator: the operator (f, g) ↦ ⇑f + ⇑g inducing the RKHS H + H'.
• OfKernelAddEquiv: isometric equivalence between the RKHS OfKernel (K + K') and the quotient space over OfKernel K × OfKernel K'.
• projection: isometry yielding the elements of H × H' achieving the norm of H + H'.

def RKHS.Add'.generator {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (H : Type u_4) [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (H' : Type u_5) [NormedAddCommGroup H'] [InnerProductSpace 𝕜 H'] [RKHS 𝕜 H X V] [RKHS 𝕜 H' X V] : WithLp 2 (H × H') →L[𝕜] X → V

The operator (f, g) ↦ ⇑f + ⇑g, where addition is in X → V.

Equations

• RKHS.Add'.generator H H' = (RKHS.coeCLM 𝕜).coprod (RKHS.coeCLM 𝕜) ∘SL ↑(WithLp.prodContinuousLinearEquiv 2 𝕜 H H')

@[simp]

theorem RKHS.Add'.generator_apply {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] {H' : Type u_5} [NormedAddCommGroup H'] [InnerProductSpace 𝕜 H'] [RKHS 𝕜 H X V] [RKHS 𝕜 H' X V] (f : H) (g : H') (x : X) : (generator H H') (WithLp.toLp 2 (f, g)) x = f x + g x

instance RKHS.Add'.instIsClosedWithLpOfNatENNRealProdCoeSubmoduleKerForallGenerator {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (H : Type u_4) [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (H' : Type u_5) [NormedAddCommGroup H'] [InnerProductSpace 𝕜 H'] [RKHS 𝕜 H X V] [RKHS 𝕜 H' X V] : IsClosed ↑(↑(generator H H')).ker

@[reducible, inline]

abbrev RKHS.Add'.sumSpace {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (H : Type u_4) [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (H' : Type u_5) [NormedAddCommGroup H'] [InnerProductSpace 𝕜 H'] [RKHS 𝕜 H X V] [RKHS 𝕜 H' X V] : Type (max (max u_5 u_4) u_4 u_5)

The sum of two RKHS embedding in the same space of functions X → V.

Equations

• RKHS.Add'.sumSpace H H' = (WithLp 2 (H × H') ⧸ (↑(RKHS.Add'.generator H H')).ker)

def RKHS.Add'.«term_+_» : Lean.TrailingParserDescr

H + H' is shorthand for the RKHS sumSpace H H', which is the sum of the two RKHS.

Equations

• RKHS.Add'.«term_+_» = Lean.ParserDescr.trailingNode `RKHS.Add'.«term_+_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " + ") (Lean.ParserDescr.cat `term 51))

@[instance_reducible]

instance RKHS.Add'.instSumSpace {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (H : Type u_4) [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (H' : Type u_5) [NormedAddCommGroup H'] [InnerProductSpace 𝕜 H'] [RKHS 𝕜 H X V] [RKHS 𝕜 H' X V] [CompleteSpace H] [CompleteSpace H'] : RKHS 𝕜 (sumSpace H H') X V

Equations

• RKHS.Add'.instSumSpace H H' = { coeCLM := (↑(RKHS.Add'.generator H H')).ker.liftQL (RKHS.Add'.generator H H') ⋯, coeCLM_injective := ⋯ }

theorem RKHS.Add'.mk_eq {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (H : Type u_4) [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (H' : Type u_5) [NormedAddCommGroup H'] [InnerProductSpace 𝕜 H'] [RKHS 𝕜 H X V] [RKHS 𝕜 H' X V] [CompleteSpace H] [CompleteSpace H'] (f : WithLp 2 (H × H')) : ⇑(Submodule.Quotient.mk f) = (generator H H') f

theorem RKHS.Add'.kerFun_mem_orthogonal {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (H : Type u_4) [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (H' : Type u_5) [NormedAddCommGroup H'] [InnerProductSpace 𝕜 H'] [RKHS 𝕜 H X V] [RKHS 𝕜 H' X V] [CompleteSpace H] [CompleteSpace H'] [CompleteSpace V] (x : X) (v : V) : WithLp.toLp 2 ((kerFun H x) v, (kerFun H' x) v) ∈ (↑(generator H H')).kerᗮ

theorem RKHS.Add'.kerFun_apply_eq_mk {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (H : Type u_4) [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (H' : Type u_5) [NormedAddCommGroup H'] [InnerProductSpace 𝕜 H'] [RKHS 𝕜 H X V] [RKHS 𝕜 H' X V] [CompleteSpace H] [CompleteSpace H'] [CompleteSpace V] (x : X) (v : V) : (kerFun (sumSpace H H') x) v = Submodule.Quotient.mk (WithLp.toLp 2 ((kerFun H x) v, (kerFun H' x) v))

theorem RKHS.Add'.kernel_sum_eq_sum_of_kernel {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (H : Type u_4) [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (H' : Type u_5) [NormedAddCommGroup H'] [InnerProductSpace 𝕜 H'] [RKHS 𝕜 H X V] [RKHS 𝕜 H' X V] [CompleteSpace H] [CompleteSpace H'] [CompleteSpace V] : kernel (sumSpace H H') = kernel H + kernel H'

theorem RKHS.Add'.instFactPosSemidefContinuousLinearMapIdHAddMatrix {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [CompleteSpace V] (K K' : Matrix X X (V →L[𝕜] V)) [Fact K.PosSemidef] [Fact K'.PosSemidef] : Fact (K + K').PosSemidef

noncomputable def RKHS.Add'.OfKernelAddEquiv {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [CompleteSpace V] (K K' : Matrix X X (V →L[𝕜] V)) [Fact K.PosSemidef] [Fact K'.PosSemidef] : OfKernel (K + K') ≃ₗᵢ[𝕜] sumSpace (OfKernel K) (OfKernel K')

The RKHSs constructed from the sum of two kernels is linearly isometrically isomorphic to the sum of the RKHSs created by the consituant kernels.

Equations

• RKHS.Add'.OfKernelAddEquiv K K' = RKHS.equiv ⋯

noncomputable def RKHS.Add'.projection {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (H : Type u_4) [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (H' : Type u_5) [NormedAddCommGroup H'] [InnerProductSpace 𝕜 H'] [RKHS 𝕜 H X V] [RKHS 𝕜 H' X V] [CompleteSpace H] [CompleteSpace H'] : sumSpace H H' →ₗᵢ[𝕜] WithLp 2 (H × H')

Projection that takes a function f : H + H' to the unique pair in H × H' that achieves its norm.

Equations

• RKHS.Add'.projection H H' = (↑(RKHS.Add'.generator H H')).kerᗮ.subtypeₗᵢ.comp (↑(RKHS.Add'.generator H H')).ker.quotientEquivOrthogonal.toLinearIsometry

@[simp]

theorem RKHS.Add'.projection_apply {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (H : Type u_4) [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (H' : Type u_5) [NormedAddCommGroup H'] [InnerProductSpace 𝕜 H'] [RKHS 𝕜 H X V] [RKHS 𝕜 H' X V] [CompleteSpace H] [CompleteSpace H'] (f : sumSpace H H') : (projection H H') f = (⇑(↑(generator H H')).kerᗮ.subtype ∘ ⇑(↑(generator H H')).ker.quotientEquivOrthogonal) f

theorem RKHS.Add'.range_projection {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (H : Type u_4) [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (H' : Type u_5) [NormedAddCommGroup H'] [InnerProductSpace 𝕜 H'] [RKHS 𝕜 H X V] [RKHS 𝕜 H' X V] [CompleteSpace H] [CompleteSpace H'] : (projection H H').range = (↑(generator H H')).kerᗮ

theorem RKHS.Add'.mk_projection {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] {H' : Type u_5} [NormedAddCommGroup H'] [InnerProductSpace 𝕜 H'] [RKHS 𝕜 H X V] [RKHS 𝕜 H' X V] [CompleteSpace H] [CompleteSpace H'] (f : sumSpace H H') : Submodule.Quotient.mk ((projection H H') f) = f

theorem RKHS.Add'.projection_kerFun {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (H : Type u_4) [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (H' : Type u_5) [NormedAddCommGroup H'] [InnerProductSpace 𝕜 H'] [RKHS 𝕜 H X V] [RKHS 𝕜 H' X V] [CompleteSpace H] [CompleteSpace H'] [CompleteSpace V] (x : X) (v : V) : (projection H H') ((kerFun (sumSpace H H') x) v) = WithLp.toLp 2 ((kerFun H x) v, (kerFun H' x) v)

theorem RKHS.Add'.norm_sq_kerFun_add {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (H : Type u_4) [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (H' : Type u_5) [NormedAddCommGroup H'] [InnerProductSpace 𝕜 H'] [RKHS 𝕜 H X V] [RKHS 𝕜 H' X V] [CompleteSpace H] [CompleteSpace H'] [CompleteSpace V] (x : X) (v : V) : ‖(kerFun (sumSpace H H') x) v‖ ^ 2 = ‖(kerFun H x) v‖ ^ 2 + ‖(kerFun H' x) v‖ ^ 2

theorem RKHS.Add'.exists_eq_add_and_norm_sq_eq_add {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (H : Type u_4) [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (H' : Type u_5) [NormedAddCommGroup H'] [InnerProductSpace 𝕜 H'] [RKHS 𝕜 H X V] [RKHS 𝕜 H' X V] [CompleteSpace H] [CompleteSpace H'] (f : sumSpace H H') : ∃ (f₁ : H) (f₂ : H'), ⇑f = ⇑f₁ + ⇑f₂ ∧ ‖f‖ ^ 2 = ‖f₁‖ ^ 2 + ‖f₂‖ ^ 2

theorem RKHS.Add'.norm_sq_le {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (H : Type u_4) [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (H' : Type u_5) [NormedAddCommGroup H'] [InnerProductSpace 𝕜 H'] [RKHS 𝕜 H X V] [RKHS 𝕜 H' X V] [CompleteSpace H] [CompleteSpace H'] (f : sumSpace H H') (f₁ : H) (f₂ : H') (h : ⇑f = ⇑f₁ + ⇑f₂) : ‖f‖ ^ 2 ≤ ‖f₁‖ ^ 2 + ‖f₂‖ ^ 2