matrix about smul

Stream: new members

[Hbz]

import Mathlib

open Matrix

theorem eigenvectors_linear_independent {k : Type*} [Field k]
    {n : ℕ} (A : Matrix (Fin n) (Fin n) k)
    {m : ℕ} (f : Fin m → k) (v : Fin m → Fin n → k)
    (distinct : ∀ i j, i ≠ j → f i ≠ f j)
    (eigen : ∀ i, A.mulVec (v i) = f i • v i)
    (nonzero : ∀ i, v i ≠ 0) :
    LinearIndependent k (v : Fin m → (Fin n → k)) := by
  rw[linearIndependent_iff']
  intro s g h
  induction' m with d hd
  · simp
  ·
    intro i
    intro hi
    specialize eigen i
    have h1 : ∑ i, f i • g i • v i = 0 := by
      have h10 : A.mulVec (g i • v i) = g i • (A.mulVec (v i)) := by exact Matrix.mulVec_smul A (g i) (v i)
      have hh1 : A.mulVec (g i • v i) = f i • g i • v i := by
        rw[h10]
        rw[eigen]
        exact smul_comm (g i) (f i) (v i)
      have h11 : A.mulVec (∑ i, g i • v i) = ∑ i, A.mulVec (g i • v i):= by
        sorry
      sorry
    sorry
#check map_sum

I don't know how to complete the proof of \( A.mulVec \left( \sum_i g_i \cdot v_i \right) = \sum_i A.mulVec \left( g_i \cdot v_i \right) \). Should I use additive group homomorphisms? (I'm not really sure how to use them.) Or is there another method?

[Kenny Lau]

can you minimize it to be one lemma with sorry?

[Kenny Lau]

#mwe

[Eric Wieser]

I have an open PR, #28130, with a missing lemma about mulVec and smul

[Hbz]

Kenny Lau said:

can you minimize it to be one lemma with sorry?

lemma mulVec_sum {k : Type*} [Field k] {n : ℕ} {m : ℕ} (A : Matrix (Fin n) (Fin n) k)
  (g : Fin m → k) (v : Fin m → Fin n → k):
  A.mulVec (∑ i, g i • v i) = ∑ i, A.mulVec (g i • v i) := by
  sorry

[Aaron Liu]

import Mathlib

lemma mulVec_sum {k : Type*} [Field k] {n : ℕ} {m : ℕ} (A : Matrix (Fin n) (Fin n) k)
    (g : Fin m → k) (v : Fin m → Fin n → k):
    A.mulVec (∑ i, g i • v i) = ∑ i, A.mulVec (g i • v i) := by
  rw [← Matrix.coe_mulVecLin, map_sum]

[Aaron Liu]

the trick is to convert it to a linear map, which distributes over sums

[Hbz]

Ah, right! I remember now. I always forget that in Lean 4, matrix operations should be converted to linear map operations. Thank you very much! :+1:

[Eric Wieser]

This lemma (after sufficient generalization) should probably be in mathlib

[Wuyang]

turning mulVec into a linear map makes it much easier to apply map_sum.
You can also explore similar lemmas in LeanFinder (www.leanfinder.org).

[Wuyang]

(deleted)

[leanfinder]

Failure! Bot is unavailable

[Wuyang]

@leanfinder Lean 4 proof that mulVec distributes over sums by converting to linear map and using map_sum

[leanfinder]

Here’s what I found:

• For any $m \times n$ matrix $A$ over a type $\alpha$ (where $n$ is finite) and any two vectors $x, y : n \to \alpha$, the matrix-vector multiplication is additive in the vector argument: $A *ᵥ (x + y) = A *ᵥ x + A *ᵥ y$ where $*ᵥ$ denotes matrix-vector multiplication. (score: 0.734)

• For any $m \times n$ matrix $A$ over a type $\alpha$ (where $n$ is finite) and any two vectors $x, y : n \to \alpha$, the matrix-vector multiplication is additive in the vector argument: $A *ᵥ (x + y) = A *ᵥ x + A *ᵥ y$ where $*ᵥ$ denotes matrix-vector multiplication. (score: 0.731)

• Let $ι$ be a type, $t$ be a finite subset of $ι$, and $f : ι \to \text{Hom}_σ(M, M₂)$ be a family of semilinear maps between $R$-module $M$ and $S$-module $M₂$ with respect to a ring homomorphism $σ : R \to S$. Then for any $b \in M$, the evaluation of the sum of these maps at $b$ equals the sum of their evaluations at $b$, i.e., \[ \left(\sum_{d \in t} f_d\right)(b) = \sum_{d \in t} f_d(b). \] (score: 0.728)

• Let $m$ be a finite index type, $A$ be an $m \times n$ matrix over a type $\alpha$, and $x, y$ be vectors in $m \to \alpha$. Then the vector-matrix multiplication satisfies the linearity property $(x + y) \ ᵥ* \ A = x \ ᵥ* \ A + y \ ᵥ* \ A$. (score: 0.720)

• For any finite type $n$ and matrices $M, N \in \text{Matrix}(m \times n, R)$ over a commutative ring $R$, the linear map associated with the sum of $M$ and $N$ is equal to the sum of the linear maps associated with $M$ and $N$ individually. That is, $\text{mulVecLin}(M + N) = \text{mulVecLin}(M) + \text{mulVecLin}(N)$. (score: 0.720)

• Let $M$, $N$, and $P$ be modules over rings with semilinear structures given by ring homomorphisms $\rho_{12} \colon R \to R_2$ and $\sigma_{12} \colon S \to S_2$. For any bilinear map $f \colon M \to_{[\rho_{12}]} N \to_{[\sigma_{12}]} P$, any finite index set $\iota$, any function $x \colon \iota \to M$, and any element $y \in N$, the following equality holds: \[ f\left(\sum_{i \in t} x_i\right) y = \sum_{i \in t} f(x_i) y. \] (score: 0.716)

• For any matrix $A$ of size $m \times n$ over a type $\alpha$ (where $m$ is finite) and any two vectors $x, y : m \to \alpha$, the vector-matrix multiplication is additive in the vector argument: $(x + y) \cdot A = x \cdot A + y \cdot A$ where $\cdot$ denotes vector-matrix multiplication. (score: 0.714)

• For any finite index type $m$, matrices $A, B : \text{Matrix } m \ n \ \alpha$, and vector $x : m \to \alpha$, the vector-matrix multiplication satisfies: $x \ ᵥ* (A + B) = x \ ᵥ* A + x \ ᵥ* B$ where $\ ᵥ*$ denotes the vector-matrix multiplication operation. (score: 0.712)

• For any finite index type $m$, matrices $A, B : \text{Matrix } m \ n \ \alpha$, and vector $x : m \to \alpha$, the vector-matrix multiplication satisfies: $x \ ᵥ* (A + B) = x \ ᵥ* A + x \ ᵥ* B$ where $\ ᵥ*$ denotes the vector-matrix multiplication operation. (score: 0.710)

• Let $t$ be a finitely supported function from $\iota$ to $\gamma$, and let $g$ be a family of $\sigma_{12}$-semilinear maps from $M$ to $M_2$ indexed by $\iota \times \gamma$. For any $b \in M$, the application of the sum $\sum_{i \in \iota} g(i, t(i))$ to $b$ equals the sum $\sum_{i \in \iota} g(i, t(i))(b)$. (score: 0.709)