Sharp mollifier_convergence witness tests

Concrete witness checks for mollifier_convergence applied to a momentum-space delta δ_{m₀}:

• W1 — δ_{m₀} ∈ H^s_* for every s.
• W2 — On a momentum-space delta, the rescaled-convolution distribution is a scalar multiple of δ_{m₀} with explicit coefficient ftRn φ (ε • m₀).
• W3 — mollifier_convergence invoked on δ_{m₀}.

noncomputable def MollifierConvergenceTests.singleMode (n : ℕ) (m₀ : Fin n → ℤ) : NashEmbedding.Sobolev.TrigPolyDual n

The Kronecker-delta distribution δ_{m₀} ∈ X_n^*.

Equations

• MollifierConvergenceTests.singleMode n m₀ = NashEmbedding.Sobolev.seqToDual n fun (m : Fin n → ℤ) => if m = m₀ then 1 else 0