Polynomial growth of multivariate polynomials along a filter

If every coordinate of x : α → ι → 𝕜 is O(u) along a filter l, and u is eventually bounded below in the sense that 1 = O(u), then evaluating a polynomial P of total degree at most n at x gives a function that is O(u ^ n). This is the multivariate analogue of the elementary bound |p(x)| ≤ C |x| ^ deg p for large |x|, with the variables allowed to grow at a common rate u rather than being the argument itself. It is the growth input for integrals of a polynomial against an exponentially decaying function.

Main results

• TauCeti.isBigO_aeval_of_totalDegree_le: aeval (x a) P = O(u a ^ n) when each coordinate of x is O(u), 1 = O(u), and P.totalDegree ≤ n.

theorem TauCeti.isBigO_aeval_of_totalDegree_le {α : Type u_1} {ι : Type u_2} {R : Type u_3} {𝕜 : Type u_4} [CommSemiring R] [SeminormedCommRing 𝕜] [Algebra R 𝕜] {l : Filter α} {P : MvPolynomial ι R} {n : ℕ} (hP : P.totalDegree ≤ n) {x : α → ι → 𝕜} {u : α → ℝ} (hx : ∀ (i : ι), (fun (a : α) => x a i) =O[l] u) (hu : (fun (x : α) => 1) =O[l] u) : (fun (a : α) => (MvPolynomial.aeval (x a)) P) =O[l] fun (a : α) => u a ^ n

Polynomial growth of a polynomial in O(u) variables. If each coordinate of x is O(u) along l, and 1 = O(u), then aeval (x a) P is O(u a ^ n) for every n ≥ P.totalDegree.