def HadamardDecomposition.coordFun (n : ℕ) (j : Fin n) : EuclideanSpace ℝ (Fin n) → ℂ

The j-th coordinate function on EuclideanSpace ℝ (Fin n), viewed as a complex-valued function.

noncomputable def HadamardDecomposition.coordCLM (n : ℕ) (j : Fin n) : EuclideanSpace ℝ (Fin n) →L[ℝ] ℂ

The j-th coordinate function on EuclideanSpace ℝ (Fin n), packaged as a continuous real-linear map into ℂ.

theorem HadamardDecomposition.coordFun_eq_coordCLM (n : ℕ) (j : Fin n) : coordFun n j = ⇑(coordCLM n j)

The plain coordinate function coordFun n j agrees pointwise with its continuous-linear-map version coordCLM n j.

theorem HadamardDecomposition.coordFun_hasTemperateGrowth (n : ℕ) (j : Fin n) : Function.HasTemperateGrowth (coordFun n j)

Each coordinate function on Euclidean space has temperate growth (it is linear, hence at most linearly bounded).

noncomputable def HadamardDecomposition.hadamardPsiFun (n : ℕ) (φ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ) (j : Fin n) (x : EuclideanSpace ℝ (Fin n)) : ℂ

The Hadamard decomposition coefficient functions: given a Schwartz function φ and a coordinate index j, this is the function whose value at x is ∫₀¹ (∂_j φ)(t · x) dt. These functions appear in the identity φ(x) = Σⱼ xⱼ · ψⱼ(x) when φ vanishes at the origin.

theorem HadamardDecomposition.hadamardPsiFun_contDiff (n : ℕ) (φ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ) (j : Fin n) : ContDiff ℝ (↑⊤) (hadamardPsiFun n φ j)

The Hadamard coefficient function hadamardPsiFun n φ j is smooth (C^∞).

theorem HadamardDecomposition.hadamardPsiFun_decay (n : ℕ) (φ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ) (j : Fin n) (k m : ℕ) : ∃ (C : ℝ), ∀ (x : EuclideanSpace ℝ (Fin n)), ‖x‖ ^ k * ‖iteratedFDeriv ℝ m (hadamardPsiFun n φ j) x‖ ≤ C

The Hadamard coefficient function hadamardPsiFun n φ j satisfies all Schwartz decay estimates: for every pair of nonnegative integers (k, m) there is a constant C bounding ‖x‖^k · ‖D^m ψ(x)‖.

theorem HadamardDecomposition.schwartz_vanishing_at_zero_eq_sum_coord_mul (n : ℕ) (φ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ) (hφ : φ 0 = 0) : ∃ (ψ : Fin n → SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ), ∀ (x : EuclideanSpace ℝ (Fin n)), φ x = ∑ j : Fin n, coordFun n j x • (ψ j) x

Hadamard decomposition: a Schwartz function on ℝⁿ that vanishes at the origin can be written as φ(x) = Σⱼ xⱼ · ψⱼ(x) for some Schwartz functions ψⱼ.

theorem HadamardDecomposition.apply_eq_zero_of_eval_origin_eq_zero (n : ℕ) (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hu : ∀ (j : Fin n), (TemperedDistribution.smulLeftCLM ℂ (coordFun n j)) u = 0) (φ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ) (hφ : φ 0 = 0) : u φ = 0

If a tempered distribution u is annihilated by multiplication by every coordinate function, then u φ = 0 for every Schwartz function φ that vanishes at the origin. Proof uses the Hadamard decomposition.

theorem HadamardDecomposition.eq_smul_delta_of_forall_coordSmul_eq_zero (n : ℕ) (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hu : ∀ (j : Fin n), (TemperedDistribution.smulLeftCLM ℂ (coordFun n j)) u = 0) : ∃ (c : ℂ), u = c • TemperedDistribution.delta 0

Characterisation of multiples of the Dirac delta at the origin: a tempered distribution u is annihilated by multiplication by every coordinate function iff u = c · δ₀ for some scalar c.