Matrix theorem proof

Stream: maths

[Anirudh Suresh]

image.png
I am facing trouble proving this goal. Is there any tactic that will help me simplify this or is there any approach I can take to solve this?

[Kevin Buzzard]

This question would be much easier to answer if you posted a #mwe rather than a screenshot. Does ext then rw [Matrix.mul_apply] and then ring do something? I can't check because you didn't post a #mwe .

[Eric Wieser]

It looks to me like you're building docs#Matrix.mul_kronecker_mul the hard way?

[Anirudh Suresh]

Kevin Buzzard said:

This question would be much easier to answer if you posted a #mwe rather than a screenshot. Does ext then rw [Matrix.mul_apply] and then ring do something? I can't check because you didn't post a #mwe .

import Mathlib.Data.Vector
import Mathlib.Data.Complex.Basic
import Mathlib.Data.Real.Basic
import Mathlib.Data.Real.Sqrt
import Mathlib.Data.Matrix.Basic
import Mathlib.Data.Complex.Basic
open scoped Matrix
open ComplexConjugate


def tensor_product_2 {m n o p: ℕ} (A : Matrix (Fin m) (Fin n) ℂ) (B : Matrix (Fin o) (Fin p) ℂ) : Matrix (Fin (m*o)) (Fin (n*p)) ℂ :=
  Matrix.of (fun (i:Fin (m*o)) (j:Fin (n*p)) => A (Fin.ofNat' (i.val / o) (by {
    have h : 0 < m * o  := Fin.pos i
    simp [Nat.pos_of_mul_pos_left] at h
    cases h
    assumption
  }))
  (Fin.ofNat' (j.val / p) (by {
    have h : 0 < n*p  := Fin.pos j
    simp [Nat.pos_of_mul_pos_left] at h
    cases h
    assumption
  })) * B (Fin.ofNat' (i.val % o) (by {
    have h : 0 < m * o  := Fin.pos i
    simp [Nat.pos_of_mul_pos_left] at h
    cases h
    assumption
  })) (Fin.ofNat' (j.val % p) (by {
    have h : 0 < n*p  := Fin.pos j
    simp [Nat.pos_of_mul_pos_left] at h
    cases h
    assumption
  })))

infix:1024  "⊗" => tensor_product_2

theorem mul_tensor {m n p q r s : ℕ}
  (A  : Matrix (Fin m) (Fin n) ℂ)
  (A' : Matrix (Fin n) (Fin p) ℂ)
  (B  : Matrix (Fin q) (Fin r) ℂ)
  (B' : Matrix (Fin r) (Fin s) ℂ) :
  (tensor_product_2 A B) * (tensor_product_2 A' B') = tensor_product_2 (A * A') (B * B') :=
by{

}

[Eric Wieser]

You're making things very hard for yourself by using Matrix (Fin (m*o)) (Fin (n*p)) ℂ instead of Matrix (Fin m × Fin o) (Fin n × Fin p) ℂ.

[Eric Wieser]

Even if you're really sure you want the former, you'd have a much better time if you constructed it in terms of the latter, using docs#Matrix.reindex and a Equiv that you should be able to find with Loogle.

[Anirudh Suresh]

Yes but changing the index to tuples makes things really hard for me as well...especially if I would like to do multiple kronecker products which would result in a matrix with nested tuples as indices

[Eric Wieser]

Are you deliberately avoiding docs#Matrix.kronecker for pedagogical reasons ("I want to build some matrix theory from scratch as an exercise"), or just because you're finding the tuple indices inconvenient?

[Anirudh Suresh]

Eric Wieser said:

Are you deliberately avoiding docs#Matrix.kronecker for pedagogical reasons ("I want to build some matrix theory from scratch as an exercise"), or just because you're finding the tuple indices inconvenient?

im finding tuple indices inconvenient

[Eric Wieser]

Eric Wieser said:

Even if you're really sure you want the former, you'd have a much better time if you constructed it in terms of the latter [ docs#Matrix.kronecker ], using docs#Matrix.reindex and a Equiv that you should be able to find with Loogle.

I recommend doing this then

[Anirudh Suresh]

would it not be possible to prove this using my definition of tensor_product?

[Eric Wieser]

Sure, but you'd be redoing lots of work. Your function is a combination of two things already in mathlib. If you rebuild it that way rather than from scratch, you can reuse all the existing proofs about those things.

[Kevin Buzzard]

Your MWE is full of errors for me. If you click on the "view in lean 4 playground" link which Zulip has put on your code, you'll see what I see (I removed the first import because it doesn't exist but this didn't help)

[Eric Wieser]

Replacing Fin.ofNat' with Fin.mk fixes it

[Eric Wieser]

But you want to avoid messing around with / and % completely here

[Eric Wieser]

Eric Wieser said:

and a Equiv that you should be able to find with Loogle.

@Anirudh Suresh, were you able to find this? (I deliberately didn't find it for you to let you practice with Loogle)

[Anirudh Suresh]

Eric Wieser said:

Anirudh Suresh, were you able to find this? (I deliberately didn't find it for you to let you practice with Loogle)

I did find Equiv but how exctly would that make it possible to use the kronecker product defined in lean? It is difficult because kronecker product changes the matrix index type to tuple. Is there a way to avoid this?

[Kevin Buzzard]

Is there a way that you can be persuaded that thinking of matrices as being indexed by an arbitrary finite type is not a scary thing? Every finite type bijects with Fin n for some n and you can use this bijection if you want but it's often just a psychological crutch.

[Kevin Buzzard]

docs#Matrix.kronecker returns matrices indexed by a tuple, but docs#Matrix.submatrix and docs#Matrix.reindex let you change the indexing types, and this enables you to do all the number-theoretic Fin a × Fin b ≃ Fin (a * b) and the matrix-theoretic products completely independently, thus meaning that you only have to deal with one problem at a time.

[Anirudh Suresh]

This makes sense. However, I could not find an Equiv that allows to complete the definition.

import Mathlib.Data.Complex.Basic
import Mathlib.Data.Real.Basic
import Mathlib.Data.Real.Sqrt
import Mathlib.Data.Matrix.Basic
import Mathlib.Data.Complex.Basic
import Mathlib.Data.Matrix.Kronecker
open scoped Matrix
open ComplexConjugate



def tensor_product_2 {m n o p : ℕ} (A : Matrix (Fin m) (Fin n) ℂ)
  (B : Matrix (Fin o) (Fin p) ℂ) : Matrix (Fin (m * o)) (Fin (n * p)) ℂ :=
Matrix.submatrix (Matrix.kronecker A B) (
  Matrix.reindex (

  ) ()
) (Matrix.reindex () ())

[Aaron Liu]

@loogle Fin, Equiv, Prod, HMul.hMul

[loogle]

:search: finProdFinEquiv, Nat.divModEquiv_symm_apply, and 5 more

[Aaron Liu]

It's docs#finProdFinEquiv

[Aaron Liu]

import Mathlib.Data.Complex.Basic
import Mathlib.Data.Matrix.Kronecker

example {m n o p : ℕ} (A : Matrix (Fin m) (Fin n) ℂ) (B : Matrix (Fin o) (Fin p) ℂ) :
    Matrix (Fin (m * o)) (Fin (n * p)) ℂ :=
  (Matrix.kronecker A B).reindex finProdFinEquiv finProdFinEquiv

[Anirudh Suresh]

Thanks this works!