Nonlinear dynamical systems & control theory

4.2. Causality🔗

We have two definitions for causal maps: one for relations and one for functions:

🔗structure
SetRel.IsCausal.{u_1, u_2, u_3, u_4} {ι : Type u_1} {α : Type u_2}
  {E : Type u_3} {F : Type u_4} [MeasurableSpace α]
  [NormedAddCommGroup E] [NormedAddCommGroup F] [PseudoMetricSpace α]
  (R : SetRel (α → E) (α → F)) (s : ι → Set α) (p : ENNReal)
  (μ : MeasureTheory.Measure α := by volume_tac) : Prop
SetRel.IsCausal.{u_1, u_2, u_3, u_4}
  {ι : Type u_1} {α : Type u_2}
  {E : Type u_3} {F : Type u_4}
  [MeasurableSpace α]
  [NormedAddCommGroup E]
  [NormedAddCommGroup F]
  [PseudoMetricSpace α]
  (R : SetRel (α → E) (α → F))
  (s : ι → Set α) (p : ENNReal)
  (μ : MeasureTheory.Measure α := by
    volume_tac) :
  Prop

A relation is causal if uₜ = u'ₜ implies yₜ = y'ₜ for (u, y) ∈ R and (u', y') ∈ R.

Constructor

SetRel.IsCausal.mk.{u_1, u_2, u_3, u_4}

Fields

memLpLoc : ∀ ⦃u : α → E⦄ ⦃y : α → F⦄, (u, y) ∈ R → MeasureTheory.MemLpLoc u p μ → MeasureTheory.MemLpLoc y p μ

The relation R maps local Lp functions to local Lp functions

causal : ∀ (t : ι) ⦃u : α → E⦄ ⦃y : α → F⦄ ⦃u' : α → E⦄ ⦃y' : α → F⦄,
  (u, y) ∈ R →
    (u', y') ∈ R →
      MeasureTheory.MemLpLoc u p μ →
        MeasureTheory.MemLpLoc y p μ →
          MeasureTheory.MemLpLoc u' p μ →
            MeasureTheory.MemLpLoc y' p μ →
              (s t).indicator u = (s t).indicator u' → (s t).indicator y = (s t).indicator y'

If (u, y) ∈ R and (u', y') ∈ R, then uₜ = u'ₜ implies that yₜ = y'ₜ.

🔗structure
Function.IsCausal.{u_1, u_2, u_3, u_4} {ι : Type u_1} {α : Type u_2}
  {E : Type u_3} {F : Type u_4} [MeasurableSpace α]
  [NormedAddCommGroup E] [NormedAddCommGroup F] [PseudoMetricSpace α]
  (f : (α → E) → α → F) (s : ι → Set α) (p : ENNReal)
  (μ : MeasureTheory.Measure α := by volume_tac) : Prop
Function.IsCausal.{u_1, u_2, u_3, u_4}
  {ι : Type u_1} {α : Type u_2}
  {E : Type u_3} {F : Type u_4}
  [MeasurableSpace α]
  [NormedAddCommGroup E]
  [NormedAddCommGroup F]
  [PseudoMetricSpace α]
  (f : (α → E) → α → F) (s : ι → Set α)
  (p : ENNReal)
  (μ : MeasureTheory.Measure α := by
    volume_tac) :
  Prop

A (nonlinear) operator f is called causal if it maps local Lp functions to local Lp functions and if (f u)_t is equal to (f u_t)_t where u_t denotes the restriction of u to s t.

The traditional definition of causality uses α := ℝ≥0 and s := Set.Ici.

Constructor

Function.IsCausal.mk.{u_1, u_2, u_3, u_4}

Fields

memLpLoc : ∀ ⦃u : α → E⦄, MeasureTheory.MemLpLoc u p μ → MeasureTheory.MemLpLoc (f u) p μ

The operator f maps local Lp functions to local Lp functions

causal : ∀ (t : ι) (u : α → E), MeasureTheory.MemLpLoc u p μ → (s t).indicator (f ((s t).indicator u)) = (s t).indicator (f u)

For each t and locally Lp u, we have that (f uₜ)ₜ = (f u)ₜ.

and if a relation is induced by a function, then these definitions agree:

🔗theorem
Function.graph_isCausal_iff_isCausal.{u_1, u_2, u_3, u_4} {ι : Type u_1}
  {α : Type u_2} {E : Type u_3} {F : Type u_4} [MeasurableSpace α]
  [NormedAddCommGroup E] [NormedAddCommGroup F] [PseudoMetricSpace α]
  {f : (α → E) → α → F} {s : ι → Set α} {p : ENNReal}
  {μ : MeasureTheory.Measure α} (hs : ∀ (t : ι), MeasurableSet (s t)) :
  (Function.graph f).IsCausal s p μ ↔ Function.IsCausal f s p μ
Function.graph_isCausal_iff_isCausal.{u_1,
    u_2, u_3, u_4}
  {ι : Type u_1} {α : Type u_2}
  {E : Type u_3} {F : Type u_4}
  [MeasurableSpace α]
  [NormedAddCommGroup E]
  [NormedAddCommGroup F]
  [PseudoMetricSpace α]
  {f : (α → E) → α → F} {s : ι → Set α}
  {p : ENNReal}
  {μ : MeasureTheory.Measure α}
  (hs : ∀ (t : ι), MeasurableSet (s t)) :
  (Function.graph f).IsCausal s p μ ↔
    Function.IsCausal f s p μ

The graph of a function is causal if and only if the function is causal.