Finite products and sums against Pi.single

A product ∏ j, f j ^ e j whose exponent vector e is Pi.single i a is the single power f i ^ a. For exponent vectors α : ι → ℕ over a finite type, this file records how the total degree ∑ j, α j controls the decomposition of α into unit vectors Pi.single i 1, and proves an induction principle over the exponent vectors of a fixed degree d: starting from the pure power Pi.single i d, every such vector is reached by moving one unit at a time from the coordinate i to another coordinate.

Main results

• Finset.univ_prod_mulSingle_mulSingle, Finset.univ_sum_single_single: double dependent product or sum of Pi.mulSingle i (Pi.mulSingle j (f i j)) / Pi.single i (Pi.single j (f i j)) equals f.
• Fintype.prod_pow_pi_single: ∏ j, f j ^ Pi.single i a j = f i ^ a.
• Pi.exists_eq_add_single_one: an exponent vector with a positive i-th entry is γ + e_i.
• Pi.eq_single_of_apply_eq_sum: an exponent vector of degree d with i-th entry d is Pi.single i d.
• Fintype.exists_ne_pos_of_apply_lt_sum: an exponent vector whose i-th entry is less than its degree has another positive entry.
• Pi.induction_on_single_of_sum_eq: induction over the exponent vectors of degree d, starting from Pi.single i d and moving one unit at a time from the coordinate i to another coordinate.

theorem Finset.univ_prod_mulSingle_mulSingle {ι : Type u_1} [Fintype ι] [DecidableEq ι] {κ : ι → Type u_2} [(i : ι) → Fintype (κ i)] [(i : ι) → DecidableEq (κ i)] {M : (i : ι) → κ i → Type u_3} [(i : ι) → (j : κ i) → CommMonoid (M i j)] (f : (i : ι) → (j : κ i) → M i j) : ∏ i : ι, ∏ j : κ i, Pi.mulSingle i (Pi.mulSingle j (f i j)) = f

Decomposing a dependent two-argument function f : ∀ i j, M i j as the iterated product of pointwise Pi.mulSingle factors.

theorem Finset.univ_sum_single_single {ι : Type u_1} [Fintype ι] [DecidableEq ι] {κ : ι → Type u_2} [(i : ι) → Fintype (κ i)] [(i : ι) → DecidableEq (κ i)] {M : (i : ι) → κ i → Type u_3} [(i : ι) → (j : κ i) → AddCommMonoid (M i j)] (f : (i : ι) → (j : κ i) → M i j) : ∑ i : ι, ∑ j : κ i, Pi.single i (Pi.single j (f i j)) = f

Decomposing a dependent two-argument function f : ∀ i j, M i j as the iterated sum of pointwise Pi.single terms.

theorem Finset.sum_pi_single_one_eq_card_filter {ι : Type u_1} {J : Type u_2} [DecidableEq ι] (s : Finset J) (x : J → ι) : ∑ j ∈ s, Pi.single (x j) 1 = fun (i : ι) => {j ∈ s | x j = i}.card

Summing one-hot vectors counts the occurrences of each label in the finite sample.

theorem Fintype.prod_pow_pi_single {ι : Type u_1} [Fintype ι] [DecidableEq ι] {M : Type u_2} [CommMonoid M] (f : ι → M) (i : ι) (a : ℕ) : ∏ j : ι, f j ^ Pi.single i a j = f i ^ a

The monomial with exponent vector Pi.single i a is the power f i ^ a.

theorem Pi.exists_eq_add_single_one {ι : Type u_1} [DecidableEq ι] {β : ι → ℕ} {i : ι} (h : 0 < β i) : ∃ (γ : ι → ℕ), β = γ + single i 1

An exponent vector with a positive i-th entry is of the form γ + e_i.

theorem Pi.eq_single_of_apply_eq_sum {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : ι → ℕ} {d : ℕ} (hα : ∑ j : ι, α j = d) {i : ι} (hi : α i = d) : α = single i d

An exponent vector of degree d whose i-th entry is d is the pure power d e_i.

theorem Fintype.exists_ne_pos_of_apply_lt_sum {ι : Type u_1} [Fintype ι] {α : ι → ℕ} {i : ι} (hi : α i < ∑ j : ι, α j) : ∃ (j : ι), j ≠ i ∧ 0 < α j

An exponent vector whose i-th entry is less than its degree has another positive entry.

theorem Pi.induction_on_single_of_sum_eq {ι : Type u_1} [Fintype ι] [DecidableEq ι] {d : ℕ} (i : ι) {P : (ι → ℕ) → Prop} (hsingle : P (single i d)) (step : ∀ (β : ι → ℕ) (j : ι), j ≠ i → ∑ k : ι, β k + 1 = d → P (β + single i 1) → P (β + single j 1)) {α : ι → ℕ} (hα : ∑ j : ι, α j = d) : P α

Induction over the exponent vectors of degree d, starting from the pure power d e_i and moving one unit at a time from the coordinate i to another coordinate j: a property of d e_i which transfers from β + e_i to β + e_j holds for every exponent vector of degree d.