inductive HasSliceRankLE {ι : Type u_1} {R : Type u_2} {α : ι → Type u_3} [Semiring R] : ℕ → (((i : ι) → α i) → R) → Prop

A function f has slice-rank at most n if it can be written as the sum of n functions of the form x ↦ g (x i) * h (x 1, ..., x (i - 1), x (i + 1), ..., x k).

• zero {ι : Type u_1} {R : Type u_2} {α : ι → Type u_3} [Semiring R] : HasSliceRankLE 0 0
• succ {ι : Type u_1} {R : Type u_2} {α : ι → Type u_3} [Semiring R] ⦃n : ℕ⦄ ⦃f : ((i : ι) → α i) → R⦄ ⦃i : ι⦄ (g : α i → R) (h : ((j : ι) → j ≠ i → α j) → R) : HasSliceRankLE n f → HasSliceRankLE (n + 1) (f + fun (x : (i : ι) → α i) => g (x i) * h fun (j : ι) (x_1 : j ≠ i) => x j)

theorem hasSliceRankLE_iff {ι : Type u_1} {R : Type u_2} {α : ι → Type u_3} [Semiring R] (a✝ : ℕ) (a✝¹ : ((i : ι) → α i) → R) : HasSliceRankLE a✝ a✝¹ ↔ a✝ = 0 ∧ a✝¹ = 0 ∨ ∃ (n : ℕ) (f : ((i : ι) → α i) → R) (i : ι) (g : α i → R) (h : ((j : ι) → j ≠ i → α j) → R), HasSliceRankLE n f ∧ a✝ = n + 1 ∧ a✝¹ = f + fun (x : (i : ι) → α i) => g (x i) * h fun (j : ι) (x_1 : j ≠ i) => x j

@[simp]

theorem hasSliceRankLE_zero {ι : Type u_1} {R : Type u_2} {α : ι → Type u_3} [Semiring R] {f : ((i : ι) → α i) → R} : HasSliceRankLE 0 f ↔ f = 0

theorem hasSliceRankLE_succ {ι : Type u_1} {R : Type u_2} {α : ι → Type u_3} [Semiring R] {n : ℕ} {f : ((i : ι) → α i) → R} : HasSliceRankLE (n + 1) f ↔ ∃ (f' : ((i : ι) → α i) → R) (i : ι) (g : α i → R) (h : ((j : ι) → j ≠ i → α j) → R), HasSliceRankLE n f' ∧ f = f' + fun (x : (i : ι) → α i) => g (x i) * h fun (j : ι) (x_1 : j ≠ i) => x j

theorem hasSliceRankLE_one {ι : Type u_1} {R : Type u_2} {α : ι → Type u_3} [Semiring R] {f : ((i : ι) → α i) → R} : HasSliceRankLE 1 f ↔ ∃ (i : ι) (g : α i → R) (h : ((j : ι) → j ≠ i → α j) → R), f = fun (x : (i : ι) → α i) => g (x i) * h fun (j : ι) (x_1 : j ≠ i) => x j

theorem hasSliceRankLE_iff_exists_sum {ι : Type u_1} {R : Type u_2} {α : ι → Type u_3} [Semiring R] {n : ℕ} {f : ((i : ι) → α i) → R} : HasSliceRankLE n f ↔ ∃ (i : Fin n → ι) (g : (k : Fin n) → α (i k) → R) (h : (k : Fin n) → ((j : ι) → j ≠ i k → α j) → R), f = ∑ k : Fin n, fun (x : (i : ι) → α i) => g k (x (i k)) * h k fun (j : ι) (x_1 : j ≠ i k) => x j

theorem HasSliceRankLE.add {ι : Type u_1} {R : Type u_2} {α : ι → Type u_3} [Semiring R] {m : ℕ} {f₁ : ((i : ι) → α i) → R} (h₁ : HasSliceRankLE m f₁) {n : ℕ} {f₂ : ((i : ι) → α i) → R} : HasSliceRankLE n f₂ → HasSliceRankLE (m + n) (f₁ + f₂)

theorem hasSliceRankLE_card {ι : Type u_1} {R : Type u_2} {α : ι → Type u_3} [Semiring R] [DecidableEq ι] [Fintype ι] [(i : ι) → Fintype (α i)] (f : ((i : ι) → α i) → R) : HasSliceRankLE (Fintype.card ((i : ι) → α i)) f

Any function has slice-rank bounded by the cardinality of its domain.

theorem exists_hasSliceRankLE {ι : Type u_1} {R : Type u_2} {α : ι → Type u_3} [Semiring R] [Finite ι] [∀ (i : ι), Finite (α i)] (f : ((i : ι) → α i) → R) : ∃ (n : ℕ), HasSliceRankLE n f

Any function from a finite type has finite slice-rank.