Sets of multi-indices bounded coordinatewise

A finite set of multi-indices m : σ →₀ ℕ with mᵢ ≤ rᵢ for every i lies in the box Iic r, so it has at most ∏ᵢ (rᵢ + 1) elements. A sum over such a set of terms bounded by C ≥ 0 is therefore at most ∏ᵢ (rᵢ + 1) C. This is how the monomials of a polynomial with partial degrees degreeOf i P ≤ r i are counted.

Since the boxes Iic m are finite, subtracting a fixed multi-index has finite fibres.

Main results

• Finsupp.card_le_prod_of_forall_le: #s ≤ ∏ᵢ (rᵢ + 1).
• Finsupp.sum_le_prod_mul_of_forall_le: ∑ m ∈ s, f m ≤ ∏ᵢ (rᵢ + 1) C when f ≤ C on s.
• Finsupp.tendsto_sub_cofinite: n ↦ n - d maps the cofinite filter into itself.

theorem Finsupp.card_le_prod_of_forall_le {σ : Type u_1} [Fintype σ] {s : Finset (σ →₀ ℕ)} {r : σ → ℕ} (h : ∀ m ∈ s, ∀ (i : σ), m i ≤ r i) : s.card ≤ ∏ i : σ, (r i + 1)

A finite set of multi-indices bounded coordinatewise by r has at most ∏ᵢ (rᵢ + 1) elements.

theorem Finsupp.sum_le_prod_mul_of_forall_le {σ : Type u_1} [Fintype σ] {R : Type u_2} [CommSemiring R] [PartialOrder R] [IsOrderedRing R] {s : Finset (σ →₀ ℕ)} {r : σ → ℕ} (hs : ∀ m ∈ s, ∀ (i : σ), m i ≤ r i) {f : (σ →₀ ℕ) → R} {C : R} (hf : ∀ m ∈ s, f m ≤ C) (hC : 0 ≤ C) : ∑ m ∈ s, f m ≤ (∏ i : σ, (↑(r i) + 1)) * C

A sum of terms bounded by C ≥ 0 over a set of multi-indices bounded coordinatewise by r is at most ∏ᵢ (rᵢ + 1) C.

theorem Finsupp.tendsto_sub_cofinite {σ : Type u_1} (d : σ →₀ ℕ) : Filter.Tendsto (fun (n : σ →₀ ℕ) => n - d) Filter.cofinite Filter.cofinite

Subtracting a fixed multi-index d has finite fibres: if n - d = m then n ≤ m + d.