theorem SmoothingOperators.smoothing_produces_smooth {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (u : TemperedDistribution E ℂ) (φ : SchwartzMap E ℂ) : ContDiff ℝ ↑⊤ fun (x : E) => u ((SchwartzMap.compSubConstCLM ℂ x) φ)

Smoothing by a tempered distribution: convolving a tempered distribution u with a Schwartz function φ (via the family of translations x ↦ u(φ(·−x))) produces a smooth function.

theorem SmoothingOperators.schwartz_translation_fderiv_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] (L : SchwartzMap E ℂ →L[ℂ] F) (ψ : SchwartzMap E ℂ) (x h : E) : (fderiv ℝ (fun (z : E) => L ((SchwartzMap.compSubConstCLM ℂ z) ψ)) x) h = L ((SchwartzMap.compSubConstCLM ℂ x) (LineDeriv.lineDerivOp (-h) ψ))

The Fréchet derivative of z ↦ L(ψ(·−z)) at x evaluated on h equals L(∂_{-h} ψ (·−x)): differentiating the family of translations in the spatial variable produces a line derivative of ψ (in the opposite direction) inside L.

theorem SmoothingOperators.smoothing_lineDeriv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (u : TemperedDistribution E ℂ) (φ : SchwartzMap E ℂ) (m x : E) : lineDeriv ℝ (fun (z : E) => u ((SchwartzMap.compSubConstCLM ℂ z) φ)) x m = u ((SchwartzMap.compSubConstCLM ℂ x) (LineDeriv.lineDerivOp (-m) φ))

Line derivative of the smoothed function: the directional derivative of x ↦ u(φ(·−x)) along m equals u applied to ∂_{-m} φ translated to x. This is the distributional identity used to differentiate the smoothing.

noncomputable def DifferentialOperators.evalAtReal {n : ℕ} (P : MvPolynomial (Fin n) ℂ) (ξ : EuclideanSpace ℝ (Fin n)) : ℂ

Evaluation of a multivariate complex polynomial at a real Euclidean point, viewed as a function EuclideanSpace ℝ (Fin n) → ℂ.

def DifferentialOperators.HasPolyLowerBound {n : ℕ} (P : MvPolynomial (Fin n) ℂ) (m : ℕ) (C : ℝ) : Prop

The polynomial P has a polynomial lower bound of degree m with constant C > 0 if, for every ξ of norm larger than 1/C, the inequality ‖P(ξ)‖ ≥ C · ‖ξ‖^m holds.

noncomputable def DifferentialOperators.polyReciprocal {n : ℕ} (P : MvPolynomial (Fin n) ℂ) : EuclideanSpace ℝ (Fin n) → ℂ

The pointwise reciprocal of a polynomial: ξ ↦ 1 / P(ξ), with P(ξ) = 0 mapped to 0 by the inverse convention.