feat(analysis/inner_product_space/reproducing_kernel): Reproducing kernel Hilbert spaces

[shingtaklam1324]

Add the definition of a reproducing kernel Hilbert space and some basic definitions, such as evaluation as a continuous linear map and the kernel of an RKHS.

---

[shingtaklam1324]

The linter is not happy with this, since in the fun_like instance 𝕜 is not used. Not sure what to do here.

[j-loreaux]

We were just discussing here about the possibility of unbundling the analysis classes from the algebraic classes. If that were the case, could you just define an rkhs as something that takes H : submodule 𝕜 (X → V), as an argument, and then extends inner_product_space 𝕜 H and has a field continuous_eval?

[shingtaklam1324]

I can define it to be a predicate on a submodule 𝕜 (X → V) as well. The issue with that approach is that

example (H : submodule 𝕜 (X → V)) : topological_space H := infer_instance

works, since it has the subspace topology of the prod topology. If I define an inner product space instance on H then there would be two distinct topologies. I'm not sure how unbundling the topological structure and the algebraic structure will help here, since it's just picking up the subtype topology.

So I suppose what I need is a way to have a vector subspace of X → V that isn't a topological subspace of X → V?

[j-loreaux]

What about using a type synonym, like algebraic_submodule (terrible name) where you only copy over the algebraic structure? This would incur a bit of overhead, but I think it wouldn't be so bad once you get past the basic API. (Of course, I could be wrong here.)

[j-loreaux]

@shingtaklam1324 I haven't checked this first idea, so it may not work, but what about just temporarily disabling the topological_space instance on functions. For example, can you just do local attribute [-instance] Pi.topological_space? Then you might be able to use an submodule 𝕜 (X → V) and avoid the topological structure.

As a second option which I'm fairly certain will work: instead of having an actual submodule or extending fun_like, just use an injective linear map, like this

class rkhs (H : Type*) [inner_product_space 𝕜 H] :=
(to_funs : H →ₗ[𝕜] (X → V))
(to_funs_injective : function.injective (to_funs : H → X → V))
(continuous_eval' : ∀ (x : X), continuous (λ (f : H), to_funs f x))

You can then set up a fun_like instance in the natural way. I think if the first one doesn't work, then the second is definitely the way to go unless I'm missing something.

Note: with this approach, rkhs.add_apply' and rkhs.smul_apply' become simp lemmas about your fun_like instance (i.e., ⇑(f + g) = ⇑f + ⇑g and ⇑(c • f) = c • ⇑f), and you can write down a "new" continuous_eval that is phrased as ∀ x : X, continuous (λ f : H, ⇑f x).

[shingtaklam1324]

There's probably a strengthening to filters other than at_top and ℕ indexed functions?

[dupuisf]

This design seems dangerous: fun_like doesn't come with any addition, which means that the addition that appears here comes from the [inner_product_space 𝕜 H] instance, which might be completely unrelated to pointwise addition. Also, in many cases this means that you would wind up with two has_add instances on H. I'm not sure what the right solution to this is at this point, but it does mean that the design should be rethought.

[shingtaklam1324]

I see... I think there is a branch somewhere that people have added typeclasses for saying when a fun_like class has pointwise ops, with the same design as what I have here, but that hasn't been merged to master.

Also I'm not sure how you'd end up with two different additions on H? This is just saying that the addition from the inner_product_space should be pointwise, not defining a new addition.

I suppose an alternative would be to define it as a predicate on a submodule of X -> k. The issue with that though is that comes with a topology (the product topology) which might not be the one that I want for arbitrary inner products, so I'll need an alias that preserves the module and pointwise structure, but not the topological structure.

[shingtaklam1324]

https://github.com/leanprover-community/mathlib/blob/0a8652754854bb42b93e7c951cd748fb6a3a4330/src/algebra/group/fun_like.lean

[dupuisf]

I agree that a type class like this would probably be the way to go, in fact something like this is probably going to be required at some point to have operator algebras.

[dupuisf]

(On second thought, you're right that my concern about having multiple additions is probably unfounded.)

[dupuisf]

(On second thought, you're right that my concern about multiple addition instances is probably unfounded.)

[urkud]

Suggested change