structure TestFunctions.ContDiffZeroAtInfty (n : ℕ) extends ZeroAtInftyContinuousMap (EuclideanSpace ℝ (Fin n)) ℂ : Type

A continuous, complex-valued function on ℝⁿ that vanishes at infinity, is C¹, and whose first-order partial derivatives also vanish at infinity.

• toFun : EuclideanSpace ℝ (Fin n) → ℂ
• continuous_toFun : Continuous self.toFun
• zero_at_infty' : Filter.Tendsto self.toFun (Filter.cocompact (EuclideanSpace ℝ (Fin n))) (nhds 0)
• contDiff_one : ContDiff ℝ 1 ⇑self.toZeroAtInftyContinuousMap
• partialDeriv_zero_at_infty (j : Fin n) : Filter.Tendsto (fun (x : EuclideanSpace ℝ (Fin n)) => (fderiv ℝ (⇑self.toZeroAtInftyContinuousMap) x) (EuclideanSpace.single j 1)) (Filter.cocompact (EuclideanSpace ℝ (Fin n))) (nhds 0)

noncomputable def TestFunctions.restrictDual {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {V : Type u_2} [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] {U : Type u_3} [SeminormedAddCommGroup U] [NormedSpace 𝕜 U] (ι : V →L[𝕜] U) : (U →L[𝕜] 𝕜) →L[𝕜] V →L[𝕜] 𝕜

Pullback of continuous linear functionals along a continuous linear map ι : V →L[𝕜] U: sends a dual element on U to its restriction along ι.

@[simp]

theorem TestFunctions.restrictDual_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {V : Type u_2} [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] {U : Type u_3} [SeminormedAddCommGroup U] [NormedSpace 𝕜 U] (ι : V →L[𝕜] U) (L : U →L[𝕜] 𝕜) : (restrictDual ι) L = L.comp ι

restrictDual ι L is just L ∘ ι.

theorem TestFunctions.norm_restrictDual_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {V : Type u_2} [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] {U : Type u_3} [SeminormedAddCommGroup U] [NormedSpace 𝕜 U] (ι : V →L[𝕜] U) (L : U →L[𝕜] 𝕜) {C : ℝ} (hC : ‖ι‖ ≤ C) : ‖(restrictDual ι) L‖ ≤ C * ‖L‖

Operator-norm bound for restrictDual: if ‖ι‖ ≤ C, then ‖L ∘ ι‖ ≤ C * ‖L‖.

theorem TestFunctions.restrictDual_injective {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {V : Type u_2} [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] {U : Type u_3} [SeminormedAddCommGroup U] [NormedSpace 𝕜 U] (ι : V →L[𝕜] U) (hd : DenseRange ⇑ι) : Function.Injective ⇑(restrictDual ι)

If ι has dense range, then its dual restrictDual ι is injective: a continuous functional is determined by its values on a dense subspace.

theorem TestFunctions.restrictDual_norm_bound_and_injective {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {V : Type u_2} [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] {U : Type u_3} [SeminormedAddCommGroup U] [NormedSpace 𝕜 U] (ι : V →L[𝕜] U) (C : ℝ) (hC : ‖ι‖ ≤ C) : (∀ (L : U →L[𝕜] 𝕜), ‖(restrictDual ι) L‖ ≤ C * ‖L‖) ∧ (DenseRange ⇑ι → Function.Injective ⇑(restrictDual ι))

Combined statement: restrictDual is bounded by C on operator norms, and is injective whenever ι has dense range.

def TestFunctions.ckNorm (n a✝ : ℕ) : (EuclideanSpace ℝ (Fin n) → ℂ) → ℝ

The C^k sup-norm of a function f : ℝⁿ → ℂ: sum of sup norms of all partial derivatives up to order k.

structure TestFunctions.ContDiffZeroAtInftyN (n k : ℕ) extends ZeroAtInftyContinuousMap (EuclideanSpace ℝ (Fin n)) ℂ : Type

The space of C^k functions on ℝⁿ vanishing at infinity together with all of their iterated derivatives up to order k.

• toFun : EuclideanSpace ℝ (Fin n) → ℂ
• continuous_toFun : Continuous self.toFun
• zero_at_infty' : Filter.Tendsto self.toFun (Filter.cocompact (EuclideanSpace ℝ (Fin n))) (nhds 0)
• contDiff_k : ContDiff ℝ ↑k ⇑self.toZeroAtInftyContinuousMap
• iteratedFDeriv_zero_at_infty (m : ℕ) (hm : m ≤ k) : Filter.Tendsto (fun (x : EuclideanSpace ℝ (Fin n)) => ‖iteratedFDeriv ℝ m (⇑self.toZeroAtInftyContinuousMap) x‖) (Filter.cocompact (EuclideanSpace ℝ (Fin n))) (nhds 0)

noncomputable def TestFunctions.ContDiffZeroAtInftyN.normCk {n k : ℕ} (u : ContDiffZeroAtInftyN n k) : ℝ

The C^k-norm of an element of ContDiffZeroAtInftyN n k.

noncomputable def TestFunctions.japaneseBracket (n : ℕ) (x : EuclideanSpace ℝ (Fin n)) : ℝ

The Japanese bracket ⟨x⟩ := √(1 + ‖x‖²), a smooth weight comparable to ‖x‖ at infinity used to define weighted function spaces.

theorem TestFunctions.japaneseBracket_pos (n : ℕ) (x : EuclideanSpace ℝ (Fin n)) : 0 < japaneseBracket n x

The Japanese bracket ⟨x⟩ is strictly positive.

theorem TestFunctions.japaneseBracket_ne_zero (n : ℕ) (x : EuclideanSpace ℝ (Fin n)) : japaneseBracket n x ≠ 0

The Japanese bracket ⟨x⟩ is nonzero.

structure TestFunctions.WeightedContDiffZeroAtInfty (n k l : ℕ) : Type

Weighted C^k-functions on ℝⁿ vanishing at infinity: an element is represented by a witness v ∈ C^k whose ratio against ⟨x⟩^{-l} lies in the original space.

• witnessV : ContDiffZeroAtInftyN n k

noncomputable def TestFunctions.WeightedContDiffZeroAtInfty.toFun (n : ℕ) {k l : ℕ} (u : WeightedContDiffZeroAtInfty n k l) (x : EuclideanSpace ℝ (Fin n)) : ℂ

Underlying function ⟨x⟩^{-l} v(x) for a weighted C^k element with witness v.

structure TestFunctions.SchwartzTestFunctionSpace (n : ℕ) : Type

The Schwartz space described as functions on ℝⁿ lying in every weighted C^k-space with weight ⟨x⟩^{-l} (Melrose Prop 7.3 characterisation).

• toFun : EuclideanSpace ℝ (Fin n) → ℂ
• mem_weightedSpace (k l : ℕ) : ∃ (w : WeightedContDiffZeroAtInfty n k l), ∀ (x : EuclideanSpace ℝ (Fin n)), self.toFun x = WeightedContDiffZeroAtInfty.toFun n w x

@[reducible, inline]

abbrev TestFunctions.schwartzSpace (n : ℕ) : Type

Standard Schwartz space 𝓢(ℝⁿ, ℂ) abbreviation.

@[implicit_reducible]

instance TestFunctions.SchwartzTestFunctionSpace.instFunLike {n : ℕ} : FunLike (SchwartzTestFunctionSpace n) (EuclideanSpace ℝ (Fin n)) ℂ

SchwartzTestFunctionSpace n coerces to functions ℝⁿ → ℂ.

theorem TestFunctions.SchwartzTestFunctionSpace.ext {n : ℕ} {f g : SchwartzTestFunctionSpace n} (h : ∀ (x : EuclideanSpace ℝ (Fin n)), f x = g x) : f = g

Function-extensionality for elements of SchwartzTestFunctionSpace.

theorem TestFunctions.SchwartzTestFunctionSpace.ext_iff {n : ℕ} {f g : SchwartzTestFunctionSpace n} : f = g ↔ ∀ (x : EuclideanSpace ℝ (Fin n)), f x = g x

@[simp]

theorem TestFunctions.SchwartzTestFunctionSpace.coe_mk {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → ℂ) (hf : ∀ (k l : ℕ), ∃ (w : WeightedContDiffZeroAtInfty n k l), ∀ (x : EuclideanSpace ℝ (Fin n)), f x = WeightedContDiffZeroAtInfty.toFun n w x) : ⇑{ toFun := f, mem_weightedSpace := hf } = f

The coercion of mk f hf is just f.

noncomputable def TestFunctions.SchwartzTestFunctionSpace.equivSchwartzMap (n : ℕ) : SchwartzTestFunctionSpace n ≃ schwartzSpace n

Equivalence between our concrete SchwartzTestFunctionSpace n and Mathlib's SchwartzMap (ℝⁿ, ℂ), expressing Melrose's characterisation of Schwartz space.

theorem TestFunctions.euclideanSpace_norm_coord_le {n : ℕ} (x : EuclideanSpace ℝ (Fin n)) (j : Fin n) : ‖x.ofLp j‖ ≤ ‖x‖

Each coordinate of a vector in ℝⁿ is bounded in absolute value by the Euclidean norm of the vector.

theorem TestFunctions.opNorm_le_sum_basis_norms {n : ℕ} (T : EuclideanSpace ℝ (Fin n) →L[ℝ] ℂ) : ‖T‖ ≤ ∑ j : Fin n, ‖T (EuclideanSpace.single j 1)‖

The operator norm of a continuous linear functional T : ℝⁿ →L[ℝ] ℂ is bounded by the sum of its values on the standard basis.