Integral feedback and perfect adaptation
Integral Feedback
StructureSingle-input single-output linear time-invariant system#✓fully proved
A single-input single-output linear time-invariant system ẋ = A x + u b,
y = c ⬝ x + d u with state space n → ℝ.
structure LinearSystem (n : Type*) where
/-- The state matrix. -/
A : Matrix n n ℝ
/-- The input vector. -/
b : n → ℝ
/-- The output functional. -/
c : n → ℝ
/-- The direct feedthrough from input to output. -/
d : ℝUsed by 11
Linear System
DefinitionVector field of a linear time-invariant system#✓fully proved
The vector field A x + u b at state x and input u.
def field (x : n → ℝ) (u : ℝ) : n → ℝ :=
S.A *ᵥ x + u • S.bUses 1 · Used by 7
DefinitionOutput of a linear time-invariant system#✓fully proved
The output c ⬝ x + d u, measured from its adapted value.
def output (x : n → ℝ) (u : ℝ) : ℝ :=
S.c ⬝ᵥ x + S.d * uUses 1 · Used by 7
DefinitionPerfect adaptation#✓fully proved
For every constant input u, the output vanishes at every
equilibrium.
def HasPerfectAdaptation : Prop :=
∀ (u : ℝ) (x : n → ℝ), S.field x u = 0 → S.output x u = 0Uses 3 · Used by 3
DefinitionIntegral feedback#✓fully proved
A linear functional z = k ⬝ x of the state integrates the output,
ż = k ⬝ (A x + u b) = y, for every state and input.
def HasIntegralFeedback : Prop :=
∃ k : n → ℝ, ∀ (x : n → ℝ) (u : ℝ), k ⬝ᵥ S.field x u = S.output x uDefinitionSteady-state (DC) gain of a linear system#✓fully proved
The steady-state (DC) gain d - c ⬝ A⁻¹ b; for nonsingular A the output at the
equilibrium for input u is dcGain * u.
noncomputable def dcGain [DecidableEq n] : ℝ :=
S.d - S.c ⬝ᵥ (S.A⁻¹ *ᵥ S.b)Uses 1 · Used by 3
TheoremIntegral feedback implies perfect adaptation#✓fully proved
Integral feedback implies perfect adaptation.
theorem hasPerfectAdaptation_of_hasIntegralFeedback (h : S.HasIntegralFeedback) :
S.HasPerfectAdaptationUses 5 · Used by 1
TheoremUnique equilibrium of a nonsingular linear system#✓fully proved
For nonsingular A, the unique equilibrium for input u is x = -u • A⁻¹ b.
theorem field_eq_zero_iff [DecidableEq n] (hA : IsUnit S.A.det) (x : n → ℝ) (u : ℝ) :
S.field x u = 0 ↔ x = -(u • (S.A⁻¹ *ᵥ S.b))Uses 2 · Used by 1
TheoremOutput at equilibrium equals DC gain times input#✓fully proved
For nonsingular A, the output at the equilibrium for input u is dcGain * u.
theorem output_equilibrium [DecidableEq n] (u : ℝ) :
S.output (-(u • (S.A⁻¹ *ᵥ S.b))) u = S.dcGain * uUses 3 · Used by 1
TheoremPerfect adaptation iff the DC gain vanishes#✓fully proved
For nonsingular A, perfect adaptation holds iff the steady-state gain vanishes.
theorem hasPerfectAdaptation_iff_dcGain_eq_zero [DecidableEq n] (hA : IsUnit S.A.det) :
S.HasPerfectAdaptation ↔ S.dcGain = 0Uses 7 · Used by 1
TheoremIntegral feedback is necessary#✓fully proved
Integral feedback is necessary (linear systems with nonsingular A): perfect
adaptation holds iff some linear functional of the state integrates the output; one such
functional is k = c A⁻¹.
theorem hasIntegralFeedback_iff_hasPerfectAdaptation [DecidableEq n] (hA : IsUnit S.A.det) :
S.HasIntegralFeedback ↔ S.HasPerfectAdaptationUses 8
TheoremIntegral-feedback functional is the time integral of the output#✓fully proved
Along a trajectory ẋ(t) = A x(t) + u(t) b, the functional k ⬝ x(t) of an
integral-feedback system has derivative y(t) = c ⬝ x(t) + d u(t): it is the time integral of
the output.
theorem hasDerivAt_integral {k : n → ℝ} (hk : ∀ x u, k ⬝ᵥ S.field x u = S.output x u)
{x : ℝ → n → ℝ} {u : ℝ → ℝ} {t : ℝ} (hx : HasDerivAt x (S.field (x t) (u t)) t) :
HasDerivAt (fun s ↦ k ⬝ᵥ x s) (S.output (x t) (u t)) tIntegral Feedback
TheoremIntegral feedback gives robust perfect adaptation#✓fully proved
Integral feedback gives robust perfect adaptation (nonlinear form). Let F p be the
vector field and y p the output of a system with parameters p, and let z be a
differentiable state function with derivative z' x satisfying
z' x (F p x) = y p x for all p, x (so ż = y along every trajectory, for
every parameter). Then the output vanishes at every equilibrium of every F p.
theorem output_eq_zero_of_integral_feedback {P E : Type*} [NormedAddCommGroup E]
[NormedSpace ℝ E] (F : P → E → E) (y : P → E → ℝ) (z : E → ℝ) (z' : E → E →L[ℝ] ℝ)
(h : ∀ p x, z' x (F p x) = y p x) (_hz : ∀ x, HasFDerivAt z (z' x) x)
{p : P} {x : E} (hx : F p x = 0) : y p x = 0Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.