noncomputable def SobolevEmbedding.contDiffZeroAtInftyN_mul_japaneseBracketInvPow {n k : ℕ} (p : ℕ) (v : TestFunctions.ContDiffZeroAtInftyN n k) : { w : TestFunctions.ContDiffZeroAtInftyN n k // ⇑w.toZeroAtInftyContinuousMap = fun (x : EuclideanSpace ℝ (Fin n)) => (↑(TestFunctions.japaneseBracket n x ^ p))⁻¹ * v.toZeroAtInftyContinuousMap x }

Multiplying a Cᵏ function vanishing at infinity by the inverse of a power of the Japanese bracket ⟨x⟩^{-p} again gives a Cᵏ function vanishing at infinity, with the prescribed pointwise formula.

theorem SobolevEmbedding.japaneseBracket_pow_ne_zero_complex {n : ℕ} (x : EuclideanSpace ℝ (Fin n)) (k : ℕ) : ↑(TestFunctions.japaneseBracket n x ^ k) ≠ 0

Any natural power of the Japanese bracket is a nonzero complex number, since ⟨x⟩ ≥ 1 > 0.

noncomputable def SobolevEmbedding.weightedSobolev_to_contDiffZeroAtInfty {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → ℂ) (hf : ∀ (k : ℕ), ∃ (u : SobolevSpace n k), u.toFun = fun (x : EuclideanSpace ℝ (Fin n)) => ↑(TestFunctions.japaneseBracket n x ^ k) * f x) (j l : ℕ) : { v : TestFunctions.ContDiffZeroAtInftyN n j // ⇑v.toZeroAtInftyContinuousMap = fun (x : EuclideanSpace ℝ (Fin n)) => ↑(TestFunctions.japaneseBracket n x ^ l) * f x }

Step in Melrose Prop. 10.4: a function lying in every weighted Sobolev space gives rise, for each smoothness index j and weight l, to a Cⱼ function vanishing at infinity whose value at x is ⟨x⟩^l · f(x). Combines the Sobolev embedding theorem with multiplication by an inverse weight.

noncomputable def SobolevEmbedding.allWeightedSobolev_to_schwartz {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → ℂ) (hf : ∀ (k : ℕ), ∃ (u : SobolevSpace n k), u.toFun = fun (x : EuclideanSpace ℝ (Fin n)) => ↑(TestFunctions.japaneseBracket n x ^ k) * f x) : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ

Melrose Prop. 10.4: a function lying in every weighted Sobolev space is a Schwartz function. This constructs the Schwartz representative explicitly from the family of weighted Sobolev witnesses.

noncomputable def SobolevEmbedding.schwartz_mul_japaneseBracket_pow {n k : ℕ} (f : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ) : { g : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ // ∀ (x : EuclideanSpace ℝ (Fin n)), g x = ↑(TestFunctions.japaneseBracket n x ^ k) * f x }

Multiplying a Schwartz function by any natural power of the Japanese bracket again gives a Schwartz function, with the prescribed pointwise formula. Uses the fact that ⟨x⟩^k has temperate growth.

theorem SobolevEmbedding.schwartz_iteratedFDeriv_memLp {n : ℕ} (g : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ) (j : ℕ) : MeasureTheory.MemLp (fun (x : EuclideanSpace ℝ (Fin n)) => iteratedFDeriv ℝ j (⇑g) x) 2 MeasureTheory.volume

Every iterated Fréchet derivative of a Schwartz function lies in L² with respect to Lebesgue measure on ℝⁿ.