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 SmoothSupportedOn (𝕜 : 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 smooth functions supported in a set s, as a submodule of the space of functions.

Equations

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

instance SmoothSupportedOn.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 (↥(SmoothSupportedOn 𝕜 E F n s)) E F

Equations

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

@[simp]

theorem SmoothSupportedOn.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 ∈ SmoothSupportedOn 𝕜 E F n s) : ⇑⟨f, h⟩ = f

theorem SmoothSupportedOn.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 : ↥(SmoothSupportedOn 𝕜 E F n s)) : tsupport ⇑f ⊆ s

theorem SmoothSupportedOn.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 : ↥(SmoothSupportedOn 𝕜 E F n s)) : Function.support ⇑f ⊆ s

theorem SmoothSupportedOn.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 : ↥(SmoothSupportedOn 𝕜 E F n s)) : ContDiff 𝕜 ↑n ⇑f

theorem SmoothSupportedOn.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 : ↥(SmoothSupportedOn 𝕜 E F n s)) : Continuous ⇑f

theorem SmoothSupportedOn.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 : ↥(SmoothSupportedOn 𝕜 E F n (Metric.closedBall 0 1))) : HasCompactSupport ⇑f

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

def L (ι : Type u_1) [Fintype ι] : MvPolynomial ι ℝ →ₗ[ℝ] Module.Dual ℝ ↥(SmoothSupportedOn ℝ (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) p • ρ x = (MvPolynomial.eval 0) p