Weighted ultrametric bounds on finite sums #
Mathlib's Valuation.map_sum_le bounds the value of a finite sum by a common bound on the values
of its terms. This file records the weighted form: if every term satisfies v (f i) * c ≤ B, then
so does the sum. Weighted bounds of this shape arise when estimating the terms of polynomial
expressions against a varying scale, as in TauCeti/RingTheory/Valuation/Polynomial.lean.
Main results #
Valuation.map_sum_mul_le: the ultrametric bound on a finite sum, with every term weighted by a common factor.
theorem
Valuation.map_sum_mul_le
{R : Type u_1}
{Γ₀ : Type u_2}
[Ring R]
[LinearOrderedCommMonoidWithZero Γ₀]
(v : Valuation R Γ₀)
{ι : Type u_3}
{s : Finset ι}
{f : ι → R}
{c B : Γ₀}
(h : ∀ i ∈ s, v (f i) * c ≤ B)
:
The ultrametric bound on a finite sum, with every term weighted by a common factor c.