Ridge Function Approximation Theorem Formalization

Stream: mathlib4

[Leorasz]

Hi guys,

I just finished a formalization of a proof about the density of the span of ridge functions in the space of continuous functions on a compact subset of R^n. It's not perfect and I'll probably work on it more but I wanted to see if there was any possibility of it getting in Mathlib4. It's mostly more of an applied math subject in approximation theory but has many applications and the theorem is pivotal in the 1993 Leshno et al. proof of the universal approximation theorem for neural networks, which is the paper that seems to have the best proof. I looked at the guide for contributing to Mathlib4 but I'm still shaky whether or not this meets the criteria.

Currently I am planning on defining ridge functions better for future use and making some theorems to make it easier to prove certain Ωs are valid and trying to clean up the proof as best I can, but please let me know if there's any more changes that could make it any better, and also whether or not this is a valid topic/good enough quality for Mathlib4.

Proof: https://github.com/Leorasz/Ridge_Function_UAT

[Kevin Buzzard]

You should make it eg a file in a branch of mathlib or something, right now there seems to be no information on which version of lean or mathlib it compiles with

[Kim Morrison]

(Or run lake initand set this up as a project depending on Mathlib. As is this code is unusable.)