Norm type mismatches for Matrices

Stream: new members

[Bashar Hamade]

Hello, I am working on a bigger proof for a project , and somewhere I got stuck on a smaller proof because I could not apply the triangle inequality due to certain norms not being able to be proven to be definitionally equal.Here is my code :

import Mathlib
open Filter Matrix ENNReal

variable {R : Type*} [NormedField R]
variable {A : Type*}
variable {n : ℕ}

open scoped ComplexOrder

abbrev StateVector (n : ℕ) := Fin n → ℂ
abbrev InputVector (p : ℕ) := Fin p → ℂ
abbrev InputMatrix (n p : ℕ) := CStarMatrix (Fin n) (Fin p) ℂ
abbrev StateMatrix (n : ℕ) := CStarMatrix (Fin n) (Fin n) ℂ

noncomputable instance (n : ℕ) : Ring (StateMatrix n) := CStarMatrix.instRing
noncomputable instance (n : ℕ) : NormedRing (StateMatrix n) := CStarMatrix.instNormedRing
noncomputable instance (n : ℕ) : NormedAlgebra ℂ (StateMatrix n) := by
{
  unfold StateMatrix
  exact CStarMatrix.instNormedAlgebra (n := Fin n) (A := ℂ)
}

structure DiscreteLinearSystemState (n p : ℕ) where
  a : StateMatrix n             -- State transition matrix (n×n)
  B : InputMatrix n p           -- Input matrix (n×p)
  x₀ : StateVector n            -- Initial state
  x : ℕ → StateVector n         -- State sequence
  u : ℕ → InputVector p         -- Input sequence

theorem bound_x_norm
    (n p : ℕ) (sys : DiscreteLinearSystemState n p)
    (hx : ∀ k, sys.x k = (sys.a ^ k) *ᵥ sys.x₀)
     (N : ℕ)


    : ∀ k, N < k → ‖sys.x k‖ ≤ ‖sys.a ^ k‖ * ‖sys.x₀‖ := by
  intro k hk
  -- Use the assumption hx to rewrite sys.x k
  rw [hx k]
  have h_eq := @Matrix.linfty_opNorm_mulVec (Fin n) (Fin n) ℂ _ _ _
        (sys.a ^ k : Matrix (Fin n) (Fin n) ℂ) sys.x₀


  convert h_eq

  sorry

I am stuck at the state goal :
CStarMatrix.instNorm = Matrix.linftyOpSeminormedAddCommGroup.toNorm

[Eric Wieser]

The goal is false

[Eric Wieser]

You can't use docs#Matrix.linfty_opNorm_mulVec here, it's a theorem about a different norm

[Eric Wieser]

You should try to prove

theorem CStarMatrix.norm_mulVec {l m R : Type*} [Fintype l] [Fintype m]
    [NonUnitalCStarAlgebra R] [PartialOrder R] [StarOrderedRing R]
    (A : CStarMatrix l m R) (v : m → R) :
    ‖CStarMatrix.ofMatrix.symm A *ᵥ v‖ ≤ ‖A‖ * ‖v‖ := by
  sorry

[Eric Wieser]

(assuming it's actually true!)

[Bashar Hamade]

Eric Wieser said:

You should try to prove

theorem CStarMatrix.norm_mulVec {l : Type u_2} {m : Type u_3} {R : Type u_5} [Fintype l] [Fintype m]
    [NonUnitalCStarAlgebra R] [PartialOrder R] [StarOrderedRing R]
    (A : CStarMatrix m m R) (v : m → R) :
    ‖CStarMatrix.ofMatrix.symm A *ᵥ v‖ ≤ ‖A‖ * ‖v‖ := by
  sorry

should this be enough ? basically I just don't wanna change all of the types rn because the bigger proof has been relying all along on these types

[Eric Wieser]

You don't need to change anything else

[Eric Wieser]

(also, note I edited my message above to be cleaner)

[Bashar Hamade]

perfect,thank you

[Eric Wieser]

I think there's a good chance this is not true

[Eric Wieser]

I think you need a different norm on v as well

[Eric Wieser]

This one is true:

theorem CStarMatrix.norm_vecMul {l : Type u_2} {m : Type u_3} {R : Type u_5} [Fintype l] [Fintype m]
    [NonUnitalCStarAlgebra R] [PartialOrder R] [StarOrderedRing R]
    (v : l → R)  (A : CStarMatrix l m R) :
    ‖(WithCStarModule.equiv R _).symm (v ᵥ* CStarMatrix.ofMatrix.symm A)‖ ≤ ‖A‖ * ‖(WithCStarModule.equiv R _).symm v‖ := by
  trans ‖A.toCLM ((WithCStarModule.equiv R _).symm v)‖
  · rfl
  · apply ContinuousLinearMap.le_of_opNorm_le
    rfl

[Eric Wieser]

I think the useful version of this statement might be a question for @Jireh Loreaux

[Bashar Hamade]

Eric Wieser said:

This one is true:

theorem CStarMatrix.norm_vecMul {l : Type u_2} {m : Type u_3} {R : Type u_5} [Fintype l] [Fintype m]
    [NonUnitalCStarAlgebra R] [PartialOrder R] [StarOrderedRing R]
    (v : l → R)  (A : CStarMatrix l m R) :
    ‖(WithCStarModule.equiv R _).symm (v ᵥ* CStarMatrix.ofMatrix.symm A)‖ ≤ ‖A‖ * ‖(WithCStarModule.equiv R _).symm v‖ := by
  trans ‖A.toCLM ((WithCStarModule.equiv R _).symm v)‖
  · rfl
  · apply ContinuousLinearMap.le_of_opNorm_le
    rfl

yeah sadly this does not work with the proof

[Eric Wieser]

Your statement of bound_x_norm is wrong

[Eric Wieser]

I think you need StateVector to be of type WithCStarModule ℂ (Fin n → ℂ)

[Eric Wieser]

You should also drop your noncomputable instances, they're at best redundant at at worse will cause problems.

[Eric Wieser]

The reality here is that things would be much easier if you skipped working with matrices at all

[Eric Wieser]

Here's the matrix-free version:

import Mathlib

open scoped ComplexOrder

variable {σ ι : Type*}
variable [NormedAddCommGroup σ] [NormedSpace ℂ σ]
variable [NormedAddCommGroup ι] [NormedSpace ℂ ι]

variable (σ ι) in
structure DiscreteLinearSystemState  where
  /-- State transition matrix (n×n) -/
  a : σ →L[ℂ] σ
  /-- Input matrix (n×p) -/
  B : ι →L[ℂ] σ
  /-- Initial state -/
  x₀ : σ
  /-- State sequence -/
  x : ℕ → σ
  /-- Input sequence -/
  u : ℕ → ι

theorem bound_x_norm
    (sys : DiscreteLinearSystemState σ ι)
    (hx : ∀ k, sys.x k = (sys.a ^ k) sys.x₀) (N : ℕ) :
    ∀ k, N < k → ‖sys.x k‖ ≤ ‖sys.a ^ k‖ * ‖sys.x₀‖ := by
  intro k hk
  -- Use the assumption hx to rewrite sys.x k
  rw [hx k]
  exact ContinuousLinearMap.le_opNorm (sys.a ^ k) sys.x₀

[Bashar Hamade]

the base of my main proof relied on using gelfand's formula, which did not seem to work in any other cases

[Bashar Hamade]

so basically I created all these instances to be able to work with the gelfand formula