theorem DifferentialOperators.prop_11_2_smul {n : ℕ} {ι : Type u_1} {p : Filter ι} {u : ι → TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ} {u₀ : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ} (hu : Filter.Tendsto u p (nhds u₀)) (c : ℂ) : Filter.Tendsto (fun (j : ι) => c • u j) p (nhds (c • u₀))

Weak-* continuity of scalar multiplication on tempered distributions (Proposition 11.1 of Melrose, scalar part): if u j → u₀ along the filter p then c · u j → c · u₀.

theorem DifferentialOperators.prop_11_2_add {n : ℕ} {ι : Type u_1} {p : Filter ι} {u u' : ι → TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ} {u₀ u₀' : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ} (hu : Filter.Tendsto u p (nhds u₀)) (hu' : Filter.Tendsto u' p (nhds u₀')) : Filter.Tendsto (fun (j : ι) => u j + u' j) p (nhds (u₀ + u₀'))

Weak-* continuity of addition on tempered distributions: if u j → u₀ and u' j → u₀', then (u j + u' j) → (u₀ + u₀').

theorem DifferentialOperators.prop_11_2_diffOp {n : ℕ} {ι : Type u_1} {p : Filter ι} {u : ι → TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ} {u₀ : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ} (hu : Filter.Tendsto u p (nhds u₀)) (P : MvPolynomial (Fin n) ℂ) : Filter.Tendsto (fun (j : ι) => (constCoeffDiffOp n P) (u j)) p (nhds ((constCoeffDiffOp n P) u₀))

Weak-* continuity of constant-coefficient differential operators: if u j → u₀, then P(D) u j → P(D) u₀ for every polynomial P.

theorem DifferentialOperators.prop_11_2_smulLeft {n : ℕ} {ι : Type u_1} {p : Filter ι} {u : ι → TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ} {u₀ : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ} (hu : Filter.Tendsto u p (nhds u₀)) (g : EuclideanSpace ℝ (Fin n) → ℂ) : Filter.Tendsto (fun (j : ι) => (TemperedDistribution.smulLeftCLM ℂ g) (u j)) p (nhds ((TemperedDistribution.smulLeftCLM ℂ g) u₀))

Weak-* continuity of multiplication by a fixed smooth function: if u j → u₀, then g · u j → g · u₀ as tempered distributions, for any (admissible) function g.

theorem DifferentialOperators.proposition_11_2_combined {n : ℕ} {ι : Type u_1} {p : Filter ι} {u u' : ι → TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ} {u₀ u₀' : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ} (hu : Filter.Tendsto u p (nhds u₀)) (hu' : Filter.Tendsto u' p (nhds u₀')) (c : ℂ) (P : MvPolynomial (Fin n) ℂ) (g : EuclideanSpace ℝ (Fin n) → ℂ) : Filter.Tendsto (fun (j : ι) => c • u j) p (nhds (c • u₀)) ∧ Filter.Tendsto (fun (j : ι) => u j + u' j) p (nhds (u₀ + u₀')) ∧ Filter.Tendsto (fun (j : ι) => (constCoeffDiffOp n P) (u j)) p (nhds ((constCoeffDiffOp n P) u₀)) ∧ Filter.Tendsto (fun (j : ι) => (TemperedDistribution.smulLeftCLM ℂ g) (u j)) p (nhds ((TemperedDistribution.smulLeftCLM ℂ g) u₀))

Proposition 11.1 of Melrose (combined): weak-* convergence of tempered distributions is preserved under all the standard operations — scalar multiplication, addition, application of a constant-coefficient differential operator, and multiplication by a function.