Binary Tower Fin Helpers

Finite-index helper lemmas for bit manipulations used in binary tower proofs.

@[simp]

theorem bit_finProdFinEquiv_symm_2_pow_succ {n : ℕ} (j : Fin (2 ^ (n + 1))) (i : Fin (n + 1)) : have e := finProdFinEquiv.symm; (↑i).getBit ↑j = if ↑i > 0 then (↑i - 1).getBit ↑(e j).1 else ↑(e j).2

def leftDivNat {m n : ℕ} (i : Fin (m * n)) : Fin n

Equivalence between Fin m × Fin n and Fin (m * n) which splits quotient part into Fin (n) and the remainder into Fin (m). If m and n are powers of 2, the Fin (n) holds MSBs and Fin (m) holds LSBs. This is a reversed version of finProdFinEquiv. We put m before n for integration with Basis.smulTower in multilinearBasis though it's a bit counter-intuitive.

def leftModNat {m n : ℕ} (h_m : m > 0) (i : Fin (m * n)) : Fin m

def revFinProdFinEquiv {m n : ℕ} (h_m : m > 0) : Fin m × Fin n ≃ Fin (m * n)

@[simp]

theorem revFinProdFinEquiv_symm_apply {m n : ℕ} (h_m : m > 0) (x : Fin (m * n)) : (revFinProdFinEquiv h_m).symm x = (leftModNat h_m x, leftDivNat x)

@[simp]

theorem revFinProdFinEquiv_apply_val {m n : ℕ} (h_m : m > 0) (x : Fin m × Fin n) : ↑((revFinProdFinEquiv h_m) x) = ↑x.1 + m * ↑x.2

@[simp]

theorem bit_revFinProdFinEquiv_symm_2_pow_succ {n : ℕ} (j : Fin (2 ^ (n + 1))) (i : Fin (n + 1)) : have e := (revFinProdFinEquiv ⋯).symm; have msb := (e j).2; have lsbs := (e j).1; (↑i).getBit ↑j = if ↑i < n then (↑i).getBit ↑lsbs else ↑msb