theorem DifferentialOperators.iteratedFDeriv_poly_reciprocal_step {n : ℕ} (P : MvPolynomial (Fin n) ℝ) (k : ℕ) (L_prev : MvPolynomial (Fin n) ℝ) (hL_deg : L_prev.totalDegree ≤ P.totalDegree.pred * k) (hL_bound : ∀ (ξ : EuclideanSpace ℝ (Fin n)), (MvPolynomial.eval fun (i : Fin n) => ξ.ofLp i) P ≠ 0 → ‖iteratedFDeriv ℝ k (fun (ξ' : EuclideanSpace ℝ (Fin n)) => ((MvPolynomial.eval fun (i : Fin n) => ξ'.ofLp i) P)⁻¹) ξ‖ ≤ ‖(MvPolynomial.eval fun (i : Fin n) => ξ.ofLp i) L_prev‖ / ‖(MvPolynomial.eval fun (i : Fin n) => ξ.ofLp i) P‖ ^ (1 + k)) : ∃ (L_next : MvPolynomial (Fin n) ℝ), L_next.totalDegree ≤ P.totalDegree.pred * (k + 1) ∧ ∀ (ξ : EuclideanSpace ℝ (Fin n)), (MvPolynomial.eval fun (i : Fin n) => ξ.ofLp i) P ≠ 0 → ‖iteratedFDeriv ℝ (k + 1) (fun (ξ' : EuclideanSpace ℝ (Fin n)) => ((MvPolynomial.eval fun (i : Fin n) => ξ'.ofLp i) P)⁻¹) ξ‖ ≤ ‖(MvPolynomial.eval fun (i : Fin n) => ξ.ofLp i) L_next‖ / ‖(MvPolynomial.eval fun (i : Fin n) => ξ.ofLp i) P‖ ^ (1 + (k + 1))

Inductive step for the structural bound on iterated Fréchet derivatives of 1/P: given a polynomial L_prev controlling the k-th iterated derivative as ‖D^k(1/P)(ξ)‖ ≤ ‖L_prev(ξ)‖ / ‖P(ξ)‖^(1+k), produce a polynomial L_next of degree at most (deg P - 1)(k+1) controlling the (k+1)-th iterated derivative analogously.

theorem DifferentialOperators.iteratedFDeriv_poly_reciprocal_structural {n : ℕ} (P : MvPolynomial (Fin n) ℝ) (k : ℕ) : ∃ (L : MvPolynomial (Fin n) ℝ), L.totalDegree ≤ P.totalDegree.pred * k ∧ ∀ (ξ : EuclideanSpace ℝ (Fin n)), (MvPolynomial.eval fun (i : Fin n) => ξ.ofLp i) P ≠ 0 → ‖iteratedFDeriv ℝ k (fun (ξ' : EuclideanSpace ℝ (Fin n)) => ((MvPolynomial.eval fun (i : Fin n) => ξ'.ofLp i) P)⁻¹) ξ‖ ≤ ‖(MvPolynomial.eval fun (i : Fin n) => ξ.ofLp i) L‖ / ‖(MvPolynomial.eval fun (i : Fin n) => ξ.ofLp i) P‖ ^ (1 + k)

Structural bound on the k-th iterated Fréchet derivative of 1/P: there exists a polynomial L of total degree at most (deg P - 1)·k such that ‖D^k(1/P)(ξ)‖ ≤ ‖L(ξ)‖ / ‖P(ξ)‖^(1+k) whenever P(ξ) ≠ 0. Proved by induction using iteratedFDeriv_poly_reciprocal_step.

theorem DifferentialOperators.mvPolynomial_eval_norm_le_pow {n : ℕ} (Q : MvPolynomial (Fin n) ℝ) : ∃ A > 0, ∀ (ξ : EuclideanSpace ℝ (Fin n)), ‖(MvPolynomial.eval fun (i : Fin n) => ξ.ofLp i) Q‖ ≤ A * (1 + ‖ξ‖) ^ Q.totalDegree

Polynomial growth bound for evaluation of a real multivariate polynomial: there exists A > 0 so that ‖Q(ξ)‖ ≤ A · (1 + ‖ξ‖)^(deg Q) for all ξ.

theorem DifferentialOperators.reciprocal_poly_iteratedFDeriv_structural_bound (n : ℕ) (P : MvPolynomial (Fin n) ℝ) (m : ℕ) (hm : 1 ≤ m) (hdeg : P.totalDegree ≤ m) (C : ℝ) (hC : C > 0) (hP : ∀ (ξ : EuclideanSpace ℝ (Fin n)), ‖ξ‖ > 1 / C → ‖(MvPolynomial.eval fun (i : Fin n) => ξ.ofLp i) P‖ ≥ C * ‖ξ‖ ^ m) (k : ℕ) : ∃ C₁ > 0, ∀ (ξ : EuclideanSpace ℝ (Fin n)), ‖ξ‖ > 1 / C → ‖iteratedFDeriv ℝ k (fun (ξ' : EuclideanSpace ℝ (Fin n)) => ((MvPolynomial.eval fun (i : Fin n) => ξ'.ofLp i) P)⁻¹) ξ‖ ≤ C₁ * (1 + ‖ξ‖) ^ ((m - 1) * k) / ‖(MvPolynomial.eval fun (i : Fin n) => ξ.ofLp i) P‖ ^ (1 + k)

Quantitative bound on iterated Fréchet derivatives of 1/P outside {‖ξ‖ > 1/C}: combining the structural polynomial bound with the polynomial growth of its coefficients, one obtains ‖D^k(1/P)(ξ)‖ ≤ C₁ · (1 + ‖ξ‖)^((m-1)·k) / ‖P(ξ)‖^(1+k).

theorem DifferentialOperators.mvPolynomial_evalAtReal_norm_le_pow {n : ℕ} (Q : MvPolynomial (Fin n) ℂ) : ∃ A > 0, ∀ (ξ : EuclideanSpace ℝ (Fin n)), ‖evalAtReal Q ξ‖ ≤ A * (1 + ‖ξ‖) ^ Q.totalDegree

Polynomial growth bound for evalAtReal Q: there exists A > 0 such that for every real input ξ, ‖Q(ξ)‖ ≤ A · (1 + ‖ξ‖)^(deg Q). Complex-coefficient analogue of mvPolynomial_eval_norm_le_pow.

theorem DifferentialOperators.reciprocal_poly_deriv_bound_multiIndex {n : ℕ} (P : MvPolynomial (Fin n) ℂ) (m : ℕ) (hm : 1 ≤ m) (hdeg : P.totalDegree ≤ m) (C : ℝ) (hP : HasPolyLowerBound P m C) (js : List (Fin n)) : ∃ Cα > 0, ∀ (ξ : EuclideanSpace ℝ (Fin n)), ‖ξ‖ > 1 / C → ‖iteratedPartialDeriv js (polyReciprocal P) ξ‖ ≤ Cα * ‖ξ‖ ^ (-↑(m + js.length))

Multi-index derivative bound for 1/P outside {‖ξ‖ > 1/C}: under the polynomial lower bound ‖P(ξ)‖ ≥ C · ‖ξ‖^m, an iterated partial derivative ∂^α (1/P) of order |α| decays like ‖ξ‖^(-(m + |α|)). This is the elliptic-style parametrix decay estimate from Melrose Cor 12.15.