More lemmas about Fin and big operators

theorem mul_two_add_bit_lt_two_pow (a b c : ℕ) (i : Fin 2) (h_a : a < 2 ^ b) (h_b : b < c) : a * 2 + ↑i < 2 ^ c

theorem div_two_pow_lt_two_pow (x i j : ℕ) (h_x_lt_2_pow_i : x < 2 ^ (i + j)) : x / 2 ^ j < 2 ^ i

theorem lt_two_pow_of_lt_two_pow_exp_le (x i j : ℕ) (h_x_lt_2_pow_i : x < 2 ^ i) (h_i_le_j : i ≤ j) : x < 2 ^ j

theorem Fin.val_add_one' {r : ℕ} [NeZero r] (a : Fin r) (h_a_add_1 : ↑a + 1 < r) : ↑(a + 1) = ↑a + 1

@[simp]

theorem Fin.cast_val_eq_val {n m : ℕ} [NeZero n] (a : Fin n) (h_eq : n = m) : ↑(Fin.cast h_eq a) = ↑a

theorem Fin.val_sub_one {r : ℕ} [NeZero r] (a : Fin r) (h_a_sub_1 : a > 0) : ↑(a - 1) = ↑a - 1

theorem Fin.lt_iff_le_pred {r : ℕ} [NeZero r] (a b : Fin r) (h_b : b > 0) : a < b ↔ a ≤ b - 1

theorem Fin.le_iff_lt_succ {r : ℕ} [NeZero r] (a b : Fin r) (h_b : ↑b + 1 < r) : a ≤ b ↔ a < b + 1

theorem Fin.lt_succ' {r : ℕ} [NeZero r] (a : Fin r) (h_a_add_1 : ↑a + 1 < r) : a < a + 1

theorem Fin.le_succ {r : ℕ} [NeZero r] (a : Fin r) (h_a_add_1 : ↑a + 1 < r) : a ≤ a + 1

@[irreducible]

def Fin.succRecOnSameFinType {r : ℕ} [NeZero r] {motive : Fin r → Prop} (zero : motive 0) (succ : ∀ (i : Fin r), ↑i + 1 < r → motive i → motive (i + 1)) (i : Fin r) : motive i

Recursion principle for Fin r that iterates upwards from 0. This is useful when the type Fin r is fixed and we want to induct on the element. It's similar to Fin.inductionOn, but formulated with an explicit upper bound check.

@[irreducible]

def Fin.predRecOnSameFinType {r : ℕ} [NeZero r] {motive : Fin r → Sort u_1} (last : motive ⟨r - 1, ⋯⟩) (succ : (i : Fin r) → ↑i > 0 → motive i → motive ⟨↑i - 1, ⋯⟩) (i : Fin r) : motive i

Recursion principle for Fin r that iterates downwards from r - 1. This is useful for definitions that process elements in reverse order, like foldr.

theorem Fin.sum_univ_odd_even {n : ℕ} {M : Type u_1} [AddCommMonoid M] (f : ℕ → M) : ∑ i : Fin (2 ^ n), f (2 * ↑i) + ∑ i : Fin (2 ^ n), f (2 * ↑i + 1) = ∑ i : Fin (2 ^ (n + 1)), f ↑i

Splits a sum over Fin (2^n) into a sum over even indices and a sum over odd indices. Useful for Fast Fourier Transform (FFT) type recursions.

theorem sum_Icc_split {α : Type u_1} [AddCommMonoid α] (f : ℕ → α) (a b c : ℕ) (h₁ : a ≤ b) (h₂ : b ≤ c) : ∑ i ∈ Finset.Icc a c, f i = ∑ i ∈ Finset.Icc a b, f i + ∑ i ∈ Finset.Icc (b + 1) c, f i

Splits a sum over an interval [a, c] into two sums over [a, b] and [b+1, c]. Requires a ≤ b ≤ c.

def equivFinFunSplitLast {F : Type u_1} [Fintype F] [Nonempty F] {ϑ : ℕ} : (Fin (ϑ + 1) → F) ≃ F × (Fin ϑ → F)