Theory HOL-Analysis.Real_Analytic_Inverse
section ‹The formal-series local inverse of a real-analytic map (majorant method)›
text ‹
For a real-analytic self-map ‹f› of a Euclidean space with ‹f 0 = 0› and
‹Df(0) = id›, we construct a convergent power series ‹h› with ‹f (h y) = y› near ‹0›.
Writing ‹f = id - φ›, the coefficients of ‹h› are determined degree by degree by
‹h y = y + φ (h y)› (‹ra_inverse_coeffs›); a bootstrap argument in the style of Gou\"ezel bounds
them by a convergent majorant.
›
theory Real_Analytic_Inverse
imports Real_Analytic
begin
subsection ‹A fixed enumeration of the Euclidean basis›
definition ra_basis_list :: "'a::euclidean_space list" where
"ra_basis_list = (SOME l. set l = (Basis::'a set) ∧ distinct l)"
lemma ra_basis_list:
"set (ra_basis_list::'a::euclidean_space list) = (Basis::'a set)"
"distinct (ra_basis_list::'a::euclidean_space list)"
proof -
obtain l :: "'a list" where l: "set l = (Basis::'a set) ∧ distinct l"
using finite_distinct_list[OF finite_Basis] by blast
have "set (ra_basis_list::'a list) = (Basis::'a set) ∧ distinct (ra_basis_list::'a list)"
unfolding ra_basis_list_def by (rule someI[of _ l]) (rule l)
thus "set (ra_basis_list::'a list) = (Basis::'a set)"
"distinct (ra_basis_list::'a list)" by simp_all
qed
subsection ‹Unit multi-indices and the concrete identity coefficient family›
definition ra_idx_unit :: "'a::euclidean_space ⇒ ('a ⇒ nat)" where
"ra_idx_unit b = (λx. if x = b then 1 else 0)"
lemma ra_idx_unit_in_ra_idx: "b ∈ Basis ⟹ ra_idx_unit b ∈ ra_idx"
by (auto simp: ra_idx_unit_def ra_idx_def)
lemma ra_deg_idx_unit: "b ∈ Basis ⟹ ra_deg (ra_idx_unit b) = 1"
by (simp add: ra_deg_def ra_idx_unit_def sum.remove[where x = b])
lemma inj_on_idx_unit: "inj_on ra_idx_unit (Basis :: 'a::euclidean_space set)"
proof (rule inj_onI)
fix b c :: 'a
assume "b ∈ Basis" "c ∈ Basis" and eq: "ra_idx_unit b = ra_idx_unit c"
have h: "ra_idx_unit b b = ra_idx_unit c b" using eq by simp
show "b = c"
proof (rule ccontr)
assume "b ≠ c"
thus False using h by (simp add: ra_idx_unit_def)
qed
qed
lemma ra_idx_unit_neq_idx_zero: "ra_idx_unit b ≠ ra_idx_zero"
proof
assume "ra_idx_unit b = ra_idx_zero"
hence "ra_idx_unit b b = ra_idx_zero b" by simp
thus False by (simp add: ra_idx_unit_def ra_idx_zero_def)
qed
lemma ra_monomial_idx_unit:
"b ∈ Basis ⟹ ra_monomial y (ra_idx_unit b) = y ∙ b" for y :: "'a::euclidean_space"
proof -
assume b: "b ∈ Basis"
have "ra_monomial y (ra_idx_unit b) =
(y ∙ b) ^ (ra_idx_unit b b) * (∏c∈Basis - {b}. (y ∙ c) ^ (ra_idx_unit b c))"
using b by (simp add: ra_monomial_def prod.remove)
also have "… = y ∙ b"
by (simp add: ra_idx_unit_def)
finally show ?thesis .
qed
text ‹Classification of the degree-one multi-indices.›
lemma ra_deg_one_unit:
fixes α :: "'a::euclidean_space ⇒ nat"
assumes a: "α ∈ ra_idx" and d1: "ra_deg α = 1"
obtains b where "b ∈ Basis" "α = ra_idx_unit b"
proof -
have s1: "(∑b∈(Basis::'a set). α b) = 1"
using d1 by (simp add: ra_deg_def)
have "∃b∈(Basis::'a set). α b ≠ 0"
proof (rule ccontr)
assume "¬ (∃b∈(Basis::'a set). α b ≠ 0)"
hence "(∑b∈(Basis::'a set). α b) = 0" by simp
thus False using s1 by simp
qed
then obtain b where b: "b ∈ Basis" and nz: "α b ≠ 0" by blast
have ble: "α b ≤ 1"
proof -
have "α b ≤ (∑c∈(Basis::'a set). α c)"
using b by (intro member_le_sum) auto
thus ?thesis using s1 by simp
qed
have b1: "α b = 1"
using nz ble by simp
have rest0: "(∑c∈Basis - {b}. α c) = 0"
using s1 b b1 by (simp add: sum.remove[where x = b])
have z: "α c = 0" if "c ∈ Basis" "c ≠ b" for c
proof -
have "α c ≤ (∑c∈Basis - {b}. α c)"
using that by (intro member_le_sum) auto
thus ?thesis using rest0 by simp
qed
have "α = ra_idx_unit b"
proof (rule ext)
fix x
show "α x = ra_idx_unit b x"
proof (cases "x ∈ Basis")
case True thus ?thesis using b1 z by (auto simp: ra_idx_unit_def)
next
case False
hence "α x = 0" using a by (auto simp: ra_idx_def)
moreover have "x ≠ b" using False b by blast
ultimately show ?thesis by (simp add: ra_idx_unit_def)
qed
qed
thus ?thesis using b that by blast
qed
text ‹The concrete identity coefficient family: ‹∑⇩α y⇧α (ra_coeff_id α) = y›.›
definition ra_coeff_id :: "('a::euclidean_space ⇒ nat) ⇒ 'a" where
"ra_coeff_id = (λα. ∑b∈Basis. if α = ra_idx_unit b then b else 0)"
lemma ra_coeff_id_unit: "b ∈ Basis ⟹ ra_coeff_id (ra_idx_unit b) = b"
proof -
assume b: "b ∈ Basis"
have "ra_coeff_id (ra_idx_unit b) = (∑c∈Basis. if c = b then c else 0)"
unfolding ra_coeff_id_def
by (rule sum.cong[OF refl])
(use b inj_on_idx_unit in ‹auto simp: inj_on_def›)
also have "… = b"
using b by simp
finally show ?thesis .
qed
lemma ra_coeff_id_off_units: "α ∉ ra_idx_unit ` Basis ⟹ ra_coeff_id α = 0"
unfolding ra_coeff_id_def by (rule sum.neutral) auto
lemma ra_coeff_id_idx_zero: "ra_coeff_id ra_idx_zero = 0"
by (rule ra_coeff_id_off_units, metis image_iff ra_idx_unit_neq_idx_zero)
lemma ra_coeff_id_deg: "ra_coeff_id α ≠ 0 ⟹ ra_deg α = 1"
proof -
assume nz: "ra_coeff_id α ≠ 0"
have "α ∈ ra_idx_unit ` Basis"
using nz ra_coeff_id_off_units by blast
then obtain b where "b ∈ Basis" "α = ra_idx_unit b" by blast
thus "ra_deg α = 1" by (simp add: ra_deg_idx_unit)
qed
lemma ra_coeff_id_series:
fixes y :: "'a::euclidean_space"
shows "((λα. ra_monomial y α *⇩R ra_coeff_id α) has_sum y) ra_idx"
proof (rule has_sum_finite_neutralI)
show "finite (ra_idx_unit ` (Basis :: 'a set))"
by simp
show "ra_idx_unit ` (Basis :: 'a set) ⊆ ra_idx"
using ra_idx_unit_in_ra_idx by blast
have "(∑α∈ra_idx_unit ` Basis. ra_monomial y α *⇩R ra_coeff_id α) =
(∑b∈Basis. ra_monomial y (ra_idx_unit b) *⇩R ra_coeff_id (ra_idx_unit b))"
by (rule sum.reindex_cong[where l = ra_idx_unit, OF inj_on_idx_unit refl]) simp
also have "… = (∑b∈Basis. (y ∙ b) *⇩R b)"
by (rule sum.cong[OF refl]) (simp add: ra_monomial_idx_unit ra_coeff_id_unit)
also have "… = y"
by (simp add: euclidean_representation)
finally show "y = (∑α∈ra_idx_unit ` Basis. ra_monomial y α *⇩R ra_coeff_id α)"
by simp
show "⋀α. α ∈ ra_idx - ra_idx_unit ` Basis ⟹ ra_monomial y α *⇩R ra_coeff_id α = 0"
by (simp add: ra_coeff_id_off_units)
qed
lemma norm_coeff_id_le: "norm (ra_coeff_id α) ≤ 1"
proof (cases "α ∈ ra_idx_unit ` Basis")
case True
then obtain b where b: "b ∈ Basis" and e: "α = ra_idx_unit b" by blast
show ?thesis using b by (simp add: e ra_coeff_id_unit)
next
case False
thus ?thesis by (simp add: ra_coeff_id_off_units)
qed
subsection ‹Cauchy-product support helpers›
lemma ra_idx_below_ra_idx: "α ∈ ra_idx_below γ ⟹ α ∈ ra_idx"
by (simp add: ra_idx_below_def)
lemma self_in_idx_below: "γ ∈ ra_idx ⟹ γ ∈ ra_idx_below γ"
by (simp add: ra_idx_below_def ra_idx_le_def)
lemma ra_idx_zero_in_idx_below: "γ ∈ ra_idx ⟹ ra_idx_zero ∈ ra_idx_below γ"
by (simp add: ra_idx_below_def ra_idx_le_def ra_idx_zero_def ra_idx_zero_in, simp add: ra_idx_def)
lemma ra_idx_diff_idx_zero: "ra_idx_diff γ ra_idx_zero = γ"
by (simp add: ra_idx_diff_def ra_idx_zero_def)
lemma ra_idx_diff_self: "ra_idx_diff γ γ = ra_idx_zero"
by (simp add: ra_idx_diff_def ra_idx_zero_def)
lemma ra_idx_add_idx_diff: "α ∈ ra_idx_below γ ⟹ ra_idx_add α (ra_idx_diff γ α) = γ"
proof (rule ext)
fix b
assume "α ∈ ra_idx_below γ"
hence "α b ≤ γ b" by (simp add: ra_idx_below_def ra_idx_le_def)
thus "ra_idx_add α (ra_idx_diff γ α) b = γ b" by (simp add: ra_idx_add_def ra_idx_diff_def)
qed
lemma ra_idx_diff_idx_add: "ra_idx_diff (ra_idx_add α δ) α = δ"
by (rule ext) (simp add: ra_idx_add_def ra_idx_diff_def)
lemma ra_deg_idx_add: "ra_deg (ra_idx_add α δ) = ra_deg α + ra_deg δ"
by (simp add: ra_deg_def ra_idx_add_def sum.distrib)
lemma ra_idx_add_in_idx_below: "α ∈ ra_idx ⟹ α ∈ ra_idx_below (ra_idx_add α δ)"
by (simp add: ra_idx_below_def ra_idx_le_def ra_idx_add_def)
lemma ra_idx_diff_deg_eq:
assumes "α ∈ ra_idx_below γ" and "ra_deg (ra_idx_diff γ α) = 0" and "γ ∈ ra_idx"
shows "α = γ"
proof -
have "ra_idx_diff γ α ∈ ra_idx" using assms(3) by (rule idx_sub)
hence sz: "ra_idx_diff γ α = ra_idx_zero" using assms(2) by (simp add: ra_deg_eq0_iff)
have le: "γ b ≤ α b" for b
proof -
have "ra_idx_diff γ α b = ra_idx_zero b" using sz by simp
thus ?thesis by (simp add: ra_idx_diff_def ra_idx_zero_def)
qed
have ge: "⋀b. α b ≤ γ b" using assms(1) by (simp add: ra_idx_below_def ra_idx_le_def)
show ?thesis by (rule ext) (use le ge le_antisym in blast)
qed
text ‹The unit ‹ra_coeff_one› is a two-sided identity for the Cauchy product (on ‹ra_idx›).›
lemma ra_cauchy_prod_coeff_one_right: "γ ∈ ra_idx ⟹ ra_cauchy_prod u ra_coeff_one γ = u γ"
proof -
assume g: "γ ∈ ra_idx"
have fin: "finite (ra_idx_below γ)" by (rule idx_lower_fin)
have "ra_cauchy_prod u ra_coeff_one γ = (∑α∈ra_idx_below γ. u α * ra_coeff_one (ra_idx_diff γ α))"
by (simp add: ra_cauchy_prod_def)
also have "… = (∑α∈{γ}. u α * ra_coeff_one (ra_idx_diff γ α))"
proof (rule sum.mono_neutral_right[OF fin])
show "{γ} ⊆ ra_idx_below γ" using self_in_idx_below[OF g] by blast
show "∀α∈ra_idx_below γ - {γ}. u α * ra_coeff_one (ra_idx_diff γ α) = 0"
proof
fix α assume a: "α ∈ ra_idx_below γ - {γ}"
have "ra_idx_diff γ α ≠ ra_idx_zero"
proof
assume "ra_idx_diff γ α = ra_idx_zero"
hence "ra_deg (ra_idx_diff γ α) = 0" by (simp add: ra_deg_def ra_idx_zero_def)
hence "α = γ" using a g by (intro ra_idx_diff_deg_eq) auto
thus False using a by blast
qed
thus "u α * ra_coeff_one (ra_idx_diff γ α) = 0" by (simp add: ra_coeff_one_def)
qed
qed
also have "… = u γ"
by (simp add: ra_idx_diff_self ra_coeff_one_def)
finally show ?thesis .
qed
lemma ra_cauchy_prod_coeff_one_left: "γ ∈ ra_idx ⟹ ra_cauchy_prod ra_coeff_one v γ = v γ"
proof -
assume g: "γ ∈ ra_idx"
have fin: "finite (ra_idx_below γ)" by (rule idx_lower_fin)
have "ra_cauchy_prod ra_coeff_one v γ = (∑α∈ra_idx_below γ. ra_coeff_one α * v (ra_idx_diff γ α))"
by (simp add: ra_cauchy_prod_def)
also have "… = (∑α∈{ra_idx_zero}. ra_coeff_one α * v (ra_idx_diff γ α))"
proof (rule sum.mono_neutral_right[OF fin])
show "{ra_idx_zero} ⊆ ra_idx_below γ" using ra_idx_zero_in_idx_below[OF g] by blast
show "∀α∈ra_idx_below γ - {ra_idx_zero}. ra_coeff_one α * v (ra_idx_diff γ α) = 0"
by (simp add: ra_coeff_one_def)
qed
also have "… = v γ"
by (simp add: ra_idx_diff_idx_zero ra_coeff_one_def)
finally show ?thesis .
qed
subsection ‹Valuation (vanishing below a degree) under Cauchy products›
text ‹‹ra_vanish_below u p›: the scalar family ‹u› has no coefficients of degree ‹< p›.›
definition ra_vanish_below :: "(('a::euclidean_space ⇒ nat) ⇒ real) ⇒ nat ⇒ bool" where
"ra_vanish_below u p ⟷ (∀α. α ∈ ra_idx ⟶ ra_deg α < p ⟶ u α = 0)"
lemma ra_vanish_below_0: "ra_vanish_below u 0"
by (simp add: ra_vanish_below_def)
lemma ra_vanish_below_mono: "ra_vanish_below u p ⟹ q ≤ p ⟹ ra_vanish_below u q"
by (auto simp: ra_vanish_below_def)
lemma ra_cauchy_prod_vanish:
assumes u: "ra_vanish_below u p" and v: "ra_vanish_below v q"
shows "ra_vanish_below (ra_cauchy_prod u v) (p + q)"
unfolding ra_vanish_below_def
proof (intro allI impI)
fix γ :: "'a ⇒ nat"
assume g: "γ ∈ ra_idx" and dg: "ra_deg γ < p + q"
have "ra_cauchy_prod u v γ = (∑α∈ra_idx_below γ. u α * v (ra_idx_diff γ α))"
by (simp add: ra_cauchy_prod_def)
also have "… = 0"
proof (rule sum.neutral, rule ballI)
fix α assume a: "α ∈ ra_idx_below γ"
have ara: "α ∈ ra_idx" using a by (rule ra_idx_below_ra_idx)
have dra: "ra_idx_diff γ α ∈ ra_idx" using g by (rule idx_sub)
have split: "ra_deg γ = ra_deg α + ra_deg (ra_idx_diff γ α)"
using a by (rule ra_deg_split)
have "ra_deg α < p ∨ ra_deg (ra_idx_diff γ α) < q"
using dg split by linarith
thus "u α * v (ra_idx_diff γ α) = 0"
using u v ara dra by (auto simp: ra_vanish_below_def)
qed
finally show "ra_cauchy_prod u v γ = 0" .
qed
lemma ra_cauchy_pow_vanish:
assumes u: "ra_vanish_below u 1"
shows "ra_vanish_below (ra_cauchy_pow u n) n"
proof (induction n)
case 0
show ?case by (simp add: ra_cauchy_pow_0 ra_vanish_below_0)
next
case (Suc n)
have "ra_vanish_below (ra_cauchy_prod u (ra_cauchy_pow u n)) (1 + n)"
by (rule ra_cauchy_prod_vanish[OF u Suc.IH])
thus ?case by (simp add: ra_cauchy_pow_Suc)
qed
subsection ‹Degree locality of Cauchy products and powers›
text ‹If two pairs of families agree up to certain degrees (and have the stated
valuations), their Cauchy products agree up to the corresponding degree.›
lemma ra_cauchy_prod_local:
fixes u u' v v' :: "('a::euclidean_space ⇒ nat) ⇒ real"
assumes up: "ra_vanish_below u p" and up': "ra_vanish_below u' p"
and vq: "ra_vanish_below v q" and vq': "ra_vanish_below v' q"
and uu': "⋀α. α ∈ ra_idx ⟹ ra_deg α ≤ Du ⟹ u α = u' α"
and vv': "⋀δ. δ ∈ ra_idx ⟹ ra_deg δ ≤ Dv ⟹ v δ = v' δ"
and g: "γ ∈ ra_idx" and dgu: "ra_deg γ ≤ Du + q" and dgv: "ra_deg γ ≤ Dv + p"
shows "ra_cauchy_prod u v γ = ra_cauchy_prod u' v' γ"
proof -
have "(∑α∈ra_idx_below γ. u α * v (ra_idx_diff γ α)) = (∑α∈ra_idx_below γ. u' α * v' (ra_idx_diff γ α))"
proof (rule sum.cong[OF refl])
fix α assume a: "α ∈ ra_idx_below γ"
have ara: "α ∈ ra_idx" using a by (rule ra_idx_below_ra_idx)
have dra: "ra_idx_diff γ α ∈ ra_idx" using g by (rule idx_sub)
have split: "ra_deg γ = ra_deg α + ra_deg (ra_idx_diff γ α)"
using a by (rule ra_deg_split)
show "u α * v (ra_idx_diff γ α) = u' α * v' (ra_idx_diff γ α)"
proof (cases "ra_deg α < p")
case True
thus ?thesis
using up up' ara by (simp add: ra_vanish_below_def)
next
case False
note ap = False
show ?thesis
proof (cases "ra_deg (ra_idx_diff γ α) < q")
case True
thus ?thesis
using vq vq' dra by (simp add: ra_vanish_below_def)
next
case False
have da: "ra_deg α ≤ Du"
using ap False split dgu by linarith
have dd: "ra_deg (ra_idx_diff γ α) ≤ Dv"
using ap False split dgv by linarith
show ?thesis
using uu'[OF ara da] vv'[OF dra dd] by simp
qed
qed
qed
thus ?thesis by (simp add: ra_cauchy_prod_def)
qed
lemma ra_cauchy_pow_local:
fixes u u' :: "('a::euclidean_space ⇒ nat) ⇒ real"
assumes u1: "ra_vanish_below u 1" and u1': "ra_vanish_below u' 1"
and uu': "⋀α. α ∈ ra_idx ⟹ ra_deg α ≤ D ⟹ u α = u' α"
and n1: "1 ≤ n"
and g: "γ ∈ ra_idx" and dg: "ra_deg γ ≤ D + n - 1"
shows "ra_cauchy_pow u n γ = ra_cauchy_pow u' n γ"
using n1 g dg
proof (induction n arbitrary: γ)
case 0
thus ?case by simp
next
case (Suc n)
show ?case
proof (cases "n = 0")
case True
have "ra_cauchy_pow u (Suc 0) γ = ra_cauchy_prod u ra_coeff_one γ"
by (simp add: ra_cauchy_pow_Suc ra_cauchy_pow_0)
also have "… = u γ" using Suc.prems(2) by (rule ra_cauchy_prod_coeff_one_right)
also have "… = u' γ"
using Suc.prems(2,3) True by (intro uu') simp_all
also have "… = ra_cauchy_prod u' ra_coeff_one γ"
using Suc.prems(2) by (simp add: ra_cauchy_prod_coeff_one_right)
also have "… = ra_cauchy_pow u' (Suc 0) γ"
by (simp add: ra_cauchy_pow_Suc ra_cauchy_pow_0)
finally show ?thesis using True by simp
next
case False
hence n1': "1 ≤ n" by simp
have IH: "⋀δ. δ ∈ ra_idx ⟹ ra_deg δ ≤ D + n - 1 ⟹ ra_cauchy_pow u n δ = ra_cauchy_pow u' n δ"
using Suc.IH n1' by blast
have "ra_cauchy_prod u (ra_cauchy_pow u n) γ = ra_cauchy_prod u' (ra_cauchy_pow u' n) γ"
proof (rule ra_cauchy_prod_local[where p = 1 and q = n and Du = D and Dv = "D + n - 1"])
show "ra_vanish_below u 1" by (rule u1)
show "ra_vanish_below u' 1" by (rule u1')
show "ra_vanish_below (ra_cauchy_pow u n) n" by (rule ra_cauchy_pow_vanish[OF u1])
show "ra_vanish_below (ra_cauchy_pow u' n) n" by (rule ra_cauchy_pow_vanish[OF u1'])
show "⋀α. α ∈ ra_idx ⟹ ra_deg α ≤ D ⟹ u α = u' α" by (rule uu')
show "⋀δ. δ ∈ ra_idx ⟹ ra_deg δ ≤ D + n - 1 ⟹ ra_cauchy_pow u n δ = ra_cauchy_pow u' n δ"
by (rule IH)
show "γ ∈ ra_idx" by (rule Suc.prems(2))
show "ra_deg γ ≤ D + n" using Suc.prems(3) n1' by simp
show "ra_deg γ ≤ (D + n - 1) + 1" using Suc.prems(3) n1' by simp
qed
thus ?thesis by (simp add: ra_cauchy_pow_Suc)
qed
qed
subsection ‹Canonical monomial-composition coefficients along the basis list›
text ‹‹ra_mono_coeffs_list c β l› is the coefficient family of ‹y ↦ ∏b←l. (H y ∙ b) ^ β b›
when ‹c› is one for ‹H›, built by iterated Cauchy products along ‹l›.›
fun ra_mono_coeffs_list :: "(('a::euclidean_space ⇒ nat) ⇒ 'a) ⇒ ('a ⇒ nat) ⇒ 'a list
⇒ (('a ⇒ nat) ⇒ real)" where
"ra_mono_coeffs_list c β [] = ra_coeff_one"
| "ra_mono_coeffs_list c β (b # bs) = ra_cauchy_prod (ra_cauchy_pow (λα. c α ∙ b) (β b)) (ra_mono_coeffs_list c β bs)"
lemma ra_mono_coeffs_list_series:
fixes c :: "('a::euclidean_space ⇒ nat) ⇒ 'a" and H :: "'a ⇒ 'a"
assumes VC: "⋀y. dist y (0::'a) < r ⟹
((λα. ra_monomial y α *⇩R c α) has_sum H y) ra_idx"
shows "ra_series_on (0::'a) r (ra_mono_coeffs_list c β l) (λy. ∏b←l. (H y ∙ b) ^ β b)"
proof (induction l)
case Nil
show ?case using ra_series_on_one[of "0::'a" r] by simp
next
case (Cons b bs)
have VC': "⋀y. dist y (0::'a) < r ⟹
((λα. ra_monomial (y - 0) α *⇩R c α) has_sum H y) ra_idx"
using VC by simp
have comp: "ra_series_on (0::'a) r (λα. c α ∙ b) (λy. H y ∙ b)"
by (rule ra_series_on_component[OF VC'])
have pow: "ra_series_on (0::'a) r (ra_cauchy_pow (λα. c α ∙ b) (β b)) (λy. (H y ∙ b) ^ β b)"
by (rule ra_series_on_power[OF comp])
have "ra_series_on (0::'a) r (ra_cauchy_prod (ra_cauchy_pow (λα. c α ∙ b) (β b)) (ra_mono_coeffs_list c β bs))
(λy. (H y ∙ b) ^ β b * (∏b'←bs. (H y ∙ b') ^ β b'))"
by (rule ra_series_on_mult[OF pow Cons.IH])
thus ?case by simp
qed
lemma ra_mono_coeffs_list_vanish:
fixes c :: "('a::euclidean_space ⇒ nat) ⇒ 'a"
assumes c0: "c ra_idx_zero = 0"
shows "ra_vanish_below (ra_mono_coeffs_list c β l) (sum_list (map β l))"
proof (induction l)
case Nil
show ?case by (simp add: ra_vanish_below_0)
next
case (Cons b bs)
have comp1: "ra_vanish_below (λα. c α ∙ b) 1"
unfolding ra_vanish_below_def
proof (intro allI impI)
fix α :: "'a ⇒ nat"
assume "α ∈ ra_idx" "ra_deg α < 1"
hence "α = ra_idx_zero" by (simp add: ra_deg_eq0_iff)
thus "c α ∙ b = 0" by (simp add: c0)
qed
have "ra_vanish_below (ra_cauchy_prod (ra_cauchy_pow (λα. c α ∙ b) (β b)) (ra_mono_coeffs_list c β bs))
(β b + sum_list (map β bs))"
by (rule ra_cauchy_prod_vanish[OF ra_cauchy_pow_vanish[OF comp1] Cons.IH])
thus ?case by simp
qed
lemma ra_mono_coeffs_list_indep:
fixes c c' :: "('a::euclidean_space ⇒ nat) ⇒ 'a"
assumes z: "sum_list (map β l) = 0" and g: "γ ∈ ra_idx"
shows "ra_mono_coeffs_list c β l γ = ra_mono_coeffs_list c' β l γ"
using z g
proof (induction l arbitrary: γ)
case Nil
show ?case by simp
next
case (Cons b bs)
have b0: "β b = 0" and bs0: "sum_list (map β bs) = 0"
using Cons.prems(1) by simp_all
have "ra_mono_coeffs_list c β (b # bs) γ = ra_cauchy_prod ra_coeff_one (ra_mono_coeffs_list c β bs) γ"
by (simp add: b0 ra_cauchy_pow_0)
also have "… = ra_mono_coeffs_list c β bs γ"
using Cons.prems(2) by (rule ra_cauchy_prod_coeff_one_left)
also have "… = ra_mono_coeffs_list c' β bs γ"
using bs0 Cons.prems(2) by (rule Cons.IH)
also have "… = ra_cauchy_prod ra_coeff_one (ra_mono_coeffs_list c' β bs) γ"
using Cons.prems(2) by (simp add: ra_cauchy_prod_coeff_one_left)
also have "… = ra_mono_coeffs_list c' β (b # bs) γ"
by (simp add: b0 ra_cauchy_pow_0)
finally show ?case .
qed
lemma ra_mono_coeffs_list_local:
fixes c c' :: "('a::euclidean_space ⇒ nat) ⇒ 'a"
assumes c0: "c ra_idx_zero = 0" and c0': "c' ra_idx_zero = 0"
and agree: "⋀α. α ∈ ra_idx ⟹ ra_deg α ≤ D ⟹ c α = c' α"
and g: "γ ∈ ra_idx"
and pos: "1 ≤ sum_list (map β l)"
and dg: "ra_deg γ ≤ D + sum_list (map β l) - 1"
shows "ra_mono_coeffs_list c β l γ = ra_mono_coeffs_list c' β l γ"
using pos dg g
proof (induction l arbitrary: γ)
case Nil
thus ?case by simp
next
case (Cons b bs)
define u where "u = (λα. c α ∙ b)"
define u' where "u' = (λα. c' α ∙ b)"
have u1: "ra_vanish_below u 1"
unfolding ra_vanish_below_def u_def
proof (intro allI impI)
fix α :: "'a ⇒ nat"
assume "α ∈ ra_idx" "ra_deg α < 1"
hence "α = ra_idx_zero" by (simp add: ra_deg_eq0_iff)
thus "c α ∙ b = 0" by (simp add: c0)
qed
have u1': "ra_vanish_below u' 1"
unfolding ra_vanish_below_def u'_def
proof (intro allI impI)
fix α :: "'a ⇒ nat"
assume "α ∈ ra_idx" "ra_deg α < 1"
hence "α = ra_idx_zero" by (simp add: ra_deg_eq0_iff)
thus "c' α ∙ b = 0" by (simp add: c0')
qed
have uu': "⋀α. α ∈ ra_idx ⟹ ra_deg α ≤ D ⟹ u α = u' α"
unfolding u_def u'_def using agree by simp
define vbs where "vbs = sum_list (map β bs)"
show ?case
proof (cases "β b = 0")
case True
have pos_bs: "1 ≤ vbs"
using Cons.prems(1) True by (simp add: vbs_def)
have dg_bs: "ra_deg γ ≤ D + vbs - 1"
using Cons.prems(2) True by (simp add: vbs_def)
have "ra_mono_coeffs_list c β (b # bs) γ = ra_cauchy_prod ra_coeff_one (ra_mono_coeffs_list c β bs) γ"
by (simp add: True ra_cauchy_pow_0)
also have "… = ra_mono_coeffs_list c β bs γ"
using Cons.prems(3) by (rule ra_cauchy_prod_coeff_one_left)
also have "… = ra_mono_coeffs_list c' β bs γ"
using pos_bs dg_bs Cons.prems(3) unfolding vbs_def by (rule Cons.IH)
also have "… = ra_cauchy_prod ra_coeff_one (ra_mono_coeffs_list c' β bs) γ"
using Cons.prems(3) by (simp add: ra_cauchy_prod_coeff_one_left)
also have "… = ra_mono_coeffs_list c' β (b # bs) γ"
by (simp add: True ra_cauchy_pow_0)
finally show ?thesis .
next
case False
hence bb1: "1 ≤ β b" by simp
show ?thesis
proof (cases "vbs = 0")
case True
have tail_eq: "⋀δ. δ ∈ ra_idx ⟹ ra_mono_coeffs_list c β bs δ = ra_mono_coeffs_list c' β bs δ"
using True unfolding vbs_def by (intro ra_mono_coeffs_list_indep)
have "ra_cauchy_prod (ra_cauchy_pow u (β b)) (ra_mono_coeffs_list c β bs) γ
= ra_cauchy_prod (ra_cauchy_pow u' (β b)) (ra_mono_coeffs_list c' β bs) γ"
proof (rule ra_cauchy_prod_local[where p = "β b" and q = 0
and Du = "D + β b - 1" and Dv = "ra_deg γ"])
show "ra_vanish_below (ra_cauchy_pow u (β b)) (β b)" by (rule ra_cauchy_pow_vanish[OF u1])
show "ra_vanish_below (ra_cauchy_pow u' (β b)) (β b)" by (rule ra_cauchy_pow_vanish[OF u1'])
show "ra_vanish_below (ra_mono_coeffs_list c β bs) 0" by (rule ra_vanish_below_0)
show "ra_vanish_below (ra_mono_coeffs_list c' β bs) 0" by (rule ra_vanish_below_0)
show "⋀α. α ∈ ra_idx ⟹ ra_deg α ≤ D + β b - 1 ⟹
ra_cauchy_pow u (β b) α = ra_cauchy_pow u' (β b) α"
by (rule ra_cauchy_pow_local[OF u1 u1' uu' bb1])
show "⋀δ. δ ∈ ra_idx ⟹ ra_deg δ ≤ ra_deg γ ⟹
ra_mono_coeffs_list c β bs δ = ra_mono_coeffs_list c' β bs δ"
using tail_eq by blast
show "γ ∈ ra_idx" by (rule Cons.prems(3))
show "ra_deg γ ≤ (D + β b - 1) + 0"
using Cons.prems(2) True
using vbs_def by fastforce
show "ra_deg γ ≤ ra_deg γ + β b" by simp
qed
thus ?thesis unfolding u_def u'_def by simp
next
case False
hence vbs1: "1 ≤ vbs" by simp
have "ra_cauchy_prod (ra_cauchy_pow u (β b)) (ra_mono_coeffs_list c β bs) γ
= ra_cauchy_prod (ra_cauchy_pow u' (β b)) (ra_mono_coeffs_list c' β bs) γ"
proof (rule ra_cauchy_prod_local[where p = "β b" and q = vbs
and Du = "D + β b - 1" and Dv = "D + vbs - 1"])
show "ra_vanish_below (ra_cauchy_pow u (β b)) (β b)" by (rule ra_cauchy_pow_vanish[OF u1])
show "ra_vanish_below (ra_cauchy_pow u' (β b)) (β b)" by (rule ra_cauchy_pow_vanish[OF u1'])
show "ra_vanish_below (ra_mono_coeffs_list c β bs) vbs"
unfolding vbs_def
by (simp add: c0 ra_mono_coeffs_list_vanish)
show "ra_vanish_below (ra_mono_coeffs_list c' β bs) vbs"
unfolding vbs_def
by (simp add: c0' ra_mono_coeffs_list_vanish)
show "⋀α. α ∈ ra_idx ⟹ ra_deg α ≤ D + β b - 1 ⟹
ra_cauchy_pow u (β b) α = ra_cauchy_pow u' (β b) α"
by (rule ra_cauchy_pow_local[OF u1 u1' uu' bb1])
show "⋀δ. δ ∈ ra_idx ⟹ ra_deg δ ≤ D + vbs - 1 ⟹
ra_mono_coeffs_list c β bs δ = ra_mono_coeffs_list c' β bs δ"
using Cons.IH vbs1 unfolding vbs_def by blast
show "γ ∈ ra_idx" by (rule Cons.prems(3))
show "ra_deg γ ≤ (D + β b - 1) + vbs"
using Cons.prems(2) bb1 by (simp add: vbs_def)
show "ra_deg γ ≤ (D + vbs - 1) + β b"
using Cons.prems(2) vbs1 by (simp add: vbs_def)
qed
thus ?thesis unfolding u_def u'_def by simp
qed
qed
qed
text ‹The packaged composition coefficients: canonical coefficients of
‹y ↦ ra_monomial (H y) β›.›
definition ra_mono_coeffs :: "(('a::euclidean_space ⇒ nat) ⇒ 'a) ⇒ ('a ⇒ nat)
⇒ (('a ⇒ nat) ⇒ real)" where
"ra_mono_coeffs c β = ra_mono_coeffs_list c β ra_basis_list"
lemma sum_list_basis_ra_deg:
"sum_list (map β (ra_basis_list::'a::euclidean_space list)) = ra_deg β"
proof -
have "sum_list (map β (ra_basis_list::'a list)) = (∑b∈set (ra_basis_list::'a list). β b)"
by (rule sum_list_distinct_conv_sum_set[OF ra_basis_list(2)])
also have "… = (∑b∈(Basis::'a set). β b)"
by (simp add: ra_basis_list(1))
finally show ?thesis by (simp add: ra_deg_def)
qed
lemma ra_mono_coeffs_series:
fixes c :: "('a::euclidean_space ⇒ nat) ⇒ 'a" and H :: "'a ⇒ 'a"
assumes VC: "⋀y. dist y (0::'a) < r ⟹
((λα. ra_monomial y α *⇩R c α) has_sum H y) ra_idx"
shows "ra_series_on (0::'a) r (ra_mono_coeffs c β) (λy. ra_monomial (H y) β)"
proof -
have base: "ra_series_on (0::'a) r (ra_mono_coeffs_list c β ra_basis_list)
(λy. ∏b←(ra_basis_list::'a list). (H y ∙ b) ^ β b)"
by (rule ra_mono_coeffs_list_series[OF VC])
have eq: "(∏b←(ra_basis_list::'a list). (H y ∙ b) ^ β b) = ra_monomial (H y) β" for y
proof -
have "ra_monomial (H y) β = (∏b∈set (ra_basis_list::'a list). (H y ∙ b) ^ β b)"
by (simp add: ra_monomial_def ra_basis_list(1))
also have "… = (∏b←(ra_basis_list::'a list). (H y ∙ b) ^ β b)"
by (rule prod.distinct_set_conv_list[OF ra_basis_list(2)])
finally show ?thesis by simp
qed
show ?thesis
using base unfolding ra_series_on_def eq ra_mono_coeffs_def by simp
qed
lemma ra_mono_coeffs_vanish:
fixes c :: "('a::euclidean_space ⇒ nat) ⇒ 'a"
assumes c0: "c ra_idx_zero = 0"
shows "ra_vanish_below (ra_mono_coeffs c β) (ra_deg β)"
unfolding ra_mono_coeffs_def
by (metis c0 ra_mono_coeffs_list_vanish sum_list_basis_ra_deg)
lemma ra_mono_coeffs_zero_below_degree:
fixes c :: "('a::euclidean_space ⇒ nat) ⇒ 'a"
assumes c0: "c ra_idx_zero = 0"
and g: "γ ∈ ra_idx"
and lt: "ra_deg γ < ra_deg β"
shows "ra_mono_coeffs c β γ = 0"
by (meson c0 g lt ra_mono_coeffs_vanish ra_vanish_below_def)
lemma ra_mono_coeffs_local:
fixes c c' :: "('a::euclidean_space ⇒ nat) ⇒ 'a"
assumes c0: "c ra_idx_zero = 0" and c0': "c' ra_idx_zero = 0"
and agree: "⋀α. α ∈ ra_idx ⟹ ra_deg α ≤ D ⟹ c α = c' α"
and g: "γ ∈ ra_idx"
and pos: "1 ≤ ra_deg β"
and dg: "ra_deg γ ≤ D + ra_deg β - 1"
shows "ra_mono_coeffs c β γ = ra_mono_coeffs c' β γ"
unfolding ra_mono_coeffs_def
by (metis agree c0 c0' dg g ra_mono_coeffs_list_local pos sum_list_basis_ra_deg)
subsection ‹Convolution algebra on scalar degree sequences›
definition ra_seq_conv :: "(nat ⇒ real) ⇒ (nat ⇒ real) ⇒ (nat ⇒ real)" where
"ra_seq_conv A B = (λd. ∑i≤d. A i * B (d - i))"
definition ra_seq_delta :: "nat ⇒ real" where
"ra_seq_delta = (λd. if d = 0 then 1 else 0)"
primrec ra_seq_conv_pow :: "(nat ⇒ real) ⇒ nat ⇒ (nat ⇒ real)" where
"ra_seq_conv_pow A 0 = ra_seq_delta"
| "ra_seq_conv_pow A (Suc k) = ra_seq_conv A (ra_seq_conv_pow A k)"
lemma ra_seq_conv_delta_right: "ra_seq_conv A ra_seq_delta = A"
proof (rule ext)
fix d :: nat
have "ra_seq_conv A ra_seq_delta d = (∑i≤d. if i = d then A d else 0)"
unfolding ra_seq_conv_def ra_seq_delta_def
by (rule sum.cong[OF refl]) auto
also have "… = A d"
by (simp add: if_distrib)
finally show "ra_seq_conv A ra_seq_delta d = A d" .
qed
lemma ra_seq_conv_delta_left: "ra_seq_conv ra_seq_delta B = B"
proof (rule ext)
fix d :: nat
have "ra_seq_conv ra_seq_delta B d = (∑i≤d. if i = 0 then B d else 0)"
unfolding ra_seq_conv_def ra_seq_delta_def
by (rule sum.cong[OF refl]) auto
also have "… = B d"
by simp
finally show "ra_seq_conv ra_seq_delta B d = B d" .
qed
lemma ra_seq_conv_nonneg:
assumes "⋀i. 0 ≤ A i" and "⋀i. 0 ≤ B i"
shows "0 ≤ ra_seq_conv A B d"
unfolding ra_seq_conv_def by (intro sum_nonneg mult_nonneg_nonneg assms)
lemma ra_seq_delta_nonneg: "0 ≤ ra_seq_delta d"
by (simp add: ra_seq_delta_def)
lemma ra_seq_conv_pow_nonneg:
assumes "⋀i. 0 ≤ A i"
shows "0 ≤ ra_seq_conv_pow A k d"
proof (induction k arbitrary: d)
case 0
show ?case by (simp add: ra_seq_delta_nonneg)
next
case (Suc k)
show ?case by (simp add: ra_seq_conv_nonneg[OF assms Suc.IH])
qed
lemma ra_seq_conv_mono:
assumes AA': "⋀i. A i ≤ A' i" and BB': "⋀i. B i ≤ B' i"
and Ann: "⋀i. 0 ≤ A i" and Bnn': "⋀i. 0 ≤ B' i"
shows "ra_seq_conv A B d ≤ ra_seq_conv A' B' d"
unfolding ra_seq_conv_def
by (rule sum_mono) (meson AA' Ann BB' Bnn' mult_left_mono mult_right_mono order_trans)
lemma ra_seq_conv_pow_mono_base:
assumes AA': "⋀i. A i ≤ A' i" and Ann: "⋀i. 0 ≤ A i"
shows "ra_seq_conv_pow A k d ≤ ra_seq_conv_pow A' k d"
proof (induction k arbitrary: d)
case 0
show ?case by simp
next
case (Suc k)
have Ann': "⋀i. 0 ≤ A' i"
using Ann AA' order_trans by blast
show ?case
unfolding ra_seq_conv_pow.simps
by (rule ra_seq_conv_mono[OF AA' Suc.IH Ann ra_seq_conv_pow_nonneg[OF Ann']])
qed
lemma ra_seq_conv_assoc: "ra_seq_conv (ra_seq_conv A B) C = ra_seq_conv A (ra_seq_conv B C)"
proof (rule ext)
fix d :: nat
have "ra_seq_conv (ra_seq_conv A B) C d = (∑m≤d. (∑i≤m. A i * B (m - i)) * C (d - m))"
by (simp add: ra_seq_conv_def)
also have "… = (∑m≤d. ∑i≤m. A i * B (m - i) * C (d - m))"
by (simp add: sum_distrib_right)
also have "… = (∑i≤d. ∑e≤d - i. A i * B e * C (d - (i + e)))"
using sum_triangle_exchange[of "λi e. A i * B e * C (d - (i + e))" d]
by (simp add: algebra_simps)
also have "… = (∑i≤d. A i * (∑e≤d - i. B e * C (d - i - e)))"
by (simp add: sum_distrib_left algebra_simps)
also have "… = ra_seq_conv A (ra_seq_conv B C) d"
by (simp add: ra_seq_conv_def)
finally show "ra_seq_conv (ra_seq_conv A B) C d = ra_seq_conv A (ra_seq_conv B C) d" .
qed
lemma ra_seq_conv_pow_add: "ra_seq_conv (ra_seq_conv_pow A m) (ra_seq_conv_pow A k) = ra_seq_conv_pow A (m + k)"
proof (induction m)
case 0
show ?case by (simp add: ra_seq_conv_delta_left)
next
case (Suc m)
have "ra_seq_conv (ra_seq_conv_pow A (Suc m)) (ra_seq_conv_pow A k)
= ra_seq_conv A (ra_seq_conv (ra_seq_conv_pow A m) (ra_seq_conv_pow A k))"
by (simp add: ra_seq_conv_assoc)
also have "… = ra_seq_conv A (ra_seq_conv_pow A (m + k))"
by (simp add: Suc.IH)
also have "… = ra_seq_conv_pow A (Suc m + k)"
by simp
finally show ?case .
qed
lemma ra_seq_conv_pow_vanish:
assumes A0: "A 0 = 0" and dk: "d < k"
shows "ra_seq_conv_pow A k d = 0"
using dk
proof (induction k arbitrary: d)
case 0
thus ?case by simp
next
case (Suc k)
have "ra_seq_conv A (ra_seq_conv_pow A k) d = (∑i≤d. A i * ra_seq_conv_pow A k (d - i))"
by (simp add: ra_seq_conv_def)
also have "… = 0"
proof (rule sum.neutral, rule ballI)
fix i assume i: "i ∈ {..d}"
show "A i * ra_seq_conv_pow A k (d - i) = 0"
proof (cases "i = 0")
case True
thus ?thesis by (simp add: A0)
next
case False
have "d - i < k" using i False Suc.prems by simp
thus ?thesis by (simp add: Suc.IH)
qed
qed
finally show ?case by simp
qed
text ‹The key partial-sum estimate: a weighted partial sum of a convolution power is
dominated by the corresponding power of a (shorter) weighted partial sum.›
lemma ra_seq_conv_pow_partial_sum_le:
fixes A :: "nat ⇒ real" and x :: real
assumes Ann: "⋀i. 0 ≤ A i" and A0: "A 0 = 0" and x0: "0 ≤ x" and k1: "1 ≤ k"
shows "(∑d≤N. ra_seq_conv_pow A k d * x ^ d) ≤ (∑i=1..N + 1 - k. A i * x ^ i) ^ k"
using k1
proof (induction k arbitrary: N)
case 0
thus ?case by simp
next
case (Suc k)
show ?case
proof (cases "k = 0")
case True
have "(∑d≤N. ra_seq_conv_pow A (Suc 0) d * x ^ d) = (∑d≤N. A d * x ^ d)"
by (simp add: ra_seq_conv_delta_right)
also have "… = (∑d=1..N. A d * x ^ d)"
proof -
have "{..N} = insert 0 {1..N}" by auto
thus ?thesis by (simp add: A0)
qed
finally show ?thesis using True by simp
next
case False
hence k1': "1 ≤ k" by simp
have expand: "(∑d≤N. ra_seq_conv_pow A (Suc k) d * x ^ d)
= (∑i≤N. ∑e≤N - i. A i * x ^ i * (ra_seq_conv_pow A k e * x ^ e))"
proof -
have "(∑d≤N. ra_seq_conv_pow A (Suc k) d * x ^ d)
= (∑d≤N. ∑i≤d. A i * ra_seq_conv_pow A k (d - i) * x ^ d)"
by (simp add: ra_seq_conv_def sum_distrib_right)
also have "… = (∑d≤N. ∑i≤d. A i * x ^ i * (ra_seq_conv_pow A k (d - i) * x ^ (d - i)))"
proof (rule sum.cong[OF refl], rule sum.cong[OF refl])
fix d i :: nat assume "d ∈ {..N}" "i ∈ {..d}"
hence "i + (d - i) = d" by simp
hence "x ^ d = x ^ i * x ^ (d - i)"
by (simp flip: power_add)
thus "A i * ra_seq_conv_pow A k (d - i) * x ^ d
= A i * x ^ i * (ra_seq_conv_pow A k (d - i) * x ^ (d - i))"
by (simp add: algebra_simps)
qed
also have "… = (∑i≤N. ∑e≤N - i. A i * x ^ i * (ra_seq_conv_pow A k e * x ^ e))"
by (rule sum_triangle_exchange)
finally show ?thesis .
qed
define S where "S = (∑i=1..N + 1 - Suc k. A i * x ^ i)"
have Snn: "0 ≤ S"
unfolding S_def by (intro sum_nonneg mult_nonneg_nonneg Ann zero_le_power x0)
have inner_bound: "(∑e≤N - i. ra_seq_conv_pow A k e * x ^ e) ≤ S ^ k"
if i: "1 ≤ i" "i ≤ N" and nz: "k ≤ N - i" for i
proof -
have "(∑e≤N - i. ra_seq_conv_pow A k e * x ^ e) ≤ (∑j=1..(N - i) + 1 - k. A j * x ^ j) ^ k"
by (rule Suc.IH[OF k1'])
also have "… ≤ S ^ k"
proof (rule power_mono)
show "(∑j=1..(N - i) + 1 - k. A j * x ^ j) ≤ S"
unfolding S_def
proof (rule sum_mono2)
show "finite {1..N + 1 - Suc k}" by simp
show "{1..(N - i) + 1 - k} ⊆ {1..N + 1 - Suc k}"
using i by auto
show "⋀j. j ∈ {1..N + 1 - Suc k} - {1..(N - i) + 1 - k} ⟹ 0 ≤ A j * x ^ j"
by (intro mult_nonneg_nonneg Ann zero_le_power x0)
qed
show "0 ≤ (∑j=1..(N - i) + 1 - k. A j * x ^ j)"
by (intro sum_nonneg mult_nonneg_nonneg Ann zero_le_power x0)
qed
finally show ?thesis .
qed
have "(∑i≤N. ∑e≤N - i. A i * x ^ i * (ra_seq_conv_pow A k e * x ^ e))
= (∑i≤N. A i * x ^ i * (∑e≤N - i. ra_seq_conv_pow A k e * x ^ e))"
by (simp add: sum_distrib_left)
also have "… ≤ (∑i≤N. (if 1 ≤ i ∧ i ≤ N + 1 - Suc k then A i * x ^ i * S ^ k else 0))"
proof (rule sum_mono)
fix i assume iN: "i ∈ {..N}"
show "A i * x ^ i * (∑e≤N - i. ra_seq_conv_pow A k e * x ^ e)
≤ (if 1 ≤ i ∧ i ≤ N + 1 - Suc k then A i * x ^ i * S ^ k else 0)"
proof (cases "i = 0")
case True
thus ?thesis by (simp add: A0)
next
case False
hence i1: "1 ≤ i" by simp
show ?thesis
proof (cases "k ≤ N - i")
case True
have iub: "i ≤ N + 1 - Suc k"
using True i1 iN by simp
have "A i * x ^ i * (∑e≤N - i. ra_seq_conv_pow A k e * x ^ e)
≤ A i * x ^ i * S ^ k"
by (intro mult_left_mono inner_bound[OF i1 _ True]
mult_nonneg_nonneg Ann zero_le_power x0) (use iN in simp)
thus ?thesis using i1 iub by simp
next
case False
have zero_inner: "(∑e≤N - i. ra_seq_conv_pow A k e * x ^ e) = 0"
proof (rule sum.neutral, rule ballI)
fix e assume "e ∈ {..N - i}"
hence "e < k" using False by simp
thus "ra_seq_conv_pow A k e * x ^ e = 0"
by (simp only: A0 ra_seq_conv_pow_vanish)
qed
show ?thesis
proof (cases "1 ≤ i ∧ i ≤ N + 1 - Suc k")
case True
thus ?thesis
using zero_inner
by (auto intro!: mult_nonneg_nonneg Ann zero_le_power x0
ra_seq_conv_pow_nonneg simp: Snn zero_le_power)
next
case False
thus ?thesis using zero_inner
by auto
qed
qed
qed
qed
also have "… = (∑i=1..N + 1 - Suc k. A i * x ^ i * S ^ k)"
proof -
have sub: "{1..N + 1 - Suc k} ⊆ {..N}" by auto
show ?thesis
by (rule sum.mono_neutral_cong_right[OF finite_atMost sub]) auto
qed
also have "… = S * S ^ k"
by (simp add: S_def sum_distrib_right)
also have "… = S ^ Suc k"
by simp
finally show ?thesis
using expand by (simp add: S_def)
qed
qed
subsection ‹Per-degree $\ell^1$ profiles of coefficient families›
definition ra_deg_block :: "nat ⇒ ('a::euclidean_space ⇒ nat) set" where
"ra_deg_block d = {α. α ∈ ra_idx ∧ ra_deg α = d}"
lemma finite_ra_deg_block: "finite (ra_deg_block d :: ('a::euclidean_space ⇒ nat) set)"
unfolding ra_deg_block_def by (rule ra_deg_block_finite)
lemma ra_deg_block_0: "(ra_deg_block 0 :: ('a::euclidean_space ⇒ nat) set) = {ra_idx_zero}"
proof
show "(ra_deg_block 0 :: ('a ⇒ nat) set) ⊆ {ra_idx_zero}"
unfolding ra_deg_block_def using ra_deg_eq0_iff by auto
have "ra_deg (ra_idx_zero :: 'a ⇒ nat) = 0"
by (simp add: ra_deg_def ra_idx_zero_def)
thus "{ra_idx_zero} ⊆ (ra_deg_block 0 :: ('a ⇒ nat) set)"
unfolding ra_deg_block_def using ra_idx_zero_in by auto
qed
definition ra_profile_real :: "(('a::euclidean_space ⇒ nat) ⇒ real) ⇒ nat ⇒ real" where
"ra_profile_real u d = (∑α∈ra_deg_block d. ¦u α¦)"
definition ra_profile :: "(('a::euclidean_space ⇒ nat) ⇒ 'a) ⇒ nat ⇒ real" where
"ra_profile c d = (∑α∈ra_deg_block d. norm (c α))"
lemma ra_profile_real_nonneg: "0 ≤ ra_profile_real u d"
unfolding ra_profile_real_def by (rule sum_nonneg) simp
lemma ra_profile_nonneg: "0 ≤ ra_profile c d"
unfolding ra_profile_def by (rule sum_nonneg) simp
text ‹The core regrouping estimate: profiles are submultiplicative under the Cauchy
product, with the scalar convolution as upper bound.›
lemma ra_profile_real_cauchy_prod:
fixes u v :: "('a::euclidean_space ⇒ nat) ⇒ real"
shows "ra_profile_real (ra_cauchy_prod u v) d ≤ ra_seq_conv (ra_profile_real u) (ra_profile_real v) d"
proof -
have step1: "ra_profile_real (ra_cauchy_prod u v) d
≤ (∑γ∈ra_deg_block d. ∑α∈ra_idx_below γ. ¦u α¦ * ¦v (ra_idx_diff γ α)¦)"
unfolding ra_profile_real_def ra_cauchy_prod_def
proof (rule sum_mono)
fix γ :: "'a ⇒ nat" assume "γ ∈ ra_deg_block d"
have "¦∑α∈ra_idx_below γ. u α * v (ra_idx_diff γ α)¦ ≤ (∑α∈ra_idx_below γ. ¦u α * v (ra_idx_diff γ α)¦)"
by (rule sum_abs)
also have "… = (∑α∈ra_idx_below γ. ¦u α¦ * ¦v (ra_idx_diff γ α)¦)"
by (simp add: abs_mult)
finally show "¦∑α∈ra_idx_below γ. u α * v (ra_idx_diff γ α)¦
≤ (∑α∈ra_idx_below γ. ¦u α¦ * ¦v (ra_idx_diff γ α)¦)" .
qed
have step2: "(∑γ∈ra_deg_block d. ∑α∈ra_idx_below γ. ¦u α¦ * ¦v (ra_idx_diff γ α)¦)
= (∑(γ, α)∈(SIGMA γ:(ra_deg_block d :: ('a ⇒ nat) set). ra_idx_below γ).
¦u α¦ * ¦v (ra_idx_diff γ α)¦)"
by (rule sum.Sigma[OF finite_ra_deg_block]) (simp add: idx_lower_fin)
define T :: "(('a ⇒ nat) × ('a ⇒ nat)) set" where
"T = {(α, δ). α ∈ ra_idx ∧ δ ∈ ra_idx ∧ ra_deg α + ra_deg δ = d}"
have step3: "(∑(γ, α)∈(SIGMA γ:(ra_deg_block d :: ('a ⇒ nat) set). ra_idx_below γ).
¦u α¦ * ¦v (ra_idx_diff γ α)¦)
= (∑(α, δ)∈T. ¦u α¦ * ¦v δ¦)"
proof (rule sum.reindex_bij_witness[where
i = "λ(α, δ). (ra_idx_add α δ, α)" and j = "λ(γ, α). (α, ra_idx_diff γ α)"])
fix a :: "('a ⇒ nat) × ('a ⇒ nat)"
assume a: "a ∈ (SIGMA γ:(ra_deg_block d :: ('a ⇒ nat) set). ra_idx_below γ)"
obtain γ α :: "'a ⇒ nat" where ga: "a = (γ, α)" by (cases a)
have gblk: "γ ∈ ra_deg_block d" and alow: "α ∈ ra_idx_below γ" using a ga by auto
have gra: "γ ∈ ra_idx" and gdeg: "ra_deg γ = d" using gblk by (auto simp: ra_deg_block_def)
have ara: "α ∈ ra_idx" using alow by (rule ra_idx_below_ra_idx)
have dra: "ra_idx_diff γ α ∈ ra_idx" using gra by (rule idx_sub)
have degsplit: "ra_deg α + ra_deg (ra_idx_diff γ α) = d"
using ra_deg_split[OF alow] gdeg by simp
show "(case case a of (γ, α) ⇒ (α, ra_idx_diff γ α) of (α, δ) ⇒ (ra_idx_add α δ, α)) = a"
using ga ra_idx_add_idx_diff[OF alow] by simp
show "(case a of (γ, α) ⇒ (α, ra_idx_diff γ α)) ∈ T"
using ga ara dra degsplit by (simp add: T_def)
next
fix b :: "('a ⇒ nat) × ('a ⇒ nat)"
assume b: "b ∈ T"
obtain α δ :: "'a ⇒ nat" where ad: "b = (α, δ)" by (cases b)
have ara: "α ∈ ra_idx" and dra: "δ ∈ ra_idx" and degs: "ra_deg α + ra_deg δ = d"
using b ad by (auto simp: T_def)
have gra: "ra_idx_add α δ ∈ ra_idx" using ara dra by (rule idx_add)
have gdeg: "ra_deg (ra_idx_add α δ) = d" using degs by (simp add: ra_deg_idx_add)
show "(case case b of (α, δ) ⇒ (ra_idx_add α δ, α) of (γ, α) ⇒ (α, ra_idx_diff γ α)) = b"
using ad ra_idx_diff_idx_add by simp
show "(case b of (α, δ) ⇒ (ra_idx_add α δ, α))
∈ (SIGMA γ:(ra_deg_block d :: ('a ⇒ nat) set). ra_idx_below γ)"
using ad gra gdeg ara ra_idx_add_in_idx_below[OF ara] by (auto simp: ra_deg_block_def)
next
show "⋀a :: ('a ⇒ nat) × ('a ⇒ nat).
a ∈ (SIGMA γ:(ra_deg_block d :: ('a ⇒ nat) set). ra_idx_below γ) ⟹
(case case a of (γ, α) ⇒ (α, ra_idx_diff γ α) of (α, δ) ⇒ ¦u α¦ * ¦v δ¦)
= (case a of (γ, α) ⇒ ¦u α¦ * ¦v (ra_idx_diff γ α)¦)"
by fastforce
qed
have Tsplit: "T = (⋃i∈{..d}. ra_deg_block i × ra_deg_block (d - i))"
proof
show "T ⊆ (⋃i∈{..d}. ra_deg_block i × ra_deg_block (d - i))"
proof
fix p :: "('a ⇒ nat) × ('a ⇒ nat)"
assume p: "p ∈ T"
obtain α δ :: "'a ⇒ nat" where ad: "p = (α, δ)" by (cases p)
have ara: "α ∈ ra_idx" and dra: "δ ∈ ra_idx" and degs: "ra_deg α + ra_deg δ = d"
using p ad by (auto simp: T_def)
have "ra_deg α ≤ d" using degs by simp
moreover have "α ∈ ra_deg_block (ra_deg α)" using ara by (simp add: ra_deg_block_def)
moreover have "δ ∈ ra_deg_block (d - ra_deg α)"
using dra degs by (simp add: ra_deg_block_def)
ultimately show "p ∈ (⋃i∈{..d}. ra_deg_block i × ra_deg_block (d - i))"
using ad by auto
qed
show "(⋃i∈{..d}. ra_deg_block i × ra_deg_block (d - i)) ⊆ T"
proof
fix p :: "('a ⇒ nat) × ('a ⇒ nat)"
assume "p ∈ (⋃i∈{..d}. ra_deg_block i × ra_deg_block (d - i))"
then obtain i and α δ :: "'a ⇒ nat" where i: "i ≤ d" and ad: "p = (α, δ)"
and a: "α ∈ ra_deg_block i" and dd: "δ ∈ ra_deg_block (d - i)"
by auto
show "p ∈ T"
using i ad a dd by (auto simp: T_def ra_deg_block_def)
qed
qed
have step4: "(∑(α, δ)∈T. ¦u α¦ * ¦v δ¦) = ra_seq_conv (ra_profile_real u) (ra_profile_real v) d"
proof -
have disj: "⋀i j. i ∈ {..d} ⟹ j ∈ {..d} ⟹ i ≠ j ⟹
(ra_deg_block i × ra_deg_block (d - i)) ∩ (ra_deg_block j × ra_deg_block (d - j)) = {}"
by (auto simp: ra_deg_block_def)
have "(∑(α, δ)∈T. ¦u α¦ * ¦v δ¦)
= (∑i≤d. ∑(α, δ)∈ra_deg_block i × ra_deg_block (d - i). ¦u α¦ * ¦v δ¦)"
unfolding Tsplit
by (rule sum.UNION_disjoint)
(auto simp: finite_ra_deg_block disj intro: finite_cartesian_product)
also have "… = (∑i≤d. (∑α∈ra_deg_block i. ¦u α¦) * (∑δ∈ra_deg_block (d - i). ¦v δ¦))"
by (simp add: sum_product sum.cartesian_product)
also have "… = ra_seq_conv (ra_profile_real u) (ra_profile_real v) d"
by (simp add: ra_seq_conv_def ra_profile_real_def)
finally show ?thesis .
qed
show ?thesis
using step1 step2 step3 step4 by simp
qed
lemma ra_profile_real_coeff_one: "ra_profile_real (ra_coeff_one :: ('a::euclidean_space ⇒ nat) ⇒ real) = ra_seq_delta"
proof (rule ext)
fix d :: nat
show "ra_profile_real (ra_coeff_one :: ('a ⇒ nat) ⇒ real) d = ra_seq_delta d"
proof (cases "d = 0")
case True
thus ?thesis
by (simp add: ra_profile_real_def ra_deg_block_0 ra_coeff_one_def ra_seq_delta_def)
next
case False
have "⋀α. α ∈ (ra_deg_block d :: ('a ⇒ nat) set) ⟹ ra_coeff_one α = 0"
proof -
fix α :: "'a ⇒ nat" assume "α ∈ ra_deg_block d"
hence da: "ra_deg α = d" by (simp add: ra_deg_block_def)
have "α ≠ ra_idx_zero"
proof
assume "α = ra_idx_zero"
hence "ra_deg α = 0" by (simp add: ra_deg_def ra_idx_zero_def)
thus False using da False by simp
qed
thus "ra_coeff_one α = 0" by (simp add: ra_coeff_one_def)
qed
thus ?thesis by (simp add: ra_profile_real_def ra_seq_delta_def False)
qed
qed
lemma ra_profile_real_cauchy_pow:
fixes u :: "('a::euclidean_space ⇒ nat) ⇒ real"
shows "ra_profile_real (ra_cauchy_pow u k) d ≤ ra_seq_conv_pow (ra_profile_real u) k d"
proof (induction k arbitrary: d)
case 0
show ?case by (simp add: ra_cauchy_pow_0 ra_profile_real_coeff_one)
next
case (Suc k)
have "ra_profile_real (ra_cauchy_pow u (Suc k)) d = ra_profile_real (ra_cauchy_prod u (ra_cauchy_pow u k)) d"
by (simp add: ra_cauchy_pow_Suc)
also have "… ≤ ra_seq_conv (ra_profile_real u) (ra_profile_real (ra_cauchy_pow u k)) d"
by (rule ra_profile_real_cauchy_prod)
also have "… ≤ ra_seq_conv (ra_profile_real u) (ra_seq_conv_pow (ra_profile_real u) k) d"
by (rule ra_seq_conv_mono[OF order_refl Suc.IH ra_profile_real_nonneg
ra_seq_conv_pow_nonneg[OF ra_profile_real_nonneg]])
finally show ?case by simp
qed
lemma ra_profile_real_component:
fixes c :: "('a::euclidean_space ⇒ nat) ⇒ 'a"
assumes b: "b ∈ Basis"
shows "ra_profile_real (λα. c α ∙ b) d ≤ ra_profile c d"
unfolding ra_profile_real_def ra_profile_def
by (rule sum_mono) (simp add: Basis_le_norm[OF b])
lemma ra_profile_real_mono_coeffs_list:
fixes c :: "('a::euclidean_space ⇒ nat) ⇒ 'a"
assumes bs: "set l ⊆ Basis"
shows "ra_profile_real (ra_mono_coeffs_list c β l) d ≤ ra_seq_conv_pow (ra_profile c) (sum_list (map β l)) d"
using bs
proof (induction l arbitrary: d)
case Nil
show ?case by (simp add: ra_profile_real_coeff_one)
next
case (Cons b bs)
have bB: "b ∈ Basis" and rest: "set bs ⊆ Basis"
using Cons.prems by auto
have "ra_profile_real (ra_mono_coeffs_list c β (b # bs)) d
= ra_profile_real (ra_cauchy_prod (ra_cauchy_pow (λα. c α ∙ b) (β b)) (ra_mono_coeffs_list c β bs)) d"
by simp
also have "… ≤ ra_seq_conv (ra_profile_real (ra_cauchy_pow (λα. c α ∙ b) (β b))) (ra_profile_real (ra_mono_coeffs_list c β bs)) d"
by (rule ra_profile_real_cauchy_prod)
also have "… ≤ ra_seq_conv (ra_seq_conv_pow (ra_profile c) (β b))
(ra_seq_conv_pow (ra_profile c) (sum_list (map β bs))) d"
proof (rule ra_seq_conv_mono)
fix i
have "ra_profile_real (ra_cauchy_pow (λα. c α ∙ b) (β b)) i ≤ ra_seq_conv_pow (ra_profile_real (λα. c α ∙ b)) (β b) i"
by (rule ra_profile_real_cauchy_pow)
also have "… ≤ ra_seq_conv_pow (ra_profile c) (β b) i"
by (rule ra_seq_conv_pow_mono_base[OF ra_profile_real_component[OF bB] ra_profile_real_nonneg])
finally show "ra_profile_real (ra_cauchy_pow (λα. c α ∙ b) (β b)) i ≤ ra_seq_conv_pow (ra_profile c) (β b) i" .
next
fix i
show "ra_profile_real (ra_mono_coeffs_list c β bs) i ≤ ra_seq_conv_pow (ra_profile c) (sum_list (map β bs)) i"
by (rule Cons.IH[OF rest])
next
fix i
show "0 ≤ ra_profile_real (ra_cauchy_pow (λα. c α ∙ b) (β b)) i" by (rule ra_profile_real_nonneg)
next
fix i
show "0 ≤ ra_seq_conv_pow (ra_profile c) (sum_list (map β bs)) i"
by (rule ra_seq_conv_pow_nonneg[OF ra_profile_nonneg])
qed
also have "… = ra_seq_conv_pow (ra_profile c) (β b + sum_list (map β bs)) d"
by (simp add: ra_seq_conv_pow_add)
finally show ?case by simp
qed
lemma ra_profile_real_mono_coeffs:
fixes c :: "('a::euclidean_space ⇒ nat) ⇒ 'a"
shows "ra_profile_real (ra_mono_coeffs c β) d ≤ ra_seq_conv_pow (ra_profile c) (ra_deg β) d"
proof -
have sub: "set (ra_basis_list :: 'a list) ⊆ Basis"
by (simp add: ra_basis_list(1))
have "ra_profile_real (ra_mono_coeffs_list c β ra_basis_list) d
≤ ra_seq_conv_pow (ra_profile c) (sum_list (map β (ra_basis_list :: 'a list))) d"
by (rule ra_profile_real_mono_coeffs_list[OF sub])
thus ?thesis
unfolding ra_mono_coeffs_def by (simp add: sum_list_basis_ra_deg)
qed
lemma ra_profile_coeff_id:
"ra_profile (ra_coeff_id :: ('a::euclidean_space ⇒ nat) ⇒ 'a) d
≤ (if d = 1 then real (card (Basis :: 'a set)) else 0)"
proof (cases "d = 1")
case False
have "⋀α. α ∈ (ra_deg_block d :: ('a ⇒ nat) set) ⟹ ra_coeff_id α = 0"
proof -
fix α :: "'a ⇒ nat" assume "α ∈ ra_deg_block d"
hence "ra_deg α = d" by (simp add: ra_deg_block_def)
thus "ra_coeff_id α = 0" using False ra_coeff_id_deg by fastforce
qed
thus ?thesis by (simp add: ra_profile_def False)
next
case True
have "ra_profile (ra_coeff_id :: ('a ⇒ nat) ⇒ 'a) d
= (∑α∈(ra_deg_block d :: ('a ⇒ nat) set). norm (ra_coeff_id α))"
by (simp add: ra_profile_def)
also have "… ≤ (∑α∈(ra_deg_block d :: ('a ⇒ nat) set). 1)"
by (rule sum_mono) (rule norm_coeff_id_le)
also have "… = real (card (ra_deg_block d :: ('a ⇒ nat) set))"
by simp
also have "… ≤ real (card (Basis :: 'a set))"
proof -
have sub: "(ra_deg_block d :: ('a ⇒ nat) set) ⊆ ra_idx_unit ` (Basis :: 'a set)"
proof
fix α :: "'a ⇒ nat" assume "α ∈ ra_deg_block d"
hence "α ∈ ra_idx" "ra_deg α = 1" using True by (auto simp: ra_deg_block_def)
thus "α ∈ ra_idx_unit ` Basis"
by (metis ra_deg_one_unit imageI)
qed
have "card (ra_deg_block d :: ('a ⇒ nat) set) ≤ card (ra_idx_unit ` (Basis :: 'a set))"
by (rule card_mono[OF finite_imageI[OF finite_Basis] sub])
also have "… = card (Basis :: 'a set)"
by (rule card_image[OF inj_on_idx_unit])
finally show ?thesis by simp
qed
finally show ?thesis using True by simp
qed
subsection ‹The composition operator ‹ra_inverse_step› and the formal fixed point›
definition ra_deg_range :: "nat ⇒ nat ⇒ ('a::euclidean_space ⇒ nat) set" where
"ra_deg_range j d = {β. β ∈ ra_idx ∧ j ≤ ra_deg β ∧ ra_deg β ≤ d}"
lemma finite_ra_deg_range: "finite (ra_deg_range j d :: ('a::euclidean_space ⇒ nat) set)"
proof -
have "(ra_deg_range j d :: ('a ⇒ nat) set) ⊆ (⋃k∈{..d}. ra_deg_block k)"
by (auto simp: ra_deg_range_def ra_deg_block_def)
moreover have "finite (⋃k∈{..d}. ra_deg_block k :: ('a ⇒ nat) set)"
by (intro finite_UN_I finite_atMost finite_ra_deg_block)
ultimately show ?thesis by (rule finite_subset)
qed
definition ra_inverse_step :: "(('a::euclidean_space ⇒ nat) ⇒ 'a) ⇒ (('a ⇒ nat) ⇒ 'a)
⇒ (('a ⇒ nat) ⇒ 'a)" where
"ra_inverse_step bphi c =
(λγ. ra_coeff_id γ + (∑β∈ra_deg_range 2 (ra_deg γ). ra_mono_coeffs c β γ *⇩R bphi β))"
lemma ra_deg_range_2_empty: "ra_deg γ < 2 ⟹ (ra_deg_range 2 (ra_deg γ)) = {}"
by (auto simp: ra_deg_range_def)
lemma ra_inverse_step_low_deg: "ra_deg γ < 2 ⟹ ra_inverse_step bphi c γ = ra_coeff_id γ"
by (simp add: ra_inverse_step_def ra_deg_range_2_empty)
lemma ra_inverse_step_idx_zero: "ra_inverse_step bphi c ra_idx_zero = 0"
proof -
have "ra_deg (ra_idx_zero :: 'a ⇒ nat) = 0"
by (simp add: ra_deg_def ra_idx_zero_def)
thus ?thesis by (simp add: ra_inverse_step_low_deg ra_coeff_id_idx_zero)
qed
lemma ra_inverse_step_sum_le_degree:
fixes bphi c :: "('a::euclidean_space ⇒ nat) ⇒ 'a"
assumes low: "⋀β. β ∈ ra_idx ⟹ ra_deg β < 2 ⟹ bphi β = 0"
shows "ra_inverse_step bphi c γ =
ra_coeff_id γ + (∑β∈ra_deg_range 0 (ra_deg γ). ra_mono_coeffs c β γ *⇩R bphi β)"
proof -
have "(∑β∈ra_deg_range 2 (ra_deg γ). ra_mono_coeffs c β γ *⇩R bphi β)
= (∑β∈ra_deg_range 0 (ra_deg γ). ra_mono_coeffs c β γ *⇩R bphi β)"
proof (rule sum.mono_neutral_cong_left)
show "finite (ra_deg_range 0 (ra_deg γ) :: ('a ⇒ nat) set)"
by (rule finite_ra_deg_range)
show "ra_deg_range 2 (ra_deg γ) ⊆ ra_deg_range 0 (ra_deg γ)"
by (auto simp: ra_deg_range_def)
show "∀β∈ra_deg_range 0 (ra_deg γ) - ra_deg_range 2 (ra_deg γ).
ra_mono_coeffs c β γ *⇩R bphi β = 0"
proof
fix β :: "'a ⇒ nat"
assume "β ∈ ra_deg_range 0 (ra_deg γ) - ra_deg_range 2 (ra_deg γ)"
hence "β ∈ ra_idx" "ra_deg β < 2"
by (auto simp: ra_deg_range_def)
hence "bphi β = 0"
by (rule low)
thus "ra_mono_coeffs c β γ *⇩R bphi β = 0"
by simp
qed
show "⋀β. β ∈ ra_deg_range 2 (ra_deg γ) ⟹
ra_mono_coeffs c β γ *⇩R bphi β = ra_mono_coeffs c β γ *⇩R bphi β"
by simp
qed
thus ?thesis
by (simp add: ra_inverse_step_def)
qed
lemma ra_inverse_step_local:
fixes c c' :: "('a::euclidean_space ⇒ nat) ⇒ 'a"
assumes c0: "c ra_idx_zero = 0" and c0': "c' ra_idx_zero = 0"
and agree: "⋀α. α ∈ ra_idx ⟹ ra_deg α ≤ D ⟹ c α = c' α"
and g: "γ ∈ ra_idx" and dg: "ra_deg γ ≤ D + 1"
shows "ra_inverse_step bphi c γ = ra_inverse_step bphi c' γ"
proof -
have "(∑β∈ra_deg_range 2 (ra_deg γ). ra_mono_coeffs c β γ *⇩R bphi β)
= (∑β∈ra_deg_range 2 (ra_deg γ). ra_mono_coeffs c' β γ *⇩R bphi β)"
proof (rule sum.cong[OF refl])
fix β :: "'a ⇒ nat" assume "β ∈ ra_deg_range 2 (ra_deg γ)"
hence b2: "2 ≤ ra_deg β" by (simp add: ra_deg_range_def)
have "ra_mono_coeffs c β γ = ra_mono_coeffs c' β γ"
proof (rule ra_mono_coeffs_local[where D = D])
show "c ra_idx_zero = 0" by (rule c0)
show "c' ra_idx_zero = 0" by (rule c0')
show "⋀α. α ∈ ra_idx ⟹ ra_deg α ≤ D ⟹ c α = c' α" by (rule agree)
show "γ ∈ ra_idx" by (rule g)
show "1 ≤ ra_deg β" using b2 by simp
show "ra_deg γ ≤ D + ra_deg β - 1" using dg b2 by simp
qed
thus "ra_mono_coeffs c β γ *⇩R bphi β = ra_mono_coeffs c' β γ *⇩R bphi β" by simp
qed
thus ?thesis by (simp add: ra_inverse_step_def)
qed
lemma ra_profile_inverse_step:
fixes bphi c :: "('a::euclidean_space ⇒ nat) ⇒ 'a"
shows "ra_profile (ra_inverse_step bphi c) d
≤ ra_profile (ra_coeff_id :: ('a ⇒ nat) ⇒ 'a) d
+ (∑k=2..d. ra_profile bphi k * ra_seq_conv_pow (ra_profile c) k d)"
proof -
have "ra_profile (ra_inverse_step bphi c) d
= (∑γ∈(ra_deg_block d :: ('a ⇒ nat) set).
norm (ra_coeff_id γ + (∑β∈ra_deg_range 2 (ra_deg γ). ra_mono_coeffs c β γ *⇩R bphi β)))"
by (simp add: ra_profile_def ra_inverse_step_def)
also have "… ≤ (∑γ∈(ra_deg_block d :: ('a ⇒ nat) set).
norm (ra_coeff_id γ)
+ norm (∑β∈ra_deg_range 2 (ra_deg γ). ra_mono_coeffs c β γ *⇩R bphi β))"
by (rule sum_mono) (rule norm_triangle_ineq)
also have "… = (∑γ∈(ra_deg_block d :: ('a ⇒ nat) set). norm (ra_coeff_id γ))
+ (∑γ∈(ra_deg_block d :: ('a ⇒ nat) set).
norm (∑β∈ra_deg_range 2 (ra_deg γ). ra_mono_coeffs c β γ *⇩R bphi β))"
by (rule sum.distrib)
finally have "ra_profile (ra_inverse_step bphi c) d
≤ (∑γ∈(ra_deg_block d :: ('a ⇒ nat) set). norm (ra_coeff_id γ))
+ (∑γ∈(ra_deg_block d :: ('a ⇒ nat) set).
norm (∑β∈ra_deg_range 2 (ra_deg γ). ra_mono_coeffs c β γ *⇩R bphi β))" .
also have "… ≤ ra_profile (ra_coeff_id :: ('a ⇒ nat) ⇒ 'a) d
+ (∑k=2..d. ra_profile bphi k * ra_seq_conv_pow (ra_profile c) k d)"
proof -
have inner: "(∑γ∈(ra_deg_block d :: ('a ⇒ nat) set).
norm (∑β∈ra_deg_range 2 (ra_deg γ). ra_mono_coeffs c β γ *⇩R bphi β))
≤ (∑k=2..d. ra_profile bphi k * ra_seq_conv_pow (ra_profile c) k d)"
proof -
have rng_const: "⋀γ. γ ∈ (ra_deg_block d :: ('a ⇒ nat) set) ⟹
ra_deg_range 2 (ra_deg γ) = ra_deg_range 2 d"
by (simp add: ra_deg_block_def)
have "(∑γ∈(ra_deg_block d :: ('a ⇒ nat) set).
norm (∑β∈ra_deg_range 2 (ra_deg γ). ra_mono_coeffs c β γ *⇩R bphi β))
≤ (∑γ∈(ra_deg_block d :: ('a ⇒ nat) set).
∑β∈ra_deg_range 2 d. ¦ra_mono_coeffs c β γ¦ * norm (bphi β))"
proof (rule sum_mono)
fix γ :: "'a ⇒ nat" assume gblk: "γ ∈ ra_deg_block d"
have "norm (∑β∈ra_deg_range 2 (ra_deg γ). ra_mono_coeffs c β γ *⇩R bphi β)
≤ (∑β∈ra_deg_range 2 (ra_deg γ). norm (ra_mono_coeffs c β γ *⇩R bphi β))"
by (rule norm_sum)
also have "… = (∑β∈ra_deg_range 2 d. ¦ra_mono_coeffs c β γ¦ * norm (bphi β))"
by (simp add: rng_const[OF gblk])
finally show "norm (∑β∈ra_deg_range 2 (ra_deg γ). ra_mono_coeffs c β γ *⇩R bphi β)
≤ (∑β∈ra_deg_range 2 d. ¦ra_mono_coeffs c β γ¦ * norm (bphi β))" .
qed
also have "… = (∑β∈ra_deg_range 2 d.
norm (bphi β) * (∑γ∈ra_deg_block d. ¦ra_mono_coeffs c β γ¦))"
by (subst sum.swap) (simp add: sum_distrib_left algebra_simps)
also have "… = (∑β∈(ra_deg_range 2 d :: ('a ⇒ nat) set).
norm (bphi β) * ra_profile_real (ra_mono_coeffs c β) d)"
by (simp add: ra_profile_real_def)
also have "… ≤ (∑β∈(ra_deg_range 2 d :: ('a ⇒ nat) set).
norm (bphi β) * ra_seq_conv_pow (ra_profile c) (ra_deg β) d)"
by (rule sum_mono) (intro mult_left_mono ra_profile_real_mono_coeffs norm_ge_zero)
also have "… = (∑k=2..d. ∑β∈(ra_deg_block k :: ('a ⇒ nat) set).
norm (bphi β) * ra_seq_conv_pow (ra_profile c) (ra_deg β) d)"
proof -
have split: "(ra_deg_range 2 d :: ('a ⇒ nat) set) = (⋃k∈{2..d}. ra_deg_block k)"
by (auto simp: ra_deg_range_def ra_deg_block_def)
show ?thesis
unfolding split using finite_ra_deg_block
apply (subst sum.UNION_disjoint)
apply simp_all
apply blast
by (simp add: disjoint_iff ra_deg_block_def)
qed
also have "… = (∑k=2..d. ra_profile bphi k * ra_seq_conv_pow (ra_profile c) k d)"
proof (rule sum.cong[OF refl])
fix k assume "k ∈ {2..d}"
have "(∑β∈(ra_deg_block k :: ('a ⇒ nat) set).
norm (bphi β) * ra_seq_conv_pow (ra_profile c) (ra_deg β) d)
= (∑β∈(ra_deg_block k :: ('a ⇒ nat) set).
norm (bphi β) * ra_seq_conv_pow (ra_profile c) k d)"
by (rule sum.cong[OF refl], simp add: ra_deg_block_def)
also have "… = ra_profile bphi k * ra_seq_conv_pow (ra_profile c) k d"
by (simp add: ra_profile_def sum_distrib_right)
finally show "(∑β∈(ra_deg_block k :: ('a ⇒ nat) set).
norm (bphi β) * ra_seq_conv_pow (ra_profile c) (ra_deg β) d)
= ra_profile bphi k * ra_seq_conv_pow (ra_profile c) k d" .
qed
finally show ?thesis .
qed
have ra_coeff_id_eq: "(∑γ∈(ra_deg_block d :: ('a ⇒ nat) set). norm (ra_coeff_id γ))
= ra_profile (ra_coeff_id :: ('a ⇒ nat) ⇒ 'a) d"
by (simp add: ra_profile_def)
show ?thesis
unfolding ra_coeff_id_eq by (rule add_left_mono[OF inner])
qed
finally show ?thesis .
qed
text ‹Stage-wise construction of the formal fixed point.›
primrec ra_inverse_stage :: "(('a::euclidean_space ⇒ nat) ⇒ 'a) ⇒ nat ⇒ (('a ⇒ nat) ⇒ 'a)" where
"ra_inverse_stage bphi 0 = (λ_. 0)"
| "ra_inverse_stage bphi (Suc d) = ra_inverse_step bphi (ra_inverse_stage bphi d)"
lemma ra_inverse_stage_idx_zero: "ra_inverse_stage bphi d ra_idx_zero = 0"
by (cases d) (simp_all add: ra_inverse_step_idx_zero)
lemma ra_inverse_stage_stable_succ:
fixes bphi :: "('a::euclidean_space ⇒ nat) ⇒ 'a"
assumes "γ ∈ ra_idx" and "ra_deg γ ≤ d"
shows "ra_inverse_stage bphi (Suc d) γ = ra_inverse_stage bphi d γ"
using assms
proof (induction d arbitrary: γ)
case 0
hence "γ = ra_idx_zero" by (simp add: ra_deg_eq0_iff)
thus ?case by (simp add: ra_inverse_step_idx_zero)
next
case (Suc d)
have "ra_inverse_step bphi (ra_inverse_stage bphi (Suc d)) γ = ra_inverse_step bphi (ra_inverse_stage bphi d) γ"
proof (rule ra_inverse_step_local[where D = d])
show "ra_inverse_stage bphi (Suc d) ra_idx_zero = 0" by (rule ra_inverse_stage_idx_zero)
show "ra_inverse_stage bphi d ra_idx_zero = 0" by (rule ra_inverse_stage_idx_zero)
show "⋀α. α ∈ ra_idx ⟹ ra_deg α ≤ d ⟹
ra_inverse_stage bphi (Suc d) α = ra_inverse_stage bphi d α"
by (rule Suc.IH)
show "γ ∈ ra_idx" by (rule Suc.prems(1))
show "ra_deg γ ≤ d + 1" using Suc.prems(2) by simp
qed
thus ?case by simp
qed
lemma ra_inverse_stage_stable:
fixes bphi :: "('a::euclidean_space ⇒ nat) ⇒ 'a"
assumes g: "γ ∈ ra_idx" and dd: "ra_deg γ ≤ d" and de: "d ≤ e"
shows "ra_inverse_stage bphi e γ = ra_inverse_stage bphi d γ"
using de
proof (induction e)
case 0
thus ?case by simp
next
case (Suc e)
show ?case
proof (cases "d = Suc e")
case True
thus ?thesis by simp
next
case False
hence "d ≤ e" using Suc.prems by simp
hence IH: "ra_inverse_stage bphi e γ = ra_inverse_stage bphi d γ" by (rule Suc.IH)
have "ra_inverse_stage bphi (Suc e) γ = ra_inverse_stage bphi e γ"
by (rule ra_inverse_stage_stable_succ[OF g]) (use dd ‹d ≤ e› in simp)
thus ?thesis using IH by simp
qed
qed
definition ra_inverse_coeffs :: "(('a::euclidean_space ⇒ nat) ⇒ 'a) ⇒ (('a ⇒ nat) ⇒ 'a)" where
"ra_inverse_coeffs bphi = (λγ. ra_inverse_stage bphi (ra_deg γ) γ)"
lemma ra_inverse_coeffs_idx_zero: "ra_inverse_coeffs bphi ra_idx_zero = 0"
by (simp add: ra_inverse_coeffs_def ra_inverse_stage_idx_zero)
lemma ra_inverse_coeffs_agrees_inverse_stage:
fixes bphi :: "('a::euclidean_space ⇒ nat) ⇒ 'a"
assumes a: "α ∈ ra_idx" and dd: "ra_deg α ≤ d"
shows "ra_inverse_coeffs bphi α = ra_inverse_stage bphi d α"
unfolding ra_inverse_coeffs_def
by (rule ra_inverse_stage_stable[OF a order_refl dd, symmetric])
theorem ra_inverse_coeffs_fixed_point:
fixes bphi :: "('a::euclidean_space ⇒ nat) ⇒ 'a"
assumes g: "γ ∈ ra_idx"
shows "ra_inverse_coeffs bphi γ = ra_inverse_step bphi (ra_inverse_coeffs bphi) γ"
proof -
define d where "d = ra_deg γ"
have T_eq: "ra_inverse_step bphi (ra_inverse_coeffs bphi) γ = ra_inverse_step bphi (ra_inverse_stage bphi d) γ"
proof (rule ra_inverse_step_local[where D = d])
show "ra_inverse_coeffs bphi ra_idx_zero = 0" by (rule ra_inverse_coeffs_idx_zero)
show "ra_inverse_stage bphi d ra_idx_zero = 0" by (rule ra_inverse_stage_idx_zero)
show "⋀α. α ∈ ra_idx ⟹ ra_deg α ≤ d ⟹ ra_inverse_coeffs bphi α = ra_inverse_stage bphi d α"
by (rule ra_inverse_coeffs_agrees_inverse_stage)
show "γ ∈ ra_idx" by (rule g)
show "ra_deg γ ≤ d + 1" by (simp add: d_def)
qed
have "ra_inverse_step bphi (ra_inverse_stage bphi d) γ = ra_inverse_stage bphi (Suc d) γ"
by simp
also have "… = ra_inverse_stage bphi d γ"
by (rule ra_inverse_stage_stable_succ[OF g]) (simp add: d_def)
also have "… = ra_inverse_coeffs bphi γ"
by (simp add: ra_inverse_coeffs_def d_def)
finally show ?thesis
using T_eq by simp
qed
corollary ra_inverse_coeffs_coeff_equation_le_degree:
fixes bphi :: "('a::euclidean_space ⇒ nat) ⇒ 'a"
assumes g: "γ ∈ ra_idx"
and low: "⋀β. β ∈ ra_idx ⟹ ra_deg β < 2 ⟹ bphi β = 0"
shows "ra_inverse_coeffs bphi γ =
ra_coeff_id γ + (∑β∈ra_deg_range 0 (ra_deg γ). ra_mono_coeffs (ra_inverse_coeffs bphi) β γ *⇩R bphi β)"
using ra_inverse_coeffs_fixed_point[OF g]
ra_inverse_step_sum_le_degree[where bphi=bphi and c="ra_inverse_coeffs bphi" and γ=γ, OF low]
by simp
lemma ra_mono_coeffs_term_has_sum_le_degree:
fixes c bphi :: "('a::euclidean_space ⇒ nat) ⇒ 'a"
assumes c0: "c ra_idx_zero = 0"
and g: "γ ∈ ra_idx"
shows "((λβ. ra_mono_coeffs c β γ *⇩R bphi β)
has_sum (∑β∈ra_deg_range 0 (ra_deg γ). ra_mono_coeffs c β γ *⇩R bphi β))
(ra_idx::('a ⇒ nat) set)"
proof -
let ?S = "ra_deg_range 0 (ra_deg γ) :: ('a ⇒ nat) set"
have finite_sum:
"((λβ. ra_mono_coeffs c β γ *⇩R bphi β)
has_sum (∑β∈?S. ra_mono_coeffs c β γ *⇩R bphi β)) ?S"
by (rule has_sum_finite) (rule finite_ra_deg_range)
have neutral:
"ra_mono_coeffs c β γ *⇩R bphi β = 0"
if "β ∈ (ra_idx::('a ⇒ nat) set) - ?S" for β
proof -
have "ra_deg γ < ra_deg β"
using that by (auto simp: ra_deg_range_def)
hence "ra_mono_coeffs c β γ = 0"
by (rule ra_mono_coeffs_zero_below_degree[where c=c and β=β, OF c0 g])
thus ?thesis by simp
qed
have "(((λβ. ra_mono_coeffs c β γ *⇩R bphi β)
has_sum (∑β∈?S. ra_mono_coeffs c β γ *⇩R bphi β))
(ra_idx::('a ⇒ nat) set))
= (((λβ. ra_mono_coeffs c β γ *⇩R bphi β)
has_sum (∑β∈?S. ra_mono_coeffs c β γ *⇩R bphi β)) ?S)"
by (rule has_sum_cong_neutral)
(use neutral in ‹auto simp: ra_deg_range_def›)
thus ?thesis
using finite_sum by simp
qed
corollary ra_inverse_coeffs_coeff_equation_infsum:
fixes bphi :: "('a::euclidean_space ⇒ nat) ⇒ 'a"
assumes g: "γ ∈ ra_idx"
and low: "⋀β. β ∈ ra_idx ⟹ ra_deg β < 2 ⟹ bphi β = 0"
shows "ra_inverse_coeffs bphi γ =
ra_coeff_id γ + (∑⇩∞β∈(ra_idx::('a ⇒ nat) set). ra_mono_coeffs (ra_inverse_coeffs bphi) β γ *⇩R bphi β)"
proof -
have hs: "((λβ. ra_mono_coeffs (ra_inverse_coeffs bphi) β γ *⇩R bphi β)
has_sum (∑β∈ra_deg_range 0 (ra_deg γ). ra_mono_coeffs (ra_inverse_coeffs bphi) β γ *⇩R bphi β))
(ra_idx::('a ⇒ nat) set)"
by (rule ra_mono_coeffs_term_has_sum_le_degree[where c = "ra_inverse_coeffs bphi", OF ra_inverse_coeffs_idx_zero g])
hence inf_eq:
"(∑⇩∞β∈(ra_idx::('a ⇒ nat) set). ra_mono_coeffs (ra_inverse_coeffs bphi) β γ *⇩R bphi β)
= (∑β∈ra_deg_range 0 (ra_deg γ). ra_mono_coeffs (ra_inverse_coeffs bphi) β γ *⇩R bphi β)"
by (rule infsumI)
show ?thesis
using ra_inverse_coeffs_coeff_equation_le_degree[OF g low] inf_eq by simp
qed
subsection ‹The majorant bootstrap for the fixed point›
text ‹Weighted partial sums of the profile of ‹ra_inverse_coeffs› stay below ‹2nσ› for small ‹σ›.›
lemma geom_tail_le:
fixes q :: real
assumes q0: "0 ≤ q" and qh: "q ≤ 1/2"
shows "(∑k=2..K. q ^ k) ≤ 2 * q⇧2"
proof -
have "(∑k=2..K. q ^ k) = (∑j<K - 1. q ^ (j + 2))"
proof (cases "2 ≤ K")
case True
show ?thesis
using le_Suc_ex
by (subst sum.reindex_bij_witness[where i = "λj. j + 2" and j = "λk. k - 2"], auto, fastforce)
next
case False
thus ?thesis by simp
qed
also have "… = q⇧2 * (∑j<K - 1. q ^ j)"
by (simp only: power_add sum_distrib_left mult.assoc mult.commute power2_eq_square)
also have "… ≤ q⇧2 * 2"
proof (rule mult_left_mono)
have "(∑j<K - 1. q ^ j) ≤ (∑j<K - 1. (1/2) ^ j)"
by (rule sum_mono) (rule power_mono[OF qh q0])
also have "… ≤ 2"
proof (cases "K - 1 = 0")
case True
thus ?thesis by simp
next
case False
have "(∑j<K - 1. (1/2::real) ^ j) = (1 - (1/2) ^ (K - 1)) / (1 - 1/2)"
by (subst geometric_sum, auto)
also have "… ≤ 2"
by simp
finally show ?thesis.
qed
finally show "(∑j<K - 1. q ^ j) ≤ 2".
show "0 ≤ q⇧2" by simp
qed
finally show ?thesis by simp
qed
text ‹Block sums of a majorized family are geometrically bounded.›
lemma ra_profile_le_majorized:
fixes bphi :: "('a::euclidean_space ⇒ nat) ⇒ 'a"
assumes t0: "0 < t" and majb: "ra_majorized t (λβ. norm (bphi β)) M"
shows "ra_profile bphi k ≤ M / t ^ k"
proof -
have summ: "ra_weighted_abs t (λβ. norm (bphi β)) summable_on ra_idx"
and inf_le: "(∑⇩∞β∈ra_idx. ra_weighted_abs t (λβ. norm (bphi β)) β) ≤ M"
using majb by (simp_all add: ra_majorized_def)
have blk_le: "(∑β∈(ra_deg_block k :: ('a ⇒ nat) set). ra_weighted_abs t (λβ. norm (bphi β)) β)
≤ (∑⇩∞β∈ra_idx. ra_weighted_abs t (λβ. norm (bphi β)) β)"
proof (rule finite_sum_le_infsum[OF summ finite_ra_deg_block])
show "(ra_deg_block k :: ('a ⇒ nat) set) ⊆ ra_idx" by (auto simp: ra_deg_block_def)
show "⋀β. β ∈ ra_idx - (ra_deg_block k :: ('a ⇒ nat) set) ⟹
0 ≤ ra_weighted_abs t (λβ. norm (bphi β)) β"
using t0 by (simp add: ra_weighted_abs_nonneg)
qed
have blk_eq: "(∑β∈(ra_deg_block k :: ('a ⇒ nat) set). ra_weighted_abs t (λβ. norm (bphi β)) β)
= ra_profile bphi k * t ^ k"
unfolding ra_weighted_abs_def ra_profile_def
by (simp add: ra_deg_block_def sum_distrib_right)
have "ra_profile bphi k * t ^ k ≤ M"
using blk_le blk_eq inf_le by simp
thus ?thesis
using t0 by (simp add: field_simps)
qed
text ‹Single coefficients of a majorized family are geometrically bounded.›
lemma coeff_le_majorized:
fixes u :: "('a::euclidean_space ⇒ nat) ⇒ real"
assumes t0: "0 < t" and majb: "ra_majorized t u M"
and unn: "⋀β. 0 ≤ u β" and b: "β ∈ ra_idx"
shows "u β ≤ M / t ^ ra_deg β"
proof -
have summ: "ra_weighted_abs t u summable_on ra_idx"
and inf_le: "(∑⇩∞β∈ra_idx. ra_weighted_abs t u β) ≤ M"
using majb by (simp_all add: ra_majorized_def)
have "(∑β'∈{β}. ra_weighted_abs t u β') ≤ (∑⇩∞β'∈ra_idx. ra_weighted_abs t u β')"
by (rule finite_sum_le_infsum[OF summ])
(use b t0 in ‹auto simp: ra_weighted_abs_nonneg›)
hence "u β * t ^ ra_deg β ≤ M"
using inf_le unn by (simp add: ra_weighted_abs_def abs_of_nonneg)
thus ?thesis
using t0 by (simp add: field_simps)
qed
text ‹The profile of the fixed point obeys the composition recursion.›
lemma ra_profile_inverse_coeffs_rec:
fixes bphi :: "('a::euclidean_space ⇒ nat) ⇒ 'a"
shows "ra_profile (ra_inverse_coeffs bphi) d
≤ ra_profile (ra_coeff_id :: ('a ⇒ nat) ⇒ 'a) d + (∑k=2..d. ra_profile bphi k * ra_seq_conv_pow (ra_profile (ra_inverse_coeffs bphi)) k d)"
proof -
have "ra_profile (ra_inverse_coeffs bphi) d = ra_profile (ra_inverse_step bphi (ra_inverse_coeffs bphi)) d"
unfolding ra_profile_def
by (rule sum.cong[OF refl])
(simp add: ra_deg_block_def ra_inverse_coeffs_fixed_point)
also have "… ≤ ra_profile (ra_coeff_id :: ('a ⇒ nat) ⇒ 'a) d + (∑k=2..d. ra_profile bphi k * ra_seq_conv_pow (ra_profile (ra_inverse_coeffs bphi)) k d)"
by (rule ra_profile_inverse_step)
finally show ?thesis .
qed
lemma ra_profile_inverse_coeffs_0:
fixes bphi :: "('a::euclidean_space ⇒ nat) ⇒ 'a"
shows "ra_profile (ra_inverse_coeffs bphi) 0 = 0"
by (simp add: ra_profile_def ra_deg_block_0 ra_inverse_coeffs_idx_zero)
text ‹The bootstrap: the weighted partial profile sums of ‹ra_inverse_coeffs› never exceed ‹2nσ›.›
lemma ra_inverse_coeffs_partial_sums_bounded:
fixes bphi :: "('a::euclidean_space ⇒ nat) ⇒ 'a"
defines "n ≡ real (card (Basis :: 'a set))"
defines "A ≡ ra_profile (ra_inverse_coeffs bphi)"
assumes t0: "0 < t" and majb: "ra_majorized t (λβ. norm (bphi β)) M"
and s0: "0 < σ"
and s1: "σ ≤ t / (4 * n)"
and s2: "σ ≤ t⇧2 / (8 * (M + 1) * n)"
shows "(∑i=1..N. A i * σ ^ i) ≤ 2 * n * σ"
proof (induction N)
case 0
have "0 ≤ 2 * n * σ"
using s0 by (simp add: n_def)
thus ?case by simp
next
case (Suc N)
define W where "W = (∑i=1..N. A i * σ ^ i)"
have Wnn: "0 ≤ W"
unfolding W_def A_def
by (intro sum_nonneg mult_nonneg_nonneg ra_profile_nonneg zero_le_power) (use s0 in simp)
have WB: "W ≤ 2 * n * σ"
unfolding W_def by (rule Suc.IH)
have n1: "1 ≤ n"
unfolding n_def
by simp
have M0: "0 ≤ M"
proof -
have "0 ≤ (∑⇩∞β∈ra_idx. ra_weighted_abs t (λβ. norm (bphi β)) β)"
using t0 by (intro infsum_nonneg) (simp add: ra_weighted_abs_nonneg)
also have "… ≤ M" using majb by (simp add: ra_majorized_def)
finally show ?thesis .
qed
have A0: "A 0 = 0" unfolding A_def by (rule ra_profile_inverse_coeffs_0)
have Ann: "⋀i. 0 ≤ A i" unfolding A_def by (rule ra_profile_nonneg)
have mknn: "⋀k. 0 ≤ ra_profile bphi k" by (rule ra_profile_nonneg)
have mkle: "⋀k. ra_profile bphi k ≤ M / t ^ k"
by (rule ra_profile_le_majorized[OF t0 majb])
have "(∑i=1..Suc N. A i * σ ^ i)
≤ (∑i=1..Suc N. (ra_profile (ra_coeff_id :: ('a ⇒ nat) ⇒ 'a) i
+ (∑k=2..i. ra_profile bphi k * ra_seq_conv_pow A k i)) * σ ^ i)"
unfolding A_def
by (rule sum_mono, rule mult_right_mono)
(rule ra_profile_inverse_coeffs_rec, use s0 in simp)
also have "… = (∑i=1..Suc N. ra_profile (ra_coeff_id :: ('a ⇒ nat) ⇒ 'a) i * σ ^ i)
+ (∑i=1..Suc N. (∑k=2..i. ra_profile bphi k * ra_seq_conv_pow A k i) * σ ^ i)"
by (simp add: algebra_simps sum.distrib)
also have "… ≤ n * σ
+ (∑i=1..Suc N. (∑k=2..i. ra_profile bphi k * ra_seq_conv_pow A k i) * σ ^ i)"
proof -
have "(∑i=1..Suc N. ra_profile (ra_coeff_id :: ('a ⇒ nat) ⇒ 'a) i * σ ^ i)
≤ (∑i=1..Suc N. (if i = 1 then n else 0) * σ ^ i)"
proof (rule sum_mono)
fix i
assume i: "i ∈ {1..Suc N}"
have cid_le: "ra_profile (ra_coeff_id :: ('a ⇒ nat) ⇒ 'a) i ≤ (if i = 1 then n else 0)"
using n_def ra_profile_coeff_id by blast
have sig_nonneg: "0 ≤ σ ^ i"
using s0 by simp
show "ra_profile (ra_coeff_id :: ('a ⇒ nat) ⇒ 'a) i * σ ^ i
≤ (if i = 1 then n else 0) * σ ^ i"
by (rule mult_right_mono[OF cid_le sig_nonneg])
qed
also have "… = n * σ"
proof -
have "{1..Suc N} = insert 1 {2..Suc N}"
by auto
then have "(∑i=1..Suc N. (if i = 1 then n else 0) * σ ^ i)
= n * σ + (∑i=2..Suc N. (if i = 1 then n else 0) * σ ^ i)"
by simp
also have "… = n * σ"
by simp
finally show ?thesis .
qed
finally show ?thesis
by linarith
qed
also have "… ≤ n * σ + M * (2 * (W / t)⇧2)"
proof -
have diag: "⋀i. i ∈ {1..Suc N} ⟹
(∑k=2..i. ra_profile bphi k * ra_seq_conv_pow A k i)
= (∑k=2..Suc N. ra_profile bphi k * ra_seq_conv_pow A k i)"
proof -
fix i assume i: "i ∈ {1..Suc N}"
show "(∑k=2..i. ra_profile bphi k * ra_seq_conv_pow A k i)
= (∑k=2..Suc N. ra_profile bphi k * ra_seq_conv_pow A k i)"
proof (rule sum.mono_neutral_left)
show "finite {2..Suc N}" by simp
show "{2..i} ⊆ {2..Suc N}" using i by auto
show "∀k∈{2..Suc N} - {2..i}. ra_profile bphi k * ra_seq_conv_pow A k i = 0"
proof
fix k assume "k ∈ {2..Suc N} - {2..i}"
hence "i < k" by auto
thus "ra_profile bphi k * ra_seq_conv_pow A k i = 0"
by (simp add: A0 ra_seq_conv_pow_vanish)
qed
qed
qed
have "(∑i=1..Suc N. (∑k=2..i. ra_profile bphi k * ra_seq_conv_pow A k i) * σ ^ i)
= (∑i=1..Suc N. ∑k=2..Suc N. ra_profile bphi k * ra_seq_conv_pow A k i * σ ^ i)"
proof (rule sum.cong[OF refl])
fix x :: nat
assume "x ∈ {1..Suc N}"
then have "(∑n = 2..x. ra_profile bphi n * ra_seq_conv_pow A n x) * σ ^ x = (∑n = 2..Suc N. ra_profile bphi n * ra_seq_conv_pow A n x) * σ ^ x"
using diag by moura
then show "(∑n = 2..x. ra_profile bphi n * ra_seq_conv_pow A n x) * σ ^ x = (∑n = 2..Suc N. ra_profile bphi n * ra_seq_conv_pow A n x * σ ^ x)"
by (metis (no_types) sum_distrib_right)
qed
also have "… = (∑k=2..Suc N. ∑i=1..Suc N. ra_profile bphi k * ra_seq_conv_pow A k i * σ ^ i)"
by (rule sum.swap)
also have "… = (∑k=2..Suc N. ra_profile bphi k * (∑i=1..Suc N. ra_seq_conv_pow A k i * σ ^ i))"
by (simp add: sum_distrib_left algebra_simps)
also have "… ≤ (∑k=2..Suc N. (M / t ^ k) * W ^ k)"
proof (rule sum_mono)
fix k assume k: "k ∈ {2..Suc N}"
hence k2: "2 ≤ k" by simp
have inner_le: "(∑i=1..Suc N. ra_seq_conv_pow A k i * σ ^ i) ≤ W ^ k"
proof -
have ext: "(∑i=1..Suc N. ra_seq_conv_pow A k i * σ ^ i)
= (∑i≤Suc N. ra_seq_conv_pow A k i * σ ^ i)"
proof -
have "{..Suc N} = insert 0 {1..Suc N}" by auto
moreover have "ra_seq_conv_pow A k 0 = 0"
using A0 k2 ra_seq_conv_pow_vanish by force
ultimately show ?thesis by simp
qed
have "(∑i≤Suc N. ra_seq_conv_pow A k i * σ ^ i)
≤ (∑i=1..Suc N + 1 - k. A i * σ ^ i) ^ k"
by (metis (no_types, lifting) A0 Ann Suc_eq_plus1 add_leE k2 linorder_le_cases
linorder_not_le ra_seq_conv_pow_partial_sum_le numeral_2_eq_2 s0)
also have "… ≤ W ^ k"
proof (rule power_mono)
show "(∑i=1..Suc N + 1 - k. A i * σ ^ i) ≤ W"
unfolding W_def
proof (rule sum_mono2)
show "finite {1..N}" by simp
show "{1..Suc N + 1 - k} ⊆ {1..N}" using k2 by auto
show "⋀i. i ∈ {1..N} - {1..Suc N + 1 - k} ⟹ 0 ≤ A i * σ ^ i"
by (intro mult_nonneg_nonneg Ann zero_le_power) (use s0 in simp)
qed
show "0 ≤ (∑i=1..Suc N + 1 - k. A i * σ ^ i)"
by (intro sum_nonneg mult_nonneg_nonneg Ann zero_le_power) (use s0 in simp)
qed
finally show ?thesis using ext by simp
qed
have Wknn: "0 ≤ (∑i=1..Suc N. ra_seq_conv_pow A k i * σ ^ i)"
by (intro sum_nonneg mult_nonneg_nonneg ra_seq_conv_pow_nonneg[OF Ann] zero_le_power)
(use s0 in simp)
have "ra_profile bphi k * (∑i=1..Suc N. ra_seq_conv_pow A k i * σ ^ i)
≤ (M / t ^ k) * (∑i=1..Suc N. ra_seq_conv_pow A k i * σ ^ i)"
by (rule mult_right_mono[OF mkle Wknn])
also have "… ≤ (M / t ^ k) * W ^ k"
by (rule mult_left_mono[OF inner_le])
(use M0 t0 in ‹simp add: divide_nonneg_pos›)
finally show "ra_profile bphi k * (∑i=1..Suc N. ra_seq_conv_pow A k i * σ ^ i)
≤ (M / t ^ k) * W ^ k" .
qed
also have "… = M * (∑k=2..Suc N. (W / t) ^ k)"
by (simp add: power_divide sum_distrib_left algebra_simps)
also have "… ≤ M * (2 * (W / t)⇧2)"
proof (rule mult_left_mono[OF _ M0])
have Wt_nn: "0 ≤ W / t" using Wnn t0 by simp
have "W / t ≤ 1/2"
proof -
have "W ≤ 2 * n * σ" by (rule WB)
also have "… ≤ 2 * n * (t / (4 * n))"
using s1 n1 by (intro mult_left_mono) simp_all
also have "… = t / 2"
using n1 by (simp add: field_simps)
finally have "W ≤ t / 2" .
thus ?thesis using t0 by (simp add: divide_le_eq)
qed
thus "(∑k=2..Suc N. (W / t) ^ k) ≤ 2 * (W / t)⇧2"
using geom_tail_le[OF Wt_nn] by presburger
qed
finally have conv_bound:
"(∑i=1..Suc N. (∑k=2..i. ra_profile bphi k * ra_seq_conv_pow A k i) * σ ^ i)
≤ M * (2 * (W / t)⇧2)" .
show ?thesis
using conv_bound by linarith
qed
also have "… ≤ n * σ + n * σ"
proof -
have "M * (2 * (W / t)⇧2) ≤ n * σ"
proof -
have "M * (2 * (W / t)⇧2) = 2 * M * W⇧2 / t⇧2"
by (simp add: power_divide)
also have "… ≤ 2 * M * (2 * n * σ)⇧2 / t⇧2"
using WB Wnn M0 t0
by (intro divide_right_mono mult_left_mono power_mono) simp_all
also have "… = 8 * M * n⇧2 * σ⇧2 / t⇧2"
by (simp add: power2_eq_square algebra_simps)
also have "… ≤ n * σ"
proof -
have "8 * (M + 1) * n * σ ≤ t⇧2"
proof -
have pos: "0 < 8 * (M + 1) * n"
using M0 n1 by (intro mult_pos_pos) simp_all
have "σ * (8 * (M + 1) * n)
≤ (t⇧2 / (8 * (M + 1) * n)) * (8 * (M + 1) * n)"
by (rule mult_right_mono[OF s2]) (use pos in simp)
also have "… = t⇧2"
using pos by (simp add: field_simps)
finally show ?thesis
by (simp add: mult_ac)
qed
moreover have "8 * M * n * σ ≤ 8 * (M + 1) * n * σ"
using n1 s0 by (intro mult_right_mono) (simp_all add: algebra_simps)
ultimately have "8 * M * n * σ ≤ t⇧2"
by linarith
hence "8 * M * n * σ * (n * σ) ≤ t⇧2 * (n * σ)"
using n1 s0 by (intro mult_right_mono) simp_all
hence "8 * M * n⇧2 * σ⇧2 ≤ t⇧2 * (n * σ)"
by (simp add: power2_eq_square algebra_simps)
thus ?thesis
using t0 by (simp add: pos_divide_le_eq, argo)
qed
finally show ?thesis .
qed
thus ?thesis by linarith
qed
also have "… = 2 * n * σ" by simp
finally show ?case .
qed
text ‹The majorant bound for @{const ra_inverse_coeffs}, and the induced bounds for the composed
monomial families.›
lemma ra_majorized_of_partial_profile_bounds:
fixes u :: "('a::euclidean_space ⇒ nat) ⇒ real"
assumes unn: "⋀γ. 0 ≤ u γ"
and s0: "0 < σ"
and bnd: "⋀D. (∑d≤D. ra_profile_real u d * σ ^ d) ≤ B"
shows "ra_majorized σ u B"
proof -
have partial: "(∑γ∈F. ra_weighted_abs σ u γ) ≤ B" if F: "finite F" "F ⊆ ra_idx" for F
proof -
define D where "D = Max (insert 0 (ra_deg ` F))"
have degF: "⋀γ. γ ∈ F ⟹ ra_deg γ ≤ D"
unfolding D_def using F(1) by (intro Max_ge) auto
have Fsub: "F ⊆ (⋃d∈{..D}. ra_deg_block d)"
using F(2) degF by (auto simp: ra_deg_block_def)
have "(∑γ∈F. ra_weighted_abs σ u γ) ≤ (∑γ∈(⋃d∈{..D}. ra_deg_block d). ra_weighted_abs σ u γ)"
by (rule sum_mono2[OF _ Fsub],
auto intro: finite_UN_I finite_ra_deg_block ra_weighted_abs_nonneg simp: ra_weighted_abs_nonneg s0 less_imp_le)
also have "… = (∑d≤D. ∑γ∈ra_deg_block d. ra_weighted_abs σ u γ)"
using finite_ra_deg_block by (subst sum.UNION_disjoint, auto, simp add: disjoint_iff ra_deg_block_def)
also have "… = (∑d≤D. ra_profile_real u d * σ ^ d)"
unfolding ra_weighted_abs_def ra_profile_real_def
by (rule sum.cong[OF refl], simp add: ra_deg_block_def sum_distrib_right abs_of_nonneg unn)
also have "… ≤ B" by (rule bnd)
finally show ?thesis .
qed
have summ: "ra_weighted_abs σ u summable_on ra_idx"
proof (rule nonneg_bdd_above_summable_on)
show "⋀γ. γ ∈ ra_idx ⟹ 0 ≤ ra_weighted_abs σ u γ"
using s0 by (simp add: ra_weighted_abs_nonneg)
show "bdd_above (sum (ra_weighted_abs σ u) ` {F. F ⊆ ra_idx ∧ finite F})"
by (rule bdd_aboveI[where M = B]) (use partial in auto)
qed
moreover have "(∑⇩∞γ∈ra_idx. ra_weighted_abs σ u γ) ≤ B"
by (rule infsum_le_finite_sums[OF summ]) (use partial in auto)
ultimately show ?thesis by (simp add: ra_majorized_def)
qed
theorem ra_inverse_coeffs_majorized:
fixes bphi :: "('a::euclidean_space ⇒ nat) ⇒ 'a"
defines "n ≡ real (card (Basis :: 'a set))"
assumes t0: "0 < t" and majb: "ra_majorized t (λβ. norm (bphi β)) M"
and s0: "0 < σ"
and s1: "σ ≤ t / (4 * n)"
and s2: "σ ≤ t⇧2 / (8 * (M + 1) * n)"
shows "ra_majorized σ (λγ. norm (ra_inverse_coeffs bphi γ)) (2 * n * σ)"
proof (rule ra_majorized_of_partial_profile_bounds)
show "⋀γ. 0 ≤ norm (ra_inverse_coeffs bphi γ)" by simp
show "0 < σ" by (rule s0)
fix D :: nat
have prof_eq: "ra_profile_real (λγ. norm (ra_inverse_coeffs bphi γ)) = ra_profile (ra_inverse_coeffs bphi)"
by (rule ext) (simp add: ra_profile_real_def ra_profile_def)
have "(∑d≤D. ra_profile (ra_inverse_coeffs bphi) d * σ ^ d) = (∑d=1..D. ra_profile (ra_inverse_coeffs bphi) d * σ ^ d)"
proof -
have "{..D} = insert 0 {1..D}" by auto
thus ?thesis by (simp add: ra_profile_inverse_coeffs_0)
qed
also have "… ≤ 2 * n * σ"
unfolding n_def
by (rule ra_inverse_coeffs_partial_sums_bounded[OF t0 majb s0])
(use s1 s2 in ‹simp_all add: n_def›)
finally show "(∑d≤D. ra_profile_real (λγ. norm (ra_inverse_coeffs bphi γ)) d * σ ^ d) ≤ 2 * n * σ"
by (simp add: prof_eq)
qed
text ‹A majorant bound on vector coefficients gives an absolutely convergent
power series on the closed working ball.›
lemma ra_majorized_vector_power_series_summable:
fixes c :: "('a::euclidean_space ⇒ nat) ⇒ 'b::banach"
assumes s0: "0 ≤ σ"
and maj: "ra_majorized σ (λγ. norm (c γ)) K"
and hle: "norm h ≤ σ"
shows "(λγ. ra_monomial h γ *⇩R c γ) summable_on (ra_idx::('a ⇒ nat) set)"
proof (rule abs_summable_summable,
rule summable_on_comparison_test[where f = "ra_weighted_abs σ (λγ. norm (c γ))"])
show "ra_weighted_abs σ (λγ. norm (c γ)) summable_on (ra_idx::('a ⇒ nat) set)"
using maj by (simp add: ra_majorized_def)
next
fix γ :: "'a ⇒ nat"
assume g: "γ ∈ ra_idx"
have "norm (ra_monomial h γ *⇩R c γ) = ¦ra_monomial h γ¦ * norm (c γ)"
by simp
also have "… ≤ σ ^ ra_deg γ * norm (c γ)"
by (rule mult_right_mono[OF ra_monomial_abs_le_pow[OF g hle]]) simp
also have "… = ra_weighted_abs σ (λγ. norm (c γ)) γ"
by (simp add: ra_weighted_abs_def mult.commute)
finally show "norm (ra_monomial h γ *⇩R c γ) ≤ ra_weighted_abs σ (λγ. norm (c γ)) γ" .
next
fix γ :: "'a ⇒ nat"
assume "γ ∈ ra_idx"
show "0 ≤ norm (ra_monomial h γ *⇩R c γ)"
by simp
qed
lemma ra_majorized_vector_power_series_has_sum:
fixes c :: "('a::euclidean_space ⇒ nat) ⇒ 'b::banach"
assumes s0: "0 ≤ σ"
and maj: "ra_majorized σ (λγ. norm (c γ)) K"
and hle: "norm h ≤ σ"
shows "((λγ. ra_monomial h γ *⇩R c γ)
has_sum (∑⇩∞γ∈(ra_idx::('a ⇒ nat) set). ra_monomial h γ *⇩R c γ))
(ra_idx::('a ⇒ nat) set)"
by (rule has_sum_infsum)
(rule ra_majorized_vector_power_series_summable[OF s0 maj hle])
corollary ra_inverse_coeffs_power_series_has_sum:
fixes bphi :: "('a::euclidean_space ⇒ nat) ⇒ 'a"
defines "n ≡ real (card (Basis :: 'a set))"
assumes t0: "0 < t" and majb: "ra_majorized t (λβ. norm (bphi β)) M"
and s0: "0 < σ"
and s1: "σ ≤ t / (4 * n)"
and s2: "σ ≤ t⇧2 / (8 * (M + 1) * n)"
and hle: "norm h ≤ σ"
shows "((λγ. ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ)
has_sum (∑⇩∞γ∈(ra_idx::('a ⇒ nat) set). ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ))
(ra_idx::('a ⇒ nat) set)"
proof (rule ra_majorized_vector_power_series_has_sum)
show "0 ≤ σ"
using s0 by simp
show "ra_majorized σ (λγ. norm (ra_inverse_coeffs bphi γ)) (2 * n * σ)"
unfolding n_def
by (rule ra_inverse_coeffs_majorized[OF t0 majb s0])
(use s1 s2 in ‹simp_all add: n_def›)
show "norm h ≤ σ"
by (rule hle)
qed
lemma ra_inverse_coeffs_value_norm_bound_at_scale:
fixes bphi :: "('a::euclidean_space ⇒ nat) ⇒ 'a"
defines "n ≡ real (card (Basis :: 'a set))"
assumes t0: "0 < t" and majb: "ra_majorized t (λβ. norm (bphi β)) M"
and s0: "0 < σ"
and s1: "σ ≤ t / (4 * n)"
and s2: "σ ≤ t⇧2 / (8 * (M + 1) * n)"
and hle: "norm h ≤ σ"
shows "norm (∑⇩∞γ∈(ra_idx::('a ⇒ nat) set).
ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ)
≤ 2 * n * σ"
proof -
let ?H = "∑⇩∞γ∈(ra_idx::('a ⇒ nat) set).
ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ"
have hs: "((λγ. ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ)
has_sum ?H) (ra_idx::('a ⇒ nat) set)"
unfolding n_def
by (rule ra_inverse_coeffs_power_series_has_sum[OF t0 majb s0])
(use s1 s2 hle in ‹simp_all add: n_def›)
have maj: "ra_majorized σ (λγ. norm (ra_inverse_coeffs bphi γ)) (2 * n * σ)"
unfolding n_def
by (rule ra_inverse_coeffs_majorized[OF t0 majb s0])
(use s1 s2 in ‹simp_all add: n_def›)
define S where "S = (∑⇩∞γ∈(ra_idx::('a ⇒ nat) set).
ra_weighted_abs σ (λγ. norm (ra_inverse_coeffs bphi γ)) γ)"
have dom_sum: "((ra_weighted_abs σ (λγ. norm (ra_inverse_coeffs bphi γ))) has_sum S)
(ra_idx::('a ⇒ nat) set)"
unfolding S_def using maj by (simp add: ra_majorized_def has_sum_infsum)
have term_bound: "norm (ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ)
≤ ra_weighted_abs σ (λγ. norm (ra_inverse_coeffs bphi γ)) γ"
if g: "γ ∈ (ra_idx::('a ⇒ nat) set)" for γ
proof -
have "norm (ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ)
= ¦ra_monomial h γ¦ * norm (ra_inverse_coeffs bphi γ)"
by simp
also have "… ≤ σ ^ ra_deg γ * norm (ra_inverse_coeffs bphi γ)"
by (rule mult_right_mono[OF ra_monomial_abs_le_pow[OF g hle]]) simp
also have "… = ra_weighted_abs σ (λγ. norm (ra_inverse_coeffs bphi γ)) γ"
by (simp add: ra_weighted_abs_def mult.commute)
finally show ?thesis .
qed
have "norm ?H ≤ S"
by (rule norm_infsum_le[OF hs dom_sum]) (use term_bound in simp)
also have "… ≤ 2 * n * σ"
using maj by (simp add: S_def ra_majorized_def)
finally show ?thesis .
qed
lemma ra_majorized_geometric_weight_summable:
fixes bphi :: "('a::euclidean_space ⇒ nat) ⇒ 'b::real_normed_vector"
assumes t0: "0 < t"
and majb: "ra_majorized t (λβ. norm (bphi β)) M"
and K0: "0 ≤ K"
and Kt: "K < t"
shows "(λβ. norm (bphi β) * K ^ ra_deg β)
summable_on (ra_idx::('a ⇒ nat) set)"
proof (rule summable_on_comparison_test
[where f = "λβ. M * (K / t) ^ ra_deg β"])
have M0: "0 ≤ M"
proof -
have "0 ≤ (∑⇩∞β∈ra_idx. ra_weighted_abs t (λβ. norm (bphi β)) β)"
using t0 by (intro infsum_nonneg) (simp add: ra_weighted_abs_nonneg)
also have "… ≤ M"
using majb by (simp add: ra_majorized_def)
finally show ?thesis .
qed
have q0: "0 ≤ K / t"
using K0 t0 by simp
have q1: "K / t < 1"
using Kt t0 by (simp add: divide_less_eq)
have "(λβ::'a ⇒ nat. (K / t) ^ ra_deg β) summable_on ra_idx"
by (rule geom_idx_summable[OF q0 q1])
thus "(λβ. M * (K / t) ^ ra_deg β)
summable_on (ra_idx::('a ⇒ nat) set)"
by (rule summable_on_cmult_right)
next
fix β :: "'a ⇒ nat"
assume b: "β ∈ ra_idx"
have "norm (bphi β) * K ^ ra_deg β
≤ (M / t ^ ra_deg β) * K ^ ra_deg β"
by (rule mult_right_mono[OF coeff_le_majorized[OF t0 majb _ b]])
(use K0 in simp_all)
also have "… = M * (K / t) ^ ra_deg β"
using t0 by (simp add: power_divide)
finally show "norm (bphi β) * K ^ ra_deg β
≤ M * (K / t) ^ ra_deg β" .
next
fix β :: "'a ⇒ nat"
assume "β ∈ ra_idx"
show "0 ≤ norm (bphi β) * K ^ ra_deg β"
using K0 by simp
qed
lemma ra_inverse_coeffs_power_series_real_analytic_on_ball_at_scale:
fixes bphi :: "('a::euclidean_space ⇒ nat) ⇒ 'a"
defines "n ≡ real (card (Basis :: 'a set))"
defines "H ≡ (λh::'a. ∑⇩∞γ∈(ra_idx::('a ⇒ nat) set).
ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ)"
assumes t0: "0 < t" and majb: "ra_majorized t (λβ. norm (bphi β)) M"
and s0: "0 < σ"
and s1: "σ ≤ t / (4 * n)"
and s2: "σ ≤ t⇧2 / (8 * (M + 1) * n)"
shows "real_analytic_on H (ball (0::'a) (σ / 2))"
proof -
have n1: "1 ≤ n"
unfolding n_def by simp
have Hmaj: "ra_majorized σ (λγ. norm (ra_inverse_coeffs bphi γ)) (2 * n * σ)"
unfolding n_def
by (rule ra_inverse_coeffs_majorized[OF t0 majb s0])
(use s1 s2 in ‹simp_all add: n_def›)
show ?thesis
unfolding real_analytic_on_def
proof (intro conjI ballI)
show "open (ball (0::'a) (σ / 2))"
by simp
next
fix y0 :: 'a
assume y0: "y0 ∈ ball (0::'a) (σ / 2)"
have y0_lt: "norm y0 < σ / 2"
using y0 by (simp add: dist_norm)
define r where "r = (σ - norm y0) / (2 * n)"
have r0: "0 < r"
using y0_lt n1 s0 by (simp add: r_def)
have rle: "r ≤ r"
by simp
define K where "K = n * r + norm y0"
have K0: "0 ≤ K"
using n1 r0 by (simp add: K_def)
have Klt: "K < σ"
proof -
have "n * r = (σ - norm y0) / 2"
using n1 by (simp add: r_def field_simps)
hence "K = (σ + norm y0) / 2"
by (simp add: K_def)
also have "… < σ"
using y0_lt s0 by simp
finally show ?thesis .
qed
obtain cid :: "('a ⇒ nat) ⇒ 'a" where
cid_series: "⋀y::'a. ((λα. ra_monomial y α *⇩R cid α) has_sum y) ra_idx"
and cid_maj: "⋀ρ::real. 0 ≤ ρ ⟹
ra_majorized ρ (λα. norm (cid α)) (real (card (Basis :: 'a set)) * ρ)"
proof -
show thesis
proof (rule identity_coeff_series_majorized)
fix cid :: "('a ⇒ nat) ⇒ 'a"
assume cid_series: "⋀y::'a. ((λα. ra_monomial y α *⇩R cid α) has_sum y) ra_idx"
and cid_maj: "⋀ρ::real. 0 ≤ ρ ⟹
ra_majorized ρ (λα. norm (cid α)) (real (card (Basis :: 'a set)) * ρ)"
show thesis
by (rule that[OF cid_series cid_maj])
qed
qed
have id_ser: "⋀x. dist x y0 < r ⟹
((λα. ra_monomial (x - y0) α *⇩R cid α) has_sum (x - y0))
(ra_idx::('a ⇒ nat) set)"
using cid_series by simp
have cidmaj_r: "ra_majorized r (λα. norm (cid α)) (n * r)"
using cid_maj[of r] r0 by (simp add: n_def)
have mon_ser: "∃cc. ra_series_majorized y0 r r cc (λx::'a. ra_monomial x β) (K ^ ra_deg β)"
if b: "β ∈ (ra_idx::('a ⇒ nat) set)" for β
proof -
have raw: "∃cc. ra_series_majorized y0 r r cc
(λx::'a. ra_monomial ((x - y0) - (- y0)) β) (K ^ ra_deg β)"
proof (rule ra_series_majorized_ra_monomial_compose[where z = "- y0", OF _ id_ser cidmaj_r _ K0])
show "0 ≤ r"
using r0 by simp
fix e :: 'a
assume e: "e ∈ Basis"
have "¦(- y0) ∙ e¦ ≤ norm y0"
using Basis_le_norm[OF e, of "- y0"] by simp
thus "n * r + ¦(- y0) ∙ e¦ ≤ K"
by (simp add: K_def)
qed
thus ?thesis
by simp
qed
obtain CC where CC:
"⋀β. β ∈ (ra_idx::('a ⇒ nat) set) ⟹
ra_series_majorized y0 r r (CC β) (λx::'a. ra_monomial x β) (K ^ ra_deg β)"
using mon_ser by metis
have ser: "ra_series_on y0 r (CC β) (λx::'a. ra_monomial x β)"
if b: "β ∈ (ra_idx::('a ⇒ nat) set)" for β
using CC[OF b] by (simp add: ra_series_majorized_def)
have maj: "ra_majorized r (CC β) (K ^ ra_deg β)"
if b: "β ∈ (ra_idx::('a ⇒ nat) set)" for β
using CC[OF b] by (simp add: ra_series_majorized_def)
have gsum: "(λβ. norm (ra_inverse_coeffs bphi β) * (K ^ ra_deg β))
summable_on (ra_idx::('a ⇒ nat) set)"
by (rule ra_majorized_geometric_weight_summable[OF s0 Hmaj K0 Klt])
have Gval: "⋀x::'a. dist x y0 < r ⟹
((λβ. ra_monomial x β *⇩R ra_inverse_coeffs bphi β) has_sum H x)
(ra_idx::('a ⇒ nat) set)"
proof -
fix x :: 'a
assume x: "dist x y0 < r"
have nx: "norm x ≤ σ"
proof -
have "norm x ≤ norm (x - y0) + norm y0"
by (metis add.commute add_diff_cancel_left' norm_triangle_sub)
also have "… < r + norm y0"
using x by (simp add: dist_norm)
also have "… ≤ n * r + norm y0"
using n1 r0 by (intro add_right_mono mult_left_le_one_le) simp_all
also have "… = K"
by (simp add: K_def)
also have "… < σ"
by (rule Klt)
finally show ?thesis
by simp
qed
show "((λβ. ra_monomial x β *⇩R ra_inverse_coeffs bphi β) has_sum H x)
(ra_idx::('a ⇒ nat) set)"
unfolding H_def n_def
by (rule ra_inverse_coeffs_power_series_has_sum[OF t0 majb s0])
(use s1 s2 nx in ‹simp_all add: n_def›)
qed
have recentered: "∀x. dist x y0 < r ⟶
((λγ. ra_monomial (x - y0) γ *⇩R
(∑⇩∞β∈(ra_idx::('a ⇒ nat) set). CC β γ *⇩R ra_inverse_coeffs bphi β))
has_sum H x) (ra_idx::('a ⇒ nat) set)"
by (rule ra_series_on_majdom_vec[OF r0 rle ser maj gsum Gval])
show "∃r>0. ∃c. ∀x. dist x y0 < r ⟶
((λα. ra_monomial (x - y0) α *⇩R c α) has_sum H x)
(ra_idx::('a ⇒ nat) set)"
by (intro exI[where x=r] conjI exI[where x="λγ. ∑⇩∞β∈(ra_idx::('a ⇒ nat) set).
CC β γ *⇩R ra_inverse_coeffs bphi β"]) (use r0 recentered in auto)
qed
qed
corollary ra_inverse_coeffs_power_series_converges_near_zero:
fixes bphi :: "('a::euclidean_space ⇒ nat) ⇒ 'a"
assumes t0: "0 < t"
and majb: "ra_majorized t (λβ. norm (bphi β)) M"
obtains σ where "0 < σ"
and "⋀h::'a. norm h < σ ⟹
((λγ. ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ)
has_sum (∑⇩∞γ∈(ra_idx::('a ⇒ nat) set). ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ))
(ra_idx::('a ⇒ nat) set)"
proof -
define n where "n = real (card (Basis :: 'a set))"
have n1: "1 ≤ n"
unfolding n_def by simp
have M0: "0 ≤ M"
proof -
have "0 ≤ (∑⇩∞β∈ra_idx. ra_weighted_abs t (λβ. norm (bphi β)) β)"
using t0 by (intro infsum_nonneg) (simp add: ra_weighted_abs_nonneg)
also have "… ≤ M"
using majb by (simp add: ra_majorized_def)
finally show ?thesis .
qed
define σ where "σ = min (t / (4 * n)) (t⇧2 / (8 * (M + 1) * n)) / 2"
have a_pos: "0 < t / (4 * n)"
using t0 n1 by simp
have b_pos: "0 < t⇧2 / (8 * (M + 1) * n)"
using t0 M0 n1 by (intro divide_pos_pos mult_pos_pos) simp_all
have σ0: "0 < σ"
using a_pos b_pos by (simp add: σ_def)
have min_nonneg: "0 ≤ min (t / (4 * n)) (t⇧2 / (8 * (M + 1) * n))"
using a_pos b_pos by simp
have half_min_le:
"min (t / (4 * n)) (t⇧2 / (8 * (M + 1) * n)) / 2
≤ min (t / (4 * n)) (t⇧2 / (8 * (M + 1) * n))"
proof -
have "min (t / (4 * n)) (t⇧2 / (8 * (M + 1) * n)) / 2
= (1/2) * min (t / (4 * n)) (t⇧2 / (8 * (M + 1) * n))"
by simp
also have "… ≤ 1 * min (t / (4 * n)) (t⇧2 / (8 * (M + 1) * n))"
by (rule mult_right_mono) (use min_nonneg in simp_all)
finally show ?thesis
by simp
qed
have s1: "σ ≤ t / (4 * n)"
proof -
have "σ ≤ min (t / (4 * n)) (t⇧2 / (8 * (M + 1) * n))"
unfolding σ_def by (rule half_min_le)
also have "… ≤ t / (4 * n)"
by simp
finally show ?thesis .
qed
have s2: "σ ≤ t⇧2 / (8 * (M + 1) * n)"
proof -
have "σ ≤ min (t / (4 * n)) (t⇧2 / (8 * (M + 1) * n))"
unfolding σ_def by (rule half_min_le)
also have "… ≤ t⇧2 / (8 * (M + 1) * n)"
by simp
finally show ?thesis .
qed
show ?thesis
proof (rule that[OF σ0])
fix h :: 'a
assume h: "norm h < σ"
have s1': "σ ≤ t / (4 * real DIM('a))"
using s1 by (simp add: n_def)
have s2': "σ ≤ t⇧2 / (8 * (M + 1) * real DIM('a))"
using s2 by (simp add: n_def)
show "((λγ. ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ)
has_sum (∑⇩∞γ∈(ra_idx::('a ⇒ nat) set). ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ))
(ra_idx::('a ⇒ nat) set)"
by (rule ra_inverse_coeffs_power_series_has_sum[OF t0 majb σ0 s1' s2'])
(use h in simp)
qed
qed
theorem ra_inverse_coeffs_formal_inverse_data:
fixes bphi :: "('a::euclidean_space ⇒ nat) ⇒ 'a"
assumes t0: "0 < t"
and majb: "ra_majorized t (λβ. norm (bphi β)) M"
and low: "⋀β. β ∈ ra_idx ⟹ ra_deg β < 2 ⟹ bphi β = 0"
obtains σ where "0 < σ"
and "⋀h::'a. norm h < σ ⟹
((λγ. ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ)
has_sum (∑⇩∞γ∈(ra_idx::('a ⇒ nat) set).
ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ))
(ra_idx::('a ⇒ nat) set)"
and "⋀γ. γ ∈ ra_idx ⟹
ra_inverse_coeffs bphi γ =
ra_coeff_id γ + (∑⇩∞β∈(ra_idx::('a ⇒ nat) set).
ra_mono_coeffs (ra_inverse_coeffs bphi) β γ *⇩R bphi β)"
proof -
show ?thesis
proof (rule ra_inverse_coeffs_power_series_converges_near_zero[OF t0 majb])
fix σ
assume s0: "0 < σ"
and conv: "⋀h::'a. norm h < σ ⟹
((λγ. ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ)
has_sum (∑⇩∞γ∈(ra_idx::('a ⇒ nat) set).
ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ))
(ra_idx::('a ⇒ nat) set)"
have coeff: "⋀γ. γ ∈ ra_idx ⟹
ra_inverse_coeffs bphi γ =
ra_coeff_id γ + (∑⇩∞β∈(ra_idx::('a ⇒ nat) set).
ra_mono_coeffs (ra_inverse_coeffs bphi) β γ *⇩R bphi β)"
by (rule ra_inverse_coeffs_coeff_equation_infsum[OF _ low])
show thesis
by (rule that[OF s0 conv coeff])
qed
qed
corollary ra_inverse_coeffs_component_series_on_near_zero:
fixes bphi :: "('a::euclidean_space ⇒ nat) ⇒ 'a"
assumes t0: "0 < t"
and majb: "ra_majorized t (λβ. norm (bphi β)) M"
obtains σ where "0 < σ"
and "⋀b. b ∈ Basis ⟹
ra_series_on (0::'a) σ (λγ. ra_inverse_coeffs bphi γ ∙ b)
(λh. (∑⇩∞γ∈(ra_idx::('a ⇒ nat) set).
ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ) ∙ b)"
proof -
show ?thesis
proof (rule ra_inverse_coeffs_power_series_converges_near_zero[OF t0 majb])
fix σ
assume s0: "0 < σ"
and conv: "⋀h::'a. norm h < σ ⟹
((λγ. ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ)
has_sum (∑⇩∞γ∈(ra_idx::('a ⇒ nat) set).
ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ))
(ra_idx::('a ⇒ nat) set)"
have ser: "ra_series_on (0::'a) σ (λγ. ra_inverse_coeffs bphi γ ∙ b)
(λh. (∑⇩∞γ∈(ra_idx::('a ⇒ nat) set).
ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ) ∙ b)"
if b: "b ∈ Basis" for b
unfolding ra_series_on_def
proof (intro allI impI)
fix h :: 'a
assume h: "dist h (0::'a) < σ"
have hs: "((λγ. ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ)
has_sum (∑⇩∞γ∈(ra_idx::('a ⇒ nat) set).
ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ))
(ra_idx::('a ⇒ nat) set)"
by (rule conv) (use h in ‹simp add: dist_norm›)
have "((λγ. (ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ) ∙ b)
has_sum ((∑⇩∞γ∈(ra_idx::('a ⇒ nat) set).
ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ) ∙ b))
(ra_idx::('a ⇒ nat) set)"
by (rule has_sum_bounded_linear[OF bounded_linear_inner_left hs])
thus "((λγ. ra_monomial (h - 0) γ *⇩R (ra_inverse_coeffs bphi γ ∙ b))
has_sum ((∑⇩∞γ∈(ra_idx::('a ⇒ nat) set).
ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ) ∙ b))
(ra_idx::('a ⇒ nat) set)"
by simp
qed
show thesis
by (rule that[OF s0 ser])
qed
qed
corollary ra_inverse_coeffs_mono_coeffs_series_on_near_zero:
fixes bphi :: "('a::euclidean_space ⇒ nat) ⇒ 'a"
assumes t0: "0 < t"
and majb: "ra_majorized t (λβ. norm (bphi β)) M"
obtains σ where "0 < σ"
and "⋀β. ra_series_on (0::'a) σ (ra_mono_coeffs (ra_inverse_coeffs bphi) β)
(λh. ra_monomial
(∑⇩∞γ∈(ra_idx::('a ⇒ nat) set).
ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ) β)"
proof -
show ?thesis
proof (rule ra_inverse_coeffs_power_series_converges_near_zero[OF t0 majb])
fix σ
assume s0: "0 < σ"
and conv: "⋀h::'a. norm h < σ ⟹
((λγ. ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ)
has_sum (∑⇩∞γ∈(ra_idx::('a ⇒ nat) set).
ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ))
(ra_idx::('a ⇒ nat) set)"
have ser: "ra_series_on (0::'a) σ (ra_mono_coeffs (ra_inverse_coeffs bphi) β)
(λh. ra_monomial
(∑⇩∞γ∈(ra_idx::('a ⇒ nat) set).
ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ) β)"
for β
by (rule ra_mono_coeffs_series[where c = "ra_inverse_coeffs bphi"])
(use conv in ‹simp add: dist_norm›)
show thesis
by (rule that[OF s0 ser])
qed
qed
text ‹Majorant bounds for the composed monomial families of any family without constant term
whose weighted profile partial sums are bounded.›
lemma ra_mono_coeffs_majorized:
fixes c :: "('a::euclidean_space ⇒ nat) ⇒ 'a"
assumes s0: "0 < σ"
and Bnn: "0 ≤ B"
and bnd: "⋀D. (∑i=1..D. ra_profile c i * σ ^ i) ≤ B"
and A0: "ra_profile c 0 = 0"
shows "ra_majorized σ (ra_mono_coeffs c β) (B ^ ra_deg β)"
proof -
have majabs: "ra_majorized σ (λγ. ¦ra_mono_coeffs c β γ¦) (B ^ ra_deg β)"
proof (rule ra_majorized_of_partial_profile_bounds)
show "⋀γ. 0 ≤ ¦ra_mono_coeffs c β γ¦" by simp
show "0 < σ" by (rule s0)
fix D :: nat
have prof_eq: "ra_profile_real (λγ. ¦ra_mono_coeffs c β γ¦) = ra_profile_real (ra_mono_coeffs c β)"
by (rule ext) (simp add: ra_profile_real_def)
show "(∑d≤D. ra_profile_real (λγ. ¦ra_mono_coeffs c β γ¦) d * σ ^ d) ≤ B ^ ra_deg β"
proof (cases "ra_deg β = 0")
case True
have "(∑d≤D. ra_profile_real (ra_mono_coeffs c β) d * σ ^ d)
≤ (∑d≤D. ra_seq_conv_pow (ra_profile c) 0 d * σ ^ d)"
by (smt (verit) True mult_right_mono ra_profile_real_mono_coeffs s0 sum_mono zero_le_power)
also have "… = 1"
proof -
have "{..D} = insert 0 {1..D}" by auto
thus ?thesis
by (simp add: ra_seq_delta_def)
qed
finally show ?thesis
using True by (simp add: prof_eq)
next
case False
hence k1: "1 ≤ ra_deg β" by simp
have "(∑d≤D. ra_profile_real (ra_mono_coeffs c β) d * σ ^ d)
≤ (∑d≤D. ra_seq_conv_pow (ra_profile c) (ra_deg β) d * σ ^ d)"
by (rule sum_mono, rule mult_right_mono)
(use ra_profile_real_mono_coeffs s0 in simp_all)
also have "… ≤ (∑i=1..D + 1 - ra_deg β. ra_profile c i * σ ^ i) ^ ra_deg β"
apply (rule ra_seq_conv_pow_partial_sum_le)
apply (simp add: ra_profile_nonneg)
apply (simp add: A0)
using s0 apply fastforce
using k1 by blast
also have "… ≤ B ^ ra_deg β"
by (rule power_mono[OF bnd])
(intro sum_nonneg mult_nonneg_nonneg ra_profile_nonneg zero_le_power,
use s0 in simp)
finally show ?thesis by (simp add: prof_eq)
qed
qed
have ra_weighted_abs_eq: "ra_weighted_abs σ (λγ. ¦ra_mono_coeffs c β γ¦) = ra_weighted_abs σ (ra_mono_coeffs c β)"
by (rule ext) (simp add: ra_weighted_abs_def)
show ?thesis
using majabs by (simp add: ra_majorized_def ra_weighted_abs_eq)
qed
corollary ra_inverse_coeffs_mono_coeffs_majorized:
fixes bphi :: "('a::euclidean_space ⇒ nat) ⇒ 'a"
defines "n ≡ real (card (Basis :: 'a set))"
assumes t0: "0 < t" and majb: "ra_majorized t (λβ. norm (bphi β)) M"
and s0: "0 < σ"
and s1: "σ ≤ t / (4 * n)"
and s2: "σ ≤ t⇧2 / (8 * (M + 1) * n)"
shows "ra_majorized σ (ra_mono_coeffs (ra_inverse_coeffs bphi) β) ((2 * n * σ) ^ ra_deg β)"
proof (rule ra_mono_coeffs_majorized)
show "0 < σ" by (rule s0)
show "0 ≤ 2 * n * σ"
using s0 by (simp add: n_def)
show "⋀D. (∑i=1..D. ra_profile (ra_inverse_coeffs bphi) i * σ ^ i) ≤ 2 * n * σ"
unfolding n_def
by (rule ra_inverse_coeffs_partial_sums_bounded[OF t0 majb s0])
(use s1 s2 in ‹simp_all add: n_def›)
show "ra_profile (ra_inverse_coeffs bphi) 0 = 0"
by (rule ra_profile_inverse_coeffs_0)
qed
lemma ra_series_on_majorized_value_bound:
fixes c :: "('a::euclidean_space ⇒ nat) ⇒ real"
assumes s0: "0 ≤ σ"
and rσ: "r ≤ σ"
and ser: "ra_series_on x0 r c F"
and maj: "ra_majorized σ c K"
and x: "dist x x0 < r"
shows "¦F x¦ ≤ K"
proof -
have hs: "((λα. ra_monomial (x - x0) α * c α) has_sum F x) ra_idx"
using ser x by (simp add: ra_series_on_def)
define S where "S = (∑⇩∞α∈ra_idx. ra_weighted_abs σ c α)"
have dom_sum: "(ra_weighted_abs σ c has_sum S) ra_idx"
unfolding S_def
using maj by (simp add: ra_majorized_def has_sum_infsum)
have hle: "norm (x - x0) ≤ σ"
using x rσ by (simp add: dist_norm)
have term_bound:
"¦ra_monomial (x - x0) α * c α¦ ≤ ra_weighted_abs σ c α"
if a: "α ∈ ra_idx" for α
proof -
have "¦ra_monomial (x - x0) α * c α¦
= ¦ra_monomial (x - x0) α¦ * ¦c α¦"
by (simp add: abs_mult)
also have "… ≤ σ ^ ra_deg α * ¦c α¦"
by (rule mult_right_mono[OF ra_monomial_abs_le_pow[OF a hle]]) simp
also have "… = ra_weighted_abs σ c α"
by (simp add: ra_weighted_abs_def mult.commute)
finally show ?thesis .
qed
have norm_le: "norm (F x) ≤ S"
by (rule norm_infsum_le[OF hs dom_sum]) (use term_bound in simp)
hence "¦F x¦ ≤ S"
by simp
also have "… ≤ K"
using maj by (simp add: S_def ra_majorized_def)
finally show ?thesis .
qed
lemma ra_inverse_coeffs_mono_coeffs_fubini_inputs_at_scale:
fixes bphi :: "('a::euclidean_space ⇒ nat) ⇒ 'a"
defines "n ≡ real (card (Basis :: 'a set))"
assumes t0: "0 < t" and majb: "ra_majorized t (λβ. norm (bphi β)) M"
and s0: "0 < σ"
and s1: "σ ≤ t / (4 * n)"
and s2: "σ ≤ t⇧2 / (8 * (M + 1) * n)"
shows mono_series:
"ra_series_on (0::'a) σ (ra_mono_coeffs (ra_inverse_coeffs bphi) β)
(λh. ra_monomial
(∑⇩∞γ∈(ra_idx::('a ⇒ nat) set).
ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ) β)"
and mono_maj:
"ra_majorized σ (ra_mono_coeffs (ra_inverse_coeffs bphi) β) ((2 * n * σ) ^ ra_deg β)"
and outer_summable:
"(λβ. norm (bphi β) * (2 * n * σ) ^ ra_deg β)
summable_on (ra_idx::('a ⇒ nat) set)"
proof -
show "ra_series_on (0::'a) σ (ra_mono_coeffs (ra_inverse_coeffs bphi) β)
(λh. ra_monomial
(∑⇩∞γ∈(ra_idx::('a ⇒ nat) set).
ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ) β)"
proof (rule ra_mono_coeffs_series[where c = "ra_inverse_coeffs bphi"])
fix h :: 'a
assume "dist h (0::'a) < σ"
show "((λγ. ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ)
has_sum (∑⇩∞γ∈(ra_idx::('a ⇒ nat) set).
ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ))
(ra_idx::('a ⇒ nat) set)"
unfolding n_def
by (rule ra_inverse_coeffs_power_series_has_sum[OF t0 majb s0])
(use s1 s2 ‹dist h (0::'a) < σ› in ‹simp_all add: n_def dist_norm›)
qed
next
show "ra_majorized σ (ra_mono_coeffs (ra_inverse_coeffs bphi) β) ((2 * n * σ) ^ ra_deg β)"
unfolding n_def
by (rule ra_inverse_coeffs_mono_coeffs_majorized[OF t0 majb s0])
(use s1 s2 in ‹simp_all add: n_def›)
next
have n1: "1 ≤ n"
unfolding n_def by simp
have K0: "0 ≤ 2 * n * σ"
using n1 s0 by simp
have Kt: "2 * n * σ < t"
proof -
have "2 * n * σ ≤ 2 * n * (t / (4 * n))"
using s1 n1 by (intro mult_left_mono) simp_all
also have "… = t / 2"
using n1 by (simp add: field_simps)
also have "… < t"
using t0 by simp
finally show ?thesis .
qed
show "(λβ. norm (bphi β) * (2 * n * σ) ^ ra_deg β)
summable_on (ra_idx::('a ⇒ nat) set)"
by (rule ra_majorized_geometric_weight_summable[OF t0 majb K0 Kt])
qed
lemma ra_inverse_coeffs_phi_comp_series_at_scale:
fixes bphi :: "('a::euclidean_space ⇒ nat) ⇒ 'a"
defines "n ≡ real (card (Basis :: 'a set))"
assumes t0: "0 < t" and majb: "ra_majorized t (λβ. norm (bphi β)) M"
and s0: "0 < σ"
and s1: "σ ≤ t / (4 * n)"
and s2: "σ ≤ t⇧2 / (8 * (M + 1) * n)"
shows "∀h. dist h (0::'a) < σ ⟶
((λγ. ra_monomial (h - 0) γ *⇩R
(∑⇩∞β∈(ra_idx::('a ⇒ nat) set).
ra_mono_coeffs (ra_inverse_coeffs bphi) β γ *⇩R bphi β))
has_sum
(∑⇩∞β∈(ra_idx::('a ⇒ nat) set).
ra_monomial
(∑⇩∞γ∈(ra_idx::('a ⇒ nat) set).
ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ) β *⇩R bphi β))
(ra_idx::('a ⇒ nat) set)"
proof -
define H where "H = (λh::'a.
∑⇩∞γ∈(ra_idx::('a ⇒ nat) set). ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ)"
have mono_series:
"ra_series_on (0::'a) σ (ra_mono_coeffs (ra_inverse_coeffs bphi) β)
(λh. ra_monomial (H h) β)" for β
unfolding H_def n_def
by (rule ra_inverse_coeffs_mono_coeffs_fubini_inputs_at_scale(1)[OF t0 majb s0])
(use s1 s2 in ‹simp_all add: n_def›)
have mono_maj:
"ra_majorized σ (ra_mono_coeffs (ra_inverse_coeffs bphi) β) ((2 * n * σ) ^ ra_deg β)" for β
unfolding n_def
by (rule ra_inverse_coeffs_mono_coeffs_fubini_inputs_at_scale(2)[OF t0 majb s0])
(use s1 s2 in ‹simp_all add: n_def›)
have outer_summable:
"(λβ. norm (bphi β) * (2 * n * σ) ^ ra_deg β)
summable_on (ra_idx::('a ⇒ nat) set)"
unfolding n_def
by (rule ra_inverse_coeffs_mono_coeffs_fubini_inputs_at_scale(3)[OF t0 majb s0])
(use s1 s2 in ‹simp_all add: n_def›)
have Gval:
"((λβ. ra_monomial (H h) β *⇩R bphi β)
has_sum
(∑⇩∞β∈(ra_idx::('a ⇒ nat) set).
ra_monomial (H h) β *⇩R bphi β))
(ra_idx::('a ⇒ nat) set)"
if h: "dist h (0::'a) < σ" for h
proof -
have val_bound:
"¦ra_monomial (H h) β¦ ≤ (2 * n * σ) ^ ra_deg β"
if b: "β ∈ (ra_idx::('a ⇒ nat) set)" for β
by (rule ra_series_on_majorized_value_bound[OF _ _ mono_series mono_maj h])
(use s0 in simp_all)
have abs_summ:
"(λβ. norm (ra_monomial (H h) β *⇩R bphi β))
summable_on (ra_idx::('a ⇒ nat) set)"
proof (rule summable_on_comparison_test[OF outer_summable])
fix β :: "'a ⇒ nat"
assume b: "β ∈ ra_idx"
have "norm (ra_monomial (H h) β *⇩R bphi β)
= ¦ra_monomial (H h) β¦ * norm (bphi β)"
by simp
also have "… ≤ (2 * n * σ) ^ ra_deg β * norm (bphi β)"
by (rule mult_right_mono[OF val_bound[OF b]]) simp
also have "… = norm (bphi β) * (2 * n * σ) ^ ra_deg β"
by (simp add: mult.commute)
finally show "norm (ra_monomial (H h) β *⇩R bphi β)
≤ norm (bphi β) * (2 * n * σ) ^ ra_deg β" .
next
fix β :: "'a ⇒ nat"
assume "β ∈ ra_idx"
show "0 ≤ norm (ra_monomial (H h) β *⇩R bphi β)"
by simp
qed
have summ: "(λβ. ra_monomial (H h) β *⇩R bphi β)
summable_on (ra_idx::('a ⇒ nat) set)"
by (rule abs_summable_summable[OF abs_summ])
show ?thesis
by (rule has_sum_infsum[OF summ])
qed
have main: "∀h. dist h (0::'a) < σ ⟶
((λγ. ra_monomial (h - 0) γ *⇩R
(∑⇩∞β∈(ra_idx::('a ⇒ nat) set).
ra_mono_coeffs (ra_inverse_coeffs bphi) β γ *⇩R bphi β))
has_sum
(∑⇩∞β∈(ra_idx::('a ⇒ nat) set).
ra_monomial (H h) β *⇩R bphi β))
(ra_idx::('a ⇒ nat) set)"
by (rule ra_series_on_majdom_vec
[where CC = "λβ. ra_mono_coeffs (ra_inverse_coeffs bphi) β"
and Fn = "λβ h. ra_monomial (H h) β"
and vg = bphi
and Kk = "λβ. (2 * n * σ) ^ ra_deg β"
and σ = σ and r = σ
and G = "λh. ∑⇩∞β∈(ra_idx::('a ⇒ nat) set).
ra_monomial (H h) β *⇩R bphi β"])
(use s0 mono_series mono_maj outer_summable Gval in auto)
show ?thesis
using main by (simp add: H_def)
qed
lemma ra_inverse_coeffs_functional_fixed_point_at_scale:
fixes bphi :: "('a::euclidean_space ⇒ nat) ⇒ 'a"
defines "n ≡ real (card (Basis :: 'a set))"
assumes t0: "0 < t" and majb: "ra_majorized t (λβ. norm (bphi β)) M"
and low: "⋀β. β ∈ ra_idx ⟹ ra_deg β < 2 ⟹ bphi β = 0"
and s0: "0 < σ"
and s1: "σ ≤ t / (4 * n)"
and s2: "σ ≤ t⇧2 / (8 * (M + 1) * n)"
shows "∀h. dist h (0::'a) < σ ⟶
(∑⇩∞γ∈(ra_idx::('a ⇒ nat) set). ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ)
= h + (∑⇩∞β∈(ra_idx::('a ⇒ nat) set).
ra_monomial
(∑⇩∞γ∈(ra_idx::('a ⇒ nat) set).
ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ) β *⇩R bphi β)"
proof (intro allI impI)
fix h :: 'a
assume h: "dist h (0::'a) < σ"
define H where "H =
(∑⇩∞γ∈(ra_idx::('a ⇒ nat) set). ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ)"
define N where "N =
(∑⇩∞β∈(ra_idx::('a ⇒ nat) set).
ra_monomial H β *⇩R bphi β)"
have Hhs: "((λγ. ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ) has_sum H)
(ra_idx::('a ⇒ nat) set)"
unfolding H_def n_def
by (rule ra_inverse_coeffs_power_series_has_sum[OF t0 majb s0])
(use s1 s2 h in ‹simp_all add: n_def dist_norm›)
have Nhs: "((λγ. ra_monomial (h - 0) γ *⇩R
(∑⇩∞β∈(ra_idx::('a ⇒ nat) set).
ra_mono_coeffs (ra_inverse_coeffs bphi) β γ *⇩R bphi β))
has_sum N) (ra_idx::('a ⇒ nat) set)"
proof -
have comp: "∀h. dist h (0::'a) < σ ⟶
((λγ. ra_monomial (h - 0) γ *⇩R
(∑⇩∞β∈(ra_idx::('a ⇒ nat) set).
ra_mono_coeffs (ra_inverse_coeffs bphi) β γ *⇩R bphi β))
has_sum
(∑⇩∞β∈(ra_idx::('a ⇒ nat) set).
ra_monomial
(∑⇩∞γ∈(ra_idx::('a ⇒ nat) set).
ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ) β *⇩R bphi β))
(ra_idx::('a ⇒ nat) set)"
unfolding n_def
by (rule ra_inverse_coeffs_phi_comp_series_at_scale[OF t0 majb s0])
(use s1 s2 in ‹simp_all add: n_def›)
show ?thesis
using comp h by (simp add: N_def H_def)
qed
have rhs_hs: "((λγ. ra_monomial h γ *⇩R
(ra_coeff_id γ + (∑⇩∞β∈(ra_idx::('a ⇒ nat) set).
ra_mono_coeffs (ra_inverse_coeffs bphi) β γ *⇩R bphi β)))
has_sum (h + N)) (ra_idx::('a ⇒ nat) set)"
proof -
have "((λγ. ra_monomial h γ *⇩R ra_coeff_id γ
+ ra_monomial h γ *⇩R
(∑⇩∞β∈(ra_idx::('a ⇒ nat) set).
ra_mono_coeffs (ra_inverse_coeffs bphi) β γ *⇩R bphi β))
has_sum (h + N)) (ra_idx::('a ⇒ nat) set)"
by (rule has_sum_add[OF ra_coeff_id_series Nhs[unfolded diff_zero]])
thus ?thesis
by (simp add: scaleR_add_right)
qed
have rhs_eq_inverse_coeffs:
"ra_monomial h γ *⇩R
(ra_coeff_id γ + (∑⇩∞β∈(ra_idx::('a ⇒ nat) set).
ra_mono_coeffs (ra_inverse_coeffs bphi) β γ *⇩R bphi β))
= ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ"
if g: "γ ∈ (ra_idx::('a ⇒ nat) set)" for γ
using ra_inverse_coeffs_coeff_equation_infsum[OF g low] by simp
have rhs_inverse_coeffs_hs: "((λγ. ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ)
has_sum (h + N)) (ra_idx::('a ⇒ nat) set)"
proof -
have "(((λγ. ra_monomial h γ *⇩R
(ra_coeff_id γ + (∑⇩∞β∈(ra_idx::('a ⇒ nat) set).
ra_mono_coeffs (ra_inverse_coeffs bphi) β γ *⇩R bphi β)))
has_sum (h + N)) (ra_idx::('a ⇒ nat) set))
= (((λγ. ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ)
has_sum (h + N)) (ra_idx::('a ⇒ nat) set))"
by (rule has_sum_cong) (use rhs_eq_inverse_coeffs in simp)
thus ?thesis
using rhs_hs by simp
qed
have "H = h + N"
using has_sum_unique[OF Hhs rhs_inverse_coeffs_hs] .
thus "(∑⇩∞γ∈(ra_idx::('a ⇒ nat) set). ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ)
= h + (∑⇩∞β∈(ra_idx::('a ⇒ nat) set).
ra_monomial
(∑⇩∞γ∈(ra_idx::('a ⇒ nat) set).
ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ) β *⇩R bphi β)"
by (simp add: H_def N_def)
qed
corollary ra_inverse_coeffs_right_inverse_at_scale:
fixes bphi :: "('a::euclidean_space ⇒ nat) ⇒ 'a"
defines "n ≡ real (card (Basis :: 'a set))"
assumes t0: "0 < t" and majb: "ra_majorized t (λβ. norm (bphi β)) M"
and low: "⋀β. β ∈ ra_idx ⟹ ra_deg β < 2 ⟹ bphi β = 0"
and s0: "0 < σ"
and s1: "σ ≤ t / (4 * n)"
and s2: "σ ≤ t⇧2 / (8 * (M + 1) * n)"
shows "∀h. dist h (0::'a) < σ ⟶
((∑⇩∞γ∈(ra_idx::('a ⇒ nat) set).
ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ)
- (∑⇩∞β∈(ra_idx::('a ⇒ nat) set).
ra_monomial
(∑⇩∞γ∈(ra_idx::('a ⇒ nat) set).
ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ) β *⇩R bphi β))
= h"
proof (intro allI impI)
fix h :: 'a
assume h: "dist h (0::'a) < σ"
have fp: "(∑⇩∞γ∈(ra_idx::('a ⇒ nat) set). ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ)
= h + (∑⇩∞β∈(ra_idx::('a ⇒ nat) set).
ra_monomial
(∑⇩∞γ∈(ra_idx::('a ⇒ nat) set).
ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ) β *⇩R bphi β)"
proof -
have allfp: "∀h. dist h (0::'a) < σ ⟶
(∑⇩∞γ∈(ra_idx::('a ⇒ nat) set). ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ)
= h + (∑⇩∞β∈(ra_idx::('a ⇒ nat) set).
ra_monomial
(∑⇩∞γ∈(ra_idx::('a ⇒ nat) set).
ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ) β *⇩R bphi β)"
unfolding n_def
by (rule ra_inverse_coeffs_functional_fixed_point_at_scale[OF t0 majb low s0])
(use s1 s2 in ‹simp_all add: n_def›)
show ?thesis
using allfp h by simp
qed
define P where "P = (∑⇩∞β∈(ra_idx::('a ⇒ nat) set).
ra_monomial
(∑⇩∞γ∈(ra_idx::('a ⇒ nat) set).
ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ) β *⇩R bphi β)"
have "(∑⇩∞γ∈(ra_idx::('a ⇒ nat) set).
ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ) - P = (h + P) - P"
using fp by (simp add: P_def)
also have "… = h"
by simp
finally show "((∑⇩∞γ∈(ra_idx::('a ⇒ nat) set).
ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ)
- (∑⇩∞β∈(ra_idx::('a ⇒ nat) set).
ra_monomial
(∑⇩∞γ∈(ra_idx::('a ⇒ nat) set).
ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ) β *⇩R bphi β))
= h"
by (simp add: P_def)
qed
lemma normalized_analytic_perturbation_coefficients:
fixes f :: "'a::euclidean_space ⇒ 'a"
assumes ana: "real_analytic_on f U"
and zero_U: "0 ∈ U"
and f0: "f 0 = 0"
and der0: "(f has_derivative id) (at 0)"
obtains r t bphi M where
"0 < r" "0 < t"
"⋀x. dist x (0::'a) < r ⟹
((λα. ra_monomial x α *⇩R bphi α) has_sum (x - f x))
(ra_idx::('a ⇒ nat) set)"
"ra_majorized t (λα. norm (bphi α)) M"
"⋀α. α ∈ ra_idx ⟹ ra_deg α < 2 ⟹ bphi α = 0"
proof -
from ana zero_U obtain r c where r0: "0 < r"
and fser: "⋀x. dist x (0::'a) < r ⟹
((λα. ra_monomial (x - 0) α *⇩R c α) has_sum f x)
(ra_idx::('a ⇒ nat) set)"
unfolding real_analytic_on_def by blast
define bphi where "bphi = (λα. ra_coeff_id α - c α)"
have phiser: "((λα. ra_monomial x α *⇩R bphi α) has_sum (x - f x))
(ra_idx::('a ⇒ nat) set)"
if x: "dist x (0::'a) < r" for x
proof -
have idser: "((λα. ra_monomial x α *⇩R ra_coeff_id α) has_sum x)
(ra_idx::('a ⇒ nat) set)"
by (rule ra_coeff_id_series)
have fserx: "((λα. ra_monomial x α *⇩R c α) has_sum f x)
(ra_idx::('a ⇒ nat) set)"
using fser[OF x] by simp
have neg_fser: "((λα. - (ra_monomial x α *⇩R c α)) has_sum (- f x))
(ra_idx::('a ⇒ nat) set)"
using fserx by (simp add: has_sum_uminus)
have "((λα. ra_monomial x α *⇩R ra_coeff_id α
+ (- (ra_monomial x α *⇩R c α))) has_sum (x + (- f x)))
(ra_idx::('a ⇒ nat) set)"
by (rule has_sum_add[OF idser neg_fser])
thus ?thesis
by (simp add: bphi_def scaleR_diff_right)
qed
have c0: "c ra_idx_zero = 0"
proof -
have hs: "((λα. ra_monomial (0::'a) α *⇩R c α) has_sum f 0)
(ra_idx::('a ⇒ nat) set)"
using fser[of 0] r0 by simp
show ?thesis
using ra_series_at_zero_coeff[OF hs] f0 by simp
qed
have fd_id: "frechet_derivative f (at 0) = id"
using frechet_derivative_at[OF der0] by simp
have low: "bphi α = 0" if a: "α ∈ ra_idx" and lt: "ra_deg α < 2" for α
proof (cases "ra_deg α = 0")
case True
hence "α = ra_idx_zero"
using ra_deg_eq0_iff[OF a] by simp
thus ?thesis
by (simp add: bphi_def c0 ra_coeff_id_idx_zero)
next
case False
hence d1: "ra_deg α = 1"
using lt by simp
obtain b where b: "b ∈ Basis" and alpha: "α = ra_idx_unit b"
by (rule ra_deg_one_unit[OF a d1])
have c_lin: "c (ra_idx_unit b) = b"
proof -
have "c (λx. if x = b then 1 else 0) = frechet_derivative f (at 0) b"
by (rule ra_linear_coeff_eq_frechet_derivative_basis[OF b r0 fser])
thus ?thesis
by (simp add: ra_idx_unit_def fd_id)
qed
show ?thesis
using b by (simp add: bphi_def alpha c_lin ra_coeff_id_unit)
qed
define eB where "eB = (∑b∈(Basis::'a set). b)"
have eBpos: "0 < norm eB"
proof -
have "eB ≠ 0"
proof
assume "eB = 0"
then have zero_inner: "eB ∙ (SOME b. b ∈ (Basis::'a set)) = 0"
by simp
obtain b0 :: 'a where b0: "b0 ∈ Basis"
using nonempty_Basis by blast
have someB: "(SOME b. b ∈ (Basis::'a set)) ∈ Basis"
using b0 by (rule someI)
hence "eB ∙ (SOME b. b ∈ (Basis::'a set)) = 1"
by (simp add: eB_def inner_sum_left inner_Basis)
thus False
using zero_inner by simp
qed
thus ?thesis by simp
qed
define ρ where "ρ = r / (2 * norm eB)"
have ρ0: "0 < ρ"
using r0 eBpos by (simp add: ρ_def)
have corner: "ρ * norm (∑b∈(Basis::'a set). b) < r"
proof -
have "ρ * norm eB = r / 2"
using eBpos by (simp add: ρ_def)
also have "… < r"
using r0 by simp
finally show ?thesis
by (simp add: eB_def)
qed
have phiser0: "⋀z. dist z (0::'a) < r ⟹
((λα. ra_monomial (z - 0) α *⇩R bphi α) has_sum (z - f z))
(ra_idx::('a ⇒ nat) set)"
using phiser by simp
obtain M0 where M0nn: "M0 ≥ 0"
and bnd: "⋀α. α ∈ ra_idx ⟹ norm (bphi α) ≤ M0 / ρ ^ ra_deg α"
using ra_coeff_bound[OF r0 phiser0 ρ0 corner] by blast
define t where "t = ρ / 2"
have t0: "0 < t"
using ρ0 by (simp add: t_def)
have t_lt: "t < ρ"
using ρ0 by (simp add: t_def)
define M where "M = M0 * (∑⇩∞α∈(ra_idx::('a ⇒ nat) set). (t / ρ) ^ ra_deg α)"
have maj: "ra_majorized t (λα. norm (bphi α)) M"
unfolding M_def
by (rule coeff_majorized_of_bound[OF M0nn bnd ρ0])
(use t0 t_lt in simp_all)
show ?thesis
by (rule that[OF r0 t0 phiser maj low])
qed
theorem normalized_analytic_formal_right_inverse:
fixes f :: "'a::euclidean_space ⇒ 'a"
assumes ana: "real_analytic_on f U"
and zero_U: "0 ∈ U"
and f0: "f 0 = 0"
and der0: "(f has_derivative id) (at 0)"
obtains σ bphi where
"0 < σ"
"real_analytic_on
(λh::'a. ∑⇩∞γ∈(ra_idx::('a ⇒ nat) set).
ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ)
(ball (0::'a) (σ / 2))"
"⋀h::'a. norm h < σ ⟹
((λγ. ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ)
has_sum (∑⇩∞γ∈(ra_idx::('a ⇒ nat) set).
ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ))
(ra_idx::('a ⇒ nat) set)"
"⋀h::'a. norm h < σ ⟹
f (∑⇩∞γ∈(ra_idx::('a ⇒ nat) set).
ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ) = h"
proof -
show ?thesis
proof (rule normalized_analytic_perturbation_coefficients[OF ana zero_U f0 der0])
fix r t bphi M
assume r0: "0 < r" and t0: "0 < t"
and phiser: "⋀x. dist x (0::'a) < r ⟹
((λα. ra_monomial x α *⇩R bphi α) has_sum (x - f x))
(ra_idx::('a ⇒ nat) set)"
and majb: "ra_majorized t (λα. norm (bphi α)) M"
and low: "⋀α. α ∈ ra_idx ⟹ ra_deg α < 2 ⟹ bphi α = 0"
define n where "n = real (card (Basis :: 'a set))"
have n1: "1 ≤ n"
unfolding n_def by simp
have M0: "0 ≤ M"
proof -
have "0 ≤ (∑⇩∞α∈ra_idx. ra_weighted_abs t (λα. norm (bphi α)) α)"
using t0 by (intro infsum_nonneg) (simp add: ra_weighted_abs_nonneg)
also have "… ≤ M"
using majb by (simp add: ra_majorized_def)
finally show ?thesis .
qed
define a where "a = t / (4 * n)"
define b where "b = t⇧2 / (8 * (M + 1) * n)"
define c where "c = r / (4 * n)"
define σ where "σ = min (min a b) c / 2"
have a0: "0 < a"
using t0 n1 by (simp add: a_def)
have b0: "0 < b"
unfolding b_def
using t0 M0 n1 by (intro divide_pos_pos mult_pos_pos) simp_all
have c0: "0 < c"
using r0 n1 by (simp add: c_def)
have min0: "0 < min (min a b) c"
using a0 b0 c0 by simp
have σ0: "0 < σ"
using min0 by (simp add: σ_def)
have half_min_le: "min (min a b) c / 2 ≤ min (min a b) c"
proof -
have "min (min a b) c / 2 = (1/2) * min (min a b) c"
by simp
also have "… ≤ 1 * min (min a b) c"
by (rule mult_right_mono) (use min0 in simp_all)
finally show ?thesis by simp
qed
have s1: "σ ≤ t / (4 * n)"
proof -
have "σ ≤ min (min a b) c"
unfolding σ_def by (rule half_min_le)
also have "… ≤ a"
by simp
finally show ?thesis
by (simp add: a_def)
qed
have s2: "σ ≤ t⇧2 / (8 * (M + 1) * n)"
proof -
have "σ ≤ min (min a b) c"
unfolding σ_def by (rule half_min_le)
also have "… ≤ b"
by simp
finally show ?thesis
by (simp add: b_def)
qed
have s3: "2 * n * σ < r"
proof -
have "σ ≤ c / 2"
proof -
have "min (min a b) c ≤ c"
by simp
hence "min (min a b) c / 2 ≤ c / 2"
by simp
thus ?thesis
by (simp add: σ_def)
qed
hence "2 * n * σ ≤ 2 * n * (c / 2)"
using n1 by (intro mult_left_mono) simp_all
also have "… = r / 4"
using n1 by (simp add: c_def field_simps)
also have "… < r"
using r0 by simp
finally show ?thesis .
qed
have Hana: "real_analytic_on
(λh::'a. ∑⇩∞γ∈(ra_idx::('a ⇒ nat) set).
ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ)
(ball (0::'a) (σ / 2))"
unfolding n_def
by (rule ra_inverse_coeffs_power_series_real_analytic_on_ball_at_scale[OF t0 majb σ0])
(use s1 s2 in ‹simp_all add: n_def›)
show ?thesis
proof (rule that[OF σ0 Hana])
fix h :: 'a
assume h: "norm h < σ"
show "((λγ. ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ)
has_sum (∑⇩∞γ∈(ra_idx::('a ⇒ nat) set).
ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ))
(ra_idx::('a ⇒ nat) set)"
unfolding n_def
by (rule ra_inverse_coeffs_power_series_has_sum[OF t0 majb σ0])
(use h s1 s2 in ‹simp_all add: n_def›)
next
fix h :: 'a
assume h: "norm h < σ"
let ?H = "∑⇩∞γ∈(ra_idx::('a ⇒ nat) set).
ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ"
let ?P = "∑⇩∞β∈(ra_idx::('a ⇒ nat) set).
ra_monomial ?H β *⇩R bphi β"
have hle: "norm h ≤ σ"
using h by simp
have Hle: "norm ?H ≤ 2 * n * σ"
unfolding n_def
by (rule ra_inverse_coeffs_value_norm_bound_at_scale[OF t0 majb σ0])
(use s1 s2 hle in ‹simp_all add: n_def›)
have Hr: "dist ?H (0::'a) < r"
using Hle s3 by (simp add: dist_norm)
have phi_hs: "((λβ. ra_monomial ?H β *⇩R bphi β) has_sum (?H - f ?H))
(ra_idx::('a ⇒ nat) set)"
using phiser[OF Hr] by simp
have phi_sum: "((λβ. ra_monomial ?H β *⇩R bphi β) has_sum ?P)
(ra_idx::('a ⇒ nat) set)"
by (rule has_sum_infsum) (rule has_sum_imp_summable[OF phi_hs])
have Peq: "?P = ?H - f ?H"
by (rule has_sum_unique[OF phi_sum phi_hs])
have right: "?H - ?P = h"
proof -
have all_right: "∀h. dist h (0::'a) < σ ⟶
((∑⇩∞γ∈(ra_idx::('a ⇒ nat) set).
ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ)
- (∑⇩∞β∈(ra_idx::('a ⇒ nat) set).
ra_monomial
(∑⇩∞γ∈(ra_idx::('a ⇒ nat) set).
ra_monomial h γ *⇩R ra_inverse_coeffs bphi γ) β *⇩R bphi β))
= h"
unfolding n_def
by (rule ra_inverse_coeffs_right_inverse_at_scale[OF t0 majb low σ0])
(use s1 s2 in ‹simp_all add: n_def›)
show ?thesis
using all_right h by (simp add: dist_norm)
qed
show "f ?H = h"
using right Peq by simp
qed
qed
qed
end