diff --git a/LeanMachineLearning.lean b/LeanMachineLearning.lean index ef058a9c..59695c25 100644 --- a/LeanMachineLearning.lean +++ b/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 diff --git a/LeanMachineLearning/ForMathlib/Algebra/Polynomial/Function.lean b/LeanMachineLearning/ForMathlib/Algebra/Polynomial/Function.lean new file mode 100644 index 00000000..a238272b --- /dev/null +++ b/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 diff --git a/LeanMachineLearning/ForMathlib/Analysis/Calculus/ContinuousMapComposition.lean b/LeanMachineLearning/ForMathlib/Analysis/Calculus/ContinuousMapComposition.lean new file mode 100644 index 00000000..ad9e65d6 --- /dev/null +++ b/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 diff --git a/LeanMachineLearning/ForMathlib/Analysis/Distribution/Polynomial.lean b/LeanMachineLearning/ForMathlib/Analysis/Distribution/Polynomial.lean new file mode 100644 index 00000000..154ee143 --- /dev/null +++ b/LeanMachineLearning/ForMathlib/Analysis/Distribution/Polynomial.lean @@ -0,0 +1,367 @@ +/- +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.Polynomial +public import Mathlib.Analysis.Distribution.Distribution +public import Mathlib.Analysis.Distribution.SchwartzSpace.Deriv +public import Mathlib.Analysis.Normed.Group.Bounded +public import Mathlib.Algebra.Exact.Basic +public import Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus +public import Mathlib.Topology.Algebra.Polynomial +public import LeanMachineLearning.ForMathlib.Algebra.Polynomial.Function + +/-! +# Regular distributions induced by polynomials + +This file proves that distributional differentiation agrees with classical differentiation for +regular distributions on the real line. The result is first established for functions with a +classical derivative and then iterated for arbitrary derivative towers. Polynomials are obtained as +a special case. + +The converse statement, that a distribution whose sufficiently high derivative vanishes is a +regular polynomial distribution, needs an additional exactness result for the derivative on the +space of test functions. In particular, one needs that every compactly supported smooth function +with integral zero has a compactly supported smooth primitive. That result is not currently +available in Mathlib. +-/ + +@[expose] public section + +open MeasureTheory +open scoped Distributions + +namespace Polynomial + +/-- Over a field of characteristic zero, formal differentiation of univariate polynomials is +surjective. + +This is the algebraic input for recovering a polynomial from its derivative. The construction +divides the coefficient of `X ^ n` by `n + 1`. -/ +theorem derivative_surjective_of_charZero {K : Type*} [Field K] [CharZero K] : + Function.Surjective (derivative : Polynomial K → Polynomial K) := by + intro p + refine ⟨p.sum fun n a ↦ C (a / (n + 1 : ℕ)) * X ^ (n + 1), ?_⟩ + rw [sum_def, derivative_sum] + simp only [derivative_C_mul_X_pow, Nat.add_sub_cancel] + calc + (∑ n ∈ p.support, C (p.coeff n / (n + 1 : ℕ) * (n + 1 : ℕ)) * X ^ n) = + ∑ n ∈ p.support, C (p.coeff n) * X ^ n := by + apply Finset.sum_congr rfl + intro n hn + congr 2 + rw [div_mul_cancel₀] + exact_mod_cast Nat.succ_ne_zero n + _ = p := p.as_sum_support_C_mul_X_pow.symm + +end Polynomial + +namespace MeasureTheory + +/-- The integral of an integrable continuous function over `Set.Iic y`, regarded as a function of +the upper endpoint `y`, has derivative equal to the integrand. + +This vector-valued version is obtained by comparing two lower-ray integrals and applying the +fundamental theorem of calculus to the resulting interval integral. -/ +theorem hasDerivAt_integral_Iic + {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] + {f : ℝ → F} (hf : Continuous f) (hfi : Integrable f) (b : ℝ) : + HasDerivAt (fun y ↦ ∫ x in Set.Iic y, f x) (f b) b := by + have hEq : (fun y ↦ ∫ x in Set.Iic y, f x) = + fun y ↦ (∫ x in b..y, f x) + ∫ x in Set.Iic b, f x := by + funext y + exact sub_eq_iff_eq_add.mp <| intervalIntegral.integral_Iic_sub_Iic + hfi.integrableOn hfi.integrableOn + rw [hEq] + exact (hf.integral_hasStrictDerivAt b b).hasDerivAt.add_const _ + +/-- If a compactly supported integrable function on the real line has integral zero, then its +indefinite integral over lower rays is compactly supported. + +This statement is independent of differentiability and works for functions with values in any +complete real normed space. -/ +theorem hasCompactSupport_integral_Iic_of_integral_eq_zero + {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] + {f : ℝ → F} (hfc : HasCompactSupport f) (hfi : Integrable f) + (hzero : ∫ x, f x = 0) : + HasCompactSupport (fun b ↦ ∫ x in Set.Iic b, f x) := by + obtain ⟨R, hR, hout⟩ := hfc.exists_pos_le_norm + apply HasCompactSupport.intro (isCompact_Icc : IsCompact (Set.Icc (-R) R)) + intro x hx + simp only [Set.mem_Icc, not_and_or, not_le] at hx + rcases hx with hx | hx + · apply setIntegral_eq_zero_of_forall_eq_zero + intro y hy + change y ≤ x at hy + apply hout y + rw [Real.norm_eq_abs, abs_of_nonpos] + · linarith + · linarith + · have hIoi : ∫ y in Set.Ioi x, f y = 0 := by + apply setIntegral_eq_zero_of_forall_eq_zero + intro y hy + change x < y at hy + apply hout y + rw [Real.norm_eq_abs, abs_of_nonneg] + · linarith + · linarith + have hsplit := intervalIntegral.integral_Iic_add_Ioi + (hfi.integrableOn : IntegrableOn f (Set.Iic x)) + (hfi.integrableOn : IntegrableOn f (Set.Ioi x)) + rwa [hIoi, hzero, add_zero] at hsplit + +/-- Every smooth compactly supported function on the real line with integral zero has a smooth +compactly supported primitive. + +The codomain is allowed to be any complete real normed space. This is the vector-valued analytic +core of exactness of differentiation and integration on real test functions. -/ +theorem exists_contDiff_primitive_hasCompactSupport + {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] + {f : ℝ → F} (hf : ContDiff ℝ (↑(⊤ : ℕ∞)) f) (hfc : HasCompactSupport f) + (hzero : ∫ x, f x = 0) : ∃ g : ℝ → F, ContDiff ℝ (↑(⊤ : ℕ∞)) g ∧ HasCompactSupport g ∧ + ∀ x, HasDerivAt g (f x) x := by + have hfcont : Continuous f := hf.continuous + have hfi : Integrable f := hfcont.integrable_of_hasCompactSupport hfc + let g : ℝ → F := fun b ↦ ∫ x in Set.Iic b, f x + have hgDeriv (x : ℝ) : HasDerivAt g (f x) x := hasDerivAt_integral_Iic hfcont hfi x + have hgderiv : deriv g = f := by + funext x + exact (hgDeriv x).deriv + have hgSmooth : ContDiff ℝ (↑(⊤ : ℕ∞)) g := by + rw [contDiff_infty_iff_deriv] + exact ⟨fun x ↦ (hgDeriv x).differentiableAt, hgderiv ▸ hf⟩ + exact ⟨g, hgSmooth, hasCompactSupport_integral_Iic_of_integral_eq_zero hfc hfi hzero, hgDeriv⟩ + +end MeasureTheory + +namespace LinearMap + +/-- A linear map annihilating the first map in an exact pair is determined by its value on any +element sent to `1` by the second map. + +This is the algebraic factorization argument underlying the fact that a distribution with zero +derivative is constant. -/ +theorem apply_eq_smul_apply_of_exact {R X Y : Type*} [CommRing R] + [AddCommGroup X] [Module R X] [AddCommGroup Y] [Module R Y] + (D : X →ₗ[R] X) (I : X →ₗ[R] R) (T : X →ₗ[R] Y) + (hExact : Function.Exact D I) {ρ : X} (hρ : I ρ = 1) + (hTD : ∀ x, T (D x) = 0) (x : X) : + T x = I x • T ρ := by + let ψ := x - I x • ρ + have hIψ : I ψ = 0 := by simp [ψ, hρ] + obtain ⟨θ, hθ⟩ := (hExact ψ).mp hIψ + have hTψ : T ψ = 0 := by + rw [← hθ] + exact hTD θ + calc + T x = T (ψ + I x • ρ) := by simp [ψ] + _ = I x • T ρ := by simp [hTψ] + +end LinearMap + +namespace TestFunction + +/-- On real-valued test functions on the real line, the directional derivative in direction `1` +is the usual one-dimensional derivative. -/ +lemma lineDerivCLM_one_apply {Ω : TopologicalSpace.Opens ℝ} (φ : 𝓓(Ω, ℝ)) (x : ℝ) : + (lineDerivCLM ℝ (1 : ℝ) φ : 𝓓(Ω, ℝ)) x = deriv φ x := by + rw [lineDerivCLM_apply_of_le] + · calc + _ = (fderiv ℝ (φ : ℝ → ℝ) x) 1 := + (φ.contDiff.differentiable (by simp)).differentiableAt.lineDeriv_eq_fderiv + _ = deriv (φ : ℝ → ℝ) x := fderiv_apply_one_eq_deriv + · simp + +/-- The analytic exactness property needed to recognize constant distributions on an open subset +of the real line: every test function of integral zero is the derivative of another test +function. + +This is a class so downstream distribution theory can be stated independently of the particular +construction of compactly supported primitives. -/ +class HasCompactSupportPrimitive (Ω : TopologicalSpace.Opens ℝ) : Prop where + exists_eq_lineDerivCLM (φ : 𝓓(Ω, ℝ)) (hφ : ∫ x, φ x = 0) : + ∃ ψ : 𝓓(Ω, ℝ), lineDerivCLM ℝ (1 : ℝ) ψ = φ + +/-- On the whole real line, smooth compactly supported primitives exist. -/ +instance instHasCompactSupportPrimitiveTop : + HasCompactSupportPrimitive (⊤ : TopologicalSpace.Opens ℝ) where + exists_eq_lineDerivCLM φ hφ := by + obtain ⟨g, hgSmooth, hgCompact, hgDeriv⟩ := + MeasureTheory.exists_contDiff_primitive_hasCompactSupport + φ.contDiff φ.hasCompactSupport hφ + let ψ : 𝓓((⊤ : TopologicalSpace.Opens ℝ), ℝ) := ⟨g, hgSmooth, hgCompact, by simp⟩ + refine ⟨ψ, ?_⟩ + ext x + rw [lineDerivCLM_one_apply] + simpa [ψ] using (hgDeriv x).deriv + +end TestFunction + +namespace Distribution + +open LineDeriv + +variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] + +/-- The distributional derivative of the regular distribution induced by `f` is the regular +distribution induced by the classical derivative of `f`. + +This vector-valued version only assumes the local integrability needed to define the two regular +distributions. -/ +theorem lineDerivCLM_ofFun_eq_of_hasDerivAt {Ω : TopologicalSpace.Opens ℝ} + {f f' : ℝ → F} (hf : ∀ x, HasDerivAt f (f' x) x) + (hfloc : LocallyIntegrableOn f Ω volume) + (hf'loc : LocallyIntegrableOn f' Ω volume) : + lineDerivCLM (1 : ℝ) (ofFun Ω f volume ⊤) = ofFun Ω f' volume ⊤ := by + ext φ + rw [lineDerivCLM_apply, ofFun_apply hfloc, ofFun_apply hf'loc] + let dφ : 𝓓(Ω, ℝ) := TestFunction.lineDerivCLM ℝ (1 : ℝ) φ + have hdφ (x : ℝ) : dφ x = deriv (φ : ℝ → ℝ) x := + TestFunction.lineDerivCLM_one_apply φ x + have hibp := MeasureTheory.integral_bilinear_hasDerivAt_right_eq_neg_left_of_integrable + (L := ContinuousLinearMap.lsmul ℝ ℝ) + (fun _ _ ↦ (φ.contDiff.differentiable (by simp)).differentiableAt.hasDerivAt) + (fun x _ ↦ hf x) (φ.integrable_smul hf'loc) + (by simpa [hdφ] using dφ.integrable_smul hfloc) (φ.integrable_smul hfloc) + simp only [ContinuousLinearMap.lsmul_apply] at hibp + rw [DFunLike.congr_fun rfl φ] + exact hibp.symm + +/-- The distributional derivative of a regular constant distribution vanishes. -/ +theorem lineDerivCLM_ofFun_const_eq_zero {Ω : TopologicalSpace.Opens ℝ} (c : F) : + (lineDerivCLM (1 : ℝ) (ofFun Ω (fun _ : ℝ ↦ c) volume ⊤) : 𝓓'(Ω, F)) = 0 := by + have hc : LocallyIntegrableOn (fun _ : ℝ ↦ c) Ω volume := + (continuous_const : Continuous (fun _ : ℝ ↦ c)).locallyIntegrable.locallyIntegrableOn Ω + rw [lineDerivCLM_ofFun_eq_of_hasDerivAt + (fun x ↦ hasDerivAt_const x c) hc locallyIntegrableOn_zero] + exact ofFun_zero + +/-- Integration annihilates derivatives of test functions. This is the easy half of the +derivative--integral exactness statement. -/ +theorem ofFun_one_comp_testFunction_lineDerivCLM_eq_zero {Ω : TopologicalSpace.Opens ℝ} : + (ofFun Ω (fun _ : ℝ ↦ (1 : ℝ)) volume ⊤) ∘ + (TestFunction.lineDerivCLM ℝ (1 : ℝ) : 𝓓(Ω, ℝ) → 𝓓(Ω, ℝ)) = 0 := by + funext φ + have h := congrArg (fun T : 𝓓'(Ω, ℝ) ↦ T φ) (lineDerivCLM_ofFun_const_eq_zero (Ω := Ω) (1 : ℝ)) + rw [lineDerivCLM_apply] at h + exact neg_eq_zero.mp h + +/-- Compactly supported primitives identify the range of differentiation with the kernel of +integration on test functions. -/ +theorem exact_testFunction_lineDerivCLM_of_hasCompactSupportPrimitive + {Ω : TopologicalSpace.Opens ℝ} [TestFunction.HasCompactSupportPrimitive Ω] : + Function.Exact (TestFunction.lineDerivCLM ℝ (1 : ℝ) : 𝓓(Ω, ℝ) → 𝓓(Ω, ℝ)) + (ofFun Ω (fun _ : ℝ ↦ (1 : ℝ)) volume ⊤) := by + apply Function.Exact.of_comp_of_mem_range ofFun_one_comp_testFunction_lineDerivCLM_eq_zero + intro φ hφ + have hOneLoc : LocallyIntegrableOn (fun _ : ℝ ↦ (1 : ℝ)) Ω volume := + (continuous_const : Continuous (fun _ : ℝ ↦ (1 : ℝ))).locallyIntegrable + |>.locallyIntegrableOn Ω + have hIntegral : ∫ x, φ x = 0 := by simpa [ofFun_apply hOneLoc] using hφ + exact TestFunction.HasCompactSupportPrimitive.exists_eq_lineDerivCLM φ hIntegral + +/-- A distribution with zero derivative is a regular constant distribution, provided the +derivative--integral pair on test functions is exact and a normalized test function is given. + +The exactness hypothesis precisely isolates the missing analytic input: every test function with +integral zero must have a compactly supported smooth primitive. -/ +theorem eq_ofFun_const_of_lineDerivCLM_eq_zero [CompleteSpace F] + {Ω : TopologicalSpace.Opens ℝ} (ρ : 𝓓(Ω, ℝ)) + (hρ : ofFun Ω (fun _ : ℝ ↦ (1 : ℝ)) volume ⊤ ρ = 1) + (hExact : Function.Exact (TestFunction.lineDerivCLM ℝ (1 : ℝ) : 𝓓(Ω, ℝ) → 𝓓(Ω, ℝ)) + (ofFun Ω (fun _ : ℝ ↦ (1 : ℝ)) volume ⊤)) (T : 𝓓'(Ω, F)) + (hT : (lineDerivCLM (1 : ℝ) T : 𝓓'(Ω, F)) = 0) : T = ofFun Ω (fun _ ↦ T ρ) volume ⊤ := by + have hOneLoc : LocallyIntegrableOn (fun _ : ℝ ↦ (1 : ℝ)) Ω volume := + (continuous_const : Continuous (fun _ : ℝ ↦ (1 : ℝ))).locallyIntegrable |>.locallyIntegrableOn Ω + have hConstLoc : LocallyIntegrableOn (fun _ : ℝ ↦ T ρ) Ω volume := + (continuous_const : Continuous (fun _ : ℝ ↦ T ρ)).locallyIntegrable |>.locallyIntegrableOn Ω + have hTD (φ : 𝓓(Ω, ℝ)) : T (TestFunction.lineDerivCLM ℝ (1 : ℝ) φ) = 0 := by + have h := congrArg (fun S : 𝓓'(Ω, F) ↦ S φ) hT + rw [lineDerivCLM_apply] at h + exact neg_eq_zero.mp h + ext φ + rw [ofFun_apply hConstLoc] + calc + T φ = (ofFun Ω (fun _ : ℝ ↦ (1 : ℝ)) volume ⊤) φ • T ρ := + LinearMap.apply_eq_smul_apply_of_exact + (TestFunction.lineDerivCLM ℝ (1 : ℝ)).toLinearMap + (ofFun Ω (fun _ : ℝ ↦ (1 : ℝ)) volume ⊤).toLinearMap + T.toLinearMap hExact hρ hTD φ + _ = (∫ x, φ x) • T ρ := by + rw [ofFun_apply hOneLoc] + congr 1 + simp + _ = ∫ x, φ x • T ρ := (integral_smul_const (φ : ℝ → ℝ) (T ρ)).symm + +/-- A distribution with zero derivative is constant whenever compactly supported primitives exist. +The test function `ρ` fixes the normalization of the resulting constant. -/ +theorem eq_ofFun_const_of_lineDerivCLM_eq_zero_of_hasCompactSupportPrimitive [CompleteSpace F] + {Ω : TopologicalSpace.Opens ℝ} [TestFunction.HasCompactSupportPrimitive Ω] + (ρ : 𝓓(Ω, ℝ)) (hρ : ∫ x, ρ x = 1) (T : 𝓓'(Ω, F)) + (hT : (lineDerivCLM (1 : ℝ) T : 𝓓'(Ω, F)) = 0) : + T = ofFun Ω (fun _ ↦ T ρ) volume ⊤ := by + have hOneLoc : LocallyIntegrableOn (fun _ : ℝ ↦ (1 : ℝ)) Ω volume := + (continuous_const : Continuous (fun _ : ℝ ↦ (1 : ℝ))).locallyIntegrable |>.locallyIntegrableOn Ω + apply eq_ofFun_const_of_lineDerivCLM_eq_zero ρ + · rw [ofFun_apply hOneLoc] + simpa using hρ + · exact exact_testFunction_lineDerivCLM_of_hasCompactSupportPrimitive + · exact hT + +/-- Iterated distributional differentiation commutes with a tower of classical derivatives. + +Using a sequence rather than iterating `deriv` makes the statement applicable when the classical +derivatives are supplied together with proofs of their values. -/ +theorem iteratedLineDerivOp_ofFun_eq_of_hasDerivAt {Ω : TopologicalSpace.Opens ℝ} + (f : ℕ → ℝ → F) (hf : ∀ n x, HasDerivAt (f n) (f (n + 1) x) x) + (hfloc : ∀ n, LocallyIntegrableOn (f n) Ω volume) (k : ℕ) : + iteratedLineDerivOp (fun _ : Fin k ↦ (1 : ℝ)) (ofFun Ω (f 0) volume ⊤) = + ofFun Ω (f k) volume ⊤ := by + rw [iteratedLineDerivOp_const_eq_iter_lineDerivOp] + induction k with + | zero => simp + | succ k ih => + rw [Function.iterate_succ_apply', ih] + exact lineDerivCLM_ofFun_eq_of_hasDerivAt (hf k) (hfloc k) (hfloc (k + 1)) + +/-- Iterated distributional differentiation of the regular distribution induced by a polynomial +agrees with iterated formal differentiation of that polynomial. -/ +theorem iteratedLineDerivOp_ofFun_polynomial {Ω : TopologicalSpace.Opens ℝ} + (p : Polynomial ℝ) (k : ℕ) : + iteratedLineDerivOp (fun _ : Fin k ↦ (1 : ℝ)) (ofFun Ω (fun x ↦ p.eval x) volume ⊤) = + ofFun Ω (fun x ↦ (((Polynomial.derivative : Polynomial ℝ → Polynomial ℝ)^[k]) p).eval x) + volume ⊤ := by + apply iteratedLineDerivOp_ofFun_eq_of_hasDerivAt + (fun n x ↦ ((Polynomial.derivative^[n]) p).eval x) + · intro n x + simpa only [Function.iterate_succ_apply'] using + (((Polynomial.derivative : Polynomial ℝ → Polynomial ℝ)^[n]) p).hasDerivAt x + · intro n + exact (((Polynomial.derivative : Polynomial ℝ → Polynomial ℝ)^[n]) p).continuous + |>.locallyIntegrable.locallyIntegrableOn Ω + +/-- Every distributional derivative of order strictly larger than the degree of a regular +polynomial distribution vanishes. -/ +theorem iteratedLineDerivOp_ofFun_polynomial_eq_zero_of_natDegree_lt + {Ω : TopologicalSpace.Opens ℝ} (p : Polynomial ℝ) (k : ℕ) (hpk : p.natDegree < k) : + iteratedLineDerivOp (fun _ : Fin k ↦ (1 : ℝ)) + (ofFun Ω (fun x ↦ p.eval x) volume ⊤) = 0 := by + rw [iteratedLineDerivOp_ofFun_polynomial, Polynomial.iterate_derivative_eq_zero hpk] + have hz : (fun x : ℝ ↦ Polynomial.eval x (0 : Polynomial ℝ)) = 0 := by + funext x + simp + rw [hz] + exact ofFun_zero + +/-- The derivative of order one above the natural degree of a regular polynomial distribution +vanishes. -/ +theorem iteratedLineDerivOp_ofFun_polynomial_natDegree_add_one_eq_zero + {Ω : TopologicalSpace.Opens ℝ} (p : Polynomial ℝ) : + iteratedLineDerivOp (fun _ : Fin (p.natDegree + 1) ↦ (1 : ℝ)) + (ofFun Ω (fun x ↦ p.eval x) volume ⊤) = 0 := + iteratedLineDerivOp_ofFun_polynomial_eq_zero_of_natDegree_lt p _ (Nat.lt_succ_self _) + +end Distribution diff --git a/LeanMachineLearning/ForMathlib/Analysis/Distribution/PolynomialCharacterization.lean b/LeanMachineLearning/ForMathlib/Analysis/Distribution/PolynomialCharacterization.lean new file mode 100644 index 00000000..d7fc10d0 --- /dev/null +++ b/LeanMachineLearning/ForMathlib/Analysis/Distribution/PolynomialCharacterization.lean @@ -0,0 +1,133 @@ +/- +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 LeanMachineLearning.ForMathlib.Analysis.Distribution.Polynomial + +/-! +# Characterizing polynomial functions by distributional derivatives + +This file proves the converse to the elementary fact that a sufficiently high distributional +derivative of a polynomial vanishes. The analytic input is isolated in +`TestFunction.HasCompactSupportPrimitive`: every test function of integral zero must be the +derivative of a compactly supported test function. + +The main results are: + +* `Distribution.exists_polynomial_of_iteratedLineDerivOp_eq_zero`, for arbitrary distributions; +* `Distribution.ofFun_eq_iff_eq_of_continuous`, a general injectivity result for regular + distributions induced by continuous functions; +* `Distribution.isPolynomial_iff_exists_iteratedLineDerivOp_ofFun_eq_zero`, the desired + characterization for continuous real functions. +-/ + +@[expose] public section + +open MeasureTheory +open scoped Distributions + +namespace Distribution + +open LineDeriv + +/-- A distribution on an open subset of the real line whose `k`th derivative vanishes is induced +by a polynomial, provided compactly supported primitives exist. + +No smoothness or regularity assumption is made on the distribution. The proof repeatedly uses +that a distribution with zero derivative is constant and the surjectivity of polynomial +differentiation over `ℝ`. -/ +theorem exists_polynomial_of_iteratedLineDerivOp_eq_zero + {Ω : TopologicalSpace.Opens ℝ} [TestFunction.HasCompactSupportPrimitive Ω] + (ρ : 𝓓(Ω, ℝ)) (hρ : ∫ x, ρ x = 1) + (T : 𝓓'(Ω, ℝ)) (k : ℕ) + (hT : iteratedLineDerivOp (fun _ : Fin k => (1 : ℝ)) T = 0) : + ∃ p : Polynomial ℝ, T = ofFun Ω (fun x => p.eval x) volume ⊤ := by + induction k generalizing T with + | zero => + refine ⟨0, ?_⟩ + rwa [show (fun x : ℝ => (0 : Polynomial ℝ).eval x) = 0 by funext x; simp, ofFun_zero] + | succ k ih => + let DT : 𝓓'(Ω, ℝ) := ∂_{(1 : ℝ)} T + have hDT : iteratedLineDerivOp (fun _ : Fin k => (1 : ℝ)) DT = 0 := by + rw [iteratedLineDerivOp_const_eq_iter_lineDerivOp] at hT ⊢ + exact hT + obtain ⟨p, hp⟩ := ih DT hDT + obtain ⟨q, hq⟩ := Polynomial.derivative_surjective_of_charZero p + let Q : 𝓓'(Ω, ℝ) := ofFun Ω (fun x => q.eval x) volume ⊤ + have hqLoc : LocallyIntegrableOn (fun x => q.eval x) Ω volume := + q.continuous.locallyIntegrable.locallyIntegrableOn _ + have hDsub : (lineDerivCLM (1 : ℝ) (T - Q) : 𝓓'(Ω, ℝ)) = 0 := by + rw [map_sub, lineDerivCLM_ofFun_eq_of_hasDerivAt (fun x => q.hasDerivAt x) hqLoc + ((q.derivative.continuous).locallyIntegrable.locallyIntegrableOn _), hq, ← hp] + exact sub_self _ + have hcLoc : LocallyIntegrableOn (fun _ : ℝ => (T - Q) ρ) Ω volume := + continuous_const.locallyIntegrable.locallyIntegrableOn _ + refine ⟨q + Polynomial.C ((T - Q) ρ), ?_⟩ + have heval : (fun x => (q + Polynomial.C ((T - Q) ρ)).eval x) = + (fun x => q.eval x) + (fun _ : ℝ => (T - Q) ρ) := by + funext x + simp + rw [heval, ofFun_add hqLoc hcLoc, ← sub_eq_iff_eq_add'] + exact eq_ofFun_const_of_lineDerivCLM_eq_zero_of_hasCompactSupportPrimitive ρ hρ (T - Q) hDsub + +/-- Two locally integrable continuous functions on a finite-dimensional real normed space induce +the same regular distribution if and only if they are equal. + +This packages `Distribution.ofFun_injective`, whose conclusion is only almost-everywhere equality, +with the fact that a full-support measure detects equality of continuous functions. -/ +theorem ofFun_eq_iff_eq_of_continuous + {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] + [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] + [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] + {μ : Measure E} [μ.IsOpenPosMeasure] {n : ℕ∞} {f g : E → F} + (hf : Continuous f) (hg : Continuous g) + (hfloc : LocallyIntegrableOn f (Set.univ : Set E) μ) + (hgloc : LocallyIntegrableOn g (Set.univ : Set E) μ) : + ofFun (⊤ : TopologicalSpace.Opens E) f μ n = + ofFun (⊤ : TopologicalSpace.Opens E) g μ n ↔ f = g := by + constructor + · intro h + have hae : f =ᵐ[μ.restrict (Set.univ : Set E)] g := ofFun_injective hfloc hgloc h + exact (Continuous.ae_eq_iff_eq μ hf hg).mp <| by simpa using hae + · rintro rfl + rfl + +/-- A continuous real function is polynomial if one of its distributional derivatives vanishes, +assuming the compactly supported primitive property on the real line. -/ +theorem isPolynomial_of_iteratedLineDerivOp_ofFun_eq_zero + [TestFunction.HasCompactSupportPrimitive (⊤ : TopologicalSpace.Opens ℝ)] + (ρ : 𝓓((⊤ : TopologicalSpace.Opens ℝ), ℝ)) (hρ : ∫ x, ρ x = 1) + {f : ℝ → ℝ} (hf : Continuous f) (k : ℕ) + (h : iteratedLineDerivOp (fun _ : Fin k => (1 : ℝ)) + (ofFun (⊤ : TopologicalSpace.Opens ℝ) f volume ⊤) = 0) : + Function.IsPolynomial f := by + obtain ⟨p, hp⟩ := exists_polynomial_of_iteratedLineDerivOp_eq_zero ρ hρ + (ofFun (⊤ : TopologicalSpace.Opens ℝ) f volume ⊤) k h + have hfloc : LocallyIntegrableOn f (Set.univ : Set ℝ) volume := + hf.locallyIntegrable.locallyIntegrableOn _ + have hploc : LocallyIntegrableOn (fun x => p.eval x) (Set.univ : Set ℝ) volume := + p.continuous.locallyIntegrable.locallyIntegrableOn _ + have heq : f = fun x => p.eval x := + (ofFun_eq_iff_eq_of_continuous hf p.continuous hfloc hploc).mp hp + exact ⟨p, fun x => (congrFun heq x).symm⟩ + +/-- A continuous real function is polynomial exactly when one of its distributional derivatives +vanishes, assuming the compactly supported primitive property on the real line. -/ +theorem isPolynomial_iff_exists_iteratedLineDerivOp_ofFun_eq_zero + [TestFunction.HasCompactSupportPrimitive (⊤ : TopologicalSpace.Opens ℝ)] + (ρ : 𝓓((⊤ : TopologicalSpace.Opens ℝ), ℝ)) (hρ : ∫ x, ρ x = 1) {f : ℝ → ℝ} (hf : Continuous f) : + Function.IsPolynomial f ↔ ∃ k : ℕ, iteratedLineDerivOp (fun _ : Fin k => (1 : ℝ)) + (ofFun (⊤ : TopologicalSpace.Opens ℝ) f volume ⊤) = 0 := by + constructor + · rintro ⟨p, hp⟩ + refine ⟨p.natDegree + 1, ?_⟩ + have heval : f = fun x => p.eval x := funext fun x => (hp x).symm + rw [heval] + exact iteratedLineDerivOp_ofFun_polynomial_natDegree_add_one_eq_zero p + · rintro ⟨k, hk⟩ + exact isPolynomial_of_iteratedLineDerivOp_ofFun_eq_zero ρ hρ hf k hk + +end Distribution diff --git a/LeanMachineLearning/ForMathlib/Analysis/Distribution/TestFunction.lean b/LeanMachineLearning/ForMathlib/Analysis/Distribution/TestFunction.lean new file mode 100644 index 00000000..55d1e83c --- /dev/null +++ b/LeanMachineLearning/ForMathlib/Analysis/Distribution/TestFunction.lean @@ -0,0 +1,31 @@ +/- +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.Distribution.TestFunction +public import Mathlib.Topology.ContinuousMap.CompactlySupported + +/-! +# Test functions as compactly supported continuous maps + +Every member of a `TestFunctionClass` is continuous and has compact support. This file packages +those two existing facts in the standard `CompactlySupportedContinuousMapClass` interface. +-/ + +@[expose] public section + +namespace TestFunctionClass + +variable {B E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] + {Ω : TopologicalSpace.Opens E} [NormedAddCommGroup F] [NormedSpace ℝ F] + {n : ℕ∞} [TestFunctionClass B Ω F n] + +/-- A test-function class is, in particular, a class of compactly supported continuous maps. -/ +instance instCompactlySupportedContinuousMapClass : + CompactlySupportedContinuousMapClass B E F := + CompactlySupportedContinuousMapClass.mk map_hasCompactSupport + +end TestFunctionClass diff --git a/LeanMachineLearning/ForMathlib/Analysis/Distribution/TestFunction/Normalize.lean b/LeanMachineLearning/ForMathlib/Analysis/Distribution/TestFunction/Normalize.lean new file mode 100644 index 00000000..a849a8b9 --- /dev/null +++ b/LeanMachineLearning/ForMathlib/Analysis/Distribution/TestFunction/Normalize.lean @@ -0,0 +1,69 @@ +/- +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.BumpFunction.FiniteDimension +public import Mathlib.Analysis.Calculus.BumpFunction.Normed +public import Mathlib.Analysis.Distribution.TestFunction + +/-! +# Test functions normalized by their integral + +This file constructs real-valued test functions of integral one from normalized smooth bump +functions inside an arbitrary nonempty open subset of a finite-dimensional real normed space. +-/ + +@[expose] public section + +noncomputable section + +open Function Set TopologicalSpace MeasureTheory +open scoped Distributions + +namespace ContDiffBump + +variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [HasContDiffBump E] + [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] + {Ω : Opens E} {c : E} (f : ContDiffBump c) (μ : Measure E) + [IsLocallyFiniteMeasure μ] [μ.IsOpenPosMeasure] + +/-- Regard a normalized smooth bump as a test function on an open set containing its support. -/ +def toTestFunctionNormed (h : Metric.closedBall c f.rOut ⊆ Ω) : 𝓓(Ω, ℝ) where + toFun := f.normed μ + contDiff' := f.contDiff_normed + hasCompactSupport' := f.hasCompactSupport_normed + tsupport_subset' := by simpa only [f.tsupport_normed_eq] using h + +@[simp] +theorem toTestFunctionNormed_apply + (h : Metric.closedBall c f.rOut ⊆ Ω) (x : E) : f.toTestFunctionNormed μ h x = f.normed μ x := + rfl + +/-- A normalized smooth bump, regarded as a test function, still has integral one. -/ +@[simp] +theorem integral_toTestFunctionNormed : ∫ (x : E), f.normed μ x ∂μ = 1 := f.integral_normed + +end ContDiffBump + +namespace TestFunction + +variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] + [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] + {Ω : Opens E} (μ : Measure E) [IsLocallyFiniteMeasure μ] [μ.IsOpenPosMeasure] + +/-- Every nonempty open subset of a finite-dimensional real normed space supports a smooth test +function of integral one. -/ +theorem exists_integral_eq_one (hΩ : (Ω : Set E).Nonempty) : + ∃ ρ : 𝓓(Ω, ℝ), ∫ x, ρ x ∂μ = 1 := by + obtain ⟨c, hc⟩ := hΩ + obtain ⟨ε, hε, hball⟩ := Metric.mem_nhds_iff.mp (Ω.isOpen.mem_nhds hc) + let f : ContDiffBump c := + ContDiffBump.mk (ε / 4) (ε / 2) (by positivity) (by linarith) + have hf : Metric.closedBall c f.rOut ⊆ Ω := + (Metric.closedBall_subset_ball (half_lt_self hε)).trans hball + exact ⟨f.toTestFunctionNormed μ hf, by simp⟩ + +end TestFunction diff --git a/LeanMachineLearning/ForMathlib/Analysis/LocallyConvex/Annihilator.lean b/LeanMachineLearning/ForMathlib/Analysis/LocallyConvex/Annihilator.lean new file mode 100644 index 00000000..8f746974 --- /dev/null +++ b/LeanMachineLearning/ForMathlib/Analysis/LocallyConvex/Annihilator.lean @@ -0,0 +1,57 @@ +/- +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.LocallyConvex.Polar +public import Mathlib.Analysis.LocallyConvex.Separation + +/-! +# Density and annihilators + +This file characterizes dense real submodules of locally convex spaces in terms of their +continuous dual annihilators. Geometric Hahn--Banach separation bounds a functional on a +nondense submodule. Its restriction must vanish, since a nonzero linear functional is surjective. +-/ + +@[expose] public section + +open Set + +namespace Submodule + +variable {E : Type*} [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] + [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] + (s : Submodule ℝ E) + +theorem dense_iff_forall_dual_eq_zero : + Dense (s : Set E) ↔ ∀ f : StrongDual ℝ E, (∀ x ∈ s, f x = 0) → f = 0 := by + constructor + · intro hs f hf + exact ContinuousLinearMap.ext_on (by simpa using hs) hf + · intro h + rw [Submodule.dense_iff_topologicalClosure_eq_top] + apply top_unique + intro x hx + by_contra hxc + obtain ⟨f, u, hfc, hfx⟩ := geometric_hahn_banach_closed_point s.topologicalClosure.convex + s.isClosed_topologicalClosure hxc + have hrestr : f.toLinearMap.comp s.subtype = 0 := by + by_contra hf + obtain ⟨y, hy⟩ := (f.toLinearMap.comp s.subtype).surjective hf u + exact (hfc y (s.le_topologicalClosure y.property)).ne hy + have hf : f = 0 := h f fun y hy ↦ DFunLike.congr_fun hrestr ⟨y, hy⟩ + simpa [hf] using (hfc 0 s.topologicalClosure.zero_mem).trans hfx + +theorem exists_dual_annihilator_of_not_dense (hs : ¬ Dense (s : Set E)) : + ∃ f : StrongDual ℝ E, f ≠ 0 ∧ ∀ x ∈ s, f x = 0 := by + simpa only [dense_iff_forall_dual_eq_zero, not_forall, exists_prop, and_comm] using hs + +theorem dense_iff_polarSubmodule_eq_bot : + Dense (s : Set E) ↔ StrongDual.polarSubmodule ℝ s = ⊥ := by + simp only [dense_iff_forall_dual_eq_zero, Submodule.eq_bot_iff, + StrongDual.mem_polarSubmodule] + +end Submodule diff --git a/LeanMachineLearning/ForMathlib/LinearAlgebra/Multilinear/Polarization.lean b/LeanMachineLearning/ForMathlib/LinearAlgebra/Multilinear/Polarization.lean new file mode 100644 index 00000000..30be1a96 --- /dev/null +++ b/LeanMachineLearning/ForMathlib/LinearAlgebra/Multilinear/Polarization.lean @@ -0,0 +1,248 @@ +/- +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.Analytic.IteratedFDeriv + +/-! +# Polarization of symmetric multilinear maps + +This file proves that a symmetric continuous multilinear map is determined by its values on the +diagonal. The main input is the existing formula +`ContinuousMultilinearMap.iteratedFDeriv_comp_diagonal`: the `n`-th derivative of the diagonal +of an `n`-linear map is the sum of the map over all permutations of its arguments. For a +symmetric map this sum is `n!` times the original value. + +The most general statements only assume that `n!` is nonzero in the scalar field. Characteristic +zero versions are provided as convenient corollaries. +-/ + +@[expose] public section + +open scoped BigOperators + +namespace MultilinearMap + +universe uR uM uN uι + +variable {R : Type uR} [Semiring R] +variable {M : Type uM} [AddCommMonoid M] [Module R M] +variable {N : Type uN} [AddCommMonoid N] [Module R N] +variable {ι : Type uι} + +/-- A multilinear map is symmetric if reindexing its arguments by a permutation leaves it +unchanged. -/ +class IsSymm (f : MultilinearMap R (fun _ : ι => M) N) : Prop where + domDomCongr_eq (σ : Equiv.Perm ι) : f.domDomCongr σ = f + +namespace IsSymm + +variable {f g : MultilinearMap R (fun _ : ι => M) N} + +/-- Pointwise characterization of symmetry. -/ +theorem isSymm_iff : f.IsSymm ↔ ∀ (v : ι → M) (σ : Equiv.Perm ι), f (v ∘ σ) = f v where + mp hf v σ := by + have h := congrArg (fun p : MultilinearMap R (fun _ : ι => M) N => p v) + (hf.domDomCongr_eq σ) + change f (fun i => v (σ i)) = f v at h + exact h + mpr h := by + constructor + intro σ + ext v + change f (v ∘ σ) = f v + exact h v σ + +/-- A symmetric multilinear map has the same value after permuting its arguments. -/ +@[simp] +lemma map_perm [hf : f.IsSymm] (v : ι → M) (σ : Equiv.Perm ι) : + f (v ∘ σ) = f v := + isSymm_iff.mp hf v σ + +instance zero : IsSymm (0 : MultilinearMap R (fun _ : ι => M) N) where + domDomCongr_eq _ := by ext; simp + +instance add [f.IsSymm] [g.IsSymm] : IsSymm (f + g) where + domDomCongr_eq σ := by + ext v + change f (v ∘ σ) + g (v ∘ σ) = f v + g v + rw [map_perm, map_perm] + +end IsSymm + +section Ring + +variable {R : Type uR} [Ring R] +variable {M : Type uM} [AddCommGroup M] [Module R M] +variable {N : Type uN} [AddCommGroup N] [Module R N] +variable {ι : Type uι} + +namespace IsSymm + +variable {f g : MultilinearMap R (fun _ : ι => M) N} + +instance neg [f.IsSymm] : IsSymm (-f) where + domDomCongr_eq σ := by + ext v + change -f (v ∘ σ) = -f v + rw [map_perm] + +instance sub [f.IsSymm] [g.IsSymm] : IsSymm (f - g) where + domDomCongr_eq σ := by + ext v + change f (v ∘ σ) - g (v ∘ σ) = f v - g v + rw [map_perm, map_perm] + +end IsSymm + +end Ring + +end MultilinearMap + +namespace ContinuousMultilinearMap + +universe u𝕜 uE uF + +variable {𝕜 : Type u𝕜} [NontriviallyNormedField 𝕜] +variable {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] +variable {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] +variable {n : ℕ} + +/-- Symmetry of a continuous multilinear map, inherited from its underlying multilinear map. -/ +class IsSymm (f : E [×n]→L[𝕜] F) : Prop extends f.toMultilinearMap.IsSymm + +namespace IsSymm + +variable {f g : E [×n]→L[𝕜] F} + +/-- Pointwise characterization of symmetry for continuous multilinear maps. -/ +theorem isSymm_iff : f.IsSymm ↔ + ∀ (v : Fin n → E) (σ : Equiv.Perm (Fin n)), f (v ∘ σ) = f v where + mp hf := MultilinearMap.IsSymm.isSymm_iff.mp hf.toIsSymm + mpr h := by + have hf : f.toMultilinearMap.IsSymm := MultilinearMap.IsSymm.isSymm_iff.mpr h + exact { domDomCongr_eq := hf.domDomCongr_eq } + +/-- A symmetric continuous multilinear map has the same value after permuting its arguments. -/ +@[simp] +lemma map_perm [f.IsSymm] (v : Fin n → E) (σ : Equiv.Perm (Fin n)) : + f (v ∘ σ) = f v := + isSymm_iff.mp ‹f.IsSymm› v σ + +instance zero : IsSymm (0 : E [×n]→L[𝕜] F) where + domDomCongr_eq _ := by ext; simp + +instance add [f.IsSymm] [g.IsSymm] : IsSymm (f + g) where + domDomCongr_eq σ := by + ext v + change f (v ∘ σ) + g (v ∘ σ) = f v + g v + rw [map_perm, map_perm] + +instance neg [f.IsSymm] : IsSymm (-f) where + domDomCongr_eq σ := by + ext v + change -f (v ∘ σ) = -f v + rw [map_perm] + +instance sub [f.IsSymm] [g.IsSymm] : IsSymm (f - g) where + domDomCongr_eq σ := by + ext v + change f (v ∘ σ) - g (v ∘ σ) = f v - g v + rw [map_perm, map_perm] + +/-- Differential form of the polarization identity: for a symmetric `n`-linear map, the `n`-th +derivative of its restriction to the diagonal is `n!` times the original map. -/ +theorem factorial_smul_eq_iteratedFDeriv_comp_diagonal [f.IsSymm] + (x : E) (v : Fin n → E) : + (n.factorial : 𝕜) • f v = + iteratedFDeriv 𝕜 n (fun y => f (fun _ => y)) x v := by + rw [f.iteratedFDeriv_comp_diagonal] + have hperm : ∀ σ : Equiv.Perm (Fin n), f (fun i => v (σ i)) = f v := by + intro σ + change f (v ∘ σ) = f v + exact map_perm v σ + simp_rw [hperm] + simp only [Finset.sum_const, Finset.card_univ, Fintype.card_perm, Fintype.card_fin, + Nat.cast_smul_eq_nsmul] + +end IsSymm + +variable {f g : E [×n]→L[𝕜] F} + +/-- A symmetric continuous `n`-linear map is zero if it vanishes on the diagonal and `n!` is +nonzero in the scalar field. -/ +theorem eq_zero_of_diagonal_eq_zero_of_factorial_ne_zero [f.IsSymm] + (hn : (n.factorial : 𝕜) ≠ 0) (hdiag : ∀ x : E, f (fun _ => x) = 0) : f = 0 := by + ext v + have h := IsSymm.factorial_smul_eq_iteratedFDeriv_comp_diagonal (f := f) (0 : E) v + have hfun : (fun x : E => f (fun _ => x)) = (fun _ : E => (0 : F)) := + funext hdiag + rw [hfun, iteratedFDeriv_fun_zero] at h + exact (smul_eq_zero.mp h).resolve_left hn + +/-- Over a characteristic-zero nontrivially normed field, a symmetric continuous multilinear map +is zero if it vanishes on the diagonal. -/ +theorem eq_zero_of_diagonal_eq_zero [CharZero 𝕜] [f.IsSymm] + (hdiag : ∀ x : E, f (fun _ => x) = 0) : f = 0 := + f.eq_zero_of_diagonal_eq_zero_of_factorial_ne_zero + (Nat.cast_ne_zero.mpr n.factorial_ne_zero) hdiag + +/-- Two symmetric continuous `n`-linear maps agree if their diagonal values agree and `n!` is +nonzero in the scalar field. -/ +theorem ext_of_diagonal_of_factorial_ne_zero [f.IsSymm] [g.IsSymm] + (hn : (n.factorial : 𝕜) ≠ 0) + (hdiag : ∀ x : E, f (fun _ => x) = g (fun _ => x)) : f = g := by + apply sub_eq_zero.mp + apply eq_zero_of_diagonal_eq_zero_of_factorial_ne_zero hn + intro x + simp only [sub_apply, hdiag x, sub_self] + +/-- Over a characteristic-zero nontrivially normed field, symmetric continuous multilinear maps +are determined by their diagonal values. -/ +theorem ext_of_diagonal [CharZero 𝕜] [f.IsSymm] [g.IsSymm] + (hdiag : ∀ x : E, f (fun _ => x) = g (fun _ => x)) : f = g := + ext_of_diagonal_of_factorial_ne_zero (Nat.cast_ne_zero.mpr n.factorial_ne_zero) hdiag + +/-- Equality of symmetric continuous multilinear maps is equivalent to equality on the diagonal. -/ +theorem ext_iff_of_isSymm [CharZero 𝕜] [f.IsSymm] [g.IsSymm] : + f = g ↔ ∀ x : E, f (fun _ => x) = g (fun _ => x) where + mp h := by simp [h] + mpr := ext_of_diagonal + +end ContinuousMultilinearMap + +namespace MultilinearMap + +universe u𝕜 uE uF + +variable {𝕜 : Type u𝕜} [NontriviallyNormedField 𝕜] +variable {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] +variable {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] +variable {n : ℕ} +variable {f : MultilinearMap 𝕜 (fun _ : Fin n => E) F} + +/-- An unbundled symmetric multilinear map which is continuous is zero if it vanishes on the +diagonal and `n!` is nonzero in the scalar field. -/ +theorem eq_zero_of_diagonal_eq_zero_of_continuous_of_factorial_ne_zero [f.IsSymm] + (hn : (n.factorial : 𝕜) ≠ 0) (hcont : Continuous f) + (hdiag : ∀ x : E, f (fun _ => x) = 0) : f = 0 := by + let fc : E [×n]→L[𝕜] F := ⟨f, hcont⟩ + have : fc.IsSymm := { domDomCongr_eq := IsSymm.domDomCongr_eq } + have hc : fc = 0 := + fc.eq_zero_of_diagonal_eq_zero_of_factorial_ne_zero hn hdiag + ext v + change fc v = 0 + rw [hc] + rfl + +/-- A continuous symmetric multilinear map over a characteristic-zero nontrivially normed field +is zero if it vanishes on the diagonal. -/ +theorem eq_zero_of_diagonal_eq_zero_of_continuous [CharZero 𝕜] [f.IsSymm] + (hcont : Continuous f) (hdiag : ∀ x : E, f (fun _ => x) = 0) : f = 0 := + f.eq_zero_of_diagonal_eq_zero_of_continuous_of_factorial_ne_zero + (Nat.cast_ne_zero.mpr n.factorial_ne_zero) hcont hdiag + +end MultilinearMap diff --git a/LeanMachineLearning/ForMathlib/MeasureTheory/Integral/ClosedSubmodule.lean b/LeanMachineLearning/ForMathlib/MeasureTheory/Integral/ClosedSubmodule.lean new file mode 100644 index 00000000..febe5fe3 --- /dev/null +++ b/LeanMachineLearning/ForMathlib/MeasureTheory/Integral/ClosedSubmodule.lean @@ -0,0 +1,89 @@ +/- +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.Normed.Group.Quotient +public import Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap +public import Mathlib.Topology.Algebra.Module.ClosedSubmodule +public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Quotient + +/-! +# Bochner integrals valued in closed submodules + +This file proves that a Bochner integral of a function taking values almost everywhere in a +closed submodule still belongs to that submodule. The main ingredient is the continuous linear +quotient map: after passing to the quotient, the integrand is almost everywhere zero. +-/ + +@[expose] public section + +open MeasureTheory + +namespace ContinuousLinearMap + +variable {α E F 𝕜 : Type*} [MeasurableSpace α] {μ : Measure α} + [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace ℝ E] + [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace ℝ F] + [CompleteSpace F] + +/-- The Bochner integral of a function valued almost everywhere in the kernel of a continuous +linear map still belongs to its kernel. -/ +theorem integral_mem_ker (L : E →L[𝕜] F) {f : α → E} + (hf : ∀ᵐ x ∂μ, f x ∈ L.ker) : + (∫ x, f x ∂μ) ∈ L.ker := by + by_cases hE : CompleteSpace E + · let _ := hE + by_cases hfi : Integrable f μ + · simp only [LinearMap.mem_ker, coe_coe, ← L.integral_comp_comm hfi] + exact integral_eq_zero_of_ae (hf.mono fun x hx ↦ LinearMap.mem_ker.mp hx) + · simp [integral_undef hfi] + · simp [integral, hE] + +end ContinuousLinearMap + +namespace Submodule + +variable {α E 𝕜 : Type*} [MeasurableSpace α] {μ : Measure α} + [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace ℝ E] + +/-- The Bochner integral of a function valued almost everywhere in a closed submodule belongs to +that submodule. No integrability or completeness assumption is needed: in the remaining cases, +the Bochner integral is defined to be zero. -/ +theorem integral_mem (S : Submodule 𝕜 E) (hS : IsClosed (S : Set E)) + {f : α → E} (hf : ∀ᵐ x ∂μ, f x ∈ S) : + (∫ x, f x ∂μ) ∈ S := by + by_cases hE : CompleteSpace E + · let _ := hE + let _ : IsClosed (S : Set E) := hS + rw [← S.ker_mkQ] + exact S.mkQL.integral_mem_ker (by + filter_upwards [hf] with x hx + exact LinearMap.mem_ker.mpr ((Submodule.Quotient.mk_eq_zero S).2 hx)) + · simp [integral, hE] + +/-- The Bochner integral of a function valued almost everywhere in a submodule belongs to the +topological closure of that submodule. -/ +theorem integral_mem_topologicalClosure (S : Submodule 𝕜 E) {f : α → E} + (hf : ∀ᵐ x ∂μ, f x ∈ S) : + (∫ x, f x ∂μ) ∈ S.topologicalClosure := + S.topologicalClosure.integral_mem S.isClosed_topologicalClosure + (hf.mono fun _ hx ↦ S.le_topologicalClosure hx) + +end Submodule + +namespace ClosedSubmodule + +variable {α E 𝕜 : Type*} [MeasurableSpace α] {μ : Measure α} + [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace ℝ E] + +/-- The Bochner integral of a function valued almost everywhere in a closed submodule belongs to +that closed submodule. -/ +theorem integral_mem (S : ClosedSubmodule 𝕜 E) {f : α → E} + (hf : ∀ᵐ x ∂μ, f x ∈ S) : + (∫ x, f x ∂μ) ∈ S := + S.toSubmodule.integral_mem S.isClosed (by simpa using hf) + +end ClosedSubmodule diff --git a/LeanMachineLearning/ForMathlib/Topology/Algebra/Module/FiniteDimension.lean b/LeanMachineLearning/ForMathlib/Topology/Algebra/Module/FiniteDimension.lean new file mode 100644 index 00000000..4a022eff --- /dev/null +++ b/LeanMachineLearning/ForMathlib/Topology/Algebra/Module/FiniteDimension.lean @@ -0,0 +1,45 @@ +/- +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.Algebra.Module.FiniteDimension + +/-! +# Density and finite-dimensional submodules + +This file records that no subset of a proper finite-dimensional submodule can be dense. +-/ + +@[expose] public section + +open Set + +namespace Submodule + +variable {𝕜 E : Type*} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] +variable [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] +variable [Module 𝕜 E] [ContinuousSMul 𝕜 E] [T2Space E] + +/-- A subset of a proper finite-dimensional submodule is not dense in the ambient space. -/ +theorem not_dense_of_subset_of_finiteDimensional (s : Submodule 𝕜 E) + [FiniteDimensional 𝕜 s] (hs : s ≠ ⊤) {t : Set E} (ht : t ⊆ s) : + ¬ Dense t := by + intro ht_dense + apply hs + apply top_unique + intro x _ + have hx : x ∈ closure (s : Set E) := by + rw [(ht_dense.mono ht).closure_eq] + exact Set.mem_univ x + rwa [s.closed_of_finiteDimensional.closure_eq] at hx + +/-- A proper finite-dimensional submodule is not dense in the ambient space. -/ +theorem not_dense_of_finiteDimensional (s : Submodule 𝕜 E) + [FiniteDimensional 𝕜 s] (hs : s ≠ ⊤) : + ¬ Dense (s : Set E) := + s.not_dense_of_subset_of_finiteDimensional hs fun _ ↦ id + +end Submodule diff --git a/LeanMachineLearning/ForMathlib/Topology/ContinuousMap/Algebra.lean b/LeanMachineLearning/ForMathlib/Topology/ContinuousMap/Algebra.lean new file mode 100644 index 00000000..8394ec64 --- /dev/null +++ b/LeanMachineLearning/ForMathlib/Topology/ContinuousMap/Algebra.lean @@ -0,0 +1,33 @@ +/- +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.Algebra + +/-! +# Continuous linear maps on continuous function spaces + +This file bundles coercion from continuous maps to arbitrary functions as a continuous linear map. +-/ + +universe u v w + +@[expose] public section + +namespace ContinuousMap + +variable (R : Type u) {X : Type v} {M : Type w} +variable [Semiring R] [TopologicalSpace X] +variable [TopologicalSpace M] [AddCommMonoid M] [ContinuousAdd M] +variable [Module R M] [ContinuousConstSMul R M] + +/-- Coercion to a function as a continuous linear map. -/ +@[simps! apply] +def coeFnCLM : C(X, M) →L[R] (X → M) where + __ := coeFnLinearMap R + cont := continuous_coeFun + +end ContinuousMap diff --git a/LeanMachineLearning/ForMathlib/Topology/ContinuousMap/InnerProduct.lean b/LeanMachineLearning/ForMathlib/Topology/ContinuousMap/InnerProduct.lean new file mode 100644 index 00000000..a564703f --- /dev/null +++ b/LeanMachineLearning/ForMathlib/Topology/ContinuousMap/InnerProduct.lean @@ -0,0 +1,66 @@ +/- +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.InnerProductSpace.Continuous +public import Mathlib.Topology.ContinuousMap.StoneWeierstrass + +/-! +# Density of polynomials in inner-product coordinates + +The linear coordinate functions given by an inner product separate points. Consequently, on a +compact subtype, the algebra that they generate is dense in the continuous real-valued functions. +-/ + +@[expose] public section + +namespace ContinuousMap + +variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] + +/-- The real inner-product coordinate `x ↦ ⟪w, x⟫` on a subtype. -/ +def innerProductCoordinate (K : Set E) (w : E) : C(K, ℝ) := + ⟨fun x ↦ inner ℝ w x.1, continuous_const.inner continuous_subtype_val⟩ + +@[simp] +theorem innerProductCoordinate_apply (K : Set E) (w : E) (x : K) : + innerProductCoordinate K w x = inner ℝ w x.1 := rfl + +/-- The algebra generated by the real inner-product coordinates on a subtype separates points. + +No compactness or finite-dimensionality assumption is needed for this fact. +-/ +theorem innerProduct_adjoin_separatesPoints (K : Set E) : + (Algebra.adjoin ℝ (Set.range (innerProductCoordinate K))).SeparatesPoints := by + intro x y hxy + let w : E := x.1 - y.1 + let f : C(K, ℝ) := innerProductCoordinate K w + refine ⟨f, ?_, ?_⟩ + · exact ⟨f, ⟨Algebra.subset_adjoin ⟨w, rfl⟩, rfl⟩⟩ + · intro h + apply hxy + apply Subtype.ext + apply sub_eq_zero.mp + apply (inner_self_eq_zero.mp : inner ℝ w w = 0 → w = 0) + rw [inner_sub_right] + exact sub_eq_zero.mpr h + +/-- On a compact subtype of a real inner-product space, the closure of the algebra generated by +the inner-product coordinates is the full algebra of continuous real-valued functions. -/ +theorem innerProduct_adjoin_topologicalClosure_eq_top (K : Set E) [CompactSpace K] : + (Algebra.adjoin ℝ (Set.range (innerProductCoordinate K))).topologicalClosure = ⊤ := + subalgebra_topologicalClosure_eq_top_of_separatesPoints _ + (innerProduct_adjoin_separatesPoints K) + +/-- On a compact subtype of a real inner-product space, the algebra generated by inner-product +coordinates is dense in the continuous real-valued functions. -/ +theorem dense_innerProduct_adjoin (K : Set E) [CompactSpace K] : + Dense (Algebra.adjoin ℝ (Set.range (innerProductCoordinate K)) : Set C(K, ℝ)) := by + rw [dense_iff_closure_eq, ← Subalgebra.topologicalClosure_coe, + innerProduct_adjoin_topologicalClosure_eq_top] + rfl + +end ContinuousMap diff --git a/LeanMachineLearning/ForMathlib/Topology/ContinuousMap/Moments.lean b/LeanMachineLearning/ForMathlib/Topology/ContinuousMap/Moments.lean new file mode 100644 index 00000000..0e5799f2 --- /dev/null +++ b/LeanMachineLearning/ForMathlib/Topology/ContinuousMap/Moments.lean @@ -0,0 +1,184 @@ +/- +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 LeanMachineLearning.ForMathlib.LinearAlgebra.Multilinear.Polarization +public import LeanMachineLearning.ForMathlib.Topology.ContinuousMap.InnerProduct +public import Mathlib.Algebra.Group.Submonoid.Membership + +/-! +# Determinacy by polynomial moments + +This file proves that a continuous linear functional on continuous functions over a compact space +vanishes if all of its moments along a linearly parametrized, algebraically generating family +vanish. Polarization first recovers mixed moments from pure powers; the algebraic span description +of `Algebra.adjoin` and density then finish the proof. + +The general theorem works over any characteristic-zero nontrivially normed field. We also provide +the specialization to the inner-product coordinates of a compact subset of a real inner-product +space. No finite-dimensionality assumption on the ambient inner-product space is needed. +-/ + +@[expose] public section + +open scoped BigOperators + +namespace StrongDual + +section Coordinate + +variable {𝕜 X V : Type*} [NontriviallyNormedField 𝕜] + [TopologicalSpace X] [CompactSpace X] + [NormedAddCommGroup V] [NormedSpace 𝕜 V] + +/-- The multilinear moment obtained by applying `Λ` to a product of coordinate functions. -/ +noncomputable def coordinateMoment (coordinate : V →L[𝕜] C(X, 𝕜)) + (Λ : StrongDual 𝕜 C(X, 𝕜)) (n : ℕ) : V [×n]→L[𝕜] 𝕜 := + Λ.compContinuousMultilinearMap <| + (ContinuousMultilinearMap.mkPiAlgebra 𝕜 (Fin n) C(X, 𝕜)).compContinuousLinearMap + fun _ ↦ coordinate + +@[simp] +theorem coordinateMoment_apply (coordinate : V →L[𝕜] C(X, 𝕜)) + (Λ : StrongDual 𝕜 C(X, 𝕜)) (n : ℕ) (v : Fin n → V) : + coordinateMoment coordinate Λ n v = Λ (∏ i, coordinate (v i)) := by + simp [coordinateMoment] + +instance coordinateMoment_isSymm (coordinate : V →L[𝕜] C(X, 𝕜)) + (Λ : StrongDual 𝕜 C(X, 𝕜)) (n : ℕ) : (coordinateMoment coordinate Λ n).IsSymm := by + rw [ContinuousMultilinearMap.IsSymm.isSymm_iff] + intro v e + simp only [coordinateMoment_apply, Function.comp_apply] + congr 1 + exact Equiv.prod_comp e (fun i ↦ coordinate (v i)) + +end Coordinate + +section CharZero + +variable {𝕜 X V : Type*} [NontriviallyNormedField 𝕜] [CharZero 𝕜] + [TopologicalSpace X] [CompactSpace X] + [NormedAddCommGroup V] [NormedSpace 𝕜 V] + +/-- A continuous linear functional is zero if it annihilates every pure coordinate power and the +coordinates algebraically generate a dense subalgebra. + +The proof first uses polarization to show that all mixed coordinate products vanish. Such products +span the generated algebra, so continuity and density imply that the functional is zero everywhere. +-/ +theorem eq_zero_of_coordinate_powers + (coordinate : V →L[𝕜] C(X, 𝕜)) + (hdense : Dense (Algebra.adjoin 𝕜 (Set.range coordinate) : Set C(X, 𝕜))) + (Λ : StrongDual 𝕜 C(X, 𝕜)) + (hpow : ∀ (n : ℕ) (v : V), Λ ((coordinate v) ^ n) = 0) : + Λ = 0 := by + have hproduct : ∀ (n : ℕ) (v : Fin n → V), Λ (∏ i, coordinate (v i)) = 0 := by + intro n v + have hdiag : ∀ w : V, coordinateMoment coordinate Λ n (fun _ ↦ w) = 0 := by + intro w + rw [coordinateMoment_apply] + simpa using hpow n w + have hm : coordinateMoment coordinate Λ n = 0 := + (coordinateMoment coordinate Λ n).eq_zero_of_diagonal_eq_zero hdiag + have hv := congrArg (fun p : V [×n]→L[𝕜] 𝕜 ↦ p v) hm + simpa using hv + have hmonoid : ∀ p ∈ Submonoid.closure (Set.range coordinate), Λ p = 0 := by + intro p hp + obtain ⟨l, hl, rfl⟩ := Submonoid.exists_list_of_mem_closure hp + have hexi : ∀ i : Fin l.length, ∃ v : V, coordinate v = l[i] := by + intro i + exact hl l[i] (List.getElem_mem ..) + choose v hv using hexi + rw [← Fin.prod_univ_getElem l] + convert hproduct l.length v using 1 + congr 1 + apply Finset.prod_congr rfl + intro i _ + exact (hv i).symm + have hadjoin : ∀ p ∈ Algebra.adjoin 𝕜 (Set.range coordinate), Λ p = 0 := by + intro p hp + change p ∈ (Algebra.adjoin 𝕜 (Set.range coordinate)).toSubmodule at hp + rw [Algebra.adjoin_eq_span] at hp + have hle : Submodule.span 𝕜 + (Submonoid.closure (Set.range coordinate) : Set C(X, 𝕜)) ≤ Λ.ker := by + rw [Submodule.span_le] + intro q hq + exact hmonoid q hq + exact hle hp + apply ContinuousLinearMap.ext_on + (hdense.mono (Submodule.subset_span (R := 𝕜))) + intro p hp + simpa using hadjoin p hp + +end CharZero + +end StrongDual + +namespace ContinuousMap + +variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] + +/-- The continuous linear map sending a vector to its inner-product coordinate on a compact +subtype. Compactness bounds the subtype, so finite-dimensionality is not required. -/ +noncomputable def innerProductCoordinateCLM (K : Set E) [CompactSpace K] : + E →L[ℝ] C(K, ℝ) := by + let coordinate : E →ₗ[ℝ] C(K, ℝ) := + { toFun := innerProductCoordinate K + map_add' := by + intro x y + ext z + simp [innerProductCoordinate, inner_add_left] + map_smul' := by + intro c x + ext z + simp [innerProductCoordinate, real_inner_smul_left] } + apply coordinate.mkContinuousOfExistsBound + have hcompact : IsCompact (Set.range fun x : K ↦ x.1) := + isCompact_range continuous_subtype_val + obtain ⟨R, hRpos, hR⟩ := hcompact.isBounded.exists_pos_norm_le + refine ⟨R, fun w ↦ + (ContinuousMap.norm_le (innerProductCoordinate K w) ?_).2 (fun x ↦ ?_)⟩ + · positivity + · change ‖inner ℝ w x.1‖ ≤ R * ‖w‖ + calc + ‖inner ℝ w x.1‖ ≤ ‖w‖ * ‖x.1‖ := norm_inner_le_norm _ _ + _ ≤ ‖w‖ * R := mul_le_mul_of_nonneg_left (hR x.1 ⟨x, rfl⟩) (norm_nonneg _) + _ = R * ‖w‖ := mul_comm _ _ + +@[simp] +theorem innerProductCoordinateCLM_apply (K : Set E) [CompactSpace K] (w : E) : + innerProductCoordinateCLM K w = innerProductCoordinate K w := by + rfl + +end ContinuousMap + +namespace StrongDual + +variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] + +/-- A continuous linear functional on a compact subtype of a real inner-product space is zero if +it annihilates every power of every inner-product coordinate. -/ +theorem eq_zero_of_innerProductCoordinate_powers (K : Set E) [CompactSpace K] + (Λ : StrongDual ℝ C(K, ℝ)) + (hpow : ∀ (n : ℕ) (w : E), + Λ ((ContinuousMap.innerProductCoordinate K w) ^ n) = 0) : + Λ = 0 := by + apply eq_zero_of_coordinate_powers (ContinuousMap.innerProductCoordinateCLM K) + (Λ := Λ) + · have hrange : Set.range (ContinuousMap.innerProductCoordinateCLM K) = + Set.range (ContinuousMap.innerProductCoordinate K) := by + ext f + constructor + · rintro ⟨w, rfl⟩ + exact ⟨w, (ContinuousMap.innerProductCoordinateCLM_apply K w).symm⟩ + · rintro ⟨w, rfl⟩ + exact ⟨w, ContinuousMap.innerProductCoordinateCLM_apply K w⟩ + rw [hrange] + exact ContinuousMap.dense_innerProduct_adjoin K + · intro n w + simpa only [ContinuousMap.innerProductCoordinateCLM_apply] using hpow n w + +end StrongDual diff --git a/LeanMachineLearning/NeuralNetwork/Shallow/Basic.lean b/LeanMachineLearning/NeuralNetwork/Shallow/Basic.lean new file mode 100644 index 00000000..fc6aba77 --- /dev/null +++ b/LeanMachineLearning/NeuralNetwork/Shallow/Basic.lean @@ -0,0 +1,39 @@ +/- +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.InnerProductSpace.Continuous +public import Mathlib.LinearAlgebra.Finsupp.LinearCombination +public import Mathlib.Topology.ContinuousMap.Algebra +public import Mathlib.Topology.ContinuousMap.Compact + +/-! +# Single-hidden-layer neural networks + +We define a neuron on a real inner product space and the vector space of finite-width shallow +networks generated by an activation function. Using `Submodule.span` means that finite linear +combinations and all their algebraic laws come from Mathlib's existing linear-algebra API. +-/ + +@[expose] public section + +namespace Learning.ShallowNetwork + +variable {E : Type*} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] + +/-- A single neuron with weight `w`, bias `b`, and activation `σ`. -/ +def neuron (σ : C(ℝ, ℝ)) (w : E) (b : ℝ) : C(E, ℝ) := + σ.comp ⟨fun x ↦ inner ℝ w x + b, by fun_prop⟩ + +@[simp] +theorem neuron_apply (σ : C(ℝ, ℝ)) (w : E) (b : ℝ) (x : E) : + neuron σ w b x = σ (inner ℝ w x + b) := rfl + +/-- The restrictions to `K` of finite-width, single-hidden-layer networks with activation `σ`. -/ +def spaceOn (σ : C(ℝ, ℝ)) (K : Set E) : Submodule ℝ C(K, ℝ) := + Submodule.span ℝ (Set.range fun p : E × ℝ ↦ (neuron σ p.1 p.2).restrict K) + +end Learning.ShallowNetwork diff --git a/LeanMachineLearning/NeuralNetwork/UniversalApproximation/Convolution.lean b/LeanMachineLearning/NeuralNetwork/UniversalApproximation/Convolution.lean new file mode 100644 index 00000000..db49aab0 --- /dev/null +++ b/LeanMachineLearning/NeuralNetwork/UniversalApproximation/Convolution.lean @@ -0,0 +1,172 @@ +/- +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.ContDiff.Convolution +public import Mathlib.MeasureTheory.Measure.Haar.OfBasis +public import Mathlib.MeasureTheory.Measure.Haar.Unique +public import Mathlib.Topology.ContinuousMap.CompactlySupported +public import LeanMachineLearning.ForMathlib.Analysis.Distribution.TestFunction +public import LeanMachineLearning.ForMathlib.MeasureTheory.Integral.ClosedSubmodule +public import LeanMachineLearning.NeuralNetwork.UniversalApproximation.Discriminatory + +/-! +# Convolution smoothing of activation functions + +Convolution against a compactly supported continuous kernel turns an activation into another +continuous activation. On a compact domain, a ridge function for the convolved activation is a +Bochner integral of ridge functions for the original activation. Consequently it belongs to the +closure of their span, and every functional annihilating the original neurons also annihilates the +convolved neurons. + +The kernel is abstracted by `CompactlySupportedContinuousMapClass`, so the closure and annihilator +results apply both to compactly supported continuous maps and to smooth test functions. + +For a smooth test-function kernel, successive derivatives of the kernel give successive +derivatives of the convolution. The resulting `iteratedDeriv` formula also identifies their +values at the origin. +-/ + +@[expose] public section + +open MeasureTheory +open scoped Distributions + +namespace Learning.ShallowNetwork + +/-! ## Compactly supported convolution kernels -/ + +/-- Convolution of a continuous activation with a compactly supported continuous kernel. + +The convention is +`convolutionActivation φ σ t = ∫ s, φ s * σ (t - s)`. -/ +noncomputable def convolutionActivation {B : Type*} [FunLike B ℝ ℝ] + [CompactlySupportedContinuousMapClass B ℝ ℝ] + (φ : B) (σ : C(ℝ, ℝ)) : C(ℝ, ℝ) := + ⟨MeasureTheory.convolution φ σ (ContinuousLinearMap.mul ℝ ℝ) volume, + (CompactlySupportedContinuousMapClass.hasCompactSupport φ).continuous_convolution_left + _ (ContinuousMapClass.map_continuous φ) σ.continuous.locallyIntegrable⟩ + +@[simp] +theorem convolutionActivation_apply {B : Type*} [FunLike B ℝ ℝ] + [CompactlySupportedContinuousMapClass B ℝ ℝ] + (φ : B) (σ : C(ℝ, ℝ)) (t : ℝ) : + convolutionActivation φ σ t = ∫ s, φ s * σ (t - s) := MeasureTheory.convolution_mul + +/-- Convolution with a compactly supported `C^n` kernel makes a continuous activation `C^n`. -/ +theorem convolutionActivation_contDiff {B : Type*} [FunLike B ℝ ℝ] + [CompactlySupportedContinuousMapClass B ℝ ℝ] + (φ : B) (σ : C(ℝ, ℝ)) {n : ℕ∞} (hφ : ContDiff ℝ n φ) : + ContDiff ℝ n (convolutionActivation φ σ) := + (CompactlySupportedContinuousMapClass.hasCompactSupport φ).contDiff_convolution_left + _ hφ σ.continuous.locallyIntegrable + +/-! ## Network spaces and annihilator transfer -/ + +/-- The activation `σ` applied to a scalar-valued continuous feature `u`, with bias `b`. -/ +def activationAlong {X : Type*} [TopologicalSpace X] (σ : C(ℝ, ℝ)) + (u : C(X, ℝ)) (b : ℝ) : C(X, ℝ) := + σ.comp (u + ContinuousMap.const X b) + +@[simp] +theorem activationAlong_apply {X : Type*} [TopologicalSpace X] + (σ : C(ℝ, ℝ)) (u : C(X, ℝ)) (b : ℝ) (x : X) : + activationAlong σ u b x = σ (u x + b) := rfl + +/-- The `C(X, ℝ)`-valued integrand expressing a ridge function of a convolved activation is +Bochner integrable. -/ +theorem integrable_smul_activationAlong_sub + {X : Type*} [TopologicalSpace X] [CompactSpace X] + {B : Type*} [FunLike B ℝ ℝ] [CompactlySupportedContinuousMapClass B ℝ ℝ] + (φ : B) (σ : C(ℝ, ℝ)) (u : C(X, ℝ)) (b : ℝ) : + Integrable (fun s : ℝ => φ s • activationAlong σ u (b - s)) := by + apply Continuous.integrable_of_hasCompactSupport + · exact (ContinuousMapClass.map_continuous φ).smul + (ContinuousMap.continuous_of_continuous_uncurry _ <| + (σ.continuous.comp + ((u.continuous.comp continuous_snd).add (continuous_const.sub continuous_fst)))) + · exact (CompactlySupportedContinuousMapClass.hasCompactSupport φ).smul_right + +/-- A ridge function of a convolved activation is the Bochner integral of shifted ridge functions +of the original activation. -/ +theorem activationAlong_convolutionActivation + {X : Type*} [TopologicalSpace X] [CompactSpace X] + {B : Type*} [FunLike B ℝ ℝ] [CompactlySupportedContinuousMapClass B ℝ ℝ] + (φ : B) (σ : C(ℝ, ℝ)) (u : C(X, ℝ)) (b : ℝ) : + activationAlong (convolutionActivation φ σ) u b = + ∫ s : ℝ, φ s • activationAlong σ u (b - s) := by + apply ContinuousMap.ext + intro x + rw [ContinuousMap.integral_apply (integrable_smul_activationAlong_sub φ σ u b)] + simp only [activationAlong_apply, convolutionActivation_apply] + congr 1 + funext s + simp [sub_eq_add_neg, add_assoc] + +/-- A continuous functional annihilating all translates of a ridge function also annihilates the +corresponding ridge function for every compactly supported convolution smoothing. -/ +theorem annihilates_convolutionActivation + {X : Type*} [TopologicalSpace X] [CompactSpace X] + {B : Type*} [FunLike B ℝ ℝ] [CompactlySupportedContinuousMapClass B ℝ ℝ] + (φ : B) {σ : C(ℝ, ℝ)} {u : C(X, ℝ)} {Λ : StrongDual ℝ C(X, ℝ)} {b : ℝ} + (hΛ : ∀ b, Λ (activationAlong σ u b) = 0) : + Λ (activationAlong (convolutionActivation φ σ) u b) = 0 := by + rw [activationAlong_convolutionActivation, + ← Λ.integral_comp_comm (integrable_smul_activationAlong_sub φ σ u b)] + simp [hΛ] + +/-- A continuous functional annihilating all neurons for `σ` also annihilates all neurons for a +compactly supported convolution smoothing of `σ`. -/ +theorem annihilates_convolutionActivation_neurons + {E : Type*} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] + {B : Type*} [FunLike B ℝ ℝ] [CompactlySupportedContinuousMapClass B ℝ ℝ] + (φ : B) {σ : C(ℝ, ℝ)} {K : Set E} {Λ : StrongDual ℝ C(K, ℝ)} + (hK : IsCompact K) (hΛ : ∀ w b, Λ ((neuron σ w b).restrict K) = 0) : + ∀ w b, Λ ((neuron (convolutionActivation φ σ) w b).restrict K) = 0 := by + let _ : CompactSpace K := isCompact_iff_compactSpace.mp hK + intro w b + let u : C(K, ℝ) := + ⟨fun x ↦ inner ℝ w (x : E), continuous_const.inner continuous_subtype_val⟩ + have htrans : ∀ c, Λ (activationAlong σ u c) = 0 := by + intro c + rw [show activationAlong σ u c = (neuron σ w c).restrict K by rfl] + exact hΛ w c + rw [show (neuron (convolutionActivation φ σ) w b).restrict K = + activationAlong (convolutionActivation φ σ) u b by rfl] + exact annihilates_convolutionActivation φ htrans + +/-! ## Iterated derivatives for smooth kernels -/ + +/-- Successive derivatives of the left kernel give successive derivatives of its convolution +with a continuous activation. -/ +theorem hasDerivAt_convolutionActivation_iterate_lineDerivCLM + (φ : 𝓓((⊤ : TopologicalSpace.Opens ℝ), ℝ)) (σ : C(ℝ, ℝ)) (n : ℕ) (x : ℝ) : + HasDerivAt (convolutionActivation (((TestFunction.lineDerivCLM ℝ (1 : ℝ))^[n]) φ) σ) + (convolutionActivation (((TestFunction.lineDerivCLM ℝ (1 : ℝ))^[n + 1]) φ) σ x) x := by + have h := (((TestFunction.lineDerivCLM ℝ (1 : ℝ))^[n]) φ).hasCompactSupport + |>.hasDerivAt_convolution_left (μ := volume) (ContinuousLinearMap.mul ℝ ℝ) + ((TestFunction.contDiff (((TestFunction.lineDerivCLM ℝ (1 : ℝ))^[n]) φ)).of_le (by simp)) + σ.continuous.locallyIntegrable x + convert h using 1 + · rfl + · rw [Function.iterate_succ_apply'] + congr 1 + +/-- The `n`-th derivative of a test-function convolution is the convolution with the +`n`-fold derivative of its kernel. -/ +@[simp] +theorem iteratedDeriv_convolutionActivation_testFunction + (φ : 𝓓((⊤ : TopologicalSpace.Opens ℝ), ℝ)) (σ : C(ℝ, ℝ)) (n : ℕ) : + iteratedDeriv n (convolutionActivation φ σ) = + convolutionActivation (((TestFunction.lineDerivCLM ℝ (1 : ℝ))^[n]) φ) σ := by + induction n with + | zero => simp + | succ n ih => + rw [iteratedDeriv_succ, ih] + funext x + exact (hasDerivAt_convolutionActivation_iterate_lineDerivCLM φ σ n x).deriv + +end Learning.ShallowNetwork diff --git a/LeanMachineLearning/NeuralNetwork/UniversalApproximation/Discriminatory.lean b/LeanMachineLearning/NeuralNetwork/UniversalApproximation/Discriminatory.lean new file mode 100644 index 00000000..f22919ba --- /dev/null +++ b/LeanMachineLearning/NeuralNetwork/UniversalApproximation/Discriminatory.lean @@ -0,0 +1,154 @@ +/- +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 LeanMachineLearning.ForMathlib.Analysis.Calculus.ContinuousMapComposition +public import LeanMachineLearning.ForMathlib.Analysis.LocallyConvex.Annihilator +public import LeanMachineLearning.ForMathlib.Topology.ContinuousMap.Moments +public import LeanMachineLearning.NeuralNetwork.Shallow.Basic +public import Mathlib.Analysis.Calculus.IteratedDeriv.Defs + +/-! +# Discriminatory criteria for universal approximation + +An activation is discriminatory on an input space if the only continuous linear functional on +`C(K, ℝ)` that annihilates every neuron is zero, for every compact `K`. Hahn--Banach makes this +property equivalent to universal approximation. + +For smooth activations, annihilating all ridges whose `n`-th derivative is nonzero somewhere +forces a functional to annihilate every `n`-th power of a linear coordinate. The resulting +criterion permits a different smooth ridge function at each degree. Smoothness and successive +derivatives are expressed using mathlib's `ContDiff` and `iteratedDeriv`. +-/ + +@[expose] public section + +open scoped ContDiff + +namespace Learning.ShallowNetwork + +/-! ## The dual criterion -/ + +section Discriminatory + +/-- An activation is discriminatory on `E` if no nonzero continuous linear functional annihilates +all of its neurons on a compact subset of `E`. -/ +class IsDiscriminatory (E : Type*) [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] + (σ : C(ℝ, ℝ)) : Prop where + annihilator_eq_zero : ∀ (K : Set E), IsCompact K → ∀ Λ : StrongDual ℝ C(K, ℝ), + (∀ w b, Λ ((neuron σ w b).restrict K) = 0) → Λ = 0 + +variable {E : Type*} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] + +/-- Density of the network space on every compact set is equivalent to the +discriminatory-functional criterion. -/ +theorem dense_spaceOn_iff_isDiscriminatory (σ : C(ℝ, ℝ)) : + (∀ (K : Set E), IsCompact K → Dense (spaceOn σ K : Set C(K, ℝ))) ↔ + IsDiscriminatory E σ := by + constructor + · intro h_dense + constructor + intro K hK + let _ : CompactSpace K := isCompact_iff_compactSpace.mp hK + intro Λ hΛ + refine (spaceOn σ K).dense_iff_forall_dual_eq_zero.mp (h_dense K hK) Λ ?_ + intro f hf + have hle : spaceOn σ K ≤ Λ.ker := by + rw [spaceOn] + apply Submodule.span_le.2 + rintro g ⟨p, rfl⟩ + exact hΛ p.1 p.2 + exact hle hf + · rintro ⟨h_disc⟩ + intro K hK + let _ : CompactSpace K := isCompact_iff_compactSpace.mp hK + rw [Submodule.dense_iff_forall_dual_eq_zero] + intro Λ hΛ + apply h_disc K hK Λ + intro w b + exact hΛ _ (Submodule.subset_span ⟨(w, b), rfl⟩) + +end Discriminatory + +/-! ## Smooth ridge criteria -/ + +section SmoothActivation + +variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] + +/-- A functional annihilating every ridge of `g` also annihilates every power of a linear +coordinate for which the corresponding derivative of `g` is nonzero somewhere. -/ +theorem annihilates_coordinate_pow_of_iteratedDeriv_ne_zero + {g : C(ℝ, ℝ)} {K : Set E} {Λ : StrongDual ℝ C(K, ℝ)} {n : ℕ} {b : ℝ} {w : E} + (hg : ContDiff ℝ ∞ g) (hK : IsCompact K) + (hΛ : ∀ w b, Λ ((neuron g w b).restrict K) = 0) (hb : iteratedDeriv n g b ≠ 0) : + Λ ((ContinuousMap.innerProductCoordinate K w) ^ n) = 0 := by + let _ : CompactSpace K := isCompact_iff_compactSpace.mp hK + let u : C(K, ℝ) := ContinuousMap.innerProductCoordinate K w + let arg (t : ℝ) : C(K, ℝ) := ContinuousMap.const K b + ContinuousMap.const K t * u + let d (m : ℕ) : C(ℝ, ℝ) := ⟨iteratedDeriv m g, hg.continuous_iteratedDeriv m (by simp)⟩ + have hstep : ∀ m t, Λ (u ^ m * (d m).comp (arg t)) = 0 := by + intro m + induction m with + | zero => + intro t + have hd0 : d 0 = g := by + ext x + simp [d] + rw [hd0] + have heq : g.comp (arg t) = (neuron g (t • w) b).restrict K := by + ext x + simp [arg, u, neuron_apply, real_inner_smul_left, add_comm] + rw [heq] + simpa using hΛ (t • w) b + | succ m ihm => + intro t + have hd : ∀ y, HasDerivAt (d m) (d (m + 1) y) y := by + intro y + simpa [d, ContinuousMap.coe_mk, iteratedDeriv_succ] using + (hg.differentiable_iteratedDeriv m + (by exact_mod_cast ENat.natCast_lt_top m) y).hasDerivAt + have hcurve := HasDerivAt.continuousMap_comp_affine hd (ContinuousMap.const K b) u t + have hmul' : HasDerivAt (fun s ↦ u ^ m * (d m).comp (arg s)) + (u ^ m * (u * (d (m + 1)).comp (arg t))) t := by + convert hcurve.const_mul (u ^ m) using 1 + ext x + simp [arg, smul_eq_mul] + have happly : HasDerivAt (fun s ↦ Λ (u ^ m * (d m).comp (arg s))) + (Λ (u ^ m * (u * (d (m + 1)).comp (arg t)))) t := by + simpa [Function.comp_def] using Λ.hasFDerivAt.comp_hasDerivAt_of_eq t hmul' rfl + have hzero : HasDerivAt (fun s ↦ Λ (u ^ m * (d m).comp (arg s))) 0 t := by + convert hasDerivAt_const t (0 : ℝ) using 1 + funext s + exact ihm s + simpa [pow_succ, mul_assoc] using happly.unique hzero + have h : d n b * Λ (u ^ n) = 0 := calc + d n b * Λ (u ^ n) = Λ (d n b • u ^ n) := by simp + _ = Λ (u ^ n * (d n).comp (arg 0)) := by + congr 1 + ext x + simp [arg, mul_comm] + _ = 0 := hstep n 0 + exact (mul_eq_zero.mp h).resolve_left hb + +/-- A degree-by-degree smooth ridge family is enough for the discriminatory property. The +smooth function may depend on the degree, as needed after mollification. -/ +theorem isDiscriminatory_of_smooth_ridges {σ : C(ℝ, ℝ)} (hsmooth : ∀ n : ℕ, ∃ (g : C(ℝ, ℝ)) (b : ℝ), + ContDiff ℝ ∞ g ∧ iteratedDeriv n g b ≠ 0 ∧ + ∀ (K : Set E) (_hK : IsCompact K) (Λ : StrongDual ℝ C(K, ℝ)), + (∀ w c, Λ ((neuron σ w c).restrict K) = 0) → ∀ w c, Λ ((neuron g w c).restrict K) = 0) : + IsDiscriminatory E σ := by + constructor + intro K hK Λ hΛ + let _ : CompactSpace K := isCompact_iff_compactSpace.mp hK + apply StrongDual.eq_zero_of_innerProductCoordinate_powers K Λ + intro n w + obtain ⟨g, b, hg, hb, htransfer⟩ := hsmooth n + exact annihilates_coordinate_pow_of_iteratedDeriv_ne_zero hg hK (htransfer K hK Λ hΛ) hb + +end SmoothActivation + +end Learning.ShallowNetwork diff --git a/LeanMachineLearning/NeuralNetwork/UniversalApproximation/Leshno.lean b/LeanMachineLearning/NeuralNetwork/UniversalApproximation/Leshno.lean new file mode 100644 index 00000000..ee9cbbe1 --- /dev/null +++ b/LeanMachineLearning/NeuralNetwork/UniversalApproximation/Leshno.lean @@ -0,0 +1,59 @@ +/- +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.InnerProductSpace.PiL2 +public import LeanMachineLearning.NeuralNetwork.UniversalApproximation.Nonpolynomial +public import LeanMachineLearning.NeuralNetwork.UniversalApproximation.PolynomialObstruction + +/-! +# The Leshno--Lin--Pinkus--Schocken theorem + +This file combines the sufficient direction from `Nonpolynomial` with the necessary direction +from `PolynomialObstruction` to characterize continuous universal activations. + +The input space is required to be nontrivial: in dimension zero, every shallow-network function +is constant, and a polynomial activation can still be universal. We characterize density on +every compact subset of an arbitrary nontrivial real inner-product space, express it as +`(spaceOn σ K).topologicalClosure = ⊤`, and specialize to the classical Euclidean-space theorem. +-/ + +@[expose] public section + +namespace Learning.ShallowNetwork + +variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] + +/-- Precise compact-set form of the Leshno--Lin--Pinkus--Schocken equivalence. + +The approximating subspace is `spaceOn σ K`, whose generators are exactly the restrictions to +`K` of biased ridge functions `x ↦ σ (⟪w, x⟫ + b)`. +-/ +theorem not_isPolynomial_iff_dense_on_compact [Nontrivial E] (σ : C(ℝ, ℝ)) : + ¬ Function.IsPolynomial σ ↔ ∀ (K : Set E), IsCompact K → Dense (spaceOn σ K : Set C(K, ℝ)) := + ⟨fun hσ _ hK ↦ dense_spaceOn_of_not_isPolynomial hσ hK, not_isPolynomial_of_dense_spaceOn σ⟩ + +/-- A continuous activation is nonpolynomial if and only if its network space has full +topological closure on every compact subset of a nontrivial real inner-product space. -/ +theorem not_isPolynomial_iff_spaceOn_topologicalClosure_eq_top [Nontrivial E] (σ : C(ℝ, ℝ)) : + ¬ Function.IsPolynomial σ ↔ + ∀ (K : Set E), IsCompact K → (spaceOn σ K).topologicalClosure = ⊤ := by + simpa only [Submodule.dense_iff_topologicalClosure_eq_top] using + (not_isPolynomial_iff_dense_on_compact (E := E) σ) + +/-- The classical theorem on `ℝ^d`, represented as `EuclideanSpace ℝ (Fin d)`. + +The hypothesis `0 < d` is essential: the claimed equivalence is false for the zero-dimensional +input space. +-/ +theorem leshno_lin_pinkus_schocken {d : ℕ} (hd : 0 < d) (σ : C(ℝ, ℝ)) : + ¬ Function.IsPolynomial σ ↔ + ∀ (K : Set (EuclideanSpace ℝ (Fin d))), IsCompact K → + (spaceOn σ K).topologicalClosure = ⊤ := by + let _ : Nonempty (Fin d) := Fin.pos_iff_nonempty.mp hd + exact not_isPolynomial_iff_spaceOn_topologicalClosure_eq_top σ + +end Learning.ShallowNetwork diff --git a/LeanMachineLearning/NeuralNetwork/UniversalApproximation/Nonpolynomial.lean b/LeanMachineLearning/NeuralNetwork/UniversalApproximation/Nonpolynomial.lean new file mode 100644 index 00000000..98dbbce8 --- /dev/null +++ b/LeanMachineLearning/NeuralNetwork/UniversalApproximation/Nonpolynomial.lean @@ -0,0 +1,157 @@ +/- +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 LeanMachineLearning.ForMathlib.Analysis.Distribution.PolynomialCharacterization +public import LeanMachineLearning.ForMathlib.Analysis.Distribution.TestFunction.Normalize +public import LeanMachineLearning.NeuralNetwork.UniversalApproximation.Convolution + +/-! +# Universal approximation for nonpolynomial activations + +A continuous nonpolynomial function defines a regular distribution whose derivative of every +order is nonzero. Evaluating the derivative on a suitable test function gives a nonzero integral +against the reflected activation `x ↦ σ (-x)`. + +For each order `n`, this constructs a smooth test-function convolution whose `n`-th derivative +at the origin is nonzero. The kernel may depend on `n`. Annihilator transfer for convolution +and the degree-by-degree smooth ridge criterion then prove that the original activation is +discriminatory and universal. + +The result applies to arbitrary real inner-product spaces. Neither nontriviality nor finite +dimensionality is needed for this sufficient direction. +-/ + +@[expose] public section + +open MeasureTheory +open scoped Distributions + +namespace Learning.ShallowNetwork + +/-! ## Reflection of the activation -/ + +/-- Reflect a continuous real function through the origin. -/ +noncomputable def reflectedActivation (σ : C(ℝ, ℝ)) : C(ℝ, ℝ) := + σ.comp (-ContinuousMap.id ℝ) + +@[simp] +theorem reflectedActivation_apply (σ : C(ℝ, ℝ)) (x : ℝ) : + reflectedActivation σ x = σ (-x) := rfl + +/-- Reflection preserves the property of being a polynomial function. -/ +theorem isPolynomial_reflectedActivation_iff (σ : C(ℝ, ℝ)) : + Function.IsPolynomial (reflectedActivation σ) ↔ Function.IsPolynomial σ := by + constructor + · rintro ⟨p, hp⟩ + exact ⟨p.comp (-Polynomial.X), by simp [hp]⟩ + · rintro ⟨p, hp⟩ + exact ⟨p.comp (-Polynomial.X), by simp [hp]⟩ + +end Learning.ShallowNetwork + +namespace Distribution + +/-! ## Nonzero distributional derivatives -/ + +open LineDeriv + +/-- Evaluate an iterated distributional derivative by moving all derivatives onto the test +function. The statement is vector-valued and valid on every open subset of the real line. -/ +theorem iteratedLineDerivOp_apply_iterated_testFunction + {F : Type*} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] + [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] + {Ω : TopologicalSpace.Opens ℝ} (T : 𝓓'(Ω, F)) (n : ℕ) (φ : 𝓓(Ω, ℝ)) : + iteratedLineDerivOp (fun _ : Fin n ↦ (1 : ℝ)) T φ = + (-1 : ℝ) ^ n • T (((TestFunction.lineDerivCLM ℝ (1 : ℝ))^[n]) φ) := by + rw [iteratedLineDerivOp_const_eq_iter_lineDerivOp] + induction n generalizing T φ with + | zero => simp + | succ n ih => + rw [Function.iterate_succ_apply'] + change Distribution.lineDerivCLM (1 : ℝ) _ φ = _ + simp [Distribution.lineDerivCLM_apply, ih, Function.iterate_succ_apply, pow_succ] + +/-- Every distributional derivative of a continuous nonpolynomial function is nonzero. + +The compactly-supported-primitive class is the exactness input used by the converse +characterization of polynomial regular distributions. -/ +theorem iteratedLineDerivOp_ofFun_ne_zero_of_not_isPolynomial + {f : C(ℝ, ℝ)} (hf : ¬ Function.IsPolynomial f) (n : ℕ) : + iteratedLineDerivOp (fun _ : Fin n ↦ (1 : ℝ)) + (ofFun (⊤ : TopologicalSpace.Opens ℝ) f volume ⊤) ≠ 0 := by + intro hzero + apply hf + obtain ⟨ρ, hρ⟩ := TestFunction.exists_integral_eq_one + (Ω := (⊤ : TopologicalSpace.Opens ℝ)) volume Set.univ_nonempty + exact isPolynomial_of_iteratedLineDerivOp_ofFun_eq_zero ρ hρ f.continuous n hzero + +end Distribution + +namespace Learning.ShallowNetwork + +/-! ## Test-function and convolution witnesses -/ + +/-- For each order, a continuous nonpolynomial activation admits a test function whose iterated +derivative has nonzero pairing with the reflected activation. + +Equivalently, this is the nonzero value at the origin of the corresponding derivative of the +left convolution of the test function with `σ`. -/ +theorem exists_testFunction_iteratedLineDeriv_integral_mul_reflected_ne_zero + {σ : C(ℝ, ℝ)} (hσ : ¬ Function.IsPolynomial σ) (n : ℕ) : + ∃ φ : 𝓓((⊤ : TopologicalSpace.Opens ℝ), ℝ), + ∫ s : ℝ, (((TestFunction.lineDerivCLM ℝ (1 : ℝ))^[n]) φ) s * σ (-s) ≠ 0 := by + let f : C(ℝ, ℝ) := reflectedActivation σ + let T : 𝓓'((⊤ : TopologicalSpace.Opens ℝ), ℝ) := + LineDeriv.iteratedLineDerivOp (fun _ : Fin n ↦ (1 : ℝ)) + (Distribution.ofFun (⊤ : TopologicalSpace.Opens ℝ) f volume ⊤) + have hf : ¬ Function.IsPolynomial f := by simpa [f, isPolynomial_reflectedActivation_iff] + have hT : T ≠ 0 := Distribution.iteratedLineDerivOp_ofFun_ne_zero_of_not_isPolynomial hf n + obtain ⟨φ, hφ⟩ := T.exists_ne_zero hT + refine ⟨φ, ?_⟩ + have hfloc : LocallyIntegrableOn f ⊤ volume := + f.continuous.locallyIntegrable.locallyIntegrableOn _ + have heval : T φ = (-1 : ℝ) ^ n * + ∫ s : ℝ, ((TestFunction.lineDerivCLM ℝ (1 : ℝ))^[n]) φ s * σ (-s) := by + rw [Distribution.iteratedLineDerivOp_apply_iterated_testFunction, + Distribution.ofFun_apply hfloc] + simp [smul_eq_mul, f, reflectedActivation_apply] + intro hzero + apply hφ + exact heval.trans (by simpa) + +/-- For every order, a nonpolynomial continuous activation has a test-function convolution whose +derivative is nonzero at the origin in that order. -/ +theorem exists_testFunction_iteratedDeriv_convolutionActivation_ne_zero + {σ : C(ℝ, ℝ)} (hσ : ¬ Function.IsPolynomial σ) (n : ℕ) : + ∃ φ : 𝓓((⊤ : TopologicalSpace.Opens ℝ), ℝ), + iteratedDeriv n (convolutionActivation φ σ) 0 ≠ 0 := by + obtain ⟨φ, hφ⟩ := exists_testFunction_iteratedLineDeriv_integral_mul_reflected_ne_zero hσ n + exact ⟨φ, by simpa⟩ + +/-! ## Universality of nonpolynomial activations -/ + +variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] + +/-- Every continuous nonpolynomial activation is discriminatory on compact subsets of an arbitrary +real inner-product space. -/ +theorem isDiscriminatory_of_not_isPolynomial {σ : C(ℝ, ℝ)} + (hσ : ¬ Function.IsPolynomial σ) : IsDiscriminatory E σ := by + apply isDiscriminatory_of_smooth_ridges + intro n + obtain ⟨φ, hφ⟩ := exists_testFunction_iteratedDeriv_convolutionActivation_ne_zero hσ n + refine ⟨convolutionActivation φ σ, 0, convolutionActivation_contDiff φ σ φ.contDiff, hφ, ?_⟩ + intro K hK Λ hΛ + exact annihilates_convolutionActivation_neurons φ hK hΛ + +/-- Every continuous nonpolynomial activation has dense network space on every compact subset +of a real inner-product space. -/ +theorem dense_spaceOn_of_not_isPolynomial + {σ : C(ℝ, ℝ)} (hσ : ¬ Function.IsPolynomial σ) {K : Set E} (hK : IsCompact K) : + Dense (spaceOn σ K : Set C(K, ℝ)) := + (dense_spaceOn_iff_isDiscriminatory σ).2 (isDiscriminatory_of_not_isPolynomial hσ) K hK + +end Learning.ShallowNetwork diff --git a/LeanMachineLearning/NeuralNetwork/UniversalApproximation/PolynomialObstruction.lean b/LeanMachineLearning/NeuralNetwork/UniversalApproximation/PolynomialObstruction.lean new file mode 100644 index 00000000..37e822a9 --- /dev/null +++ b/LeanMachineLearning/NeuralNetwork/UniversalApproximation/PolynomialObstruction.lean @@ -0,0 +1,115 @@ +/- +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 LeanMachineLearning.ForMathlib.Algebra.Polynomial.Function +public import LeanMachineLearning.ForMathlib.Topology.Algebra.Module.FiniteDimension +public import LeanMachineLearning.ForMathlib.Topology.ContinuousMap.Algebra +public import LeanMachineLearning.NeuralNetwork.Shallow.Basic +public import Mathlib.RingTheory.Polynomial.DegreeLT +public import Mathlib.Topology.Separation.Basic + +/-! +# Polynomial obstructions to universal approximation + +On sufficiently many collinear sample points, every ridge function obtained from a polynomial +activation belongs to a fixed finite-dimensional space of univariate polynomials. This gives the +necessary direction of the Leshno--Lin--Pinkus--Schocken theorem. +-/ + +@[expose] public section + +open Polynomial + +namespace Learning.ShallowNetwork + +variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] + +/-- The space of continuous real-valued functions on `n` distinct scalar multiples of a nonzero +vector has dimension `n`. + +The statement is phrased using a range, so it applies without choosing a finite set enumeration. +-/ +theorem finrank_continuousMap_range_fin_smul {e : E} (he : e ≠ 0) (n : ℕ) : + Module.finrank ℝ C(Set.range (fun i : Fin n ↦ (i : ℝ) • e), ℝ) = n := by + classical + let emb : Fin n ↪ E := + ⟨fun i ↦ (i : ℝ) • e, fun i j hij ↦ by + apply Fin.ext + exact_mod_cast (smul_left_injective ℝ he hij)⟩ + let K : Set E := Set.range emb + have hcard : Fintype.card K = n := + (Fintype.card_congr emb.toEquivRange).symm.trans (Fintype.card_fin n) + change Module.finrank ℝ C(K, ℝ) = n + rw [(LinearEquiv.ofBijective (ContinuousMap.coeFnCLM ℝ).toLinearMap + ContinuousMap.equivFnOfDiscrete.bijective).finrank_eq, Module.finrank_pi, hcard] + +private theorem aeval_degreeLT_range_ne_top {X : Type*} [TopologicalSpace X] + {coordinate : C(X, ℝ)} {n : ℕ} + (hfinrank : Module.finrank ℝ C(X, ℝ) = n + 1) : + ((Polynomial.aeval coordinate).toLinearMap.domRestrict (degreeLT ℝ n)).range ≠ ⊤ := by + intro htop + have hrank := LinearMap.finrank_range_le + ((Polynomial.aeval coordinate).toLinearMap.domRestrict (degreeLT ℝ n)) + rw [htop, finrank_top, hfinrank, + Module.finrank_eq_card_basis (degreeLT.basis ℝ n), Fintype.card_fin] at hrank + lia + +/-- If the activation is polynomial, then its shallow-network space fails to be dense on some +finite (hence compact) set. No finite-dimensionality assumption on the input space is needed. -/ +theorem exists_compact_not_dense_of_isPolynomial [Nontrivial E] + {σ : C(ℝ, ℝ)} (hσ : Function.IsPolynomial σ) : + ∃ K : Set E, IsCompact K ∧ ¬ Dense (spaceOn σ K : Set C(K, ℝ)) := by + obtain ⟨p, hp⟩ := hσ + obtain ⟨e, he⟩ : ∃ e : E, e ≠ 0 := exists_ne 0 + let emb : Fin (p.natDegree + 2) ↪ E := + ⟨fun i ↦ (i : ℝ) • e, fun i j hij ↦ by + apply Fin.ext + exact_mod_cast (smul_left_injective ℝ he hij)⟩ + let K : Set E := Set.range emb + let coordinate : C(K, ℝ) := ⟨fun x ↦ inner ℝ e x / inner ℝ e e, by fun_prop⟩ + let evalDegree : degreeLT ℝ (p.natDegree + 1) →ₗ[ℝ] C(K, ℝ) := + (Polynomial.aeval coordinate).toLinearMap.domRestrict (degreeLT ℝ (p.natDegree + 1)) + have hfinrank : Module.finrank ℝ C(K, ℝ) = p.natDegree + 2 := + finrank_continuousMap_range_fin_smul he _ + have hproper : evalDegree.range ≠ ⊤ := aeval_degreeLT_range_ne_top hfinrank + have hspace : (spaceOn σ K : Set C(K, ℝ)) ⊆ evalDegree.range := by + rw [SetLike.coe_subset_coe, spaceOn] + apply Submodule.span_le.2 + rintro _ ⟨⟨w, b⟩, rfl⟩ + let q := p.comp (C (inner ℝ w e) * X + C b) + have hq : q ∈ degreeLT ℝ (p.natDegree + 1) := by + rw [degreeLT_succ_eq_degreeLE, mem_degreeLE, ← natDegree_le_iff_degree_le] + calc + q.natDegree ≤ p.natDegree * (C (inner ℝ w e) * X + C b).natDegree := natDegree_comp_le + _ ≤ p.natDegree * 1 := Nat.mul_le_mul_left _ <| natDegree_add_le_of_degree_le + (by simpa using natDegree_C_mul_X_pow_le (inner ℝ w e) 1) (by simp) + _ = p.natDegree := Nat.mul_one _ + refine ⟨⟨q, hq⟩, ?_⟩ + ext x + obtain ⟨i, hi⟩ := x.property + simp only [evalDegree, LinearMap.domRestrict_apply, AlgHom.toLinearMap_apply, + Polynomial.aeval_continuousMap_apply, coordinate, ContinuousMap.coe_mk, + ContinuousMap.restrict_apply, neuron_apply] + rw [← hp, ← hi] + have hemb : emb i = (i : ℝ) • e := rfl + have : inner ℝ e ((i : ℝ) • e) / inner ℝ e e = (i : ℝ) := by + rw [real_inner_smul_right, div_eq_iff (inner_self_ne_zero.mpr he)] + rw [hemb, this] + simp [q, real_inner_smul_right, mul_comm (inner ℝ w e)] + exact ⟨K, (Set.finite_range emb).isCompact, + evalDegree.range.not_dense_of_subset_of_finiteDimensional hproper hspace⟩ + +/-- Density of the network space on every compact set forces the activation not to be a +polynomial, provided the input space is nontrivial. -/ +theorem not_isPolynomial_of_dense_spaceOn [Nontrivial E] (σ : C(ℝ, ℝ)) + (hσ : ∀ (K : Set E), IsCompact K → Dense (spaceOn σ K : Set C(K, ℝ))) : + ¬ Function.IsPolynomial σ := by + intro hPolynomial + obtain ⟨K, hK, hnotDense⟩ := exists_compact_not_dense_of_isPolynomial (E := E) hPolynomial + exact hnotDense (hσ K hK) + +end Learning.ShallowNetwork