Theory Invariance
section ‹Invariance›
theory Invariance
imports ODE_Misc
begin
context auto_ll_on_open begin
definition "invariant M ⟷ (∀x∈M. trapped x M)"
definition "positively_invariant M ⟷ (∀x∈M. trapped_forward x M)"
definition "negatively_invariant M ⟷ (∀x∈M. trapped_backward x M)"
lemma positively_invariant_iff:
"positively_invariant M ⟷
(⋃x∈M. flow0 x ` (existence_ivl0 x ∩ {0..})) ⊆ M"
unfolding positively_invariant_def trapped_forward_def
by auto
lemma negatively_invariant_iff:
"negatively_invariant M ⟷
(⋃x∈M. flow0 x ` (existence_ivl0 x ∩ {..0})) ⊆ M"
unfolding negatively_invariant_def trapped_backward_def
by auto
lemma invariant_iff_pos_and_neg_invariant:
"invariant M ⟷ positively_invariant M ∧ negatively_invariant M"
unfolding invariant_def trapped_def positively_invariant_def negatively_invariant_def
by blast
lemma invariant_iff:
"invariant M ⟷ (⋃x∈M. flow0 x ` (existence_ivl0 x)) ⊆ M"
unfolding invariant_iff_pos_and_neg_invariant positively_invariant_iff negatively_invariant_iff
by (metis (mono_tags) SUP_le_iff invariant_def invariant_iff_pos_and_neg_invariant negatively_invariant_iff positively_invariant_iff trapped_iff_on_existence_ivl0)
lemma positively_invariant_restrict_dom: "positively_invariant M = positively_invariant (M ∩ X)"
unfolding positively_invariant_def trapped_forward_def
by (auto intro!: flow_in_domain dest: mem_existence_ivl_iv_defined)
lemma negatively_invariant_restrict_dom: "negatively_invariant M = negatively_invariant (M ∩ X)"
unfolding negatively_invariant_def trapped_backward_def
by (auto intro!: flow_in_domain dest: mem_existence_ivl_iv_defined)
lemma invariant_restrict_dom: "invariant M = invariant (M ∩ X)"
using invariant_iff_pos_and_neg_invariant
negatively_invariant_restrict_dom
positively_invariant_restrict_dom by auto
end context auto_ll_on_open begin
lemma positively_invariant_eq_rev: "positively_invariant M = rev.negatively_invariant M"
unfolding positively_invariant_def rev.negatively_invariant_def
by (simp add: rev.trapped_backward_iff_rev_trapped_forward)
lemma negatively_invariant_eq_rev: "negatively_invariant M = rev.positively_invariant M"
unfolding negatively_invariant_def rev.positively_invariant_def
by (simp add: trapped_backward_iff_rev_trapped_forward)
lemma invariant_eq_rev: "invariant M = rev.invariant M"
unfolding invariant_iff_pos_and_neg_invariant rev.invariant_iff_pos_and_neg_invariant
positively_invariant_eq_rev negatively_invariant_eq_rev by auto
lemma negatively_invariant_complI: "negatively_invariant (X-M)" if "positively_invariant M"
unfolding negatively_invariant_def trapped_backward_def
proof clarsimp
fix x t
assume x: "x ∈ X" "x ∉ M" "t ∈ existence_ivl0 x" "t ≤ 0"
have a1:"flow0 x t ∈ X" using x
using flow_in_domain by blast
have a2:"flow0 x t ∉ M"
proof (rule ccontr)
assume "¬ flow0 x t ∉ M"
then have "trapped_forward (flow0 x t) M"
using positively_invariant_def that by auto
moreover have "flow0 (flow0 x t) (-t) = x"
using ‹t ∈ existence_ivl0 x› flows_reverse by auto
moreover have "-t ∈ existence_ivl0 (flow0 x t) ∩ {0..}"
using existence_ivl_reverse x(3) x(4) by auto
ultimately have "x ∈ M" unfolding trapped_forward_def
by (metis image_subset_iff)
thus False using x(2) by auto
qed
show "flow0 x t ∈ X ∧ flow0 x t ∉ M" using a1 a2 by auto
qed
end context auto_ll_on_open begin
lemma negatively_invariant_complD: "positively_invariant M" if "negatively_invariant (X-M)"
proof -
have "rev.positively_invariant (X-M)" using that
by (simp add: negatively_invariant_eq_rev)
then have "rev.negatively_invariant (X-(X-M))"
by (simp add: rev.negatively_invariant_complI)
then have "positively_invariant (X-(X-M))"
using rev.negatively_invariant_eq_rev by auto
thus ?thesis using Diff_Diff_Int
by (metis inf_commute positively_invariant_restrict_dom)
qed
lemma pos_invariant_iff_compl_neg_invariant: "positively_invariant M ⟷ negatively_invariant (X - M)"
by (safe intro!: negatively_invariant_complI dest!: negatively_invariant_complD)
lemma neg_invariant_iff_compl_pos_invariant:
shows "negatively_invariant M ⟷ positively_invariant (X - M)"
by (simp add: auto_ll_on_open.pos_invariant_iff_compl_neg_invariant negatively_invariant_eq_rev positively_invariant_eq_rev rev.auto_ll_on_open_axioms)
lemma invariant_iff_compl_invariant:
shows "invariant M ⟷ invariant (X - M)"
using invariant_iff_pos_and_neg_invariant neg_invariant_iff_compl_pos_invariant pos_invariant_iff_compl_neg_invariant by blast
lemma invariant_iff_pos_invariant_and_compl_pos_invariant:
shows "invariant M ⟷ positively_invariant M ∧ positively_invariant (X-M)"
by (simp add: invariant_iff_pos_and_neg_invariant neg_invariant_iff_compl_pos_invariant)
end
subsection ‹Tools for proving invariance›
context auto_ll_on_open begin
lemma positively_invariant_left_inter:
assumes "positively_invariant C"
assumes "∀x ∈ C ∩ D. trapped_forward x D"
shows "positively_invariant (C ∩ D)"
using assms positively_invariant_def trapped_forward_def by auto
lemma trapped_forward_le:
fixes V :: "'a ⇒ real"
assumes "V x ≤ 0"
assumes contg: "continuous_on (flow0 x ` (existence_ivl0 x ∩ {0..})) g"
assumes "⋀x. (V has_derivative V' x) (at x)"
assumes "⋀s. s ∈ existence_ivl0 x ∩ {0..} ⟹ V' (flow0 x s) (f (flow0 x s)) ≤ g (flow0 x s) * V (flow0 x s)"
shows "trapped_forward x {x. V x ≤ 0}"
unfolding trapped_forward_def
proof clarsimp
fix t
assume t: "t ∈ existence_ivl0 x" "0 ≤ t"
then have ex:"{0..t} ⊆ existence_ivl0 x"
by (simp add: local.ivl_subset_existence_ivl)
have contV: "continuous_on UNIV V"
using assms(3) has_derivative_continuous_on by blast
have 1: "continuous_on {0..t} (g ∘ flow0 x)"
apply (rule continuous_on_compose)
using continuous_on_subset ex local.flow_continuous_on apply blast
by (meson Int_subset_iff atLeastAtMost_iff atLeast_iff contg continuous_on_subset ex image_mono subsetI)
have 2: "(⋀s. s ∈ {0..t} ⟹
(V ∘ flow0 x has_real_derivative (V' (flow0 x s) ∘ f ∘ flow0 x) s) (at s))"
apply (auto simp add:o_def has_field_derivative_def)
proof -
fix s
assume "0 ≤ s" "s ≤ t"
then have "s ∈ existence_ivl0 x" using ex by auto
from flow_has_derivative[OF this] have
"(flow0 x has_derivative (λi. i *⇩R f (flow0 x s))) (at s)" .
from has_derivative_compose[OF this assms(3)]
have "((λt. V (flow0 x t)) has_derivative (λt. V' (flow0 x s) (t *⇩R f (flow0 x s)))) (at s)" .
moreover have "linear (V' (flow0 x s))" using assms(3) has_derivative_linear by blast
ultimately
have "((λt. V (flow0 x t)) has_derivative (λt. t *⇩R V' (flow0 x s) (f (flow0 x s)))) (at s)"
unfolding linear_cmul[OF ‹linear (V' (flow0 x s))›] by blast
thus "((λt. V (flow0 x t)) has_derivative (*) (V' (flow0 x s) (f (flow0 x s)))) (at s)"
by (auto intro!: derivative_eq_intros simp add: mult_commute_abs)
qed
have 3: "(⋀s. s ∈ {0..t} ⟹
(V' (flow0 x s) ∘ f ∘ flow0 x) s ≤ (g ∘ flow0 x) s *⇩R (V ∘ flow0 x) s)"
using ex by (auto intro!:assms(4))
from comparison_principle_le_linear[OF 1 2 _ 3] assms(1)
have "∀s ∈ {0..t}. (V ∘ flow0 x) s ≤ 0"
using local.mem_existence_ivl_iv_defined(2) t(1) by auto
thus " V (flow0 x t) ≤ 0"
by (simp add: t(2))
qed
lemma positively_invariant_le_domain:
fixes V :: "'a ⇒ real"
assumes "positively_invariant D"
assumes contg: "continuous_on D g"
assumes "⋀x. (V has_derivative V' x) (at x)"
assumes "⋀s. s ∈ D ⟹ V' s (f s) ≤ g s * V s"
shows "positively_invariant (D ∩ {x. V x ≤ 0})"
apply (auto intro!:positively_invariant_left_inter[OF assms(1)])
proof -
fix x
assume "x ∈ D" "V x ≤ 0"
have "continuous_on (flow0 x ` (existence_ivl0 x ∩ {0..})) g"
by (meson ‹x ∈ D› assms(1) contg continuous_on_subset positively_invariant_def trapped_forward_def)
from trapped_forward_le[OF ‹V x ≤ 0› this assms(3)]
show "trapped_forward x {x. V x ≤ 0}" using assms(4)
using ‹x ∈ D› assms(1) positively_invariant_def trapped_forward_def by auto
qed
lemma positively_invariant_barrier_domain:
fixes V :: "'a ⇒ real"
assumes "positively_invariant D"
assumes "⋀x. (V has_derivative V' x) (at x)"
assumes "continuous_on D (λx. V' x (f x))"
assumes "⋀s. s ∈ D ⟹ V s = 0 ⟹ V' s (f s) < 0"
shows "positively_invariant (D ∩ {x. V x ≤ 0})"
apply (auto intro!:positively_invariant_left_inter[OF assms(1)])
proof -
fix x
assume "x ∈ D" "V x ≤ 0"
have contV: "continuous_on UNIV V" using assms(2) has_derivative_continuous_on by blast
then have *: "continuous_on (flow0 x ` (existence_ivl0 x ∩ {0..})) V"
using continuous_on_subset by blast
have sub: "flow0 x ` (existence_ivl0 x ∩ {0..}) ⊆ D"
using ‹x ∈ D› assms(1) positively_invariant_def trapped_forward_def by auto
then have contV': "continuous_on (flow0 x ` (existence_ivl0 x ∩ {0..})) (λx. V' x (f x))"
by (metis assms(3) continuous_on_subset)
have nz: "⋀i t. t ∈ existence_ivl0 x ⟹
0 ≤ t ⟹ max (-V' (flow0 x t) (f (flow0 x t))) ((V (flow0 x t))⇧2) > 0"
proof -
fix i t
assume "t ∈ existence_ivl0 x" "0 ≤ t"
then have "flow0 x t ∈ D"
using ‹x ∈ D› assms(1) positively_invariant_def trapped_forward_def by auto
then have "V (flow0 x t) = 0 ⟹ - V' (flow0 x t) (f (flow0 x t)) > 0" using assms(4) by simp
then have "(V (flow0 x t))^2 > 0 ∨ - V' (flow0 x t) (f (flow0 x t)) > 0" by simp
thus "max (-V' (flow0 x t) (f (flow0 x t))) ((V (flow0 x t))⇧2) > 0" unfolding less_max_iff_disj
by auto
qed
have *: "continuous_on (flow0 x ` (existence_ivl0 x ∩ {0..})) (λx. V' x (f x) * V x / max (- V' x (f x)) ((V x)^2))"
apply (auto intro!:continuous_intros continuous_on_max simp add: * contV')
using nz by fastforce
have "(⋀t. t ∈ existence_ivl0 x ∩ {0..} ⟹
V' (flow0 x t) (f (flow0 x t)) ≤
(V' (flow0 x t) (f (flow0 x t)) * V (flow0 x t)
/ max (- V' (flow0 x t) (f (flow0 x t))) ((V (flow0 x t))⇧2)) * V (flow0 x t))"
proof clarsimp
fix t
assume "t ∈ existence_ivl0 x" "0 ≤ t"
then have p: "max (-V' (flow0 x t) (f (flow0 x t))) ((V (flow0 x t))⇧2) > 0" using nz by auto
have " V' (flow0 x t) (f (flow0 x t)) * max (- V' (flow0 x t) (f (flow0 x t))) ((V (flow0 x t))⇧2)
≤ V' (flow0 x t) (f (flow0 x t)) * (V (flow0 x t))⇧2"
by (smt (z3) mult_minus_left mult_minus_right power2_eq_square mult_le_cancel_left_pos)
then have "V' (flow0 x t) (f (flow0 x t))
≤ V' (flow0 x t) (f (flow0 x t)) * (V (flow0 x t))⇧2
/ max (- V' (flow0 x t) (f (flow0 x t))) ((V (flow0 x t))⇧2)"
using p pos_le_divide_eq by blast
thus " V' (flow0 x t) (f (flow0 x t))
≤ V' (flow0 x t) (f (flow0 x t)) * (V (flow0 x t)) * V (flow0 x t) /
max (- V' (flow0 x t) (f (flow0 x t))) ((V (flow0 x t))⇧2)"
by (simp add: power2_eq_square)
qed
from trapped_forward_le[OF ‹V x ≤ 0› * assms(2) this]
show "trapped_forward x {x. V x ≤ 0}" by auto
qed
lemma positively_invariant_UNIV:
shows "positively_invariant UNIV"
using positively_invariant_iff by blast
lemma positively_invariant_conj:
assumes "positively_invariant C"
assumes "positively_invariant D"
shows "positively_invariant (C ∩ D)"
using assms positively_invariant_def
using positively_invariant_left_inter by auto
lemma positively_invariant_le:
fixes V :: "'a ⇒ real"
assumes contg: "continuous_on UNIV g"
assumes "⋀x. (V has_derivative V' x) (at x)"
assumes "⋀s. V' s (f s) ≤ g s * V s"
shows "positively_invariant {x. V x ≤ 0}"
proof -
from positively_invariant_le_domain[OF positively_invariant_UNIV assms]
have "positively_invariant (UNIV ∩ {x. V x ≤ 0})" .
thus ?thesis by auto
qed
lemma positively_invariant_barrier:
fixes V :: "'a ⇒ real"
assumes "⋀x. (V has_derivative V' x) (at x)"
assumes "continuous_on UNIV (λx. V' x (f x))"
assumes "⋀s. V s = 0 ⟹ V' s (f s) < 0"
shows "positively_invariant {x. V x ≤ 0}"
proof -
from positively_invariant_barrier_domain[OF positively_invariant_UNIV assms]
have "positively_invariant (UNIV ∩ {x. V x ≤ 0})" .
thus ?thesis by auto
qed
end
end