archive: smooth functions whose integral calculates the values of pol…

…ynomials (#9138)

Test case of the library suggested by Martin Hairer, see https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Hairer.20challenge/near/404836147.



Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
Co-authored-by: Johan Commelin <johan@commelin.net>

Archive.lean

@@ -4,6 +4,7 @@ import Archive.Examples.IfNormalization.Statement
 import Archive.Examples.IfNormalization.WithoutAesop
 import Archive.Examples.MersennePrimes
 import Archive.Examples.PropEncodable
+import Archive.Hairer
 import Archive.Imo.Imo1959Q1
 import Archive.Imo.Imo1960Q1
 import Archive.Imo.Imo1962Q1

Archive/Hairer.lean

@@ -0,0 +1,135 @@
+/-
+Copyright (c) 2023 Floris Van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johan Commelin, Sébastien Gouëzel, Patrick Massot, Ruben Van de Velde, Floris Van Doorn,
+Junyan Xu
+-/
+import Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff
+import Mathlib.RingTheory.MvPolynomial.Basic
+import Mathlib.Analysis.Analytic.Polynomial
+import Mathlib.Analysis.Analytic.Uniqueness
+import Mathlib.Data.MvPolynomial.Funext
+
+/-!
+# Smooth functions whose integral calculates the values of polynomials
+
+In any space `ℝᵈ` and given any `N`, we construct a smooth function supported in the unit ball
+whose integral against a multivariate polynomial `P` of total degree at most `N` is `P 0`.
+
+This is a test of the state of the library suggested by Martin Hairer.
+-/
+
+noncomputable section
+
+open Metric Set MeasureTheory
+open MvPolynomial hiding support
+open Function hiding eval
+
+section normed
+variable {𝕜 E F : Type*} [NontriviallyNormedField 𝕜]
+variable [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F]
+
+variable (𝕜 E F) in
+/-- The set of smooth functions supported in a set `s`, as a submodule of the space of functions. -/
+def SmoothSupportedOn (n : ℕ∞) (s : Set E) : Submodule 𝕜 (E → F) where
+  carrier := { f : E → F | tsupport f ⊆ s ∧ ContDiff 𝕜 n f }
+  add_mem' hf hg := ⟨tsupport_add.trans <| union_subset hf.1 hg.1, hf.2.add hg.2⟩
+  zero_mem' :=
+    ⟨(tsupport_eq_empty_iff.mpr rfl).subset.trans (empty_subset _), contDiff_const (c := 0)⟩
+  smul_mem' r f hf :=
+    ⟨(closure_mono <| support_smul_subset_right r f).trans hf.1, contDiff_const.smul hf.2⟩
+
+namespace SmoothSupportedOn
+
+variable {n : ℕ∞} {s : Set E}
+
+instance : FunLike (SmoothSupportedOn 𝕜 E F n s) E (fun _ ↦ F) where
+  coe := Subtype.val
+  coe_injective' := Subtype.coe_injective
+
+@[simp]
+lemma coe_mk (f : E → F) (h) : (⟨f, h⟩ : SmoothSupportedOn 𝕜 E F n s) = f := rfl
+
+lemma tsupport_subset (f : SmoothSupportedOn 𝕜 E F n s) : tsupport f ⊆ s := f.2.1
+
+lemma support_subset (f : SmoothSupportedOn 𝕜 E F n s) :
+    support f ⊆ s := subset_tsupport _ |>.trans (tsupport_subset f)
+
+lemma contDiff (f : SmoothSupportedOn 𝕜 E F n s) :
+    ContDiff 𝕜 n f := f.2.2
+
+theorem continuous (f : SmoothSupportedOn 𝕜 E F n s) : Continuous f :=
+  (SmoothSupportedOn.contDiff _).continuous
+
+lemma hasCompactSupport [ProperSpace E] (f : SmoothSupportedOn 𝕜 E F n (closedBall 0 1)) :
+    HasCompactSupport f :=
+  HasCompactSupport.of_support_subset_isCompact (isCompact_closedBall 0 1) (support_subset f)
+
+end SmoothSupportedOn
+
+end normed
+open SmoothSupportedOn
+
+instance {R σ : Type*} [CommSemiring R] [Finite σ] (N : ℕ) :
+    Module.Finite R (restrictTotalDegree σ R N) :=
+  have : Finite {n : σ →₀ ℕ | ∀ i, n i ≤ N} := by
+    erw [Finsupp.equivFunOnFinite.subtypeEquivOfSubtype'.finite_iff, Set.finite_coe_iff]
+    convert Set.Finite.pi fun _ : σ ↦ Set.finite_le_nat N using 1
+    ext; rw [mem_univ_pi]; rfl
+  have : Finite {s : σ →₀ ℕ | s.sum (fun _ e ↦ e) ≤ N} := by
+    rw [Set.finite_coe_iff] at this ⊢
+    exact this.subset fun n hn i ↦ (eq_or_ne (n i) 0).elim
+      (fun h ↦ h.trans_le N.zero_le) fun h ↦
+        (Finset.single_le_sum (fun _ _ ↦ Nat.zero_le _) <| Finsupp.mem_support_iff.mpr h).trans hn
+  Module.Finite.of_basis (basisRestrictSupport R _)
+
+variable {ι : Type*}
+lemma MvPolynomial.continuous_eval (p : MvPolynomial ι ℝ) :
+    Continuous fun x ↦ (eval x) p := by
+  continuity
+
+variable [Fintype ι]
+theorem SmoothSupportedOn.integrable_eval_mul (p : MvPolynomial ι ℝ)
+    (f : SmoothSupportedOn ℝ (EuclideanSpace ℝ ι) ℝ ⊤ (closedBall 0 1)) :
+    Integrable fun (x : EuclideanSpace ℝ ι) ↦ eval x p * f x :=
+  (p.continuous_eval.mul (SmoothSupportedOn.contDiff f).continuous).integrable_of_hasCompactSupport
+    (hasCompactSupport f).mul_left
+
+variable (ι)
+/-- Interpreting a multivariate polynomial as an element of the dual of smooth functions supported
+in the unit ball, via integration against Lebesgue measure. -/
+def L : MvPolynomial ι ℝ →ₗ[ℝ]
+    Module.Dual ℝ (SmoothSupportedOn ℝ (EuclideanSpace ℝ ι) ℝ ⊤ (closedBall 0 1)) :=
+  have int := SmoothSupportedOn.integrable_eval_mul (ι := ι)
+  .mk₂ ℝ (fun p f ↦ ∫ x : EuclideanSpace ℝ ι, eval x p • f x)
+    (fun p₁ p₂ f ↦ by simp [add_mul, integral_add (int p₁ f) (int p₂ f)])
+    (fun r p f ↦ by simp [mul_assoc, integral_mul_left])
+    (fun p f₁ f₂ ↦ by simp_rw [smul_eq_mul, ← integral_add (int p _) (int p _), ← mul_add]; rfl)
+    fun r p f ↦ by simp_rw [← integral_smul, smul_comm r]; rfl
+
+lemma inj_L : Injective (L ι) :=
+  (injective_iff_map_eq_zero _).mpr fun p hp ↦ by
+    have H : ∀ᵐ x : EuclideanSpace ℝ ι, x ∈ ball 0 1 → eval x p = 0 :=
+      isOpen_ball.ae_eq_zero_of_integral_contDiff_smul_eq_zero
+        (by exact continuous_eval p |>.locallyIntegrable.locallyIntegrableOn _)
+        fun g hg _h2g g_supp ↦ by
+          simpa [mul_comm (g _), L] using congr($hp ⟨g, g_supp.trans ball_subset_closedBall, hg⟩)
+    simp_rw [MvPolynomial.funext_iff, map_zero]
+    refine fun x ↦ AnalyticOn.eval_linearMap (EuclideanSpace.equiv ι ℝ).toLinearMap p
+      |>.eqOn_zero_of_preconnected_of_eventuallyEq_zero
+      (preconnectedSpace_iff_univ.mp inferInstance) (z₀ := 0) trivial
+      (Filter.mem_of_superset (Metric.ball_mem_nhds 0 zero_lt_one) ?_) trivial
+    rw [← ae_restrict_iff'₀ measurableSet_ball.nullMeasurableSet] at H
+    apply Measure.eqOn_of_ae_eq H p.continuous_eval.continuousOn continuousOn_const
+    rw [isOpen_ball.interior_eq]
+    apply subset_closure
+
+lemma hairer (N : ℕ) (ι : Type*) [Fintype ι] :
+    ∃ (ρ : EuclideanSpace ℝ ι → ℝ), tsupport ρ ⊆ closedBall 0 1 ∧ ContDiff ℝ ⊤ ρ ∧
+    ∀ (p : MvPolynomial ι ℝ), p.totalDegree ≤ N →
+    ∫ x : EuclideanSpace ℝ ι, eval x p • ρ x = eval 0 p := by
+  have := (inj_L ι).comp (restrictTotalDegree ι ℝ N).injective_subtype
+  rw [← LinearMap.coe_comp] at this
+  obtain ⟨⟨φ, supφ, difφ⟩, hφ⟩ :=
+    LinearMap.flip_surjective_iff₁.2 this ((aeval 0).toLinearMap.comp <| Submodule.subtype _)
+  exact ⟨φ, supφ, difφ, fun P hP ↦ congr($hφ ⟨P, (mem_restrictTotalDegree ι N P).mpr hP⟩)⟩

Mathlib.lean

@@ -560,6 +560,7 @@ import Mathlib.Analysis.Analytic.Constructions
 import Mathlib.Analysis.Analytic.Inverse
 import Mathlib.Analysis.Analytic.IsolatedZeros
 import Mathlib.Analysis.Analytic.Linear
+import Mathlib.Analysis.Analytic.Polynomial
 import Mathlib.Analysis.Analytic.RadiusLiminf
 import Mathlib.Analysis.Analytic.Uniqueness
 import Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Mathlib/Analysis/Analytic/Polynomial.lean

@@ -0,0 +1,77 @@
+/-
+Copyright (c) 2023 Junyan Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Junyan Xu
+-/
+import Mathlib.Analysis.Analytic.Constructions
+import Mathlib.Data.Polynomial.AlgebraMap
+import Mathlib.Data.MvPolynomial.Basic
+import Mathlib.Topology.Algebra.Module.FiniteDimension
+
+/-!
+# Polynomials are analytic
+
+This file combines the analysis and algebra libraries and shows that evaluation of a polynomial
+is an analytic function.
+-/
+
+variable {𝕜 E A B : Type*} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]
+  [CommSemiring A] {z : E} {s : Set E}
+
+section Polynomial
+open Polynomial
+
+variable [NormedRing B] [NormedAlgebra 𝕜 B] [Algebra A B] {f : E → B}
+
+theorem AnalyticAt.aeval_polynomial (hf : AnalyticAt 𝕜 f z) (p : A[X]) :
+    AnalyticAt 𝕜 (fun x ↦ aeval (f x) p) z := by
+  refine p.induction_on (fun k ↦ ?_) (fun p q hp hq ↦ ?_) fun p i hp ↦ ?_
+  · simp_rw [aeval_C]; apply analyticAt_const
+  · simp_rw [aeval_add]; exact hp.add hq
+  · convert hp.mul hf
+    simp_rw [pow_succ', aeval_mul, ← mul_assoc, aeval_X]
+
+theorem AnalyticOn.aeval_polynomial (hf : AnalyticOn 𝕜 f s) (p : A[X]) :
+    AnalyticOn 𝕜 (fun x ↦ aeval (f x) p) s := fun x hx ↦ (hf x hx).aeval_polynomial p
+
+theorem AnalyticOn.eval_polynomial {A} [NormedCommRing A] [NormedAlgebra 𝕜 A] (p : A[X]) :
+    AnalyticOn 𝕜 (eval · p) Set.univ := (analyticOn_id 𝕜).aeval_polynomial p
+
+end Polynomial
+
+section MvPolynomial
+open MvPolynomial
+
+variable [NormedCommRing B] [NormedAlgebra 𝕜 B] [Algebra A B] {σ : Type*} {f : E → σ → B}
+
+theorem AnalyticAt.aeval_mvPolynomial (hf : ∀ i, AnalyticAt 𝕜 (f · i) z) (p : MvPolynomial σ A) :
+    AnalyticAt 𝕜 (fun x ↦ aeval (f x) p) z := by
+  apply p.induction_on (fun k ↦ ?_) (fun p q hp hq ↦ ?_) fun p i hp ↦ ?_ -- `refine` doesn't work
+  · simp_rw [aeval_C]; apply analyticAt_const
+  · simp_rw [map_add]; exact hp.add hq
+  · simp_rw [map_mul, aeval_X]; exact hp.mul (hf i)
+
+theorem AnalyticOn.aeval_mvPolynomial (hf : ∀ i, AnalyticOn 𝕜 (f · i) s) (p : MvPolynomial σ A) :
+    AnalyticOn 𝕜 (fun x ↦ aeval (f x) p) s := fun x hx ↦ .aeval_mvPolynomial (hf · x hx) p
+
+theorem AnalyticOn.eval_continuousLinearMap (f : E →L[𝕜] σ → B) (p : MvPolynomial σ B) :
+    AnalyticOn 𝕜 (fun x ↦ eval (f x) p) Set.univ :=
+  fun x _ ↦ .aeval_mvPolynomial (fun i ↦ ((ContinuousLinearMap.proj i).comp f).analyticAt x) p
+
+theorem AnalyticOn.eval_continuousLinearMap' (f : σ → E →L[𝕜] B) (p : MvPolynomial σ B) :
+    AnalyticOn 𝕜 (fun x ↦ eval (f · x) p) Set.univ :=
+  fun x _ ↦ .aeval_mvPolynomial (fun i ↦ (f i).analyticAt x) p
+
+variable [CompleteSpace 𝕜] [T2Space E] [FiniteDimensional 𝕜 E]
+
+theorem AnalyticOn.eval_linearMap (f : E →ₗ[𝕜] σ → B) (p : MvPolynomial σ B) :
+    AnalyticOn 𝕜 (fun x ↦ eval (f x) p) Set.univ :=
+  AnalyticOn.eval_continuousLinearMap { f with cont := f.continuous_of_finiteDimensional } p
+
+theorem AnalyticOn.eval_linearMap' (f : σ → E →ₗ[𝕜] B) (p : MvPolynomial σ B) :
+    AnalyticOn 𝕜 (fun x ↦ eval (f · x) p) Set.univ := AnalyticOn.eval_linearMap (.pi f) p
+
+theorem AnalyticOn.eval_mvPolynomial [Fintype σ] (p : MvPolynomial σ 𝕜) :
+    AnalyticOn 𝕜 (eval · p) Set.univ := AnalyticOn.eval_linearMap (.id (R := 𝕜) (M := σ → 𝕜)) p
+
+end MvPolynomial

Mathlib/RingTheory/MvPolynomial/Basic.lean

@@ -76,17 +76,38 @@ end Homomorphism
 
 section Degree
 
+variable {σ}
+
+/-- The submodule of polynomials that are sum of monomials in the set `s`. -/
+def restrictSupport (s : Set (σ →₀ ℕ)) : Submodule R (MvPolynomial σ R) :=
+  Finsupp.supported _ _ s
+
+/-- `restrictSupport R s` has a canonical `R`-basis indexed by `s`. -/
+def basisRestrictSupport (s : Set (σ →₀ ℕ)) : Basis s R (restrictSupport R s) where
+  repr := Finsupp.supportedEquivFinsupp s
+
+theorem restrictSupport_mono {s t : Set (σ →₀ ℕ)} (h : s ⊆ t) :
+    restrictSupport R s ≤ restrictSupport R t := Finsupp.supported_mono h
+
+variable (σ)
+
 /-- The submodule of polynomials of total degree less than or equal to `m`.-/
-def restrictTotalDegree : Submodule R (MvPolynomial σ R) :=
-  Finsupp.supported _ _ { n | (n.sum fun _ e => e) ≤ m }
+def restrictTotalDegree (m : ℕ) : Submodule R (MvPolynomial σ R) :=
+  restrictSupport R { n | (n.sum fun _ e => e) ≤ m }
 #align mv_polynomial.restrict_total_degree MvPolynomial.restrictTotalDegree
 
 /-- The submodule of polynomials such that the degree with respect to each individual variable is
 less than or equal to `m`.-/
 def restrictDegree (m : ℕ) : Submodule R (MvPolynomial σ R) :=
-  Finsupp.supported _ _ { n | ∀ i, n i ≤ m }
+  restrictSupport R { n | ∀ i, n i ≤ m }
 #align mv_polynomial.restrict_degree MvPolynomial.restrictDegree
 
+theorem restrictTotalDegree_le_restrictDegree (m : ℕ) :
+    restrictTotalDegree σ R m ≤ restrictDegree σ R m :=
+  restrictSupport_mono R fun n hn i ↦ (eq_or_ne (n i) 0).elim
+    (fun h ↦ h.trans_le m.zero_le) fun h ↦
+      (Finset.single_le_sum (fun _ _ ↦ Nat.zero_le _) <| Finsupp.mem_support_iff.mpr h).trans hn
+
 variable {R}
 
 theorem mem_restrictTotalDegree (p : MvPolynomial σ R) :
@@ -97,7 +118,7 @@ theorem mem_restrictTotalDegree (p : MvPolynomial σ R) :
 
 theorem mem_restrictDegree (p : MvPolynomial σ R) (n : ℕ) :
     p ∈ restrictDegree σ R n ↔ ∀ s ∈ p.support, ∀ i, (s : σ →₀ ℕ) i ≤ n := by
-  rw [restrictDegree, Finsupp.mem_supported]
+  rw [restrictDegree, restrictSupport, Finsupp.mem_supported]
   rfl
 #align mv_polynomial.mem_restrict_degree MvPolynomial.mem_restrictDegree