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.

def ContDiffSupportedOn (𝕜 : Type u_2) (E : Type u_3) (F : Type u_4) [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n : ℕ∞) (s : Set E) : Submodule 𝕜 (E → F)

The set of C^n functions supported in a set s, as a submodule of the space of functions.

Equations

• ContDiffSupportedOn 𝕜 E F n s = { carrier := {f : E → F | tsupport f ⊆ s ∧ ContDiff 𝕜 (↑n) f}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[instance_reducible]

instance ContDiffSupportedOn.instFunLikeSubtypeForallMemSubmodule {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ∞} {s : Set E} : FunLike (↥(ContDiffSupportedOn 𝕜 E F n s)) E F

Equations

• ContDiffSupportedOn.instFunLikeSubtypeForallMemSubmodule = { coe := Subtype.val, coe_injective := ⋯ }

@[simp]

theorem ContDiffSupportedOn.coe_mk {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ∞} {s : Set E} (f : E → F) (h : f ∈ ContDiffSupportedOn 𝕜 E F n s) : ⇑⟨f, h⟩ = f

theorem ContDiffSupportedOn.tsupport_subset {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ∞} {s : Set E} (f : ↥(ContDiffSupportedOn 𝕜 E F n s)) : tsupport ⇑f ⊆ s

theorem ContDiffSupportedOn.support_subset {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ∞} {s : Set E} (f : ↥(ContDiffSupportedOn 𝕜 E F n s)) : Function.support ⇑f ⊆ s

theorem ContDiffSupportedOn.contDiff {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ∞} {s : Set E} (f : ↥(ContDiffSupportedOn 𝕜 E F n s)) : ContDiff 𝕜 ↑n ⇑f

theorem ContDiffSupportedOn.continuous {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ∞} {s : Set E} (f : ↥(ContDiffSupportedOn 𝕜 E F n s)) : Continuous ⇑f

theorem ContDiffSupportedOn.hasCompactSupport {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ∞} [ProperSpace E] (f : ↥(ContDiffSupportedOn 𝕜 E F n (Metric.closedBall 0 1))) : HasCompactSupport ⇑f

theorem ContDiffSupportedOn.integrable_eval_mul {ι : Type u_1} [Fintype ι] (p : MvPolynomial ι ℝ) (f : ↥(ContDiffSupportedOn ℝ (EuclideanSpace ℝ ι) ℝ ⊤ (Metric.closedBall 0 1))) : MeasureTheory.Integrable (fun (x : EuclideanSpace ℝ ι) => (MvPolynomial.eval x.ofLp) p * f x) MeasureTheory.volume

noncomputable def L (ι : Type u_1) [Fintype ι] : MvPolynomial ι ℝ →ₗ[ℝ] Module.Dual ℝ ↥(ContDiffSupportedOn ℝ (EuclideanSpace ℝ ι) ℝ ⊤ (Metric.closedBall 0 1))

Interpreting a multivariate polynomial as an element of the dual of smooth functions supported in the unit ball, via integration against Lebesgue measure.

Equations

• One or more equations did not get rendered due to their size.

theorem inj_L (ι : Type u_1) [Fintype ι] : Function.Injective ⇑(L ι)

theorem hairer (N : ℕ) (ι : Type u_2) [Fintype ι] : ∃ (ρ : EuclideanSpace ℝ ι → ℝ), tsupport ρ ⊆ Metric.closedBall 0 1 ∧ ContDiff ℝ (↑⊤) ρ ∧ ∀ (p : MvPolynomial ι ℝ), p.totalDegree ≤ N → ∫ (x : EuclideanSpace ℝ ι), (MvPolynomial.eval x.ofLp) p • ρ x = (MvPolynomial.eval 0) p