Power bounds in ordered commutative monoids

This file contains exponent bookkeeping for elements bounded by a power of an element at most 1 in an ordered commutative monoid. It turns valuation estimates for exponential and logarithm coefficients into geometric decay on deep ideals.

Main results

• TauCeti.pow_mul_pow_le_of_le: bounds a product of powers using a bound t ≤ γ ^ i and inequalities between the exponents.

theorem TauCeti.pow_mul_pow_le_of_le {M : Type u_1} [CommMonoid M] [Preorder M] [MulLeftMono M] {γ t : M} (hγ : γ ≤ 1) {d e i m q : ℕ} (ht : t ≤ γ ^ i) (hi : e ≤ d * i) (hq : d * q < m) : t ^ (m * d) * γ ^ (d * i - e) ≤ t ^ d * (γ ^ (d * i - e)) ^ m * γ ^ (d * (e * q))

If γ ≤ 1, t ≤ γ ^ i, e ≤ d * i and d * q < m, then t ^ (m * d) * γ ^ (d * i - e) ≤ t ^ d * (γ ^ (d * i - e)) ^ m * γ ^ (d * (e * q)).