Matrices are isomorphic with linear maps between Lp spaces

This file provides a WithLp version of Matrix.toLin'.

def Matrix.toLpLin {m : Type u_1} {n : Type u_2} {R : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] (p q : ENNReal) : Matrix m n R ≃ₗ[R] WithLp p (n → R) →ₗ[R] WithLp q (m → R)

Matrix.toLin' adapted for PiLp R _.

@[simp]

theorem Matrix.toLpLin_toLp {m : Type u_1} {n : Type u_2} {R : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] (p q : ENNReal) (A : Matrix m n R) (x : n → R) : ((toLpLin p q) A) (WithLp.toLp p x) = WithLp.toLp q ((toLin' A) x)

@[simp]

theorem Matrix.ofLp_toLpLin {m : Type u_1} {n : Type u_2} {R : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] (p q : ENNReal) (A : Matrix m n R) (x : WithLp p (n → R)) : (((toLpLin p q) A) x).ofLp = (toLin' A) x.ofLp

theorem Matrix.toLpLin_apply {m : Type u_1} {n : Type u_2} {R : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] (p q : ENNReal) (M : Matrix m n R) (v : WithLp p (n → R)) : ((toLpLin p q) M) v = WithLp.toLp q (M.mulVec v.ofLp)

theorem Matrix.toLpLin_eq_toLin {m : Type u_1} {n : Type u_2} {R : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] (p q : ENNReal) [Finite m] : toLpLin p q = toLin (PiLp.basisFun p R n) (PiLp.basisFun q R m)

@[simp]

theorem Matrix.toLpLin_one {n : Type u_2} {R : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] (p : ENNReal) : (toLpLin p p) 1 = LinearMap.id

theorem Matrix.toLpLin_mul {m : Type u_1} {n : Type u_2} {o : Type u_3} {R : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] (p q r : ENNReal) [Fintype o] [DecidableEq o] (A : Matrix m n R) (B : Matrix n o R) : (toLpLin p r) (A * B) = (toLpLin q r) A ∘ₗ (toLpLin p q) B

Note that applying this theorem needs an explicit choice of q.

@[simp]

theorem Matrix.toLpLin_mul_same {m : Type u_1} {n : Type u_2} {o : Type u_3} {R : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] (p : ENNReal) [Fintype o] [DecidableEq o] (A : Matrix m n R) (B : Matrix n o R) : (toLpLin p p) (A * B) = (toLpLin p p) A ∘ₗ (toLpLin p p) B

A copy of toLpLin_mul that works for simp, for the common case where the domain and codomain have the same norm.

@[simp]

theorem Matrix.toLpLin_symm_id {n : Type u_2} {R : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] (p : ENNReal) : (toLpLin p p).symm LinearMap.id = 1

theorem Matrix.toLpLin_symm_comp {m : Type u_1} {n : Type u_2} {o : Type u_3} {R : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] (p q r : ENNReal) [Fintype o] [DecidableEq o] (A : WithLp q (n → R) →ₗ[R] WithLp r (m → R)) (B : WithLp p (o → R) →ₗ[R] WithLp q (n → R)) : (toLpLin p r).symm (A ∘ₗ B) = (toLpLin q r).symm A * (toLpLin p q).symm B

Note that applying this theorem needs an explicit choice of q.

def Matrix.toLpLinAlgEquiv {n : Type u_2} {R : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] (p : ENNReal) : Matrix n n R ≃ₐ[R] Module.End R (WithLp p (n → R))

Matrix.toLinAlgEquiv' adapted for PiLp R _.

@[simp]

theorem Matrix.toLpLinAlgEquiv_symm_apply {n : Type u_2} {R : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] (p : ENNReal) (a : Module.End R (WithLp p (n → R))) : (toLpLinAlgEquiv p).symm a = (toLpLin p p).symm a

@[simp]

theorem Matrix.toLpLinAlgEquiv_apply_apply_ofLp {n : Type u_2} {R : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] (p : ENNReal) (a : Matrix n n R) (a✝ : WithLp p (n → R)) (a✝¹ : n) : (((toLpLinAlgEquiv p) a) a✝).ofLp a✝¹ = a.mulVec a✝.ofLp a✝¹

@[simp]

theorem Matrix.toLpLin_pow {n : Type u_2} {R : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] (p : ENNReal) (A : Matrix n n R) (k : ℕ) : (toLpLin p p) (A ^ k) = (toLpLin p p) A ^ k

@[simp]

theorem Matrix.toLpLin_symm_pow {n : Type u_2} {R : Type u_4} [Fintype n] [DecidableEq n] [CommRing R] (p : ENNReal) (A : Module.End R (WithLp p (n → R))) (k : ℕ) : (toLpLin p p).symm (A ^ k) = (toLpLin p p).symm A ^ k

@[simp]

theorem LinearMap.det_toLpLin {ι : Type u_5} {R : Type u_6} [Fintype ι] [DecidableEq ι] [CommRing R] (p : ENNReal) (m : Matrix ι ι R) : LinearMap.det ((Matrix.toLpLin p p) m) = m.det