Formalize the Leshno universal approximation theorem

LeanMachineLearning.lean

@@ -1,14 +1,23 @@
 module  -- shake: keep-all --deprecated_module: ignore
 
+public import LeanMachineLearning.ForMathlib.Algebra.Polynomial.Function
+public import LeanMachineLearning.ForMathlib.Analysis.Calculus.ContinuousMapComposition
 public import LeanMachineLearning.ForMathlib.Analysis.Convex.Bregman.Basic
 public import LeanMachineLearning.ForMathlib.Analysis.Convex.Subgradient.Basic
 public import LeanMachineLearning.ForMathlib.Analysis.Convex.Subgradient.Deriv
+public import LeanMachineLearning.ForMathlib.Analysis.Distribution.Polynomial
+public import LeanMachineLearning.ForMathlib.Analysis.Distribution.PolynomialCharacterization
+public import LeanMachineLearning.ForMathlib.Analysis.Distribution.TestFunction
+public import LeanMachineLearning.ForMathlib.Analysis.Distribution.TestFunction.Normalize
+public import LeanMachineLearning.ForMathlib.Analysis.LocallyConvex.Annihilator
 public import LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.ChainRule
 public import LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.CompProd
 public import LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.Convex
 public import LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.DataProcessing
 public import LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.MapSequence
 public import LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.Restrict
+public import LeanMachineLearning.ForMathlib.LinearAlgebra.Multilinear.Polarization
+public import LeanMachineLearning.ForMathlib.MeasureTheory.Integral.ClosedSubmodule
 public import LeanMachineLearning.ForMathlib.MeasureTheory.Measurable
 public import LeanMachineLearning.ForMathlib.MeasureTheory.MeasurableSpace.Embedding
 public import LeanMachineLearning.ForMathlib.MeasureTheory.MeasurableSpace.Sigma
@@ -38,7 +47,17 @@ public import LeanMachineLearning.ForMathlib.Probability.Moments.SubExponential
 public import LeanMachineLearning.ForMathlib.Probability.Moments.SubGaussian
 public import LeanMachineLearning.ForMathlib.Probability.Process.HittingTime
 public import LeanMachineLearning.ForMathlib.Probability.WithDensity
+public import LeanMachineLearning.ForMathlib.Topology.Algebra.Module.FiniteDimension
+public import LeanMachineLearning.ForMathlib.Topology.ContinuousMap.Algebra
+public import LeanMachineLearning.ForMathlib.Topology.ContinuousMap.InnerProduct
+public import LeanMachineLearning.ForMathlib.Topology.ContinuousMap.Moments
 public import LeanMachineLearning.ForMathlib.Topology.Instances.ENNReal.Lemmas
+public import LeanMachineLearning.NeuralNetwork.Shallow.Basic
+public import LeanMachineLearning.NeuralNetwork.UniversalApproximation.Convolution
+public import LeanMachineLearning.NeuralNetwork.UniversalApproximation.Discriminatory
+public import LeanMachineLearning.NeuralNetwork.UniversalApproximation.Leshno
+public import LeanMachineLearning.NeuralNetwork.UniversalApproximation.Nonpolynomial
+public import LeanMachineLearning.NeuralNetwork.UniversalApproximation.PolynomialObstruction
 public import LeanMachineLearning.Online.Bandit.Algorithms.ETC
 public import LeanMachineLearning.Online.Bandit.Algorithms.Regret.BayesRegretTS
 public import LeanMachineLearning.Online.Bandit.Algorithms.Regret.ETC

LeanMachineLearning/ForMathlib/Algebra/Polynomial/Function.lean

@@ -0,0 +1,94 @@
+/-
+Copyright (c) 2026 Yi Yuan. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yi Yuan
+-/
+module
+
+public import Mathlib.Topology.ContinuousMap.Polynomial
+
+/-!
+# Functions represented by polynomials
+
+This file defines the predicate that a function is globally represented by a univariate
+polynomial. This is different from the local analytic predicate `CPolynomialOn`.
+-/
+
+@[expose] public section
+
+open Polynomial
+
+namespace Function
+
+/-- A function from a semiring to itself is polynomial if it agrees everywhere with the
+evaluation of a univariate polynomial. -/
+def IsPolynomial {R : Type*} [Semiring R] (f : R → R) : Prop :=
+  ∃ p : R[X], ∀ x, p.eval x = f x
+
+namespace IsPolynomial
+
+section CommSemiring
+
+variable {R : Type*} [CommSemiring R] {f g : R → R}
+
+protected theorem const (c : R) : IsPolynomial (fun _ : R ↦ c) :=
+  ⟨C c, by simp⟩
+
+protected theorem id : IsPolynomial (id : R → R) :=
+  ⟨X, by simp⟩
+
+protected theorem add (hf : IsPolynomial f) (hg : IsPolynomial g) :
+    IsPolynomial (f + g) := by
+  obtain ⟨p, hp⟩ := hf
+  obtain ⟨q, hq⟩ := hg
+  exact ⟨p + q, fun x ↦ by simp only [eval_add, Pi.add_apply, hp x, hq x]⟩
+
+protected theorem mul (hf : IsPolynomial f) (hg : IsPolynomial g) :
+    IsPolynomial (f * g) := by
+  obtain ⟨p, hp⟩ := hf
+  obtain ⟨q, hq⟩ := hg
+  exact ⟨p * q, fun x ↦ by simp only [eval_mul, Pi.mul_apply, hp x, hq x]⟩
+
+protected theorem comp (hf : IsPolynomial f) (hg : IsPolynomial g) :
+    IsPolynomial (f ∘ g) := by
+  obtain ⟨p, hp⟩ := hf
+  obtain ⟨q, hq⟩ := hg
+  exact ⟨p.comp q, fun x ↦ by rw [eval_comp, hp, hq]; rfl⟩
+
+/-- A bundled continuous map is polynomial exactly when it is in the range of
+`Polynomial.toContinuousMap`. -/
+theorem iff_exists_toContinuousMap [TopologicalSpace R] [IsTopologicalSemiring R]
+    (f : C(R, R)) :
+    IsPolynomial f ↔ ∃ p : R[X], p.toContinuousMap = f := by
+  constructor
+  · rintro ⟨p, hp⟩
+    exact ⟨p, ContinuousMap.ext hp⟩
+  · rintro ⟨p, rfl⟩
+    exact ⟨p, by simp⟩
+
+protected theorem continuous [TopologicalSpace R] [IsTopologicalSemiring R]
+    (hf : IsPolynomial f) : Continuous f := by
+  obtain ⟨p, hp⟩ := hf
+  rw [← funext hp]
+  exact p.continuous
+
+end CommSemiring
+
+section CommRing
+
+variable {R : Type*} [CommRing R] {f g : R → R}
+
+protected theorem neg (hf : IsPolynomial f) : IsPolynomial (-f) := by
+  obtain ⟨p, hp⟩ := hf
+  exact ⟨-p, fun x ↦ by simp only [eval_neg, Pi.neg_apply, hp x]⟩
+
+protected theorem sub (hf : IsPolynomial f) (hg : IsPolynomial g) :
+    IsPolynomial (f - g) := by
+  rw [sub_eq_add_neg]
+  exact hf.add hg.neg
+
+end CommRing
+
+end IsPolynomial
+
+end Function

LeanMachineLearning/ForMathlib/Analysis/Calculus/ContinuousMapComposition.lean

@@ -0,0 +1,81 @@
+/-
+Copyright (c) 2026 Yi Yuan. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yi Yuan
+-/
+module
+
+public import Mathlib.Analysis.Calculus.Deriv.Comp
+public import Mathlib.Analysis.Calculus.Deriv.Mul
+public import Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
+public import Mathlib.Topology.ContinuousMap.Algebra
+public import Mathlib.Topology.ContinuousMap.Compact
+
+/-!
+# Differentiating curves of continuous maps
+
+This file supplies a general criterion for differentiating a curve with values in `C(X, E)`
+when `X` is compact: pointwise differentiability and continuity of the proposed derivative as a
+`C(X, E)`-valued curve suffice.  As an application, it differentiates a continuously
+differentiable function after composition with a continuously varying affine argument.
+
+The results are stated for maps into an arbitrary real Banach space rather than only for
+real-valued maps.
+-/
+
+open MeasureTheory
+
+universe u v
+
+@[expose] public section
+
+namespace HasDerivAt
+
+variable {X : Type u} {E : Type v} [TopologicalSpace X] [CompactSpace X]
+  [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
+
+/-- A curve of continuous maps has a derivative if all of its evaluations have the proposed
+derivative and the proposed derivative is continuous in the uniform norm.
+
+The compactness of `X` equips `C(X, E)` with its supremum norm.  The proof uses the fundamental
+theorem of calculus after applying each continuous evaluation map. -/
+theorem continuousMap_of_continuous {f f' : ℝ → C(X, E)}
+    (hf : ∀ x t, HasDerivAt (fun s ↦ f s x) (f' t x) t) (hf' : Continuous f') (t : ℝ) :
+    HasDerivAt f (f' t) t := by
+  have hfi : ∀ a b, IntervalIntegrable f' volume a b :=
+    fun a b ↦ hf'.intervalIntegrable a b
+  let q : ℝ → C(X, E) :=
+    (fun _ ↦ f 0) + fun s ↦ ∫ r in 0..s, f' r
+  have hEq : q = f := by
+    funext s
+    apply ContinuousMap.ext
+    intro x
+    have hFTC : ∫ r in 0..s, (ContinuousMap.evalCLM ℝ x) (f' r) = f s x - f 0 x :=
+      intervalIntegral.integral_eq_sub_of_hasDerivAt (fun r _ ↦ hf x r)
+        (((ContinuousMap.evalCLM ℝ x).continuous.comp hf').intervalIntegrable 0 s)
+    change f 0 x + (ContinuousMap.evalCLM ℝ x) (∫ r in 0..s, f' r) = f s x
+    rw [← ContinuousLinearMap.intervalIntegral_comp_comm
+      (ContinuousMap.evalCLM ℝ x) (hfi 0 s), hFTC]
+    simp
+  have hder : HasDerivAt q (0 + f' t) t :=
+    (hasDerivAt_const t (f 0)).add (hf'.integral_hasStrictDerivAt 0 t).hasDerivAt
+  simpa [hEq] using hder
+
+/-- Compose a differentiable Banach-valued function with the family of affine arguments
+`x ↦ u x + t * v x`.  Differentiation in `t` may be performed in the uniform norm on
+`C(X, E)`.
+
+Bundling `g` and `dg` as continuous maps records exactly the continuity needed to upgrade the
+pointwise derivatives `hg` to a derivative in the function space. -/
+theorem continuousMap_comp_affine {g dg : C(ℝ, E)} (hg : ∀ y, HasDerivAt g (dg y) y)
+   (u v : C(X, ℝ)) (t : ℝ) : HasDerivAt (fun s ↦ g.comp (u + ContinuousMap.const X s * v))
+    ⟨fun x ↦ v x • dg (u x + t * v x), by fun_prop⟩ t := by
+  apply continuousMap_of_continuous (t := t)
+  · intro x s
+    convert (hg (u x + s * v x)).scomp s
+        ((hasDerivAt_const s (u x)).add (hasDerivAt_mul_const (v x))) using 1 <;>
+      simp [Function.comp_def]
+  · apply ContinuousMap.continuous_of_continuous_uncurry
+    exact (v.continuous.comp continuous_snd).smul <| by fun_prop
+
+end HasDerivAt