# Theory Affine_Arithmetic.Affine_Form

section ‹Affine Form›
theory Affine_Form
imports

Affine_Arithmetic_Auxiliarities
Executable_Euclidean_Space
begin

subsection ‹Auxiliary developments›

lemma sum_list_mono:
shows
"length xs = length ys  (x y. (x, y)  set (zip xs ys)  x  y)
sum_list xs  sum_list ys"
by (induct xs ys rule: list_induct2) (auto simp: algebra_simps intro: add_mono)

lemma
fixes xs::
shows sum_list_nonneg: "(x. x  set xs  x  0)  sum_list xs  0"
by (induct xs) (auto intro!: add_nonneg_nonneg)

lemma map_filter:
"map f (filter (λx. P (f x)) xs) = filter P (map f xs)"
by (induct xs) simp_all

lemma
map_of_zip_upto2_length_eq_nth:
assumes "distinct B"
assumes "i < length B"
shows "(map_of (zip B [0..<length B]) (B ! i)) = Some i"
proof -
have
by simp
from map_of_zip_is_Some[OF this, of i] assms
have "map_of (zip B [0..<length B]) (B ! i) = Some i"
using assms by (auto simp: in_set_zip)
thus ?thesis by simp
qed

lemma distinct_map_fst_snd_eqD:
"distinct (map fst xs)  (i, a)  set xs  (i, b)  set xs  a = b"
by (metis (lifting) map_of_is_SomeI option.inject)

lemma length_filter_snd_zip:
"length ys = length xs  length (filter (p  snd) (zip ys xs)) = length (filter p xs)"
by (induct ys xs rule: list_induct2) (auto )

lemma filter_snd_nth:
"length ys = length xs  n < length (filter p xs)
snd (filter (p  snd) (zip ys xs) ! n) = filter p xs ! n"
by (induct ys xs arbitrary: n rule: list_induct2) (auto simp: o_def nth_Cons split: nat.split)

lemma distinct_map_snd_fst_eqD:
"distinct (map snd xs)  (i, a)  set xs  (j, a)  set xs  i = j"
by (metis Pair_inject inj_on_contraD snd_conv distinct_map)

lemma map_of_mapk_inj_on_SomeI:
"inj_on f (fst ` (set t))  map_of t k = Some x
map_of (map (case_prod (λk. Pair (f k))) t) (f k) = Some x"
by (induct t) (auto simp add: inj_on_def dest!: map_of_SomeD split: if_split_asm)

lemma map_abs_nonneg[simp]:
fixes xs::
shows "list_all (λx. x  0) xs  map abs xs = xs"
by (induct xs) auto

lemma the_inv_into_image_eq: "inj_on f A  Y  f ` A  the_inv_into A f ` Y = f -` Y  A"
using f_the_inv_into_f the_inv_into_f_f[where f = f and A = A]
by force

lemma image_fst_zip: "length ys = length xs  fst ` set (zip ys xs) = set ys"
by (metis dom_map_of_conv_image_fst dom_map_of_zip)

lemma inj_on_fst_set_zip_distinct[simp]:
"distinct xs  length xs = length ys  inj_on fst (set (zip xs ys))"
by (force simp add: in_set_zip distinct_conv_nth intro!: inj_onI)

lemma mem_greaterThanLessThan_absI:
fixes x::real
assumes "abs x < 1"
shows "x  {-1 <..< 1}"
using assms by (auto simp: abs_real_def split: if_split_asm)

lemma minus_one_less_divideI: "b > 0  -b < a  -1 < a / (b::real)"
by (auto simp: field_simps)

lemma divide_less_oneI: "b > 0  b > a  a / (b::real) < 1"
by (auto simp: field_simps)

lemma closed_segment_real:
fixes a b::real
shows "closed_segment a b = (if a  b then {a .. b} else {b .. a})" (is "_ = ?if")
proof safe
fix x assume "x  closed_segment a b"
from segment_bound[OF this]
show "x  ?if" by (auto simp: abs_real_def split: if_split_asm)
next
fix x
assume "x  ?if"
thus "x  closed_segment a b"
by (auto simp: closed_segment_def intro!: exI[where x="(x - a)/(b - a)"]
simp: divide_simps algebra_simps)
qed

subsection ‹Partial Deviations›

typedef (overloaded) 'a pdevs = "{x::nat  'a::zero. finite {i. x i  0}}"
― ‹TODO: unify with polynomials›
morphisms pdevs_apply Abs_pdev
by (auto intro!: exI[where x="λx. 0"])

setup_lifting type_definition_pdevs

lemma pdevs_eqI: "(i. pdevs_apply x i = pdevs_apply y i)  x = y"
by transfer auto

definition pdevs_val :: "(nat  real)  'a::real_normed_vector pdevs  'a"
where "pdevs_val e x = (i. e i *R pdevs_apply x i)"

definition valuate:: "((nat  real)  'a)  'a set"
where "valuate x = x ` (UNIV  {-1 .. 1})"

lemma valuate_ex: "x  valuate f  (e. (i. e i  {-1 .. 1})  x = f e)"
unfolding valuate_def
by (auto simp add: valuate_def Pi_iff) blast

instantiation pdevs :: (equal) equal
begin

definition equal_pdevs::"'a pdevs  'a pdevs  bool"
where "equal_pdevs a b  a = b"

instance proof qed (simp add: equal_pdevs_def)
end

subsection ‹Affine Forms›

text ‹The data structure of affine forms represents particular sets, zonotopes›

type_synonym 'a aform = "'a × 'a pdevs"

subsection ‹Evaluation, Range, Joint Range›

definition aform_val :: "(nat  real)  'a::real_normed_vector aform  'a"
where "aform_val e X = fst X + pdevs_val e (snd X)"

definition Affine ::
"'a::real_normed_vector aform  'a set"
where "Affine X = valuate (λe. aform_val e X)"

definition Joints ::
"'a::real_normed_vector aform list  'a list set"
where "Joints XS = valuate (λe. map (aform_val e) XS)"

lemma Joints_nthE:
assumes "zs  Joints ZS"
obtains e where
"i. i < length zs  zs ! i = aform_val e (ZS ! i)"
"i. e i  {-1..1}"
using assms
by atomize_elim (auto simp: Joints_def Pi_iff valuate_ex)

lemma Joints_mapE:
assumes "ys  Joints YS"
obtains e where
"ys = map (λx. aform_val e x) YS"
"i. e i  {-1 .. 1}"
using assms
by (force simp: Joints_def valuate_def)

lemma
zipped_subset_mapped_Elem:
assumes "xs = map (aform_val e) XS"
assumes e: "i. e i  {-1 .. 1}"
assumes [simp]: "length xs = length XS"
assumes [simp]: "length ys = length YS"
assumes "set (zip ys YS)  set (zip xs XS)"
shows "ys = map (aform_val e) YS"
proof -
from assms have ys: "i. i < length xs  xs ! i = aform_val e (XS ! i)"
by auto
from assms have set_eq: "{(ys ! i, YS ! i) |i. i < length ys  i < length YS}
{(xs ! i, XS ! i) |i. i < length xs  i < length XS}"
using assms(2)
by (auto simp: set_zip)
hence "i<length YS. j<length XS. ys ! i = xs ! j  YS ! i = XS ! j"
by auto
then obtain j where j: "i. i < length YS  ys ! i = xs ! (j i)"
"i. i < length YS  YS ! i = XS ! (j i)"
"i. i < length YS  j i < length XS"
by metis
show ?thesis
using assms
by (auto simp: Joints_def j ys intro!: exI[where x=e] nth_equalityI)
qed

lemma Joints_set_zip_subset:
assumes "xs  Joints XS"
assumes "length xs = length XS"
assumes "length ys = length YS"
assumes "set (zip ys YS)  set (zip xs XS)"
shows "ys  Joints YS"
proof -
from Joints_mapE assms obtain e where
ys: "xs = map (λx. aform_val e x) XS"
and e: "i. e i  {-1 .. 1}"
by blast
show "ys  Joints YS"
using e zipped_subset_mapped_Elem[OF ys e assms(2-4)]
by (auto simp: Joints_def valuate_def intro!: exI[where x=e])
qed

lemma Joints_set_zip:
assumes "ys  Joints YS"
assumes "length xs = length XS"
assumes "length YS = length XS"
assumes sets_eq: "set (zip xs XS) = set (zip ys YS)"
shows "xs  Joints XS"
proof -
from assms have "length ys = length YS"
by (auto simp: Joints_def valuate_def)
from assms(1) this assms(2) show ?thesis
by (rule Joints_set_zip_subset) (simp add: assms)
qed

definition Joints2 ::
"'a::real_normed_vector aform list 'b::real_normed_vector aform  ('a list × 'b) set"
where "Joints2 XS Y = valuate (λe. (map (aform_val e) XS, aform_val e Y))"

lemma Joints2E:
assumes "zs_y  Joints2 ZS Y"
obtains e where
"i. i < length (fst zs_y)  (fst zs_y) ! i = aform_val e (ZS ! i)"
"snd (zs_y) = aform_val e Y"
"i. e i  {-1..1}"
using assms
by atomize_elim (auto simp: Joints2_def Pi_iff valuate_ex)

lemma nth_in_AffineI:
assumes "xs  Joints XS"
assumes "i < length XS"
shows "xs ! i  Affine (XS ! i)"
using assms by (force simp: Affine_def Joints_def valuate_def)

lemma Cons_nth_in_Joints1:
assumes "xs  Joints XS"
assumes "i < length XS"
shows "((xs ! i) # xs)  Joints ((XS ! i) # XS)"
using assms by (force simp: Joints_def valuate_def)

lemma Cons_nth_in_Joints2:
assumes "xs  Joints XS"
assumes "i < length XS"
assumes "j < length XS"
shows "((xs ! i) #(xs ! j) # xs)  Joints ((XS ! i)#(XS ! j) # XS)"
using assms by (force simp: Joints_def valuate_def)

lemma Joints_swap:
"x#y#xsJoints (X#Y#XS)  y#x#xs  Joints (Y#X#XS)"
by (force simp: Joints_def valuate_def)

lemma Joints_swap_Cons_append:
"length xs = length XS  x#ys@xsJoints (X#YS@XS)  ys@x#xs  Joints (YS@X#XS)"
by (auto simp: Joints_def valuate_def)

lemma Joints_ConsD:
"x#xsJoints (X#XS)  xs  Joints XS"
by (force simp: Joints_def valuate_def)

lemma Joints_appendD1:
"ys@xsJoints (YS@XS)  length xs = length XS  xs  Joints XS"
by (force simp: Joints_def valuate_def)

lemma Joints_appendD2:
"ys@xsJoints (YS@XS)  length ys = length YS  ys  Joints YS"
by (force simp: Joints_def valuate_def)

lemma Joints_imp_length_eq: "xs  Joints XS  length xs = length XS"
by (auto simp: Joints_def valuate_def)

lemma Joints_rotate[simp]: "xs@[x]  Joints (XS @[X])  x#xs  Joints (X#XS)"
by (auto simp: Joints_def valuate_def)

subsection ‹Domain›

definition "pdevs_domain x = {i. pdevs_apply x i  0}"

lemma finite_pdevs_domain[intro, simp]: "finite (pdevs_domain x)"
unfolding pdevs_domain_def by transfer

lemma in_pdevs_domain[simp]:
by (auto simp: pdevs_domain_def)

subsection ‹Least Fresh Index›

definition degree::"'a::real_vector pdevs  nat"
where "degree x = (LEAST i. ji. pdevs_apply x j = 0)"

lemma degree[rule_format, intro, simp]:
shows "jdegree x. pdevs_apply x j = 0"
unfolding degree_def
proof (rule LeastI_ex)
have "j. j > Max (pdevs_domain x)  j  (pdevs_domain x)"
by (metis Max_less_iff all_not_in_conv less_irrefl_nat finite_pdevs_domain)
then show "xa. jxa. pdevs_apply x j = 0"
by (auto intro!: exI[where x="Max (pdevs_domain x) + 1"])
qed

lemma degree_le:
assumes d: "j  d. pdevs_apply x j = 0"
shows "degree x  d"
unfolding degree_def
by (rule Least_le) (rule d)

lemma degree_gt: "pdevs_apply x j  0  degree x > j"
by auto

lemma pdevs_val_pdevs_domain: "pdevs_val e X = (ipdevs_domain X. e i *R pdevs_apply X i)"
by (auto simp: pdevs_val_def intro!: suminf_finite)

lemma pdevs_val_sum_le: "degree X  d  pdevs_val e X = (i < d. e i *R pdevs_apply X i)"
by (force intro!: degree_gt sum.mono_neutral_cong_left simp: pdevs_val_pdevs_domain)

lemmas pdevs_val_sum = pdevs_val_sum_le[OF order_refl]

lemma pdevs_val_zero[simp]: "pdevs_val (λ_. 0) x = 0"
by (auto simp: pdevs_val_sum)

lemma degree_eqI:
assumes "pdevs_apply x d  0"
assumes "j. j > d  pdevs_apply x j = 0"
shows "degree x = Suc d"
unfolding eq_iff
by (auto intro!: degree_gt degree_le assms simp: Suc_le_eq)

lemma finite_degree_nonzero[intro, simp]: "finite {i. pdevs_apply x i  0}"
by transfer (auto simp: vimage_def Collect_neg_eq)

lemma degree_eq_Suc_max:
"degree x = (if (i. pdevs_apply x i = 0) then 0 else Suc (Max {i. pdevs_apply x i  0}))"
proof -
{
assume "i. pdevs_apply x i = 0"
hence ?thesis
by auto (metis degree_le le_0_eq)
} moreover {
fix i assume "pdevs_apply x i  0"
hence ?thesis
using Max_in[OF finite_degree_nonzero, of x]
by (auto intro!: degree_eqI) (metis Max.coboundedI[OF finite_degree_nonzero] in_pdevs_domain
le_eq_less_or_eq less_asym pdevs_domain_def)
} ultimately show ?thesis
by blast
qed

lemma pdevs_val_degree_cong:
assumes "b = d"
assumes "i. i < degree b  a i = c i"
shows "pdevs_val a b = pdevs_val c d"
using assms
by (auto simp: pdevs_val_sum)

abbreviation degree_aform::"'a::real_vector aform  nat"
where "degree_aform X  degree (snd X)"

lemma degree_cong: "(i. (pdevs_apply x i = 0) = (pdevs_apply y i = 0))  degree x = degree y"
unfolding degree_def
by auto

lemma Least_True_nat[intro, simp]: "(LEAST i::nat. True) = 0"
by (metis (lifting) One_nat_def less_one not_less_Least not_less_eq)

lemma sorted_list_of_pdevs_domain_eq:

by (auto simp: degree_gt intro!: sorted_distinct_set_unique sorted_filter[of "λx. x", simplified])

subsection ‹Total Deviation›

definition tdev::"'a::ordered_euclidean_space pdevs  'a" where
"tdev x = (i<degree x. ¦pdevs_apply x i¦)"

lemma abs_pdevs_val_le_tdev:
by (force simp: pdevs_val_sum tdev_def abs_scaleR Pi_iff
intro!: order_trans[OF sum_abs] sum_mono scaleR_left_le_one_le
intro: abs_leI)

subsection ‹Binary Pointwise Operations›

definition binop_pdevs_raw::"('a::zero  'b::zero  'c::zero)
(nat  'a)  (nat  'b)  nat  'c"
where "binop_pdevs_raw f x y i = (if x i = 0  y i = 0 then 0 else f (x i) (y i))"

lemma nonzeros_binop_pdevs_subset:
"{i. binop_pdevs_raw f x y i  0}  {i. x i  0}  {i. y i  0}"
by (auto simp: binop_pdevs_raw_def)

lift_definition binop_pdevs::
"('a  'b  'c)  'a::zero pdevs  'b::zero pdevs  'c::zero pdevs"
is binop_pdevs_raw
using nonzeros_binop_pdevs_subset
by (rule finite_subset) auto

lemma pdevs_apply_binop_pdevs[simp]: "pdevs_apply (binop_pdevs f x y) i =
(if pdevs_apply x i = 0  pdevs_apply y i = 0 then 0 else f (pdevs_apply x i) (pdevs_apply y i))"
by transfer (auto simp: binop_pdevs_raw_def)

definition add_pdevs::"'a::real_vector pdevs  'a pdevs  'a pdevs"

"pdevs_apply (add_pdevs X Y) n = pdevs_apply X n + pdevs_apply Y n"

fixes x y::"'a::euclidean_space"
shows "pdevs_val e (add_pdevs X Y) = pdevs_val e X + pdevs_val e Y"
proof -
let ?sum = "λm X. i < m. e i *R pdevs_apply X i"
let ?m = "max (degree X) (degree Y)"
have "pdevs_val e X + pdevs_val e Y = ?sum (degree X) X + ?sum (degree Y) Y"
also have "?sum (degree X) X = ?sum ?m X"
by (rule sum.mono_neutral_cong_left) auto
also have "?sum (degree Y) Y = ?sum ?m Y"
by (rule sum.mono_neutral_cong_left) auto
also have "?sum ?m X + ?sum ?m Y = (i < ?m. e i *R (pdevs_apply X i + pdevs_apply Y i))"
also have " = (i. e i *R (pdevs_apply X i + pdevs_apply Y i))"
by (rule suminf_finite[symmetric]) auto
also have " = pdevs_val e (add_pdevs X Y)"
finally show "pdevs_val e (add_pdevs X Y) = pdevs_val e X + pdevs_val e Y" by simp
qed

subsection ‹Total Deviation›

lemma tdev_eq_zero_iff: fixes X:: shows "tdev X = 0  (e. pdevs_val e X = 0)"
by (force simp add: pdevs_val_sum tdev_def sum_nonneg_eq_0_iff
dest!: spec[where x="λi. if pdevs_apply X i  0 then 1 else -1"] split: if_split_asm)

lemma tdev_nonneg[intro, simp]: "tdev X  0"
by (auto simp: tdev_def)

lemma tdev_nonpos_iff[simp]: "tdev X  0  tdev X = 0"
by (auto simp: order.antisym)

subsection ‹Unary Operations›

definition unop_pdevs_raw::
"('a::zero  'b::zero)  (nat  'a)  nat  'b"
where "unop_pdevs_raw f x i = (if x i = 0 then 0 else f (x i))"

lemma nonzeros_unop_pdevs_subset: "{i. unop_pdevs_raw f x i  0}  {i. x i  0}"
by (auto simp: unop_pdevs_raw_def)

lift_definition unop_pdevs::
"('a  'b)  'a::zero pdevs  'b::zero pdevs"
is unop_pdevs_raw
using nonzeros_unop_pdevs_subset
by (rule finite_subset) auto

lemma pdevs_apply_unop_pdevs[simp]: "pdevs_apply (unop_pdevs f x) i =
(if pdevs_apply x i = 0 then 0 else f (pdevs_apply x i))"
by transfer (auto simp: unop_pdevs_raw_def)

lemma pdevs_domain_unop_linear:
assumes "linear f"
shows
proof -
interpret f: linear f by fact
show ?thesis
by (auto simp: f.zero)
qed

lemma
pdevs_val_unop_linear:
assumes "linear f"
shows "pdevs_val e (unop_pdevs f x) = f (pdevs_val e x)"
proof -
interpret f: linear f by fact
have *: "i. (if pdevs_apply x i = 0 then 0 else f (pdevs_apply x i)) = f (pdevs_apply x i)"
by (auto simp: f.zero)
have "pdevs_val e (unop_pdevs f x) =
(ipdevs_domain (unop_pdevs f x). e i *R f (pdevs_apply x i))"
by (auto simp add: pdevs_val_pdevs_domain *)
also have " = (xapdevs_domain x. e xa *R f (pdevs_apply x xa))"
by (auto intro!: sum.mono_neutral_cong_left)
also have " = f (pdevs_val e x)"
by (auto simp add: pdevs_val_pdevs_domain f.sum f.scaleR)
finally show ?thesis .
qed

subsection ‹Pointwise Scaling of Partial Deviations›

definition scaleR_pdevs::"real  'a::real_vector pdevs  'a pdevs"
where "scaleR_pdevs r x = unop_pdevs ((*R) r) x"

lemma pdevs_apply_scaleR_pdevs[simp]:
"pdevs_apply (scaleR_pdevs x Y) n = x *R pdevs_apply Y n"
by (auto simp: scaleR_pdevs_def)

lemma degree_scaleR_pdevs[simp]: "degree (scaleR_pdevs r x) = (if r = 0 then 0 else degree x)"
unfolding degree_def
by auto

lemma pdevs_val_scaleR_pdevs[simp]:
fixes x::real and Y::"'a::real_normed_vector pdevs"
shows "pdevs_val e (scaleR_pdevs x Y) = x *R pdevs_val e Y"
by (auto simp: pdevs_val_sum scaleR_sum_right ac_simps)

subsection ‹Partial Deviations Scale Pointwise›

definition pdevs_scaleR::"real pdevs  'a::real_vector  'a pdevs"
where "pdevs_scaleR r x = unop_pdevs (λr. r *R x) r"

lemma pdevs_apply_pdevs_scaleR[simp]:
"pdevs_apply (pdevs_scaleR X y) n = pdevs_apply X n *R y"
by (auto simp: pdevs_scaleR_def)

lemma degree_pdevs_scaleR[simp]: "degree (pdevs_scaleR r x) = (if x = 0 then 0 else degree r)"
unfolding degree_def
by auto

lemma pdevs_val_pdevs_scaleR[simp]:
fixes X:: and y::"'a::real_normed_vector"
shows "pdevs_val e (pdevs_scaleR X y) = pdevs_val e X *R y"
by (auto simp: pdevs_val_sum scaleR_sum_left)

subsection ‹Pointwise Unary Minus›

definition uminus_pdevs::"'a::real_vector pdevs  'a pdevs"
where "uminus_pdevs = unop_pdevs uminus"

lemma pdevs_apply_uminus_pdevs[simp]:
by (auto simp: uminus_pdevs_def)

lemma degree_uminus_pdevs[simp]:
by (rule degree_cong) simp

lemma pdevs_val_uminus_pdevs[simp]: "pdevs_val e (uminus_pdevs x) = - pdevs_val e x"
unfolding pdevs_val_sum
by (auto simp: sum_negf)

definition "uminus_aform X = (- fst X, uminus_pdevs (snd X))"

lemma fst_uminus_aform[simp]: "fst (uminus_aform Y) = - fst Y"

lemma aform_val_uminus_aform[simp]: "aform_val e (uminus_aform X) = - aform_val e X"
by (auto simp: uminus_aform_def aform_val_def)

subsection ‹Constant›

lift_definition zero_pdevs::"'a::zero pdevs" is "λ_. 0" by simp

lemma pdevs_apply_zero_pdevs[simp]:
by transfer simp

lemma pdevs_val_zero_pdevs[simp]:
by (auto simp: pdevs_val_def)

definition "num_aform f = (f, zero_pdevs)"

subsection ‹Inner Product›

definition pdevs_inner::"'a::euclidean_space pdevs  'a  real pdevs"
where "pdevs_inner x b = unop_pdevs (λx. x  b) x"

lemma pdevs_apply_pdevs_inner[simp]: "pdevs_apply (pdevs_inner p a) i = pdevs_apply p i  a"

lemma pdevs_val_pdevs_inner[simp]: "pdevs_val e (pdevs_inner p a) = pdevs_val e p  a"
by (auto simp add: inner_sum_left pdevs_val_pdevs_domain intro!: sum.mono_neutral_cong_left)

definition inner_aform::"'a::euclidean_space aform  'a  real aform"
where "inner_aform X b = (fst X  b, pdevs_inner (snd X) b)"

subsection ‹Inner Product Pair›

definition inner2::"'a::euclidean_space  'a  'a  real*real"
where "inner2 x n l = (x  n, x  l)"

definition pdevs_inner2::"'a::euclidean_space pdevs  'a  'a  (real*real) pdevs"
where "pdevs_inner2 X n l = unop_pdevs (λx. inner2 x n l) X"

lemma pdevs_apply_pdevs_inner2[simp]: "pdevs_apply (pdevs_inner2 p a b) i = (pdevs_apply p i  a, pdevs_apply p i  b)"
by (simp add: pdevs_inner2_def inner2_def zero_prod_def)

definition inner2_aform::"'a::euclidean_space aform  'a  'a  (real*real) aform"
where "inner2_aform X a b = (inner2 (fst X) a b, pdevs_inner2 (snd X) a b)"

lemma linear_inner2[intro, simp]: "linear (λx. inner2 x n i)"
by unfold_locales (auto simp: inner2_def algebra_simps)

lemma aform_val_inner2_aform[simp]: "aform_val e (inner2_aform Z n i) = inner2 (aform_val e Z) n i"
proof -
have "aform_val e (inner2_aform Z n i) = inner2 (fst Z) n i + inner2 (pdevs_val e (snd Z)) n i"
by (auto simp: aform_val_def inner2_aform_def pdevs_inner2_def pdevs_val_unop_linear)
also have " = inner2 (aform_val e Z) n i"
by (simp add: inner2_def algebra_simps aform_val_def)
finally show ?thesis .
qed

subsection ‹Update›

lemma pdevs_val_upd[simp]:
"pdevs_val (e(n := e')) X = pdevs_val e X - e n * pdevs_apply X n + e' * pdevs_apply X n"
unfolding pdevs_val_def
by (subst suminf_finite[OF finite.insertI[OF finite_degree_nonzero], of n X],
auto simp: pdevs_val_def sum.insert_remove)+

lemma nonzeros_fun_upd:
"{i. (f(n := a)) i  0}  {i. f i  0}  {n}"
by (auto split: if_split_asm)

lift_definition pdev_upd::"'a::real_vector pdevs  nat  'a  'a pdevs"
is "λx n a. x(n:=a)"
by (rule finite_subset[OF nonzeros_fun_upd]) simp

lemma pdevs_apply_pdev_upd[simp]:
"pdevs_apply (pdev_upd X n x) = (pdevs_apply X)(n:=x)"
by transfer simp

lemma pdevs_val_pdev_upd[simp]:
"pdevs_val e (pdev_upd X n x) = pdevs_val e X + e n *R x - e n *R pdevs_apply X n"
unfolding pdevs_val_def
by (subst suminf_finite[OF finite.insertI[OF finite_degree_nonzero], of n X],
auto simp: pdevs_val_def sum.insert_remove)+

lemma degree_pdev_upd:
assumes "x = 0  pdevs_apply X n = 0"
shows "degree (pdev_upd X n x) = degree X"
using assms
by (auto intro!: degree_cong split: if_split_asm)

lemma degree_pdev_upd_le:
assumes "degree X  n"
shows "degree (pdev_upd X n x)  Suc n"
using assms
by (auto intro!: degree_le)

subsection ‹Inf/Sup›

definition "Inf_aform X = fst X - tdev (snd X)"

definition "Sup_aform X = fst X + tdev (snd X)"

lemma Inf_aform:
assumes
shows "Inf_aform X  aform_val e X"
using order_trans[OF abs_ge_minus_self abs_pdevs_val_le_tdev[OF assms]]
by (auto simp: Inf_aform_def aform_val_def minus_le_iff)

lemma Sup_aform:
assumes
shows "aform_val e X  Sup_aform X"
using order_trans[OF abs_ge_self abs_pdevs_val_le_tdev[OF assms]]
by (auto simp: Sup_aform_def aform_val_def)

subsection ‹Minkowski Sum›

definition msum_pdevs_raw::"nat(nat  'a::real_vector)(nat  'a)(nat'a)" where
"msum_pdevs_raw n x y i = (if i < n then x i else y (i - n))"

lemma nonzeros_msum_pdevs_raw:
"{i. msum_pdevs_raw n f g i  0} = ({0..<n}  {i. f i  0})  (+) n ` ({i. g i  0})"
by (force simp: msum_pdevs_raw_def not_less split: if_split_asm)

lift_definition msum_pdevs::"nat'a::real_vector pdevs'a pdevs'a pdevs" is msum_pdevs_raw
unfolding nonzeros_msum_pdevs_raw by simp

lemma pdevs_apply_msum_pdevs: "pdevs_apply (msum_pdevs n f g) i =
(if i < n then pdevs_apply f i else pdevs_apply g (i - n))"
by transfer (auto simp: msum_pdevs_raw_def)

lemma degree_least_nonzero:
assumes "degree f  0"
shows "pdevs_apply f (degree f - 1)  0"
proof
assume H: "pdevs_apply f (degree f - 1) = 0"
{
fix j
assume "jdegree f - 1"
with H have "pdevs_apply f j = 0"
by (cases "degree f - 1 = j") auto
}
from degree_le[rule_format, OF this]
have "degree f  degree f - 1"
by blast
with assms show False by simp
qed

lemma degree_leI:
assumes "(i. pdevs_apply y i = 0  pdevs_apply x i = 0)"
shows "degree x  degree y"
proof cases
assume "degree x  0"
from degree_least_nonzero[OF this]
have "pdevs_apply y (degree x - 1)  0"
by (auto simp: assms split: if_split_asm)
from degree_gt[OF this] show ?thesis
by simp
qed simp

lemma degree_msum_pdevs_ge1:
shows "degree f  n  degree f  degree (msum_pdevs n f g)"
by (rule degree_leI) (auto simp: pdevs_apply_msum_pdevs split: if_split_asm)

lemma degree_msum_pdevs_ge2:
assumes "degree f  n"
shows "degree g  degree (msum_pdevs n f g) - n"
proof cases
assume "degree g  0"
hence "pdevs_apply g (degree g - 1)  0" by (rule degree_least_nonzero)
hence "pdevs_apply (msum_pdevs n f g) (n + degree g - 1)  0"
using assms
by (auto simp: pdevs_apply_msum_pdevs)
from degree_gt[OF this]
show ?thesis
by simp
qed simp

lemma degree_msum_pdevs_le:
shows "degree (msum_pdevs n f g)  n + degree g"
by (auto intro!: degree_le simp: pdevs_apply_msum_pdevs)

lemma
sum_msum_pdevs_cases:
assumes "degree f  n"
assumes [simp]: "i. e i 0 = 0"
shows
"(i <degree (msum_pdevs n f g).
e i (if i < n then pdevs_apply f i else pdevs_apply g (i - n))) =
(i <degree f. e i (pdevs_apply f i)) + (i <degree g. e (i + n) (pdevs_apply g i))"
(is "?lhs = ?rhs")
proof -
have "?lhs = (i{..<degree (msum_pdevs n f g)}  {i. i < n}. e i (pdevs_apply f i)) +
(i{..<degree (msum_pdevs n f g)}  - {i. i < n}. e i (pdevs_apply g (i - n)))"
(is "_ = ?sum_f + ?sum_g")
also have "?sum_f = (i = 0..<degree f. e i (pdevs_apply f i))"
using assms degree_msum_pdevs_ge1[of f n g]
by (intro sum.mono_neutral_cong_right) auto
also
have "?sum_g = (i{0 + n..<degree (msum_pdevs n f g) - n + n}. e i (pdevs_apply g (i - n)))"
by (rule sum.cong) auto
also have " = (i = 0..<degree (msum_pdevs n f g) - n. e (i + n) (pdevs_apply g (i + n - n)))"
by (rule sum.shift_bounds_nat_ivl)
also have " = (i = 0..<degree g. e (i + n) (pdevs_apply g i))"
using assms degree_msum_pdevs_ge2[of f n]
by (intro sum.mono_neutral_cong_right) (auto intro!: sum.mono_neutral_cong_right)
finally show ?thesis
qed

lemma tdev_msum_pdevs: "degree f  n  tdev (msum_pdevs n f g) = tdev f + tdev g"
by (auto simp: tdev_def pdevs_apply_msum_pdevs intro!: sum_msum_pdevs_cases)

lemma pdevs_val_msum_pdevs:
"degree f  n  pdevs_val e (msum_pdevs n f g) = pdevs_val e f + pdevs_val (λi. e (i + n)) g"
by (auto simp: pdevs_val_sum pdevs_apply_msum_pdevs intro!: sum_msum_pdevs_cases)

definition msum_aform::"nat  'a::real_vector aform  'a aform  'a aform"
where "msum_aform n f g = (fst f + fst g, msum_pdevs n (snd f) (snd g))"

lemma fst_msum_aform[simp]: "fst (msum_aform n f g) = fst f + fst g"

lemma snd_msum_aform[simp]: "snd (msum_aform n f g) = msum_pdevs n (snd f) (snd g)"

lemma finite_nonzero_summable: "finite {i. f i  0}  summable f"
by (auto intro!: sums_summable sums_finite)

lemma aform_val_msum_aform:
assumes "degree_aform f  n"
shows "aform_val e (msum_aform n f g) = aform_val e f + aform_val (λi. e (i + n)) g"
using assms
by (auto simp: pdevs_val_msum_pdevs aform_val_def)

lemma Inf_aform_msum_aform:

lemma Sup_aform_msum_aform:

definition "independent_from d Y = msum_aform d (0, zero_pdevs) Y"

definition "independent_aform X Y = independent_from (degree_aform X) Y"

lemma degree_zero_pdevs[simp]:
by (metis degree_least_nonzero pdevs_apply_zero_pdevs)

lemma independent_aform_Joints:
assumes "x  Affine X"
assumes "y  Affine Y"
shows "[x, y]  Joints [X, independent_aform X Y]"
using assms
unfolding Affine_def valuate_def Joints_def
apply safe
subgoal premises prems for e ea
using prems
by (intro image_eqI[where x="λi.  i  degree_aform X  e i  ea (i  degree_aform X)"])
(auto simp: aform_val_def pdevs_val_msum_pdevs Pi_iff
independent_aform_def independent_from_def intro!: pdevs_val_degree_cong)
done

lemma msum_aform_Joints:
assumes "d  degree_aform X"
assumes "X. X  set XS  d  degree_aform X"
assumes "(x#xs)  Joints (X#XS)"
assumes "y  Affine Y"
shows "((x + y)#x#xs)  Joints (msum_aform d X Y#X#XS)"
using assms
unfolding Joints_def valuate_def Affine_def
proof (safe, goal_cases)
case (1 e ea a b zs)
then show ?case
by (intro image_eqI[where x = "λi.  i  d  e i  ea (i  d)"])
(force simp: aform_val_def pdevs_val_msum_pdevs intro!: intro!: pdevs_val_degree_cong)+
qed

lemma Joints_msum_aform:
assumes "d  degree_aform X"
assumes "Y. Y  set YS  d  degree_aform Y"
shows "Joints (msum_aform d X Y#YS) = {((x + y)#ys) |x y ys. y  Affine Y  x#ys  Joints (X#YS)}"
unfolding Affine_def valuate_def Joints_def
proof (safe, goal_cases)
case (1 x e)
thus ?case
using assms
by (intro exI[where x = "aform_val e X"] exI[where x = "aform_val ((λi. e (i  d))) Y"])
next
case (2 x xa y ys e ea)
thus ?case using assms
by (intro image_eqI[where x="λi.  i  d  ea i  e (i  d)"])
(force simp: aform_val_def pdevs_val_msum_pdevs Pi_iff intro!: pdevs_val_degree_cong)+
qed

lemma Joints_singleton_image: "Joints [x] = (λx. [x]) ` Affine x"
by (auto simp: Joints_def Affine_def valuate_def)

lemma Collect_extract_image: "{g (f x y) |x y. P x y} = g ` {f x y |x y. P x y}"
by auto

lemma inj_Cons: "inj (λx. x#xs)"
by (auto intro!: injI)

lemma Joints_Nil[simp]: "Joints [] = {[]}"
by (force simp: Joints_def valuate_def)

lemma msum_pdevs_zero_ident[simp]:
by transfer (auto simp: msum_pdevs_raw_def)

lemma msum_aform_zero_ident[simp]: "msum_aform 0 (0, zero_pdevs) x = x"

lemma mem_Joints_singleton: "(x  Joints [X]) = (y. x = [y]  y  Affine X)"
by (auto simp: Affine_def valuate_def Joints_def)

lemma singleton_mem_Joints[simp]: "[x]  Joints [X]  x  Affine X"
by (auto simp: mem_Joints_singleton)

lemma msum_aform_Joints_without_first:
assumes "d  degree_aform X"
assumes "X. X  set XS  d  degree_aform X"
assumes "(x#xs)  Joints (X#XS)"
assumes "y  Affine Y"
assumes "z = x + y"
shows "z#xs  Joints (msum_aform d X Y#XS)"
unfolding z = x + y
using msum_aform_Joints[OF assms(1-4)]
by (force simp: Joints_def valuate_def)

lemma Affine_msum_aform:
assumes "d  degree_aform X"
shows "Affine (msum_aform d X Y) = {x + y |x y. x  Affine X  y  Affine Y}"
using Joints_msum_aform[OF assms, of Nil Y, simplified, unfolded mem_Joints_singleton]
by (auto simp add: Joints_singleton_image Collect_extract_image[where g="λx. [x]"]
inj_image_eq_iff[OF inj_Cons] )

lemma Affine_zero_pdevs[simp]: "Affine (0, zero_pdevs) = {0}"
by (force simp: Affine_def valuate_def aform_val_def)

lemma Affine_independent_aform:

by (auto simp: independent_aform_def independent_from_def Affine_msum_aform)

lemma
abs_diff_eq1:
fixes l u::"'a::ordered_euclidean_space"
shows "l  u  ¦u - l¦ = u - l"

lemma compact_sum:
fixes f :: "'a  'b::topological_space  'c::real_normed_vector"
assumes "finite I"
assumes "i. i  I  compact (S i)"
assumes "i. i  I  continuous_on (S i) (f i)"
assumes "I  J"
shows "compact {iI. f i (x i) | x. x  Pi J S}"
using assms
proof (induct I)
case empty
thus ?case
proof (cases "x. x  Pi J S")
case False
hence *: "{i{}. f i (x i) |x. x  Pi J S} = {}"
by (auto simp: Pi_iff)
show ?thesis unfolding * by simp
qed auto
next
case (insert a I)
hence "{iinsert a I. f i (xa i) |xa. xa  Pi J S}
= {x + y |x y. x  f a ` S a  y  {iI. f i (x i) |x. x  Pi J S}}"
proof safe
fix s x
assume "s  S a" "x  Pi J S"
thus "xa. f a s + (iI. f i (x i)) = (iinsert a I. f i (xa i))  xa  Pi J S"
using insert
by (auto intro!: exI[where x="x(a:=s)"] sum.cong)
qed force
also have "compact "
using insert
by (intro compact_sums) (auto intro!: compact_continuous_image)
finally show ?case .
qed

lemma compact_Affine:
fixes X::
shows "compact (Affine X)"
proof -
have "Affine X = {x + y|x y. x  {fst X}
y  {(i  {0..<degree_aform X}. e i *R pdevs_apply (snd X) i) | e. e  UNIV  {-1 .. 1}}}"
by (auto simp: Affine_def valuate_def aform_val_def pdevs_val_sum atLeast0LessThan)
also have "compact "
by (rule compact_sums) (auto intro!: compact_sum continuous_intros)
finally show ?thesis .
qed

lemma Joints2_JointsI:
"(xs, x)  Joints2 XS X  x#xs  Joints (X#XS)"
by (auto simp: Joints_def Joints2_def valuate_def)

subsection ‹Splitting›

definition "split_aform X i =
(let xi = pdevs_apply (snd X) i /R 2
in ((fst X - xi, pdev_upd (snd X) i xi), (fst X + xi, pdev_upd (snd X) i xi)))"

lemma split_aformE:
assumes
assumes "x = aform_val e X"
obtains err where "x = aform_val (e(i:=err)) (fst (split_aform X i))" "err  {-1 .. 1}"
| err where "x = aform_val (e(i:=err)) (snd (split_aform X i))" "err  {-1 .. 1}"
proof (atomize_elim)
let ?thesis = "(err. x = aform_val (e(i := err)) (fst (split_aform X i))  err  {- 1..1})
(err. x = aform_val (e(i := err)) (snd (split_aform X i))  err  {- 1..1})"
{
assume "pdevs_apply (snd X) i = 0"
hence "X = fst (split_aform X i)"
by (auto simp: split_aform_def intro!: prod_eqI pdevs_eqI)
with assms have ?thesis by (auto intro!: exI[where x="e i"])
} moreover {
assume "pdevs_apply (snd X) i  0"
hence [simp]: "degree_aform X > i"
by (rule degree_gt)
note assms(2)
also
have "aform_val e X = fst X + (i<degree_aform X. e i *R pdevs_apply (snd X) i)"
also
have rewr: "{..<degree_aform X} = {0..<degree_aform X} - {i}  {i}"
by auto
have "(i<degree_aform X. e i *R pdevs_apply (snd X) i) =
(i  {0..<degree_aform X} - {i}. e i *R pdevs_apply (snd X) i) +
e i *R pdevs_apply (snd X) i"
by (subst rewr, subst sum.union_disjoint) auto
finally have "x = fst X + " .
hence "x = aform_val (e(i:=2 * e i - 1)) (snd (split_aform X i))"
"x = aform_val (e(i:=2 * e i + 1)) (fst (split_aform X i))"
by (auto simp: aform_val_def split_aform_def Let_def pdevs_val_sum atLeast0LessThan
Diff_eq degree_pdev_upd if_distrib sum.If_cases field_simps
scaleR_left_distrib[symmetric])
moreover
have "2 * e i - 1  {-1 .. 1}  2 * e i + 1  {-1 .. 1}"
using assms by (auto simp: not_le Pi_iff dest!: spec[where x=i])
ultimately have ?thesis by blast
} ultimately show ?thesis by blast
qed

lemma pdevs_val_add: "pdevs_val (λi. e i + f i) xs = pdevs_val e xs + pdevs_val f xs"
by (auto simp: pdevs_val_pdevs_domain algebra_simps sum.distrib)

lemma pdevs_val_minus: "pdevs_val (λi. e i - f i) xs = pdevs_val e xs - pdevs_val f xs"
by (auto simp: pdevs_val_pdevs_domain algebra_simps sum_subtractf)

lemma pdevs_val_cmul: "pdevs_val (λi. u * e i) xs = u *R pdevs_val e xs"
by (auto simp: pdevs_val_pdevs_domain scaleR_sum_right)

lemma atLeastAtMost_absI: "- a  a  ¦x::real¦  ¦a¦  x  atLeastAtMost (- a) a"
by auto

lemma divide_atLeastAtMost_1_absI: "¦x::real¦  ¦a¦  x/a  {-1 .. 1}"
by (intro atLeastAtMost_absI) (auto simp: divide_le_eq_1)

lemma convex_scaleR_aux: "u + v = 1  u *R x + v *R x = (x::'a::real_vector)"

lemma convex_mult_aux: "u + v = 1  u * x + v * x = (x::real)"
using convex_scaleR_aux[of u v x] by simp

lemma convex_Affine: "convex (Affine X)"
proof (rule convexI)
fix x y::'a and u v::real
assume "x  Affine X" "y  Affine X" and convex: "0  u" "0  v" "u + v = 1"
then obtain e f where x: "x = aform_val e X"
and y: "y = aform_val f X"
by (auto simp: Affine_def valuate_def)
let ?conv = "λi. u * e i + v * f i"
{
fix i
have "¦?conv i¦  u * ¦e i¦ + v * ¦f i¦"
using convex by (intro order_trans[OF abs_triangle_ineq]) (simp add: abs_mult)
also have "  1"
using convex x y
by (intro convex_bound_le) (auto simp: Pi_iff abs_real_def)
finally have "?conv i  1" "-1  ?conv i"
by (auto simp: abs_real_def split: if_split_asm)
}
thus "u *R x + v *R y  Affine X"
using convex x y
by (auto simp: Affine_def valuate_def aform_val_def pdevs_val_add pdevs_val_cmul algebra_simps
convex_scaleR_aux intro!: image_eqI[where x="?conv"])
qed

lemma segment_in_aform_val:
assumes
assumes
shows "closed_segment (aform_val e X) (aform_val f X)  Affine X"
proof -
have "aform_val e X  Affine X" "aform_val f X  Affine X"
using assms by (auto simp: Affine_def valuate_def)
with convex_Affine[of X, simplified convex_contains_segment]
show ?thesis
by simp
qed

subsection ‹From List of Generators›

lift_definition pdevs_of_list::"'a::zero list  'a pdevs"
is "λxs i. if i < length xs then xs ! i else 0"
by auto

lemma pdevs_apply_pdevs_of_list:
"pdevs_apply (pdevs_of_list xs) i = (if i < length xs then xs ! i else 0)"
by transfer simp

lemma pdevs_apply_pdevs_of_list_Nil[simp]:

by transfer auto

lemma pdevs_apply_pdevs_of_list_Cons:
"pdevs_apply (pdevs_of_list (x # xs)) i =
(if i = 0 then x else pdevs_apply (pdevs_of_list xs) (i - 1))"
by transfer auto

lemma pdevs_domain_pdevs_of_list_Cons[simp]:
by (force simp: pdevs_apply_pdevs_of_list_Cons split: if_split_asm)

lemma pdevs_val_pdevs_of_list_eq[simp]:
"pdevs_val e (pdevs_of_list (x # xs)) = e 0 *R x + pdevs_val (e o (+) 1) (pdevs_of_list xs)"
proof -
have "pdevs_val e (pdevs_of_list (x # xs)) =
(ipdevs_domain (pdevs_of_list (x # xs))  {0}. e i *R x) +
(ipdevs_domain (pdevs_of_list (x # xs))  - {0}.
e i *R pdevs_apply (pdevs_of_list xs) (i - Suc 0))"
(is "_ = ?l + ?r")
by (simp add: pdevs_val_pdevs_domain if_distrib sum.If_cases pdevs_apply_pdevs_of_list_Cons)
also
have "?r = (ipdevs_domain (pdevs_of_list xs). e (Suc i) *R pdevs_apply (pdevs_of_list xs) i)"
by (rule sum.reindex_cong[of "λi. i  "]) auto
also have " = pdevs_val (e o (+) 1) (pdevs_of_list xs)"
also have "?l = (i{0}. e i *R x)"
by (rule sum.mono_neutral_cong_left) auto
also have " = e 0 *R x" by simp
finally show ?thesis .
qed

lemma
less_degree_pdevs_of_list_imp_less_length:
assumes "i < degree (pdevs_of_list xs)"
shows "i < length xs"
proof -
from assms have "pdevs_apply (pdevs_of_list xs) (degree (pdevs_of_list xs) - 1)  0"
by (metis degree_least_nonzero less_nat_zero_code)
hence "degree (pdevs_of_list xs) - 1 < length xs"
by (simp add: pdevs_apply_pdevs_of_list split: if_split_asm)
with assms show ?thesis
by simp
qed

lemma tdev_pdevs_of_list[simp]: "tdev (pdevs_of_list xs) = sum_list (map abs xs)"
by (auto simp: tdev_def pdevs_apply_pdevs_of_list sum_list_sum_nth
less_degree_pdevs_of_list_imp_less_length
intro!: sum.mono_neutral_cong_left degree_gt)

lemma pdevs_of_list_Nil[simp]:
by (auto intro!: pdevs_eqI)

lemma pdevs_val_inj_sumI:
fixes K::"'a set" and g::"'a  nat"
assumes "finite K"
assumes "inj_on g K"
assumes "pdevs_domain x  g ` K"
assumes "i. i  K  g i  pdevs_domain x  f i = 0"
assumes "i. i  K  g i  pdevs_domain x  f i = e (g i) *R pdevs_apply x (g i)"
shows "pdevs_val e x = (iK. f i)"
proof -
have [simp]: "inj_on (the_inv_into K g) (pdevs_domain x)"
using assms
by (auto simp: intro!: subset_inj_on[OF inj_on_the_inv_into])
{
fix y assume y: "y  pdevs_domain x"
have g_inv: "g (the_inv_into K g y) = y"
by (meson assms(2) assms(3) y f_the_inv_into_f subset_eq)
have inv_in: "the_inv_into K g y  K"
by (meson assms(2) assms(3) y subset_iff in_pdevs_domain the_inv_into_into)
have inv3: "the_inv_into (pdevs_domain x) (the_inv_into K g) (the_inv_into K g y) =
g (the_inv_into K g y)"
using assms y
by (subst the_inv_into_f_f) (auto simp: f_the_inv_into_f[OF assms(2)])
note g_inv inv_in inv3
} note this[simp]
have "pdevs_val e x = (ipdevs_domain x. e i *R pdevs_apply x i)"
also have " = (i  the_inv_into K g ` pdevs_domain x. e (g i) *R pdevs_apply x (g i))"
by (rule sum.reindex_cong[OF inj_on_the_inv_into]) auto
also have " = (iK. f i)"
using assms
by (intro sum.mono_neutral_cong_left) (auto simp: the_inv_into_image_eq)
finally show ?thesis .
qed

lemma pdevs_domain_pdevs_of_list_le:
by (auto simp: pdevs_apply_pdevs_of_list split: if_split_asm)

lemma pdevs_val_zip: "pdevs_val e (pdevs_of_list xs) = ((i,x)zip [0..<length xs] xs. e i *R x)"
by (auto simp: sum_list_distinct_conv_sum_set
in_set_zip image_fst_zip pdevs_apply_pdevs_of_list distinct_zipI1
intro!: pdevs_val_inj_sumI[of _ fst]
split: if_split_asm)

lemma pdevs_val_map:
pdevs_val e (pdevs_of_list xs)
= (n[0..<length xs]. e n *R xs ! n)
proof -
have map2 (λi. (*R) (e i)) [0..<length xs] xs =
map (λn. e n *R xs ! n) [0..<length xs]
by (rule nth_equalityI) simp_all
then show ?thesis
qed

lemma scaleR_sum_list:
fixes xs::"'a::real_vector list"
shows "a *R sum_list xs = sum_list (map (scaleR a) xs)"
by (induct xs) (auto simp: algebra_simps)

lemma pdevs_val_const_pdevs_of_list: "pdevs_val (λ_. c) (pdevs_of_list xs) = c *R sum_list xs"
unfolding pdevs_val_zip split_beta' scaleR_sum_list
by (rule arg_cong) (auto intro!: nth_equalityI)

lemma pdevs_val_partition:
assumes "e  UNIV  I"
obtains f g where "pdevs_val e (pdevs_of_list xs) =
pdevs_val f (pdevs_of_list (filter p xs)) +
pdevs_val g (pdevs_of_list (filter (Not o p) xs))"
"f  UNIV  I"
"g  UNIV  I"
proof -
obtain i where i: "i  I"
by (metis assms funcset_mem iso_tuple_UNIV_I)
let ?zip = "zip [0..<length xs] xs"
define part where "part = partition (p  snd) ?zip"
let ?f =
"(λn. if n < degree (pdevs_of_list (filter p xs)) then e (map fst (fst part) ! n) else i)"
let ?g =
"(λn. if n < degree (pdevs_of_list (filter (Not  p) xs))
then e (map fst (snd part) ! n)
else i)"
show ?thesis
proof
have "pdevs_val e (pdevs_of_list xs) = ((i,x)?zip. e i *R x)"
by (rule pdevs_val_zip)
also have " = ((i, x)set ?zip. e i *R x)"
also
have [simp]: "set (fst part)  set (snd part) = {}"
by (auto simp: part_def)
from partition_set[of "p o snd" ?zip "fst part" "snd part"]
have "set ?zip = set (fst part)  set (snd part)"
by (auto simp: part_def)
also have "(aset (fst part)  set (snd part). case a of (i, x)  e i *R x) =
((i, x)set (fst part). e i *R x) + ((i, x)set (snd part). e i *R x)"
by (auto simp: split_beta sum_Un)
also
have "((i, x)set (fst part). e i *R x) = ((i, x)(fst part). e i *R x)"
by (simp add: sum_list_distinct_conv_sum_set distinct_zipI1 part_def)
also have " = (i<length (fst part). case (fst part ! i) of (i, x)  e i *R x)"
by (subst sum_list_sum_nth) (simp add: split_beta' atLeast0LessThan)
also have " =
pdevs_val (λn. e (map fst (fst part) ! n)) (pdevs_of_list (map snd (fst part)))"
by (force
simp: pdevs_val_zip sum_list_distinct_conv_sum_set distinct_zipI1 split_beta' in_set_zip
intro!:
sum.reindex_cong[where l=fst] image_eqI[where x = "(x, map snd (fst part) ! x)" for x])
also
have "((i, x)set (snd part). e i *R x) = ((i, x)(snd part). e i *R x)"
by (simp add: sum_list_distinct_conv_sum_set distinct_zipI1 part_def)
also have " = (i<length (snd part). case (snd part ! i) of (i, x)  e i *R x)"
by (subst sum_list_sum_nth) (simp add: split_beta' atLeast0LessThan)
also have " =
pdevs_val (λn. e (map fst (snd part) ! n)) (pdevs_of_list (map snd (snd part)))"
by (force simp: pdevs_val_zip sum_list_distinct_conv_sum_set distinct_zipI1 split_beta'
in_set_zip
intro!: sum.reindex_cong[where l=fst]
image_eqI[where x = "(x, map snd (snd part) ! x)" for x])
also
have "pdevs_val (λn. e (map fst (fst part) ! n)) (pdevs_of_list (map snd (fst part))) =
pdevs_val (λn.
if n < degree (pdevs_of_list (map snd (fst part))) then e (map fst (fst part) ! n) else i)
(pdevs_of_list (map snd (fst part)))"
by (rule pdevs_val_degree_cong) simp_all
also
have "pdevs_val (λn. e (map fst (snd part) ! n)) (pdevs_of_list (map snd (snd part))) =
pdevs_val (λn.
if n < degree (pdevs_of_list (map snd (snd part))) then e (map fst (snd part) ! n) else i)
(pdevs_of_list (map snd (snd part)))"
by (rule pdevs_val_degree_cong) simp_all
also have "map snd (snd part) = filter (Not o p) xs"
by (simp add: part_def filter_map[symmetric] o_assoc)
also have "map snd (fst part) = filter p xs"
finally
show
"pdevs_val e (pdevs_of_list xs) =
pdevs_val ?f (pdevs_of_list (filter p xs)) +
pdevs_val ?g (pdevs_of_list (filter (Not  p) xs))" .
show "?f  UNIV  I" "?g  UNIV  I"
using assms iI
by (auto simp: Pi_iff)
qed
qed

lemma pdevs_apply_pdevs_of_list_append:
"pdevs_apply (pdevs_of_list (xs @ zs)) i =
(if i < length xs
then pdevs_apply (pdevs_of_list xs) i else pdevs_apply (pdevs_of_list zs) (i - length xs))"
by (auto simp: pdevs_apply_pdevs_of_list nth_append)

lemma degree_pdevs_of_list_le_length[intro, simp]: "degree (pdevs_of_list xs)  length xs"
by (metis less_irrefl_nat le_less_linear less_degree_pdevs_of_list_imp_less_length)

lemma degree_pdevs_of_list_append:
"degree (pdevs_of_list (xs @ ys))  length xs + degree (pdevs_of_list ys)"
by (rule degree_le) (auto simp: pdevs_apply_pdevs_of_list_append)

lemma pdevs_val_pdevs_of_list_append:
assumes "f  UNIV  I"
assumes "g  UNIV  I"
obtains e where
"pdevs_val f (pdevs_of_list xs) + pdevs_val g (pdevs_of_list ys) =
pdevs_val e (pdevs_of_list (xs @ ys))"
"e  UNIV  I"
proof
let ?e = "(λi. if i < length xs then f i else g (i - length xs))"
have f: "pdevs_val f (pdevs_of_list xs) =
(i{..<length xs}. ?e i *R pdevs_apply (pdevs_of_list (xs @ ys)) i)"
by (auto simp: pdevs_val_sum degree_gt pdevs_apply_pdevs_of_list_append
intro: sum.mono_neutral_cong_left)
have g: "pdevs_val g (pdevs_of_list ys) =
(i=length xs ..<length xs + degree (pdevs_of_list ys).
?e i *R pdevs_apply (pdevs_of_list (xs @ ys)) i)"
(is "_ = ?sg")
by (auto simp: pdevs_val_sum pdevs_apply_pdevs_of_list_append
intro!: inj_onI image_eqI[where x="length xs + x" for x]
sum.reindex_cong[where l="λi. i - length xs"])
show "pdevs_val f (pdevs_of_list xs) + pdevs_val g (pdevs_of_list ys) =
pdevs_val ?e (pdevs_of_list (xs @ ys))"
unfolding f g
by (subst sum.union_disjoint[symmetric])
(force simp: pdevs_val_sum ivl_disj_un degree_pdevs_of_list_append
intro!: sum.mono_neutral_cong_right
split: if_split_asm)+
show "?e  UNIV  I"
using assms by (auto simp: Pi_iff)
qed

lemma
sum_general_mono:
assumes [simp,intro]: "finite s" "finite t"
assumes f: "x. x  s - t  f x  0"
assumes g: "x. x  t - s  g x  0"
assumes fg: "x. x  s  t  f x  g x"
shows "(x  s. f x)  (x  t. g x)"
proof -
have "s = (s - t)  (s  t)" and [intro, simp]: "(s - t)  (s  t) = {}" by auto
hence "(x  s. f x) = (x  s - t  s  t. f x)"
using assms by simp
also have " = (x  s - t. f x) + (x  s  t. f x)"
also have "(x  s - t. f x)  0"
by (auto intro!: sum_nonpos f)
also have "0  (x  t - s. g x)"
by (auto intro!: sum_nonneg g)
also have "(x  s  t. f x)  (x  s  t. g x)"
by (auto intro!: sum_mono fg)
also
have [intro, simp]: "(t - s)  (s  t) = {}" by auto
hence "sum g (t - s) + sum g (s  t) = sum g ((t - s)  (s  t))"
also have " = sum g t"
by (auto intro!: sum.cong)
finally show ?thesis by simp
qed

lemma degree_pdevs_of_list_eq':
degree (pdevs_of_list xs) = Min {n. n  length xs  (m. n  m  m < length xs  xs ! m = 0)}
apply (rule Least_equality)
apply auto
apply (subst (asm) Min_le_iff)
apply auto
apply (subst Min_le_iff)
apply auto
apply (metis le_cases not_less)
done

lemma pdevs_val_permuted:
pdevs_val (e  p) (pdevs_of_list (permute_list p xs)) = pdevs_val e (pdevs_of_list xs) (is ?r = ?s)
if perm: p permutes {..<length xs}
proof -
from that have