Hairer challenge

Stream: maths

[Kevin Buzzard]

I'm visiting EPFL. Martin Hairer said he wanted to see how Lean worked in practice, so asked me a challenge question: to prove that for $d$ and $N$ naturals, there is a C^infty function $\rho$ on $\R^d$ supported on the closed ball such that $\int\rho(x)P(x)dx=P(0)$ for all polynomials of total degree at most $N$. He sketched some proofs, e.g. "it's true for the delta function and now just perturb it a bit, you only need to satisfy finitely many criteria" or "use integration by parts and the fact that if you differentiate $P$ $N+1$ times you get zero" or "consider functions supported very close to a point in $\R^d$ and now use lots of points and take a linear combination". But I told him that I couldn't possibly code up any of these in real time because I had no idea what was in the library :-( Are any of these straightforward to push through given what we have?

[Floris van Doorn]

Am I right that it follow for purely abstract reasons if we prove that
dimension(C^infty functions supported on the closed ball) > dimension(polynomials of degree N)?
If so, we just need to show that the LHS is infinite.

[Damiano Testa]

Floris, I think that you need a little more: the space of C-infty functions supported on the unit ball that are also 0 at 0 is also infinite-dimensional, but is no good for the conclusion that you want. This is an affine-linear problem, so you should embed in your statement the fact that there is a solution to the affine version, before you can get the whole "add a general solution of the associated linear problem".

... or am I wrong? :smile:

EDIT: maybe I am wrong. This problem is linear in P.

[Damiano Testa]

Btw, to get infinite dimensionality, you can take any non-zero function supported on the unit ball and show that multiplication by polynomials is injective by arguing that two polynomials multiplying to the same function would be polynomials that agree on the support of the initial function, which is open and non-empty, by the assumption that the function is non-zero.

[Damiano Testa]

But this argument still does not give you an example, I think.

[Ruben Van de Velde]

Somebody once told me you should formalise the statement first if you want help with a proof ;)

[Kevin Buzzard]

I think Damiano's right; this was the method I wanted to use but you have a big vector space V and finitely many linear maps from V to the reals, you have the intersection W of their kernels (so W has finite codimension in V so it's huge) and then you have the preimage of {1} under another linear map and you need to check that this preimage of {1} meets W, which is not formal, it probably boils down to an assertion of the form "the linear map sending rho to integral of rho(x) is not in the span of the linear maps sending rho to integral of rho(x).x^n for 0<n<=d (where n is a vector).

[Damiano Testa]

Ok, I think that my confusion arises from the fact that the problem is linear in P but only affine-linear in $\rho$. I think that, to use Floris' idea, we would like linearity in $\rho$.

[Kevin Buzzard]

Ruben Van de Velde said:

Somebody once told me you should formalise the statement first if you want help with a proof ;)

:heart: My problem was that I know this part of the library so poorly that it would take me forever to even state the question formally :-) I used LaTeX though, what more do you want?!

[Damiano Testa]

I like Floris' point of view, but here is an example to show that you need more work.

Let $V$ be the vector space of C-infinity functions supported on the unit ball and with integral 0. We informally know that this vector space is infinite-dimensional. However, by definition, for all of these functions, the integral with the constant polynomial $1$ yields $0$, not $1 = P(0)$.

[Damiano Testa]

Given Floris' argument, all that seems to be missing is the following assertion:

for every finite set $F$ of monomials, there is a compactly supported C-infinity function $f_F$ such that, for all $m \in F$, the integral of $f_Fm$ is zero iff $m$ is non-constant.

[Floris van Doorn]

Yes, I think we need more than what I said at the start. And I agree we need something like Damiano's last statement.

[Floris van Doorn]

Here is a statement of the original challenge:

import Mathlib.Geometry.Manifold.PartitionOfUnity
import Mathlib.Data.MvPolynomial.Variables

open Metric MvPolynomial

lemma hairer (N : ℕ) (ι : Type*) [Fintype ι] :
  ∃(ρ : (ι → ℝ) → ℝ), tsupport ρ ⊆ closedBall 0 1 ∧ ContDiff ℝ ⊤ ρ ∧
  ∀ (p : MvPolynomial ι ℝ), p.totalDegree ≤ N → ∫ x, eval x p • ρ x = eval 0 p  :=
  sorry

[Floris van Doorn]

(or maybe EuclideanSpace ℝ ι instead of ι → ℝ to have the usual metric)

[Yury G. Kudryashov]

We have BumpFunction for either case.

[Damiano Testa]

We can probably reduce to the 1-dimensional case by considering products of 1-variable functions that are solutions, right?

[Damiano Testa]

So, for n : ℕ, does there exist a BumbFunction f on ℝ such that, for i < n, the integral of f * X ^ i vanishes if and only if i \ne 0?

[Damiano Testa]

(the answer is

Floris van Doorn said:

Here is a statement of the original challenge:

import Mathlib.Geometry.Manifold.PartitionOfUnity
import Mathlib.Data.MvPolynomial.Variables

open Metric MvPolynomial

lemma hairer (N : ℕ) (ι : Type*) [Fintype ι] :
  ∃(ρ : (ι → ℝ) → ℝ), tsupport ρ ⊆ closedBall 0 1 ∧ ContDiff ℝ ⊤ ρ ∧
  ∀ (p : MvPolynomial ι ℝ), p.totalDegree ≤ N → ∫ x, eval x p • ρ x = eval 0 p  :=
  sorry

This is a good proof_wanted example, right? :smile:

[Damiano Testa]

And this might be a formalization of the missing step, after Floris' reduction:

open Polynomial Metric

proof_wanted one_d (n : ℕ) : ∃ ρ : ℝ → ℝ, tsupport ρ ⊆ closedBall 0 1 ∧ ContDiff ℝ ⊤ ρ ∧
  ∀ i, i ≤ n → ∫ x, eval x (X ^ i) • ρ x ≠ 0 ↔ i = 0

[Floris van Doorn]

I was thinking of something like this originally, which should be sufficient to prove the challenge, I think:

import Mathlib.Geometry.Manifold.PartitionOfUnity

open Metric

variable {𝕜 E E' F : Type*} [NontriviallyNormedField 𝕜]
  [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  [NormedAddCommGroup F] [NormedSpace 𝕜 F]

variable (𝕜 E F) in
@[reducible]
def SmoothSupportedOn (n : ℕ∞) (s : Set E) : Submodule 𝕜 (E → F) where
  carrier := { f : E → F | tsupport f ⊆ s ∧ ContDiff 𝕜 n f }
  add_mem' := sorry
  zero_mem' := sorry
  smul_mem' := sorry

example {ι} [Fintype ι] :
    ∃ s : ℕ → SmoothSupportedOn ℝ (EuclideanSpace ℝ ι) ℝ ⊤ (closedBall 0 1),
    LinearIndependent ℝ s ∧ ∀ n, ∫ x, (s n).1 x = 1 := sorry

The proof sketch of this sorry is: choose countably infinite many disjoint closed balls inside closedBall 0 1 and take a bump function on each of these balls.
And the proof sketch of the challenge then is: take an affine combination of the s i.

[Damiano Testa]

I suspect that there is still something missing to be spelled out: if your functions are all odd, is it a problem? Is it ruled out by something that I am failing to see?

[Floris van Doorn]

I assume that their integral is 1.
The only non-linear condition is for the constant polynomial, which is to say that the integral of $\rho$ must be nonzero. But an affine combination of bump functions will have integral 1.

[Damiano Testa]

Ah, I had missed the integral 1 condition!

[Damiano Testa]

I still need to wrap my head around some thoughts that are bugging me about this.

[Damiano Testa]

If all functions that you use are non-negative and all contained in the positive orthant, you need negative coefficients. Affine combination is simply that the sum of the coefficients is 1, not that they are non-negative, right? I guess that would be convex combination. Maybe this is what was bugging me!

[Damiano Testa]

Sorry, have to go, but this is a fun question!

[Yury G. Kudryashov]

@Floris van Doorn Your statement follows from the following one: if f n is a sequence of functions with strictly decreasing supports, then they are linearly independent.

[Yury G. Kudryashov]

I don't understand why your statement implies the original one.

[Yury G. Kudryashov]

I.e., we still need to show that the conditions are linearly independent on our subspace.

[Floris van Doorn]

Yury G. Kudryashov said:

Floris van Doorn Your statement follows from the following one: if f n is a sequence of functions with strictly decreasing supports, then they are linearly independent.

I was using disjoint (non-empty) supports, which should also work.

[Floris van Doorn]

But maybe fixing around a single point and only changing the radius is easier...

[Floris van Doorn]

Yury G. Kudryashov said:

I don't understand why your statement implies the original one.

Here is the proof sketch I'm imagining.

import Mathlib.Geometry.Manifold.PartitionOfUnity
import Mathlib.Data.MvPolynomial.Variables

open Metric Set MeasureTheory

section linear

variable {𝕜 : Type*} [Field 𝕜]
variable {E E' F  : Type*}
  [AddCommGroup E] [Module 𝕜 E]

lemma exists_affineSpan_zero {ι ι'} (s : Finset ι) [Infinite ι'] (L : ι → E →ₗ[𝕜] 𝕜) (x : ι' → E)
  (hx : LinearIndependent 𝕜 x) : ∃ y ∈ affineSpan 𝕜 (range x), ∀ i ∈ s, L i y = 0 := sorry

end linear

section normed
open Function
variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
variable {E E' F  : Type*}
  [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  [NormedAddCommGroup E'] [NormedSpace 𝕜 E']
  [NormedAddCommGroup F] [NormedSpace 𝕜 F]

variable (𝕜 E F) in
@[reducible]
def SmoothSupportedOn (n : ℕ∞) (s : Set E) : Submodule 𝕜 (E → F) where
  carrier := { f : E → F | tsupport f ⊆ s ∧ ContDiff 𝕜 n f }
  add_mem' hf hg := ⟨sorry, 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⟩

end normed

noncomputable section real

open Metric MvPolynomial

lemma step (ι) [Fintype ι] :
    ∃ f : ℕ → SmoothSupportedOn ℝ (EuclideanSpace ℝ ι) ℝ ⊤ (closedBall 0 1),
    LinearIndependent ℝ f ∧ ∀ n, ∫ x, (f n).1 x = 1 := by
  obtain ⟨s, r, hs, hr, h2s⟩ : ∃ (s : ℕ → EuclideanSpace ℝ ι) (r : ℕ → ℝ),
    Pairwise (Disjoint on (fun i ↦ closedBall (s i) (r i))) ∧
    (∀ i, 0 < r i) ∧ (∀ i, ball (s i) (r i) ⊆ closedBall 0 1)
  · sorry
  let f1 n : ContDiffBump (s n) := ⟨r n / 2, r n, half_pos (hr n), half_lt_self (hr n)⟩
  let f2 n : SmoothSupportedOn ℝ (EuclideanSpace ℝ ι) ℝ ⊤ (closedBall 0 1) :=
    ⟨(f1 n).normed volume, sorry⟩
  refine ⟨f2, ?_, fun n ↦ (f1 n).integral_normed⟩
  sorry

def L {ι : Type*} [Fintype ι] (p : MvPolynomial ι ℝ) :
  SmoothSupportedOn ℝ (EuclideanSpace ℝ ι) ℝ ⊤ (closedBall 0 1) →ₗ[ℝ] ℝ where
    toFun f := ∫ x, eval x p • f.1 x
    map_add' := sorry
    map_smul' := sorry

lemma hairer (N : ℕ) (ι : Type*) [Fintype ι] :
    ∃ (ρ : EuclideanSpace ℝ ι → ℝ), tsupport ρ ⊆ closedBall 0 1 ∧ ContDiff ℝ ⊤ ρ ∧
    ∀ (p : MvPolynomial ι ℝ), p.totalDegree ≤ N → ∫ x, eval x p • ρ x = eval 0 p := by
  obtain ⟨f, hf, h2f⟩ := step ι
  suffices : ∃ (ρ : EuclideanSpace ℝ ι → ℝ), tsupport ρ ⊆ closedBall 0 1 ∧ ContDiff ℝ ⊤ ρ ∧
    ∫ x, ρ x = 1 ∧
    ∀ i : ι →₀ ℕ, let p := monomial i 1; i ≠ 0 → i.sum (fun _ j ↦ j) ≤ N → ∫ x, eval x p • ρ x = 0
  · sorry
  let s : Finset (ι →₀ ℕ) := Finite.toFinset (s := {i | i ≠ 0 ∧ i.sum (fun _ j ↦ j) ≤ N}) sorry
  obtain ⟨ρ, hρ, h2ρ⟩ := exists_affineSpan_zero s (fun i ↦ L (monomial i 1)) f hf
  refine ⟨ρ, ?_, ?_, ?_, ?_⟩
  all_goals sorry

end real

[Floris van Doorn]

Or maybe this is a better proof sketch, because it doesn't require us to reduce the general case to monomials:

import Mathlib.Geometry.Manifold.PartitionOfUnity
import Mathlib.Data.MvPolynomial.Variables

open Metric Set MeasureTheory

section linear

variable {𝕜 : Type*} [Field 𝕜]
variable {E E' F  : Type*}
  [AddCommGroup E] [Module 𝕜 E]
  [AddCommGroup F] [Module 𝕜 F]

lemma exists_affineSpan_zero {ι'} (s : Submodule 𝕜 F) [FiniteDimensional 𝕜 s] [Infinite ι']
  (L : F →ₗ[𝕜] E →ₗ[𝕜] 𝕜) (x : ι' → E) (hx : LinearIndependent 𝕜 x) :
  ∃ y ∈ affineSpan 𝕜 (range x), ∀ i ∈ s, L i y = 0 := sorry

variable (𝕜) in
def totalDegreeIn (ι : Type*) (s : Set ℕ) : Submodule 𝕜 (MvPolynomial ι 𝕜) where
  carrier := { p | p.totalDegree ∈ s}
  add_mem' := sorry
  zero_mem' := sorry
  smul_mem' := sorry

instance (ι : Type*) [Finite ι] (s : Finset ℕ) :
  FiniteDimensional 𝕜 (totalDegreeIn 𝕜 ι s) := sorry

end linear

section normed
open Function
variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
variable {E E' F  : Type*}
  [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  [NormedAddCommGroup E'] [NormedSpace 𝕜 E']
  [NormedAddCommGroup F] [NormedSpace 𝕜 F]

variable (𝕜 E F) in
@[reducible]
def SmoothSupportedOn (n : ℕ∞) (s : Set E) : Submodule 𝕜 (E → F) where
  carrier := { f : E → F | tsupport f ⊆ s ∧ ContDiff 𝕜 n f }
  add_mem' hf hg := ⟨sorry, 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⟩

end normed

noncomputable section real

open Metric MvPolynomial

lemma step (ι) [Fintype ι] :
    ∃ f : ℕ → SmoothSupportedOn ℝ (EuclideanSpace ℝ ι) ℝ ⊤ (closedBall 0 1),
    LinearIndependent ℝ f ∧ ∀ n, ∫ x, (f n).1 x = 1 := by
  obtain ⟨s, r, hs, hr, h2s⟩ : ∃ (s : ℕ → EuclideanSpace ℝ ι) (r : ℕ → ℝ),
    Pairwise (Disjoint on (fun i ↦ closedBall (s i) (r i))) ∧
    (∀ i, 0 < r i) ∧ (∀ i, ball (s i) (r i) ⊆ closedBall 0 1)
  · sorry
  let f1 n : ContDiffBump (s n) := ⟨r n / 2, r n, half_pos (hr n), half_lt_self (hr n)⟩
  let f2 n : SmoothSupportedOn ℝ (EuclideanSpace ℝ ι) ℝ ⊤ (closedBall 0 1) :=
    ⟨(f1 n).normed volume, sorry⟩
  refine ⟨f2, ?_, fun n ↦ (f1 n).integral_normed⟩
  sorry

def L {ι : Type*} [Fintype ι] :
  MvPolynomial ι ℝ →ₗ[ℝ] SmoothSupportedOn ℝ (EuclideanSpace ℝ ι) ℝ ⊤ (closedBall 0 1) →ₗ[ℝ] ℝ where
    toFun p :=
      { toFun := fun f ↦ ∫ x, eval x p • f.1 x
        map_add' := sorry
        map_smul' := sorry }
    map_add' := sorry
    map_smul' := sorry

lemma hairer (N : ℕ) (ι : Type*) [Fintype ι] :
    ∃ (ρ : EuclideanSpace ℝ ι → ℝ), tsupport ρ ⊆ closedBall 0 1 ∧ ContDiff ℝ ⊤ ρ ∧
    ∀ (p : MvPolynomial ι ℝ), p.totalDegree ≤ N → ∫ x, eval x p • ρ x = eval 0 p := by
  obtain ⟨f, hf, h2f⟩ := step ι
  obtain ⟨ρ, hρ, h2ρ⟩ := exists_affineSpan_zero (totalDegreeIn ℝ ι (Finset.Icc 1 N)) L f hf
  refine ⟨ρ, ?_, ?_, ?_⟩
  all_goals sorry

end real

[Floris van Doorn]

I should stop spending time on this, but here is the progress I have so far:
https://github.com/leanprover-community/mathlib4/blob/hairer/Mathlib/Hairer.lean

[Floris van Doorn]

Feel free to push to that branch!

[Floris van Doorn]

Ok, I am missing an additional condition in the lemma exists_affineSpan_zero that I proposed, and that is that the L imust be nonconstant on affineSpan 𝕜 (range x). I think that is sufficient, but now I'm not sure about that anymore.

[Vincent Beffara]

The integration by parts sound simpler to implement: once you have a smooth bump function, its kth derivative integrates to 0 against any monomial of degree less than k by integration by parts k times. So start with a bump function f of integral 1, this integrates correctly against constants. Then subtract a multiple of f' so it integrates to 0 against x, then a multiple of f'' so it integrates to 0 against x^2, and so on. So in the end \rho is a rather explicit linear combination of the first derivatives of f.

It might not be easier to turn into a Lean proof though ...

[Martin Hairer]

Hi all, just for a bit of background, the idea behind my question to Kevin was to formalise a proof of the "reconstruction theorem" which is the fundamental piece of analysis that makes regularity structures work. One reason for choosing this particular result is that it is a modern piece of analysis that has a proof that is quite short and doesn't rely on much machinery, so the hope was that it wouldn't be too hard to formalise (in particular the version for "germs" given by Caravenna and Zambotti). For me, the goal is to figure out how easy it is to actually formalise analysis with the current state of the art...

[Martin Hairer]

Regarding the proof of this particular statement, the two strategies I had in mind are either the one sketched by Vincent or the more abstract one that uses the fact that if one has N linearly independent elements y_i of the dual V^* of some real vector space V, then one can always find an element v in V such that y_0(v) = 1 and y_j(v) = 0 for every j>0 (or actually y_i(v) = a_i for any given numbers a_i). I guess there might already be something to that effect in the linear algebra part of mathlib, so maybe that's the cheapest one. Showing that integration against monomials are independent is easy since otherwise one could find a fixed non-zero polynomial that annihilates every test function which is absurd.

[Patrick Massot]

I formalized the outline based on what @Floris van Doorn wrote:

import Mathlib

noncomputable section

section missing_polynomial
open MvPolynomial Submodule

variable {R σ : Type*} [CommSemiring R] (n : ℕ)

lemma totalDegree_le_iff_mem_span {R σ : Type*} [CommSemiring R] {n : ℕ}
    {P : MvPolynomial σ R} : totalDegree P ≤ n ↔
    P ∈ span R ((fun c : σ →₀ ℕ ↦ monomial c (1 : R)) '' {s : σ →₀ ℕ | s.sum (fun _ e ↦ e) ≤ n}) := by
  sorry

/- Is this really missing?? -/
def evalAtₗ {R σ : Type*} [CommSemiring R] (x : σ → R) : MvPolynomial σ R →ₗ[R] R where
  toFun P := eval x P
  map_add' := by simp
  map_smul' := by simp

lemma finite_stuff [Finite σ] (N : ℕ) : {s : σ →₀ ℕ | s.sum (fun _ e ↦ e) ≤ N}.Finite := by
  sorry

end missing_polynomial

section missing_linear_algebra

open Module Submodule BigOperators

variable {K V V' ι : Type*} [Field K] [AddCommGroup V] [Module K V] [AddCommMonoid V'] [Module K V']
   {B : V' →ₗ[K] Dual K V} {m : ι → V'}

lemma exists_predual_of_finite {μ : ι → Dual K V} [FiniteDimensional K V]
    (hμ : LinearIndependent K μ) {s : Set ι} (i : ι) :
    ∃ v : V, μ i v = 1 ∧ ∀ j ∈ s, j ≠ i → μ j v = 0 := by
sorry

lemma exists_predual {μ : ι → Dual K V} (hμ : LinearIndependent K μ) {s : Set ι} (hs : s.Finite)
    (i : ι) : ∃ v : V, μ i v = 1 ∧ ∀ j ∈ s, j ≠ i → μ j v = 0 := by
  sorry

lemma exists_stuff (hm : LinearIndependent K (B ∘ m)) {s : Set ι} (hs : s.Finite) (i : ι) :
    ∃ v : V, B (m i) v = 1 ∧ ∀ j ∈ s , j ≠ i → B (m j) v = 0 :=
  exists_predual hm hs i

variable (hm : LinearIndependent K (B ∘ m)) {s : Set ι} (hs : s.Finite)

def stuff (i : ι) : V := (exists_stuff hm hs i).choose

lemma stuff_eval_self (i : ι) : B (m i) (stuff hm hs i) = 1 := (exists_stuff hm hs i).choose_spec.1

lemma stuff_eval_other {i j : ι} (hj : j ∈ s) (h : j ≠ i) : B (m j) (stuff hm hs i) = 0 :=
  (exists_stuff hm hs i).choose_spec.2 j hj h

lemma foo {s : Set ι} (hs : s.Finite) (μ : V' →ₗ[K] K) :
    ∃ φ : V, ∀ v' ∈ span K (m '' s), μ v' = B v' φ := by
  use ∑ i in hs.toFinset, (μ (m i)) • stuff hm hs i
  intro v' hv'
  apply span_induction hv' (p := fun v' ↦ μ v' = B v' (∑ i in hs.toFinset, (μ (m i)) • stuff hm hs i))
  all_goals clear v' hv'
  · rintro _ ⟨i, hi, rfl⟩
    have : ∀ j ∈ hs.toFinset, j ≠ i → B (m i) (μ (m j) • stuff hm hs j) = 0 := by
      intros j _ hij
      rw [map_smul, stuff_eval_other hm hs hi hij.symm, smul_zero]
    rw [map_sum, Finset.sum_eq_single_of_mem i (hs.mem_toFinset.mpr hi) this, map_smul,
        stuff_eval_self, smul_eq_mul, mul_one]
  · simp only [_root_.map_zero, map_sum, map_smul, LinearMap.zero_apply, smul_eq_mul, mul_zero,
    Finset.sum_const_zero]
  · intros x y hx hy
    simp [map_add, hx, hy, mul_add, ← Finset.sum_add_distrib]
  · intros a v' hv'
    simp only [map_smul, hv', map_sum, smul_eq_mul, Finset.mul_sum, LinearMap.smul_apply]

end missing_linear_algebra

open Metric Set MeasureTheory Module
open MvPolynomial hiding support
open Function hiding eval

section normed
variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
variable {E E' F  : Type*}
  [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  [NormedAddCommGroup E'] [NormedSpace 𝕜 E']
  [NormedAddCommGroup F] [NormedSpace 𝕜 F]

variable (𝕜 E F) in
def SmoothSupportedOn (n : ℕ∞) (s : Set E) : Submodule 𝕜 (E → F) where
  carrier := { f : E → F | tsupport f ⊆ s ∧ ContDiff 𝕜 n f }
  add_mem' hf hg := ⟨sorry, 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⟩

variable {n : ℕ∞} {s : Set E}

instance : FunLike (SmoothSupportedOn 𝕜 E F n s) E (fun _ ↦ F) where
  coe := Subtype.val
  coe_injective' := Subtype.coe_injective
end normed

def L {ι : Type*} [Fintype ι] :
  MvPolynomial ι ℝ →ₗ[ℝ] Dual ℝ (SmoothSupportedOn ℝ (EuclideanSpace ℝ ι) ℝ ⊤ (closedBall 0 1)) where
    toFun p :=
      { toFun := fun f ↦ ∫ x : EuclideanSpace ℝ ι, eval x p • f x
        map_add' := sorry
        map_smul' := sorry }
    map_add' := sorry
    map_smul' := sorry

lemma indep (ι : Type*) [Fintype ι] : LinearIndependent ℝ (L ∘ fun c : ι →₀ ℕ ↦ monomial c 1) := by
  sorry

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 :=
  let ⟨⟨φ, supp_φ, diff_φ⟩, hφ⟩ :=  foo (indep ι) (finite_stuff _) (evalAtₗ 0)
  ⟨φ, supp_φ, diff_φ, fun P hP ↦ (hφ P (totalDegree_le_iff_mem_span.1 hP)).symm⟩

[Patrick Massot]

@algebra people: what is missing (or at least I couldn't find) is mostly polynomial and linear algebra stuff.

[Patrick Massot]

The only thing that involves analysis is the indep lemma.

[Ruben Van de Velde]

I found docs#MvPolynomial.evalₗ but that doesn't seem to be it

[Ruben Van de Velde]

I'm sure there's an easier way than this:

lemma finite_stuff' [Finite σ] (N : ℕ) : {s : Multiset σ | Multiset.card s ≤ N}.Finite := by
  classical
  have := Fintype.ofFinite σ
  let S := N • (Finset.univ.val : Multiset σ)
  apply Finset.finite_toSet (Multiset.toFinset (Multiset.powerset S)) |>.subset
  intro s hs
  rw [Set.mem_setOf] at hs
  rw [Finset.mem_coe, Multiset.mem_toFinset, Multiset.mem_powerset, Multiset.le_iff_count]
  intro x
  simp only [S, Multiset.count_nsmul, Multiset.count_univ, mul_one]
  exact le_trans (s.count_le_card x) hs

lemma finite_stuff [Finite σ] (N : ℕ) : {s : σ →₀ ℕ | s.sum (fun _ e ↦ e) ≤ N}.Finite := by
  classical
  change {s : σ →₀ ℕ | s.sum (fun _ => id) ≤ N}.Finite
  simp only [← Finsupp.card_toMultiset]
  refine Set.Finite.of_finite_image ?_ (Multiset.toFinsupp.symm.injective.injOn _)
  convert finite_stuff' N
  ext x
  rw [← AddEquiv.coe_toEquiv]
  simp

[Johan Commelin]

@Ruben Van de Velde the final simp doesn't close the goal for me...

[Johan Commelin]

I pushed Patrick's file + Ruben's lemmas to Archive/Hairer.lean on the branch hairer-challenge

[Johan Commelin]

I closed the sorry about tsupport.

[Johan Commelin]

I reduced a few more sorries about linearity to sorries about integrability.

[Junyan Xu]

I solved exists_predual without using exists_predual_of_finite. The idea is similar to this and makes use of annihilator theory introduced by @Kyle Miller.

variable {K V V' ι : Type*} [Field K] [AddCommGroup V] [Module K V] [AddCommGroup V'] [Module K V']
   {B : V' →ₗ[K] Dual K V} {m : ι → V'}

lemma surj_of_inj (hB : Function.Injective B) [FiniteDimensional K V'] :
    Function.Surjective (B.dualMap.comp (Module.Dual.eval K V)) := by
  rw [← LinearMap.range_eq_top]
  apply Submodule.eq_top_of_finrank_eq
  set W : Subspace K _ := LinearMap.range (B.dualMap.comp (Module.Dual.eval K V))
  have := W.finrank_add_finrank_dualCoannihilator_eq
  rw [Subspace.dual_finrank_eq, ← this, eq_comm, add_right_eq_self, finrank_eq_zero, eq_bot_iff]
  intro x hx
  apply hB
  ext v
  rw [Submodule.mem_dualCoannihilator] at hx
  simpa using hx _ (LinearMap.mem_range_self _ v)

lemma exists_predual {μ : ι → Dual K V} (hμ : LinearIndependent K μ) {s : Set ι} (hs : s.Finite)
    (i : ι) : ∃ v : V, μ i v = 1 ∧ ∀ j ∈ s, j ≠ i → μ j v = 0 := by
  have hμ := hμ.comp (_ : ↑(s ∪ {i}) → ι) Subtype.val_injective
  rw [linearIndependent_iff_injective_total] at hμ
  have : Finite ↑(s ∪ {i}) := (hs.union <| Set.finite_singleton i).to_subtype
  classical
  have ⟨v, hv⟩ := surj_of_inj hμ (Finsupp.total _ _ _ fun j ↦ if j = i then 1 else 0)
  refine ⟨v, ?_, fun j hjs hji ↦ ?_⟩
  · simpa using FunLike.congr_fun hv (Finsupp.single ⟨i, .inr rfl⟩ 1)
  · simpa [if_neg hji] using FunLike.congr_fun hv (Finsupp.single ⟨j, .inl hjs⟩ 1)

[Junyan Xu]

Did this in web editor; feel free to put into the branch.

[Johan Commelin]

Thanks! I'll push it.

[Johan Commelin]

Several of the remaining sorries are of the following type:

ι: Type u_1
inst✝: Fintype ι
p: MvPolynomial ι ℝ
fg: ↥(SmoothSupportedOn ℝ (EuclideanSpace ℝ ι) ℝ ⊤ (closedBall 0 1))
⊢ Integrable fun x ↦ (eval x) p • f x

I've never used integration theory in mathlib. How do we close these?

[Sebastien Gouezel]

You probably want docs#Continuous.integrable_of_hasCompactSupport

[Ruben Van de Velde]

That seems to work assuming

variable {ι : Type*} [Fintype ι]
lemma MvPolynomial.continuous_eval (p: MvPolynomial ι ℝ) :
    Continuous fun x ↦ (eval x) p := by
  sorry

is true

[Ruben Van de Velde]

And continuity says it is

[Johan Commelin]

@Ruben Van de Velde are you pushing this? If not, I can copy it into the file.

[Ruben Van de Velde]

Yeah, just pushed

[Ruben Van de Velde]

Leaving it alone for a while now

[Sebastien Gouezel]

I've killed a few sorries, in particular completing the main proof. There was a dramatic oversight that the argument was wrong in the case where the indexing space is empty :-) -- but in this case the constant function 1 will do, so no need to add a further assumption to the statement.

[Ruben Van de Velde]

Sebastien Gouezel said:

I've killed a few sorries, in particular completing the main proof. There was a dramatic oversight that the argument was wrong in the case where the indexing space is empty :-) -- but in this case the constant function 1 will do, so no need to add a further assumption to the statement.

Did you push them?

[Sebastien Gouezel]

Yes.

[Ruben Van de Velde]

Where?

[Sebastien Gouezel]

I've just pushed again, in case I did something wrong before.

PS C:\Users\sgouezel_A\Desktop\mathlib4> git push
Enumerating objects: 7, done.
Counting objects: 100% (7/7), done.
Delta compression using up to 8 threads
Compressing objects: 100% (4/4), done.
Writing objects: 100% (4/4), 607 bytes | 607.00 KiB/s, done.
Total 4 (delta 3), reused 0 (delta 0), pack-reused 0
remote: Resolving deltas: 100% (3/3), completed with 3 local objects.
To https://github.com/leanprover-community/mathlib4.git
   6b874f2421..8686deea3c  hairer -> hairer

[Ruben Van de Velde]

Only thing that went wrong is that there's also branch#hairer-challenge

[Sebastien Gouezel]

Ah, crap. Which one is the right one?

[Sebastien Gouezel]

I've merged hairer-challenge into hairer.

[Sebastien Gouezel]

It was only missing one additional commit by Floris. Can I delete hairer-challenge, to make sure everyone is on the same branch?

[Johan Commelin]

yes, please go ahead

[Johan Commelin]

:warning: the branch name hairer-challenge is going out of business! From now on use hairer

[Patrick Massot]

I'm completely confused about what @Sebastien Gouezel is working on.

[Patrick Massot]

And what is this story of a missing empty case.

[Patrick Massot]

My main proof was completed already, only algebraic lemmas and the independence proof was missing.

[Patrick Massot]

What's wrong with my

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 :=
  let ⟨⟨φ, supp_φ, diff_φ⟩, hφ⟩ :=  foo (indep ι) (finite_stuff _) (evalAtₗ 0)
  ⟨φ, supp_φ, diff_φ, fun P hP ↦ (hφ P (totalDegree_le_iff_mem_span.1 hP)).symm⟩

[Patrick Massot]

This is a full proof of the target statement.

[Patrick Massot]

Why is there a hairer2 lemma below it on the branch?

[Ruben Van de Velde]

That one's from @Floris van Doorn

[Patrick Massot]

Do we now try to get two different proofs?

[Patrick Massot]

My message here was a complete proof modulo sorries, it did not require any other code from Floris's earlier attempt.

[Sebastien Gouezel]

I hadn't seen the first hairer, I was just closing the sorries in the last theorem in the file, which I thought was the current state of things. This is silly!

[Patrick Massot]

I'm sorry the situation was confusing. I should have pushed to the branch instead of posting full files here.

[Patrick Massot]

If you want something to do then one of the missing (I think) things to prove is that a polynomial which vanishes on a non-empty open set in $\R^n$ is the zero polynomial. But maybe @Floris van Doorn is already proving it.

[Sebastien Gouezel]

It looks to me that the point of hairer2 is that it avoids indep completely, and instead only uses that you have countably many independent smooth functions with integral 1 (but for this you indeed need the indexing set to be nonempty). This looks easier to prove than indep.

[Sebastien Gouezel]

(But maybe with something like docs#ae_eq_zero_of_integral_contDiff_smul_eq_zero then indep is also easy).

[Patrick Massot]

docs#ae_eq_zero_of_integral_contDiff_smul_eq_zero is half the proof of indep, the other half is the lemma I mentioned above (non-empty Zariski opens are dense in Euclidean topology).

[Patrick Massot]

And I think this missing half is something Mathlib should know anyway.

[Sebastien Gouezel]

I'm sure mathlib should know about this. It's just maybe not the path of least resistance in the current situation.

[Patrick Massot]

If we wanted to get a proof as fast as possible then the integration path explored by Vincent would probably be faster. I think we should try to get the elegant proof and improve Mathlib along the way. There is no hurry.

[Sebastien Gouezel]

I'm sure Vincent's approach would be more efficient in dimension 1, but not so sure in higher dimension where multivariate polynomials are a mess. Anyway, completing both paths (I mean, hairer and hairer2) is definitely worthwile, because they will both highlight different gaps in the library that are worth filling.

[Martin Hairer]

Sebastien Gouezel said:

I'm sure Vincent's approach would be more efficient in dimension 1, but not so sure in higher dimension where multivariate polynomials are a mess. Anyway, completing both paths (I mean, hairer and hairer2) is definitely worthwile, because they will both highlight different gaps in the library that are worth filling.

As Damiano Testa pointed out, it actually reduces to the 1D case, but it looks like the current proof is more likely to produce useful stuff for the linear algebra part of matlib. Regarding foo, you currently assume that B m is linearly independent. If I understand the statement correctly though, it would also hold without assuming anything on the linear independence of the m, but assuming instead that B is injective, right? Wouldn't that be a more natural statement to merge into matlib?

[Floris van Doorn]

Oh, good to know about docs#ae_eq_zero_of_integral_contDiff_smul_eq_zero, that makes indep easier.
However, we want a variant of this lemma where the support of g is assumed to lie within some compact set K, and conclude from this that f is a.e. equal to 0 on (the interior of?) K. This is not super easy to get from the current mathlib version. I currently wrote this version (also on the branch), but I'm not sure if it holds in exactly this form

theorem IsCompact.ae_eq_zero_of_integral_contDiff_smul_eq_zero {K : Set E}
    (hU : IsCompact K) (hf : LocallyIntegrableOn f K μ)
    (h : ∀ (g : E → ℝ), ContDiff ℝ ⊤ g → tsupport g ⊆ K → ∫ x, g x • f x ∂μ = 0) :
    ∀ᵐ x ∂μ, x ∈ K → f x = 0 := by
  sorry

[Sebastien Gouezel]

What you can do to prove this is multiply your initial function by a smooth function with compact support in the ball. Then the resulting function will have integral zero against any smooth compactly supported function, so you can apply docs#ae_eq_zero_of_integral_contDiff_smul_eq_zero to it and deduce that it vanishes almost everywhere.

[Sebastien Gouezel]

For this, you probably need your compact set to be the closure of its interior (otherwise, your statement can not be true).

[Patrick Massot]

You can also use a different measure.

[Patrick Massot]

Heather just pointed out to me that we know that that analytic functions that coincide on an open set are equal. This could be a way to cheat in the independence proof (although this is really a ridiculously overpowered path).

[Patrick Massot]

And there is also docs#MvPolynomial.funext

[Junyan Xu]

docs#MvPolynomial.funext isn't quite applicable as it requires two polynomials being equal everywhere rather than on a nonempty open set. (Edit: it's applicable once you use the identity principle docs#AnalyticOn.eq_of_eventuallyEq to show they agree everywhere.) The easiest elementary proof is probably by induction on dimension (for the induction step you'd use docs#Polynomial.eq_zero_of_infinite_isRoot and that a MvPolynomial ring over $\mathbb{R}$ is a domain). However, you'd need to work with docs#MvPolynomial.finSuccEquiv like in this proof, and I expect the proof via analyticity will be simpler. Showing a polynomial is analytic is almost tautology but missing in mathlib apparently. (In the complex case we can combine docs#Differentiable.analyticAt with docs#Polynomial.differentiable, but the former isn't valid in the real case.)

[Kevin Buzzard]

I have a bit of time now, I'm trying some of the sorries in the hairer branch.

...and indeed we have a bunch of missing API for multivariable polynomials :-(

[Kevin Buzzard]

I made minor progress on finite-dimensional lemmas. I was surprised I couldn't find

MvPolynomial.degreeOf_le_totalDegree {𝕜 : Type*} [Field 𝕜] {ι : Type*} (i : ι)
  (f : MvPolynomial ι 𝕜) : degreeOf i f ≤ totalDegree f

[Junyan Xu]

Martin Hairer said:

Regarding foo, you currently assume that B m is linearly independent. If I understand the statement correctly though, it would also hold without assuming anything on the linear independence of the m, but assuming instead that B is injective, right? Wouldn't that be a more natural statement to merge into matlib?

In my latest commit I realized B.dualMap.comp (Module.Dual.eval K V) is otherwise known as B.flip :exploding_head: and now I directly use my surj_of_inj lemma in the final proof, so that everything from exists_predual to foo in @Patrick Massot's original code can now be removed.

[Junyan Xu]

The final sorry in the first approach (hairer) is moved into IsOpen.ae_eq_zero_of_integral_contDiff_smul_eq_zero, and I'm attempting to use the manifold version ae_eq_zero_of_integral_smooth_smul_eq_zero to prove it, but it's bedtime now ... Not sure it's the quickest approach, maybe it's easier to generalize the manifold version.

The remaining sorries in the second approach (hairer2) don't seem hard; the FiniteDimensional sorry should follow easily from the existing

instance [Finite σ] : Module.Finite R (restrictTotalDegree σ R n)

because nonConstantTotalDegreeLE is a smaller submodule.

[Sebastien Gouezel]

In fact I am not sure I understand the first lemma in Floris' approach. It reads

lemma exists_affineSpan_zero {ι'} (s : Submodule 𝕜 F) [FiniteDimensional 𝕜 s] [Infinite ι']
    (L : F →ₗ[𝕜] E →ₗ[𝕜] 𝕜) (x : ι' → E) (hx : LinearIndependent 𝕜 x) :
    ∃ y ∈ affineSpan 𝕜 (range x), ∀ i ∈ s, L i y = 0 := sorry

but what if L i is constant equal to 1 on the affine subspace spanned by the range of x? (I don't see anything in the assumptions of the lemma that excludes this).

[Sebastien Gouezel]

I killed the final sorry in the hairer approach:

#printaxioms hairer
'hairer' depends on axioms: [propext, Quot.sound, Classical.choice]

[Sebastien Gouezel]

(But all the hard work had already been done by @Junyan Xu , to be fair!)

[Ruben Van de Velde]

:clock: 3 days, 6 hours, 45 minutes

[Mario Carneiro]

Is the final result something that can be decomposed to mathlib PRs + something small enough for a zulip post?

[Junyan Xu]

Sebastien Gouezel said:

I killed the final sorry in the hairer approach:

Nice! (just got back from hiking) I read your proof of IsOpen.ae_eq_zero_of_integral_contDiff_smul_eq_zero and pushed a bit of cleanup; to be fair it's quite different from my unfinished approach.

[Junyan Xu]

Mario Carneiro said:

Is the final result something that can be decomposed to mathlib PRs + something small enough for a zulip post?

The first (completed) approach takes about 300 lines. Not sure how many will end up in mathlib proper; maybe 100-200?

[Mario Carneiro]

I would say that we should make this provable within 50 lines and move the rest into mathlib

[Mario Carneiro]

or possibly just move the whole thing, I am not the best judge of whether this theorem is itself library material

[Sebastien Gouezel]

Since nothing seems to be moving on this front, I have opened #9138 as a PR to Archive with the current state of the file. You can have a look to see if there are pieces you would like to move to mathlib.

[Ruben Van de Velde]

I've got #9060 open with a small addition, fwiw

[Sebastien Gouezel]

Thanks! I've merged master (with #9060 already in it) into the hairer branch.