Theory MTX_Flows
section ‹ Affine systems of ODEs ›
text ‹Affine systems of ordinary differential equations (ODEs) are those whose vector
fields are linear operators. Broadly speaking, if there are functions $A$ and $B$ such that the
system of ODEs $X'\, t = f\, (X\, t)$ turns into $X'\, t = (A\, t)\cdot (X\, t)+(B\, t)$, then it
is affine. The end goal of this section is to prove that every affine system of ODEs has a unique
solution, and to obtain a characterization of said solution. ›
theory MTX_Flows
imports
SQ_MTX
Hybrid_Systems_VCs.HS_ODEs
begin
subsection ‹ Existence and uniqueness for affine systems ›
definition matrix_continuous_on :: "real set ⇒ (real ⇒ ('a::real_normed_algebra_1)^'n^'m) ⇒ bool"
where "matrix_continuous_on T A = (∀t ∈ T. ∀ε > 0. ∃ δ > 0. ∀τ∈T. ¦τ - t¦ < δ ⟶ ∥A τ - A t∥⇩o⇩p ≤ ε)"
lemma continuous_on_matrix_vector_multl:
assumes "matrix_continuous_on T A"
shows "continuous_on T (λt. A t *v s)"
proof(rule continuous_onI, simp add: dist_norm)
fix e t::real assume "0 < e" and "t ∈ T"
let ?ε = "e/(∥(if s = 0 then 1 else s)∥)"
have "?ε > 0"
using ‹0 < e› by simp
then obtain δ where dHyp: "δ > 0 ∧ (∀τ∈T. ¦τ - t¦ < δ ⟶ ∥A τ - A t∥⇩o⇩p ≤ ?ε)"
using assms ‹t ∈ T› unfolding dist_norm matrix_continuous_on_def by fastforce
{fix τ assume "τ ∈ T" and "¦τ - t¦ < δ"
have obs: "?ε * (∥s∥) = (if s = 0 then 0 else e)"
by auto
have "∥A τ *v s - A t *v s∥ = ∥(A τ - A t) *v s∥"
by (simp add: matrix_vector_mult_diff_rdistrib)
also have "... ≤ (∥A τ - A t∥⇩o⇩p) * (∥s∥)"
using norm_matrix_le_mult_op_norm by blast
also have "... ≤ ?ε * (∥s∥)"
using dHyp ‹τ ∈ T› ‹¦τ - t¦ < δ› mult_right_mono norm_ge_zero by blast
finally have "∥A τ *v s - A t *v s∥ ≤ e"
by (subst (asm) obs) (metis (mono_tags) ‹0 < e› less_eq_real_def order_trans)}
thus "∃d>0. ∀τ∈T. ¦τ - t¦ < d ⟶ ∥A τ *v s - A t *v s∥ ≤ e"
using dHyp by blast
qed
lemma lipschitz_cond_affine:
fixes A :: "real ⇒ 'a::real_normed_algebra_1^'n^'m" and T::"real set"
defines "L ≡ Sup {∥A t∥⇩o⇩p |t. t ∈ T}"
assumes "t ∈ T" and "bdd_above {∥A t∥⇩o⇩p |t. t ∈ T}"
shows "∥A t *v x - A t *v y∥ ≤ L * (∥x - y∥)"
proof-
have obs: "∥A t∥⇩o⇩p ≤ Sup {∥A t∥⇩o⇩p |t. t ∈ T}"
apply(rule cSup_upper)
using continuous_on_subset assms by (auto simp: dist_norm)
have "∥A t *v x - A t *v y∥ = ∥A t *v (x - y)∥"
by (simp add: matrix_vector_mult_diff_distrib)
also have "... ≤ (∥A t∥⇩o⇩p) * (∥x - y∥)"
using norm_matrix_le_mult_op_norm by blast
also have "... ≤ Sup {∥A t∥⇩o⇩p |t. t ∈ T} * (∥x - y∥)"
using obs mult_right_mono norm_ge_zero by blast
finally show "∥A t *v x - A t *v y∥ ≤ L * (∥x - y∥)"
unfolding assms .
qed
lemma local_lipschitz_affine:
fixes A :: "real ⇒ 'a::real_normed_algebra_1^'n^'m"
assumes "open T" and "open S"
and Ahyp: "⋀τ ε. ε > 0 ⟹ τ ∈ T ⟹ cball τ ε ⊆ T ⟹ bdd_above {∥A t∥⇩o⇩p |t. t ∈ cball τ ε}"
shows "local_lipschitz T S (λt s. A t *v s + B t)"
proof(unfold local_lipschitz_def lipschitz_on_def, clarsimp)
fix s t assume "s ∈ S" and "t ∈ T"
then obtain e1 e2 where "cball t e1 ⊆ T" and "cball s e2 ⊆ S" and "min e1 e2 > 0"
using open_cballE[OF _ ‹open T›] open_cballE[OF _ ‹open S›] by force
hence obs: "cball t (min e1 e2) ⊆ T"
by auto
let ?L = "Sup {∥A τ∥⇩o⇩p |τ. τ ∈ cball t (min e1 e2)}"
have "∥A t∥⇩o⇩p ∈ {∥A τ∥⇩o⇩p |τ. τ ∈ cball t (min e1 e2)}"
using ‹min e1 e2 > 0› by auto
moreover have bdd: "bdd_above {∥A τ∥⇩o⇩p |τ. τ ∈ cball t (min e1 e2)}"
by (rule Ahyp, simp only: ‹min e1 e2 > 0›, simp_all add: ‹t ∈ T› obs)
moreover have "Sup {∥A τ∥⇩o⇩p |τ. τ ∈ cball t (min e1 e2)} ≥ 0"
apply(rule order.trans[OF op_norm_ge_0[of "A t"]])
by (rule cSup_upper[OF calculation])
moreover have "∀x∈cball s (min e1 e2) ∩ S. ∀y∈cball s (min e1 e2) ∩ S.
∀τ∈cball t (min e1 e2) ∩ T. dist (A τ *v x) (A τ *v y) ≤ ?L * dist x y"
apply(clarify, simp only: dist_norm, rule lipschitz_cond_affine)
using ‹min e1 e2 > 0› bdd by auto
ultimately show "∃e>0. ∃L. ∀t∈cball t e ∩ T. 0 ≤ L ∧
(∀x∈cball s e ∩ S. ∀y∈cball s e ∩ S. dist (A t *v x) (A t *v y) ≤ L * dist x y)"
using ‹min e1 e2 > 0› by blast
qed
lemma picard_lindeloef_affine:
fixes A :: "real ⇒ 'a::{banach,real_normed_algebra_1,heine_borel}^'n^'n"
assumes Ahyp: "matrix_continuous_on T A"
and "⋀τ ε. τ ∈ T ⟹ ε > 0 ⟹ bdd_above {∥A t∥⇩o⇩p |t. dist τ t ≤ ε}"
and Bhyp: "continuous_on T B" and "open S"
and "t⇩0 ∈ T" and Thyp: "open T" "is_interval T"
shows "picard_lindeloef (λ t s. A t *v s + B t) T S t⇩0"
apply (unfold_locales, simp_all add: assms, clarsimp)
apply (rule continuous_on_add[OF continuous_on_matrix_vector_multl[OF Ahyp] Bhyp])
by (rule local_lipschitz_affine) (simp_all add: assms)
lemma picard_lindeloef_autonomous_affine:
fixes A :: "'a::{banach,real_normed_field,heine_borel}^'n^'n"
shows "picard_lindeloef (λ t s. A *v s + B) UNIV UNIV t⇩0"
using picard_lindeloef_affine[of _ "λt. A" "λt. B"]
unfolding matrix_continuous_on_def by (simp only: diff_self op_norm0, auto)
lemma picard_lindeloef_autonomous_linear:
fixes A :: "'a::{banach,real_normed_field,heine_borel}^'n^'n"
shows "picard_lindeloef (λ t. (*v) A) UNIV UNIV t⇩0"
using picard_lindeloef_autonomous_affine[of A 0] by force
lemmas unique_sol_autonomous_affine = picard_lindeloef.ivp_unique_solution[OF
picard_lindeloef_autonomous_affine UNIV_I _ subset_UNIV]
lemmas unique_sol_autonomous_linear = picard_lindeloef.ivp_unique_solution[OF
picard_lindeloef_autonomous_linear UNIV_I _ subset_UNIV]
subsection ‹ Flow for affine systems ›
subsubsection ‹ Derivative rules for square matrices ›
declare has_derivative_component [simp del]
lemma has_derivative_exp_scaleRl[derivative_intros]:
fixes f::"real ⇒ real"
assumes "D f ↦ f' at t within T"
shows "D (λt. exp (f t *⇩R A)) ↦ (λh. f' h *⇩R (exp (f t *⇩R A) * A)) at t within T"
proof -
have "bounded_linear f'"
using assms by auto
then obtain m where obs: "f' = (λh. h * m)"
using real_bounded_linear by blast
thus ?thesis
using vector_diff_chain_within[OF _ exp_scaleR_has_vector_derivative_right]
assms obs by (auto simp: has_vector_derivative_def comp_def)
qed
lemma vderiv_on_exp_scaleRlI[poly_derivatives]:
assumes "D f = f' on T" and "g' = (λx. f' x *⇩R exp (f x *⇩R A) * A)"
shows "D (λx. exp (f x *⇩R A)) = g' on T"
using assms unfolding has_vderiv_on_def has_vector_derivative_def apply clarsimp
by (rule has_derivative_exp_scaleRl, auto simp: fun_eq_iff)
lemma has_derivative_mtx_ith[derivative_intros]:
fixes t::real and T :: "real set"
defines "t⇩0 ≡ netlimit (at t within T)"
assumes "D A ↦ (λh. h *⇩R A' t) at t within T"
shows "D (λt. A t $$ i) ↦ (λh. h *⇩R A' t $$ i) at t within T"
using assms unfolding has_derivative_def apply safe
apply(force simp: bounded_linear_def bounded_linear_axioms_def)
apply(rule_tac F="λτ. (A τ - A t⇩0 - (τ - t⇩0) *⇩R A' t) /⇩R (∥τ - t⇩0∥)" in tendsto_zero_norm_bound)
by (clarsimp, rule mult_left_mono, metis (no_types, lifting) norm_column_le_norm
sq_mtx_minus_ith sq_mtx_scaleR_ith) simp_all
lemmas has_derivative_mtx_vec_mult[derivative_intros] =
bounded_bilinear.FDERIV[OF bounded_bilinear_sq_mtx_vec_mult]
lemma vderiv_on_mtx_vec_multI[poly_derivatives]:
assumes "D u = u' on T" and "D A = A' on T"
and "g = (λt. A t *⇩V u' t + A' t *⇩V u t )"
shows "D (λt. A t *⇩V u t) = g on T"
using assms unfolding has_vderiv_on_def has_vector_derivative_def apply clarify
apply(erule_tac x=x in ballE, simp_all)+
apply(rule derivative_eq_intros)
by (auto simp: fun_eq_iff mtx_vec_scaleR_commute pth_6 scaleR_mtx_vec_assoc)
lemmas has_vderiv_on_ivl_integral = ivl_integral_has_vderiv_on[OF vderiv_on_continuous_on]
declare has_vderiv_on_ivl_integral [poly_derivatives]
lemma has_derivative_mtx_vec_multl[derivative_intros]:
assumes "⋀ i j. D (λt. (A t) $$ i $ j) ↦ (λτ. τ *⇩R (A' t) $$ i $ j) (at t within T)"
shows "D (λt. A t *⇩V x) ↦ (λτ. τ *⇩R (A' t) *⇩V x) at t within T"
unfolding sq_mtx_vec_mult_sum_cols
apply(rule_tac f'1="λi τ. τ *⇩R (x $ i *⇩R 𝖼𝗈𝗅 i (A' t))" in derivative_eq_intros(10))
apply(simp_all add: scaleR_right.sum)
apply(rule_tac g'1="λτ. τ *⇩R 𝖼𝗈𝗅 i (A' t)" in derivative_eq_intros(4), simp_all add: mult.commute)
using assms unfolding sq_mtx_col_def column_def
by (transfer, simp add: has_derivative_component)
declare has_derivative_component [simp]
lemma continuous_on_mtx_vec_multr: "continuous_on S ((*⇩V) A)"
by transfer (simp add: matrix_vector_mult_linear_continuous_on)
text ‹Isabelle automatically generates derivative rules from this subsubsection ›
thm derivative_eq_intros(140-)
subsubsection ‹ Existence and uniqueness with square matrices ›
text ‹Finally, we can use the @{term exp} operation to characterize the general solutions for affine
systems of ODEs. We show that they satisfy the @{term "local_flow"} locale.›
lemma continuous_on_sq_mtx_vec_multl:
fixes A :: "real ⇒ ('n::finite) sq_mtx"
assumes "continuous_on T A"
shows "continuous_on T (λt. A t *⇩V s)"
proof-
have "matrix_continuous_on T (λt. to_vec (A t))"
using assms by (force simp: continuous_on_iff dist_norm norm_sq_mtx_def matrix_continuous_on_def)
hence "continuous_on T (λt. to_vec (A t) *v s)"
by (rule continuous_on_matrix_vector_multl)
thus ?thesis
by transfer
qed
lemmas continuous_on_affine = continuous_on_add[OF continuous_on_sq_mtx_vec_multl]
lemma local_lipschitz_sq_mtx_affine:
fixes A :: "real ⇒ ('n::finite) sq_mtx"
assumes "continuous_on T A" "open T" "open S"
shows "local_lipschitz T S (λt s. A t *⇩V s + B t)"
proof-
have obs: "⋀τ ε. 0 < ε ⟹ τ ∈ T ⟹ cball τ ε ⊆ T ⟹ bdd_above {∥A t∥ |t. t ∈ cball τ ε}"
by (rule bdd_above_norm_cont_comp, rule continuous_on_subset[OF assms(1)], simp_all)
hence "⋀τ ε. 0 < ε ⟹ τ ∈ T ⟹ cball τ ε ⊆ T ⟹ bdd_above {∥to_vec (A t)∥⇩o⇩p |t. t ∈ cball τ ε}"
by (simp add: norm_sq_mtx_def)
hence "local_lipschitz T S (λt s. to_vec (A t) *v s + B t)"
using local_lipschitz_affine[OF assms(2,3), of "λt. to_vec (A t)"] by force
thus ?thesis
by transfer
qed
lemma picard_lindeloef_sq_mtx_affine:
assumes "continuous_on T A" and "continuous_on T B"
and "t⇩0 ∈ T" "is_interval T" "open T" and "open S"
shows "picard_lindeloef (λt s. A t *⇩V s + B t) T S t⇩0"
apply(unfold_locales, simp_all add: assms, clarsimp)
using continuous_on_affine assms apply blast
by (rule local_lipschitz_sq_mtx_affine, simp_all add: assms)
lemmas sq_mtx_unique_sol_autonomous_affine = picard_lindeloef.ivp_unique_solution[OF
picard_lindeloef_sq_mtx_affine[OF
continuous_on_const
continuous_on_const
UNIV_I is_interval_univ
open_UNIV open_UNIV]
UNIV_I _ subset_UNIV]
lemma has_vderiv_on_sq_mtx_linear:
"D (λt. exp ((t - t⇩0) *⇩R A) *⇩V s) = (λt. A *⇩V (exp ((t - t⇩0) *⇩R A) *⇩V s)) on {t⇩0--t}"
by (rule poly_derivatives)+ (auto simp: exp_times_scaleR_commute sq_mtx_times_vec_assoc)
lemma has_vderiv_on_sq_mtx_affine:
fixes t⇩0::real and A :: "('a::finite) sq_mtx"
defines "lSol c t ≡ exp ((c * (t - t⇩0)) *⇩R A)"
shows "D (λt. lSol 1 t *⇩V s + lSol 1 t *⇩V (∫⇩t⇩0⇧t (lSol (-1) τ *⇩V B) ∂τ)) =
(λt. A *⇩V (lSol 1 t *⇩V s + lSol 1 t *⇩V (∫⇩t⇩0⇧t (lSol (-1) τ *⇩V B) ∂τ)) + B) on {t⇩0--t}"
unfolding assms apply(simp only: mult.left_neutral mult_minus1)
apply(rule poly_derivatives, (force)?, (force)?, (force)?, (force)?)+
by (simp add: mtx_vec_mult_add_rdistl sq_mtx_times_vec_assoc[symmetric]
exp_minus_inverse exp_times_scaleR_commute mult_exp_exp scale_left_distrib[symmetric])
lemma autonomous_linear_sol_is_exp:
assumes "D X = (λt. A *⇩V X t) on {t⇩0--t}" and "X t⇩0 = s"
shows "X t = exp ((t - t⇩0) *⇩R A) *⇩V s"
apply(rule sq_mtx_unique_sol_autonomous_affine[of "λs. {t⇩0--t}" _ t X A 0])
using assms apply(simp_all add: ivp_sols_def)
using has_vderiv_on_sq_mtx_linear by force+
lemma autonomous_affine_sol_is_exp_plus_int:
assumes "D X = (λt. A *⇩V X t + B) on {t⇩0--t}" and "X t⇩0 = s"
shows "X t = exp ((t - t⇩0) *⇩R A) *⇩V s + exp ((t - t⇩0) *⇩R A) *⇩V (∫⇩t⇩0⇧t(exp (- (τ - t⇩0) *⇩R A) *⇩V B)∂τ)"
apply(rule sq_mtx_unique_sol_autonomous_affine[of "λs. {t⇩0--t}" _ t X A B])
using assms apply(simp_all add: ivp_sols_def)
using has_vderiv_on_sq_mtx_affine by force+
lemma local_flow_sq_mtx_linear: "local_flow ((*⇩V) A) UNIV UNIV (λt s. exp (t *⇩R A) *⇩V s)"
unfolding local_flow_def local_flow_axioms_def apply safe
using picard_lindeloef_sq_mtx_affine[of _ "λt. A" "λt. 0"] apply force
using has_vderiv_on_sq_mtx_linear[of 0] by auto
lemma local_flow_sq_mtx_affine: "local_flow (λs. A *⇩V s + B) UNIV UNIV
(λt s. exp (t *⇩R A) *⇩V s + exp (t *⇩R A) *⇩V (∫⇩0⇧t(exp (- τ *⇩R A) *⇩V B)∂τ))"
unfolding local_flow_def local_flow_axioms_def apply safe
using picard_lindeloef_sq_mtx_affine[of _ "λt. A" "λt. B"] apply force
using has_vderiv_on_sq_mtx_affine[of 0 A] by auto
end