Defining a [NormedAlgebra ℂ A] for a Matrix

Stream: new members

[Bashar Hamade]

Hello , I need to define a NormedAlgebra for my StateMatrix as defined in this code :

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



def spectral_radius_less_than_one3 [NormedRing A] [NormedAlgebra ℂ A] (a : A) : Prop :=
  spectralRadius ℂ a < 1

abbrev StateVector (n : ℕ) := Fin n → ℝ
abbrev InputVector (p : ℕ) := Fin p → ℝ


abbrev StateMatrix (n : ℕ) := CStarMatrix (Fin n) (Fin n) ℝ
abbrev InputMatrix (n p : ℕ) := Matrix (Fin n) (Fin p) ℝ


noncomputable instance (n : ℕ) : Ring (StateMatrix n) := Matrix.instRing


noncomputable instance (n : ℕ) : SeminormedAddCommGroup (StateMatrix n) := Matrix.seminormedAddCommGroup


noncomputable instance (n : ℕ) : NormedRing (StateMatrix n) := Matrix.frobeniusNormedRing

noncomputable instance (n : ℕ) : NormedAlgebra ℂ (StateMatrix n) := sorry

/--
noncomputable instance (n : ℕ) : NormedAlgebra ℂ (StateMatrix n) := CStarMatrix.instNormedAlgebra

Gives the following error:
type mismatch
  CStarMatrix.instNormedAlgebra
has type
  @NormedAlgebra ℂ (CStarMatrix ?m.3869 ?m.3869 ?m.3865) Complex.instNormedField
    (@NormedRing.toSeminormedRing (CStarMatrix ?m.3869 ?m.3869 ?m.3865)
      CStarMatrix.instNormedRing) : Type (max ?u.3864 ?u.3863)
but is expected to have type
  @NormedAlgebra ℂ (StateMatrix n) Complex.instNormedField
    (@NormedRing.toSeminormedRing (StateMatrix n) (instNormedRingStateMatrix n)) : Type
-/


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

-- System evolution function
def system_evolution {n p : ℕ} (sys : DiscreteLinearSystemState n p) : ℕ → StateVector n
  | 0 => sys.x₀
  | k + 1 => sys.a.mulVec (system_evolution sys k) + sys.B.mulVec (sys.u k)

-- State system equation
def state_system_equation {n p : ℕ} (sys : DiscreteLinearSystemState n p) : Prop :=
  ∀ k : ℕ, sys.x (k + 1) = sys.a.mulVec (sys.x k) + sys.B.mulVec (sys.u k)

-- Now you can use properties that require NormedRing/NormedAlgebra
def system_is_stable {n p : ℕ} (sys : DiscreteLinearSystemState n p) : Prop :=
  spectral_radius_less_than_one3 sys.a

I need to basically make sure everything compiles well and is compatible with the gelfand formula definition,such that the following also compiles :

theorem gelfand_le_one_when_spectral_radius_le_one
    [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] (a : A) :
    spectral_radius_less_than_one3 a →
    Filter.limsup (fun (n : ℕ) => (‖a ^ n‖₊ : ENNReal) ^ (1 / n : ℝ)) Filter.atTop < 1 := by
  intro h_spectral
  unfold spectral_radius_less_than_one3 at h_spectral

  have h_gelfand := spectrum.limsup_pow_nnnorm_pow_one_div_le_spectralRadius a

  convert lt_of_le_of_lt h_gelfand h_spectral

I am trying to use CStarMatrix to get such a NormedAlgebra, but it did not work out completely

[Kevin Buzzard]

Can you edit your post to make this a #mwe ? I clicked on the "View in Lean 4 playground" link on your code and I got a screenful of errors.

[Bashar Hamade]

Kevin Buzzard said:

Can you edit your post to make this a #mwe ? I clicked on the "View in Lean 4 playground" link on your code and I got a screenful of errors.

here is the full working code :

import Mathlib



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



def spectral_radius_less_than_one3 [NormedRing A] [NormedAlgebra ℂ A] (a : A) : Prop :=
  spectralRadius ℂ a < 1




theorem gelfand_le_one_when_spectral_radius_le_one
    [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] (a : A) :
    spectral_radius_less_than_one3 a →
    Filter.limsup (fun (n : ℕ) => (‖a ^ n‖₊ : ENNReal) ^ (1 / n : ℝ)) Filter.atTop < 1 := by
  intro h_spectral
  unfold spectral_radius_less_than_one3 at h_spectral

  have h_gelfand := spectrum.limsup_pow_nnnorm_pow_one_div_le_spectralRadius a

  convert lt_of_le_of_lt h_gelfand h_spectral





abbrev StateVector (n : ℕ) := Fin n → ℝ
abbrev InputVector (p : ℕ) := Fin p → ℝ


abbrev StateMatrix (n : ℕ) := CStarMatrix (Fin n) (Fin n) ℝ
abbrev InputMatrix (n p : ℕ) := Matrix (Fin n) (Fin p) ℝ


noncomputable instance (n : ℕ) : Ring (StateMatrix n) := Matrix.instRing


noncomputable instance (n : ℕ) : SeminormedAddCommGroup (StateMatrix n) := Matrix.seminormedAddCommGroup


noncomputable instance (n : ℕ) : NormedRing (StateMatrix n) := Matrix.frobeniusNormedRing

noncomputable instance (n : ℕ) : NormedAlgebra ℂ (StateMatrix n) := sorry

/--
noncomputable instance (n : ℕ) : NormedAlgebra ℂ (StateMatrix n) := CStarMatrix.instNormedAlgebra

Gives the following error:
type mismatch
  CStarMatrix.instNormedAlgebra
has type
  @NormedAlgebra ℂ (CStarMatrix ?m.3869 ?m.3869 ?m.3865) Complex.instNormedField
    (@NormedRing.toSeminormedRing (CStarMatrix ?m.3869 ?m.3869 ?m.3865)
      CStarMatrix.instNormedRing) : Type (max ?u.3864 ?u.3863)
but is expected to have type
  @NormedAlgebra ℂ (StateMatrix n) Complex.instNormedField
    (@NormedRing.toSeminormedRing (StateMatrix n) (instNormedRingStateMatrix n)) : Type
-/


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

-- System evolution function
def system_evolution {n p : ℕ} (sys : DiscreteLinearSystemState n p) : ℕ → StateVector n
  | 0 => sys.x₀
  | k + 1 => sys.a.mulVec (system_evolution sys k) + sys.B.mulVec (sys.u k)

-- State system equation
def state_system_equation {n p : ℕ} (sys : DiscreteLinearSystemState n p) : Prop :=
  ∀ k : ℕ, sys.x (k + 1) = sys.a.mulVec (sys.x k) + sys.B.mulVec (sys.u k)

-- Now you can use properties that require NormedRing/NormedAlgebra
def system_is_stable {n p : ℕ} (sys : DiscreteLinearSystemState n p) : Prop :=
  spectral_radius_less_than_one3 sys.a

[Kenny Lau]

@Bashar Hamade I specified the implicit arguments:

noncomputable instance (n : ℕ) : NormedAlgebra ℂ (StateMatrix n) := CStarMatrix.instNormedAlgebra (n := Fin n) (A := ℂ)

and then got the error:

failed to synthesize
  PartialOrder ℂ

so that's the reason

[Kenny Lau]

and I'm not familiar with this part of the library to tell you further reason, hopefully others will know

[Eric Wieser]

open scoped ComplexOrder

[Eric Wieser]

But you can't mix and match the frobenius and star and elementwise norm like that

[Eric Wieser]

Which norm do you actually want?