Kronecker Product with 2^n sized Matrix

Stream: new members

[Jake Jongejans]

Hi! I am hitting a wall with this problem: I want to define H^⊗n (so H ⊗ₖ H ⊗ₖ H ⊗ₖ ....... ⊗ₖ H). I'm struggling with the fact that Lean doesn't seem to like working out (Fin (2 ^ (x + 1)) × Fin 2) to (Fin (2 ^ (x + 2))). I don't know how to work this out anymore.

Here is the code I've written (it runs for me, so I believe it is MWE):

import Mathlib.Data.Matrix.Basic
import Mathlib.Data.Matrix.Notation
import Mathlib.Data.Matrix.Kronecker

open Matrix
open Kronecker


@[simp]
def Hadamard : (n : ℕ) -> Matrix (Fin (2 ^ n)) (Fin (2 ^ n)) ℤ
  | 0 => ![![1]]
  | 1 => !![1, 1; 1, -1]
  | (x+2) => (Hadamard (x + 1)) ⊗ₖ !![1, 1; 1, -1]

I also have a second question that pertains similar content. I want to prove that H * H = 2 (given how they are non-normal). This works when using !![1, 1; 1, -1] but not with a matrix made from a function. Note that part of the code in the MWE is copied from a merged PR that isn't released yet.

import Mathlib.Data.Matrix.Basic
import Mathlib.Data.Matrix.Notation
import Mathlib.Data.Matrix.Kronecker


-- This code is merged in the mathlib4 PR #10592, but it is not yet released.

import Mathlib.Data.Matrix.Notation

open Matrix

section AddMonoidWithOne
 variable [AddMonoidWithOne α]

 theorem natCast_fin_two (n : ℕ) : (n : Matrix (Fin 2) (Fin 2) α) = !![↑n, 0; 0, ↑n] := by
   ext i j
   fin_cases i <;> fin_cases j <;> rfl

 -- See note [no_index around OfNat.ofNat]
 theorem ofNat_fin_two (n : ℕ) [n.AtLeastTwo] :
     (no_index (OfNat.ofNat n) : Matrix (Fin 2) (Fin 2) α) =
       !![OfNat.ofNat n, 0; 0, OfNat.ofNat n] :=
   natCast_fin_two _

 end AddMonoidWithOne

 -- End of the merged code


open Matrix
open Kronecker


@[simp]
def Hadamard : Matrix (Fin 2) (Fin 2) ℤ :=
  of (λ x y => (-1) ^ (x.val * y.val))
  -- !![1, 1; 1, -1]  -- WORKS


theorem HH : Hadamard * Hadamard = 2 :=
  by
    simp [mul_apply]
    rw [ofNat_fin_two]
    norm_num

Any help would be much appreciated <3

[Gareth Ma]

Isn't $\mathbb{Z}_{2^x} \times \mathbb{Z}_2 \cong \mathbb{Z}_{2^{x+1}}$ instead?

[Jake Jongejans]

Gareth Ma said:

Isn't $\mathbb{Z}_{2^x} \times \mathbb{Z}_2 \cong \mathbb{Z}_{2^{x+1}}$ instead?

Yes, I messed up the last line of my MWE when copying it over and cleaning it up. I will edit my initial message.

[Junyan Xu]

You'll need to use docs#Matrix.reindex with docs#finProdFinEquiv.

[Jake Jongejans]

I see, those are very helpful pointers. I sadly am not versed enough with Lean to know how to apply these to a definition. Would it be possible to help me on my way a bit more?

[Junyan Xu]

This works:

def Hadamard : (n : ℕ) -> Matrix (Fin (2 ^ n)) (Fin (2 ^ n)) ℤ
  | 0 => ![![1]]
  | (n + 1) => Matrix.reindex finProdFinEquiv finProdFinEquiv (Hadamard n ⊗ₖ !![1, 1; 1, -1])

[Eric Wieser]

(I think #10592 is "released" now, for all reasonable senses of the word)

[Eric Wieser]

I think this hadarmard matrix stuff came up on the zulip a few years ago; you might want to search the history for more ideas

[Jake Jongejans]

Thank you, @Junyan Xu for the working code. This works (at least when #eval'ing) :)
Using this to e.g. prove Hadamard * Hadamard = 2 is giving me a lot of trouble with kroneckerMap, submatrix and finProdFinEquivs (see code below). Any idea how I could try solve this issue?

import Mathlib.Data.Matrix.Basic
import Mathlib.Data.Matrix.Notation
import Mathlib.Data.Matrix.Kronecker

open Matrix
open Kronecker

@[simp]
def Hadamard : (n : ℕ) -> Matrix (Fin (2 ^ n)) (Fin (2 ^ n)) ℤ
  | 0 => 1
  | (n + 1) => reindex finProdFinEquiv finProdFinEquiv (Hadamard n ⊗ₖ !![1, 1; 1, -1])

theorem HxH : Hadamard 1 * Hadamard 1 = 2 :=
  by
    simp [Hadamard]
    norm_num

@Eric Wieser Thanks! I'll have to check that out, I am on lean stable. I'll see it pop into existence at some point.

[Eric Wieser]

I don't think lean stable exists any more

[Eric Wieser]

You should pick a lean-4.x.0 if you want stability, but if you're using mathlib it's probably best to just be on the bleeding edge

[Patrick Massot]

Mathlib is not on the bleeding edge, it’s on release candidates.

[Jake Jongejans]

I'll check GitHub for what is used for newest code, thanks for the heads-ups!

[Junyan Xu]

theorem HxH : Hadamard 1 * Hadamard 1 = 2 := by decide works here.

[Eric Wieser]

Patrick Massot said:

Mathlib is not on the bleeding edge, it’s on release candidates.

Sorry, what I meant is 'use the bleeding edge of mathlib, don't pick a lean version'