Formalize the Leshno universal approximation theorem

[yuanyi-350]

• mathlib4#43746 ([Merged by Bors] - feat(Topology/ContinuousMap): add coeFnCLM leanprover-community/mathlib4#43746)
• mathlib4#43747 (feat(Analysis/LocallyConvex): characterize dense submodules by annihilators leanprover-community/mathlib4#43747)
• mathlib4#41767 (feat: the line derivative of a distribution induced by a differentiable function leanprover-community/mathlib4#41767)
• mathlib4#41426 (feat: add symmetric multilinear maps leanprover-community/mathlib4#41426)

Formalizes the continuous Leshno–Lin–Pinkus–Schocken theorem: for every positive input dimension and continuous activation σ, biased single-hidden-layer networks are uniformly dense on every compact set if and only if σ is not a polynomial.

Roadmap

All files below are in LeanMachineLearning/NeuralNetwork/UniversalApproximation/ , Here, universal means uniformly dense on every compact set.

• Leshno.lean — main theorem: on a nontrivial real inner-product space, a continuous activation is universal if and
  only if it is nonpolynomial.
• Nonpolynomial.lean: every continuous nonpolynomial activation is universal.
• PolynomialObstruction.lean: for every polynomial activation on a nontrivial real inner-product space, there exists a
  finite compact set on which its networks are not dense.
• Discriminatory.lean: universality is equivalent to the following dual criterion: on every compact K, any continuous
  linear functional on C(K, ℝ) vanishing on all neurons is zero. In particular, a smooth activation is universal if
  none of its derivatives is identically zero.
• Convolution.lean: if φ ∗ σ is universal for some compactly supported continuous kernel φ, then σ is universal.

The proof also establishes the equivalence for every nontrivial real inner-product space.

AI usage: I planned the blueprint in advance and used GPT-5.6 Sol to help implement the code according to that blueprint.

Closes #244.