Fin Sigma Equivalences

We re-define big-operators sum and product over Fin to have good definitional equalities.

def Fin.addCast {n : ℕ} (m : ℕ) (i : Fin n) : Fin (m + n)

def Fin.vprod {α : Type u_1} [CommMonoid α] {n : ℕ} (a : Fin n → α) : α

Version of multiplying over Fin vectors with good definitional equalities, using dfoldl'.

The definitional equality we want is that: vprod a = a 0 * (a 1 * (... * (a (n-1) * 1)))

def Fin.vsum {α : Type u_1} [AddCommMonoid α] {n : ℕ} (a : Fin n → α) : α

Version of summing over Fin vectors with good definitional equalities, using dfoldl'.

The definitional equality we want is that: vsum a = a 0 + (a 1 + (... + (a (n-1) + 0))).

When x + 0 = x definitionally in α, we have the following definitional equalities:

• vsum !v[] = 0
• vsum !v[a] = a
• vsum !v[a, b] = a + b
• vsum !v[a, b, c] = a + (b + c)
• and so on

@[simp]

theorem Fin.vprod_zero {α : Type u_1} [CommMonoid α] {a : Fin 0 → α} : vprod a = 1

@[simp]

theorem Fin.vsum_zero {α : Type u_1} [AddCommMonoid α] {a : Fin 0 → α} : vsum a = 0

@[simp]

theorem Fin.vprod_succ {α : Type u_1} {n : ℕ} [CommMonoid α] {a : Fin (n + 1) → α} : vprod a = a 0 * vprod (a ∘ succ)

@[simp]

theorem Fin.vsum_succ {α : Type u_1} {n : ℕ} [AddCommMonoid α] {a : Fin (n + 1) → α} : vsum a = a 0 + vsum (a ∘ succ)

theorem Fin.vprod_eq_univ_prod {α : Type u_1} {n : ℕ} [CommMonoid α] {a : Fin n → α} : vprod a = ∏ i : Fin n, a i

vprod a is equivalent to the standard Finset-based definition, ∏ i, a i.

theorem Fin.vsum_eq_univ_sum {α : Type u_1} {n : ℕ} [AddCommMonoid α] {a : Fin n → α} : vsum a = ∑ i : Fin n, a i

theorem Fin.vprod_castSucc {α : Type u_1} {n : ℕ} [CommMonoid α] {a : Fin (n + 1) → α} : vprod a = vprod (a ∘ castSucc) * a (last n)

theorem Fin.vsum_castSucc {α : Type u_1} {n : ℕ} [AddCommMonoid α] {a : Fin (n + 1) → α} : vsum a = vsum (a ∘ castSucc) + a (last n)

def Fin.embedSum {m : ℕ} {n : Fin m → ℕ} (i : Fin m) (j : Fin (n i)) : Fin (vsum n)

Embed nested indices (i : Fin m, j : Fin (n i)) into a single index Fin (vsum n). This converts from nested indexing to indexing into the vector sum, preserving lexicographic order.

@[simp]

theorem Fin.embedSum_zero {n : Fin 0 → ℕ} {i : Fin 0} (j : Fin (n i)) : i.embedSum j = i

theorem Fin.embedSum_succ {m : ℕ} {n : Fin (m + 1) → ℕ} {i : Fin (m + 1)} (j : Fin (n i)) : i.embedSum j = match i, j with | ⟨0, ⋯⟩, j => castAdd (dfoldrM' m ((fun (x : Fin (m + 1 + 1)) => ℕ) ∘ succ) (fun (i : Fin m) => (fun (i : Fin (m + 1)) (acc : ℕ) => n i + acc) i.succ) 0) j | ⟨i.succ, h⟩, j => natAdd (n 0) (⟨i, ⋯⟩.embedSum j)

@[simp]

theorem Fin.embedSum_succ_zero {m : ℕ} {n : Fin (m + 1) → ℕ} {j : Fin (n 0)} : embedSum 0 j = castAdd (dfoldrM' m ((fun (x : Fin (m + 1 + 1)) => ℕ) ∘ succ) (fun (i : Fin m) => (fun (i : Fin (m + 1)) (acc : ℕ) => n i + acc) i.succ) 0) j

@[simp]

theorem Fin.embedSum_succ_succ {m : ℕ} {n : Fin (m + 1) → ℕ} {i : Fin m} (j : Fin (n i.succ)) : i.succ.embedSum j = natAdd (n 0) (i.embedSum j)

def Fin.splitSum {m : ℕ} {n : Fin m → ℕ} (k : Fin (vsum n)) : (i : Fin m) × Fin (n i)

Split a vector sum index k : Fin (vsum n) into nested indices (i : Fin m) × Fin (n i). This converts from indexing into the vector sum back to nested indexing, inverse of embedSum.

@[simp]

theorem Fin.splitSum_zero {n : Fin 0 → ℕ} {k : Fin (vsum n)} : k.splitSum = k.elim0

@[simp]

theorem Fin.splitSum_succ {m : ℕ} {n : Fin (m + 1) → ℕ} {k : Fin (vsum n)} : k.splitSum = ((fun (k : Fin (n 0)) => ⟨0, k⟩) ++ᵈ fun (k : Fin (dfoldrM' m ((fun (x : Fin (m + 1 + 1)) => ℕ) ∘ succ) (fun (i : Fin m) => (fun (i : Fin (m + 1)) (acc : ℕ) => n i + acc) i.succ) 0)) => ⟨k.splitSum.fst.succ, k.splitSum.snd⟩) k

@[simp]

theorem Fin.embedSum_splitSum {m : ℕ} {n : Fin m → ℕ} (k : Fin (vsum n)) : k.splitSum.fst.embedSum k.splitSum.snd = k

@[simp]

theorem Fin.splitSum_embedSum {m : ℕ} {n : Fin m → ℕ} (i : Fin m) (j : Fin (n i)) : (i.embedSum j).splitSum = ⟨i, j⟩

def Fin.finSum'FinEquiv' {m : ℕ} {n : Fin m → ℕ} : (i : Fin m) × Fin (n i) ≃ Fin (vsum n)

def Fin.dflatten {m : ℕ} {n : Fin m → ℕ} {motive : Fin (vsum n) → Sort u_2} (v : (i : Fin m) → (j : Fin (n i)) → motive (i.embedSum j)) (k : Fin (vsum n)) : motive k

Dependent flatten with unified motive: flattens a nested dependent vector (i : Fin m) → (j : Fin (n i)) → motive (embedSum i j) into a single dependent vector (k : Fin (vsum n)) → motive k, preserving element order.

This is meant to replace nested iteration for dependent families with a unified motive.

@[simp]

theorem Fin.dflatten_zero {n : Fin 0 → ℕ} {motive : Fin (vsum n) → Sort u_2} {v : (i : Fin 0) → (j : Fin (n i)) → motive (i.embedSum j)} : dflatten v = fun (k : Fin 0) => k.elim0

@[simp]

theorem Fin.dflatten_succ {m : ℕ} {n : Fin (m + 1) → ℕ} {motive : Fin (vsum n) → Sort u_2} {v : (i : Fin (m + 1)) → (j : Fin (n i)) → motive (i.embedSum j)} : dflatten v = fun (i : Fin (n 0 + dfoldrM' m ((fun (x : Fin (m + 1 + 1)) => ℕ) ∘ succ) (fun (i : Fin m) => (fun (i : Fin (m + 1)) (acc : ℕ) => n i + acc) i.succ) 0)) => (v 0 ++ᵈ fun (k : Fin (vsum fun (i : Fin m) => n i.succ)) => dflatten (fun (i : Fin m) => v i.succ) k) i

@[simp]

theorem Fin.dflatten_one {n : Fin 1 → ℕ} {motive : Fin (vsum n) → Sort u_2} {v : (i : Fin 1) → (j : Fin (n i)) → motive (i.embedSum j)} : dflatten v = v 0

@[simp]

theorem Fin.dflatten_two_eq_append {n : Fin 2 → ℕ} {motive : Fin (vsum n) → Sort u_2} {v : (i : Fin 2) → (j : Fin (n i)) → motive (i.embedSum j)} : dflatten v = fun (i : Fin (n 0 + dfoldrM' 1 ((fun (x : Fin (2 + 1)) => ℕ) ∘ succ) (fun (i : Fin 1) => (fun (i : Fin 2) (acc : ℕ) => n i + acc) i.succ) 0)) => (v 0 ++ᵈ v 1) i

@[simp]

theorem Fin.dflatten_splitSum {m : ℕ} {n : Fin m → ℕ} {motive : Fin (vsum n) → Sort u_2} (v : (k : Fin (vsum n)) → motive k) (k : Fin (vsum n)) : dflatten (fun (i : Fin m) (j : Fin (n i)) => v (i.embedSum j)) k = v k

@[simp]

theorem Fin.dflatten_embedSum {m : ℕ} {n : Fin m → ℕ} {motive : Fin (vsum n) → Sort u_2} (v : (i : Fin m) → (j : Fin (n i)) → motive (i.embedSum j)) (i : Fin m) (j : Fin (n i)) : dflatten v (i.embedSum j) = v i j

def Fin.vflatten {α : Sort u_1} {m : ℕ} {n : Fin m → ℕ} (v : (i : Fin m) → Fin (n i) → α) : Fin (vsum n) → α

Homogeneous flatten: flattens a nested homogeneous vector (i : Fin m) → (j : Fin (n i)) → α into a single homogeneous vector Fin (vsum n) → α by specializing dflatten to the constant-type motive fun _ => α.

@[simp]

theorem Fin.vflatten_zero {α : Sort u_1} {n : Fin 0 → ℕ} {v : (i : Fin 0) → Fin (n i) → α} : vflatten v = !v[]

@[simp]

theorem Fin.vflatten_succ {α : Sort u_1} {m : ℕ} {n : Fin (m + 1) → ℕ} {v : (i : Fin (m + 1)) → Fin (n i) → α} : vflatten v = v 0 ++ᵛ vflatten fun (i : Fin m) => v i.succ

@[simp]

theorem Fin.vflatten_one {α : Sort u_1} {n : Fin 1 → ℕ} {v : (i : Fin 1) → Fin (n i) → α} : vflatten v = v 0

@[simp]

theorem Fin.vflatten_two_eq_append {α : Sort u_1} {n : Fin 2 → ℕ} {v : (i : Fin 2) → Fin (n i) → α} : vflatten v = v 0 ++ᵛ v 1

theorem Fin.vflatten_eq_vappend_last {α : Sort u_1} {m : ℕ} {n : Fin (m + 1) → ℕ} {v : (i : Fin (m + 1)) → Fin (n i) → α} : vflatten v = ((vflatten fun (i : Fin m) => v i.castSucc) ++ᵛ v (last m)) ∘ Fin.cast ⋯

@[simp]

theorem Fin.vflatten_splitSum {α : Sort u_1} {m : ℕ} {n : Fin m → ℕ} (v : Fin (vsum n) → α) (k : Fin (vsum n)) : vflatten (fun (i : Fin m) (j : Fin (n i)) => v (i.embedSum j)) k = v k

@[simp]

theorem Fin.vflatten_embedSum {α : Sort u_1} {m : ℕ} {n : Fin m → ℕ} (v : (i : Fin m) → Fin (n i) → α) (i : Fin m) (j : Fin (n i)) : vflatten v (i.embedSum j) = v i j

def Fin.fflatten {A : Sort u} {F : A → Sort v} {m : ℕ} {n : Fin m → ℕ} {α : (i : Fin m) → Fin (n i) → A} (v : (i : Fin m) → (j : Fin (n i)) → F (α i j)) (k : Fin (vsum n)) : F (vflatten α k)

Functorial flatten: flattens a nested heterogeneous tuple (i : Fin m) → (j : Fin (n i)) → F (α i j) into a single heterogeneous tuple with type (k : Fin (vsum n)) → F (vflatten α k) where vflatten operates on the vector of types α.

Unlike dflatten which requires an explicit unified motive, fflatten uses vflatten to automatically construct the motive from the input type family.

@[simp]

theorem Fin.fflatten_zero {A : Sort u} {F : A → Sort v} {n : Fin 0 → ℕ} {α : (i : Fin 0) → Fin (n i) → A} {v : (i : Fin 0) → (j : Fin (n i)) → F (α i j)} : fflatten v = !h[]

@[simp]

theorem Fin.fflatten_succ {A : Sort u} {F : A → Sort v} {m : ℕ} {n : Fin (m + 1) → ℕ} {α : (i : Fin (m + 1)) → Fin (n i) → A} {v : (i : Fin (m + 1)) → (j : Fin (n i)) → F (α i j)} : fflatten v = fappend (v 0) (fflatten fun (i : Fin m) => v i.succ)

@[simp]

theorem Fin.fflatten_one {A : Sort u} {F : A → Sort v} {n : Fin 1 → ℕ} {α : (i : Fin 1) → Fin (n i) → A} {v : (i : Fin 1) → (j : Fin (n i)) → F (α i j)} : fflatten v = v 0

@[simp]

theorem Fin.fflatten_two_eq_append {A : Sort u} {F : A → Sort v} {n : Fin 2 → ℕ} {α : (i : Fin 2) → Fin (n i) → A} {v : (i : Fin 2) → (j : Fin (n i)) → F (α i j)} : fflatten v = fappend (v 0) (v 1)

@[simp]

theorem Fin.fflatten_splitSum {A : Sort u} {F : A → Sort v} {m : ℕ} {n : Fin m → ℕ} {α : Fin (vsum n) → A} (v : (k : Fin (vsum n)) → F (α k)) (k : Fin (vsum n)) : fflatten (fun (i : Fin m) (j : Fin (n i)) => v (i.embedSum j)) k = cast ⋯ (v k)

@[simp]

theorem Fin.fflatten_embedSum {A : Sort u} {F : A → Sort v} {m : ℕ} {n : Fin m → ℕ} {α : (i : Fin m) → Fin (n i) → A} (v : (i : Fin m) → (j : Fin (n i)) → F (α i j)) (i : Fin m) (j : Fin (n i)) : fflatten v (i.embedSum j) = cast ⋯ (v i j)

def Fin.fflatten₂ {A : Sort u} {B : Sort v} {F : A → B → Sort w} {m : ℕ} {n : Fin m → ℕ} {α : (i : Fin m) → Fin (n i) → A} {β : (i : Fin m) → Fin (n i) → B} (v : (i : Fin m) → (j : Fin (n i)) → F (α i j) (β i j)) (k : Fin (vsum n)) : F (vflatten α k) (vflatten β k)

Functorial flatten with two arguments: flattens two nested heterogeneous tuple (i : Fin m) → (j : Fin (n i)) → F (α i j) into a single heterogeneous tuple with type (k : Fin (vsum n)) → F (vflatten α k) where vflatten operates on the vector of types α.

Unlike dflatten which requires an explicit unified motive, fflatten uses vflatten to automatically construct the motive from the input type family.

@[simp]

theorem Fin.fflatten₂_zero {A : Sort u} {B : Sort v} {F : A → B → Sort w} {n : Fin 0 → ℕ} {α : (i : Fin 0) → Fin (n i) → A} {β : (i : Fin 0) → Fin (n i) → B} {v : (i : Fin 0) → (j : Fin (n i)) → F (α i j) (β i j)} : fflatten₂ v = !h[]

@[simp]

theorem Fin.fflatten₂_succ {A : Sort u} {B : Sort v} {F : A → B → Sort w} {m : ℕ} {n : Fin (m + 1) → ℕ} {α : (i : Fin (m + 1)) → Fin (n i) → A} {β : (i : Fin (m + 1)) → Fin (n i) → B} {v : (i : Fin (m + 1)) → (j : Fin (n i)) → F (α i j) (β i j)} : fflatten₂ v = fappend₂ (v 0) (fflatten₂ fun (i : Fin m) => v i.succ)

@[simp]

theorem Fin.fflatten₂_one {A : Sort u} {B : Sort v} {F : A → B → Sort w} {n : Fin 1 → ℕ} {α : (i : Fin 1) → Fin (n i) → A} {β : (i : Fin 1) → Fin (n i) → B} {v : (i : Fin 1) → (j : Fin (n i)) → F (α i j) (β i j)} : fflatten₂ v = v 0

@[simp]

theorem Fin.fflatten₂_two_eq_append {A : Sort u} {B : Sort v} {F : A → B → Sort w} {n : Fin 2 → ℕ} {α : (i : Fin 2) → Fin (n i) → A} {β : (i : Fin 2) → Fin (n i) → B} {v : (i : Fin 2) → (j : Fin (n i)) → F (α i j) (β i j)} : fflatten₂ v = fappend₂ (v 0) (v 1)

@[simp]

theorem Fin.fflatten₂_splitSum {A : Sort u} {B : Sort v} {F : A → B → Sort w} {m : ℕ} {n : Fin m → ℕ} {α : (i : Fin m) → Fin (n i) → A} {β : (i : Fin m) → Fin (n i) → B} (v : (k : Fin (vsum n)) → F (vflatten α k) (vflatten β k)) (k : Fin (vsum n)) : fflatten₂ (fun (i : Fin m) (j : Fin (n i)) => v (i.embedSum j)) k = cast ⋯ (v k)

@[simp]

theorem Fin.fflatten₂_embedSum {A : Sort u} {B : Sort v} {F : A → B → Sort w} {m : ℕ} {n : Fin m → ℕ} {α : (i : Fin m) → Fin (n i) → A} {β : (i : Fin m) → Fin (n i) → B} (v : (i : Fin m) → (j : Fin (n i)) → F (α i j) (β i j)) (i : Fin m) (j : Fin (n i)) : fflatten₂ v (i.embedSum j) = cast ⋯ (v i j)

def Fin.hflatten {m : ℕ} {n : Fin m → ℕ} {α : (i : Fin m) → Fin (n i) → Sort u_2} (v : (i : Fin m) → (j : Fin (n i)) → α i j) (k : Fin (vsum n)) : vflatten α k

Heterogeneous flatten: flattens a nested heterogeneous tuple (i : Fin m) → (j : Fin (n i)) → α i j into a single heterogeneous tuple with type (k : Fin (vsum n)) → vflatten α k where vflatten operates on the vector of types α.

Unlike dflatten which requires an explicit unified motive, hflatten uses vflatten to automatically construct the motive from the input type family.

@[simp]

theorem Fin.hflatten_zero {n : Fin 0 → ℕ} {α : (i : Fin 0) → Fin (n i) → Sort u_2} {v : (i : Fin 0) → (j : Fin (n i)) → α i j} : hflatten v = !h[]

@[simp]

theorem Fin.hflatten_succ {m : ℕ} {n : Fin (m + 1) → ℕ} {α : (i : Fin (m + 1)) → Fin (n i) → Sort u_2} {v : (i : Fin (m + 1)) → (j : Fin (n i)) → α i j} : hflatten v = v 0 ++ʰ hflatten fun (i : Fin m) => v i.succ

@[simp]

theorem Fin.hflatten_one {n : Fin 1 → ℕ} {α : (i : Fin 1) → Fin (n i) → Sort u_2} {v : (i : Fin 1) → (j : Fin (n i)) → α i j} : hflatten v = v 0

@[simp]

theorem Fin.hflatten_two_eq_append {n : Fin 2 → ℕ} {α : (i : Fin 2) → Fin (n i) → Sort u_2} {v : (i : Fin 2) → (j : Fin (n i)) → α i j} : hflatten v = v 0 ++ʰ v 1

@[simp]

theorem Fin.hflatten_splitSum {m : ℕ} {n : Fin m → ℕ} {α : Fin (vsum n) → Sort u_2} (v : (k : Fin (vsum n)) → α k) (k : Fin (vsum n)) : hflatten (fun (i : Fin m) (j : Fin (n i)) => v (i.embedSum j)) k = cast ⋯ (v k)

@[simp]

theorem Fin.hflatten_embedSum {m : ℕ} {n : Fin m → ℕ} {α : (i : Fin m) → Fin (n i) → Sort u_2} (v : (i : Fin m) → (j : Fin (n i)) → α i j) (i : Fin m) (j : Fin (n i)) : hflatten v (i.embedSum j) = cast ⋯ (v i j)

def Fin.map {n : ℕ} {α : Fin n → Sort u_2} {β : Fin n → Sort u_3} (f : (i : Fin n) → α i → β i) (a : (i : Fin n) → α i) (i : Fin n) : β i

def Fin.range (n : ℕ) : Fin n → ℕ

def Fin.ranges {n : ℕ} (a : Fin n → ℕ) (i : Fin n) : Fin (a i) → ℕ

def Fin.divSum? {m : ℕ} (n : Fin m → ℕ) (k : ℕ) : Option (Fin m)

Find the first index i such that k is smaller than ∑ j < i, a j, and return none otherwise.

This is the dependent version of Fin.divNat.

theorem Fin.divSum?_is_some_iff_lt_sum {m : ℕ} {n : Fin m → ℕ} {k : ℕ} : (divSum? n k).isSome = true ↔ k < ∑ i : Fin m, n i

def Fin.divSum {m : ℕ} {n : Fin m → ℕ} (k : Fin (∑ j : Fin m, n j)) : Fin m

theorem Fin.sum_le_of_divSum?_eq_some {m : ℕ} {n : Fin m → ℕ} {k : Fin (∑ j : Fin m, n j)} {i : Fin m} (hi : divSum? n ↑k = some i) : ∑ j : Fin ↑i, n (castLE ⋯ j) ≤ ↑k

def Fin.modSum {m : ℕ} {n : Fin m → ℕ} (k : Fin (∑ j : Fin m, n j)) : Fin (n k.divSum)

def Fin.finSigmaFinEquiv' {m : ℕ} {n : Fin m → ℕ} : (i : Fin m) × Fin (n i) ≃ Fin (∑ i : Fin m, n i)

Equivalence between (i : Fin m) × Fin (n i) and Fin (∑ i, n i).

Put this as the prime version since it already exists in mathlib (though with a different definition that's not def'eq to this one).

@[simp]

theorem Fin.finSigmaFinEquiv'_apply {m : ℕ} {n : Fin m → ℕ} (k : (i : Fin m) × Fin (n i)) : ↑(finSigmaFinEquiv' k) = ∑ i : Fin ↑k.fst, n (castLE ⋯ i) + ↑k.snd

theorem Fin.finSigmaFinEquiv'_pair {m : ℕ} {n : Fin m → ℕ} (i : Fin m) (k : Fin (n i)) : ↑(finSigmaFinEquiv' ⟨i, k⟩) = ∑ j : Fin ↑i, n (castLE ⋯ j) + ↑k