def WeightedDerivExpansion.multiIndexSize {n : ℕ} (γ : Fin n → ℕ) : ℕ

Size (sum of components) of a multi-index γ : Fin n → ℕ.

def WeightedDerivExpansion.multiIndexLE {n : ℕ} (α γ : Fin n → ℕ) : Prop

Componentwise order on multi-indices: α ≤ γ iff α i ≤ γ i for every i.

@[implicit_reducible]

instance WeightedDerivExpansion.instDecidableMultiIndexLE {n : ℕ} (α γ : Fin n → ℕ) : Decidable (multiIndexLE α γ)

The componentwise order on multi-indices is decidable.

def WeightedDerivExpansion.multiIndexDiffSize {n : ℕ} (γ α : Fin n → ℕ) : ℕ

The total size of the componentwise difference γ - α of multi-indices.

theorem WeightedDerivExpansion.diff_size_update_lt {n : ℕ} {γ α : Fin n → ℕ} {j₀ : Fin n} (hj₀ : 0 < γ j₀) (hα : multiIndexLE α (Function.update γ j₀ (γ j₀ - 1))) : 1 + multiIndexDiffSize (Function.update γ j₀ (γ j₀ - 1)) α ≤ multiIndexDiffSize γ α

Decreasing the j₀-th coordinate of γ by one strictly decreases the difference size multiIndexDiffSize γ α by at least one (and α still bounds the updated γ).