Theory Universal_Approximation
section ‹Universal Approximation Theorem›
theory Universal_Approximation
imports Asymptotic_Qualitative_Properties
begin
text ‹
In this theory, we formalize the Universal Approximation Theorem (UAT)
for continuous functions on a closed interval \([a,b]\). The theorem
states that any continuous function \(f\colon [a,b]\to \mathbb{R}\) can be
uniformly approximated by a finite linear combination of shifted and
scaled sigmoidal functions. The classical result was first proved by
Cybenko~\cite{Cybenko} and later constructively by Costarelli and Spigler~\cite{CostarelliSpigler},
the latter approach forms the basis of our formalization.
Their paper is available online at
\url{https://link.springer.com/article/10.1007/s10231-013-0378-y}.
›
lemma uniform_continuity_interval:
fixes f :: "real ⇒ real"
assumes "a < b"
assumes "continuous_on {a..b} f"
assumes "ε > 0"
shows "∃δ>0. (∀x y. x ∈ {a..b} ∧ y ∈ {a..b} ∧ ¦x - y¦ < δ ⟶ ¦f x - f y¦ < ε)"
proof -
have "uniformly_continuous_on {a..b} f"
using assms(1,2) compact_uniformly_continuous by blast
thus ?thesis
unfolding uniformly_continuous_on_def
by (metis assms(3) dist_real_def)
qed
definition bounded_function :: "(real ⇒ real) ⇒ bool" where
"bounded_function f ⟷ bdd_above (range (λx. ¦f x¦))"
definition unif_part :: "real ⇒ real ⇒ nat ⇒ real list" where
"unif_part a b N =
map (λk. a + (real k -1 ) * ((b - a) / real N )) [0..<N+2]"
value "unif_part (0::real) 1 4"
theorem sigmoidal_approximation_theorem:
assumes sigmoidal_function: "sigmoidal σ"
assumes bounded_sigmoidal: "bounded_function σ"
assumes a_lt_b: "a < b"
assumes contin_f: "continuous_on {a..b} f"
assumes eps_pos: "0 < ε"
defines "xs N ≡ unif_part a b N"
shows "∃N::nat. ∃(w::real) > 0.(N > 0) ∧
(∀x ∈ {a..b}.
¦(∑k∈{2..N+1}. (f(xs N ! k) - f(xs N ! (k - 1))) * σ(w * (x - xs N ! k)))
+ f(a) * σ(w * (x - xs N ! 0)) - f x¦ < ε)"
proof-
obtain η where η_def: "η = ε / ((Sup ((λx. ¦f x¦) ` {a..b})) + (2 * (Sup ((λx. ¦σ x¦) ` UNIV))) + 2)"
by blast
have η_pos: "η > 0"
unfolding η_def
proof -
have sup_abs_nonneg: "Sup ((λx. ¦f x¦) ` {a..b}) ≥ 0"
proof -
have "∀x ∈ {a..b}. ¦f x¦ ≥ 0"
by simp
hence "bdd_above ((λx. ¦f x¦) ` {a..b})"
by (metis a_lt_b bdd_above_Icc contin_f continuous_image_closed_interval continuous_on_rabs order_less_le)
thus ?thesis
by (meson a_lt_b abs_ge_zero atLeastAtMost_iff cSUP_upper2 order_le_less)
qed
have sup_σ_nonneg: "Sup ((λx. ¦σ x¦) ` UNIV) ≥ 0"
proof -
have "∀x ∈ {a..b}. ¦σ x¦ ≥ 0"
by simp
hence "bdd_above ((λx. ¦σ x¦) ` UNIV)"
using bounded_function_def bounded_sigmoidal by presburger
thus ?thesis
by (meson abs_ge_zero cSUP_upper2 iso_tuple_UNIV_I)
qed
obtain denom where denom_def: "denom = (Sup ((λx. ¦f x¦) ` {a..b})) + (2 * (Sup ((λx. ¦σ x¦) ` UNIV))) + 2"
by blast
have denom_pos: "denom > 0"
proof -
have two_sup_σ_nonneg: "0 ≤ 2 * (Sup ((λx. ¦σ x¦) ` UNIV))"
by(rule mult_nonneg_nonneg, simp, simp add: sup_σ_nonneg)
have "0 ≤ (Sup ((λx. ¦f x¦) ` {a..b})) + 2 * (Sup ((λx. ¦σ x¦) ` UNIV))"
by(rule add_nonneg_nonneg, smt sup_abs_nonneg, smt two_sup_σ_nonneg)
then have "denom ≥ 2" unfolding denom_def
by linarith
thus "denom > 0" by linarith
qed
then show "0 < ε / ((SUP x ∈ {a..b}. ¦f x¦) + 2 * (SUP x ∈ UNIV . ¦σ x¦) + 2)"
using eps_pos sup_σ_nonneg sup_abs_nonneg by auto
qed
have "∃δ>0. ∀x y. x ∈ {a..b} ∧ y ∈ {a..b} ∧ ¦x - y¦ < δ ⟶ ¦f x - f y¦ < η"
by(rule uniform_continuity_interval,(simp add: assms(3,4))+, simp add: η_pos)
then obtain δ where δ_pos: "δ > 0"
and δ_prop: "∀x ∈ {a..b}. ∀y ∈ {a..b}. ¦x - y¦ < δ ⟶ ¦f x - f y¦ < η"
by blast
obtain N where N_def: "N = (nat (⌊max 3 (max (2 * (b - a) / δ) (1 / η))⌋) + 1)"
by simp
have N_defining_properties: "N > 2 * (b - a) / δ ∧ N > 3 ∧ N > 1 / η"
unfolding N_def
proof -
have "max 3 (max (2 * (b - a) / δ) (1 / η)) ≥ 2 * (b - a) / δ ∧
max 3 (max (2 * (b - a) / δ) (1 / η)) ≥ 2 ∧
max 3 (max (2 * (b - a) / δ) (1 / η)) ≥ 1 / η"
unfolding max_def by simp
then show "2 * (b - a) / δ < nat ⌊max 3 (max (2 * (b - a) / δ) (1 / η))⌋ + 1 ∧
3 < nat ⌊max 3 (max (2 * (b - a) / δ) (1 / η))⌋ + 1 ∧
1 / η < nat ⌊max 3 (max (2 * (b - a) / δ) (1 / η))⌋ + 1"
by (smt (verit, best) floor_le_one numeral_Bit1 numeral_less_real_of_nat_iff numeral_plus_numeral of_nat_1 of_nat_add of_nat_nat one_plus_numeral real_of_int_floor_add_one_gt)
qed
then have N_gt_3: "N > 3"
by simp
then have N_pos: "N > 0"
by simp
obtain h where h_def: "h = (b-a)/N"
by simp
then have h_pos: "h > 0"
using N_defining_properties a_lt_b by force
have h_lt_δ_half: "h < δ / 2"
proof -
have "N > 2 * (b - a) / δ"
using N_defining_properties by force
then have "N /2 > (b - a) / δ"
by (simp add: mult.commute)
then have " (N /2) * δ > (b - a)"
by (smt (verit, ccfv_SIG) δ_pos divide_less_cancel nonzero_mult_div_cancel_right)
then have " (δ /2) * N > (b - a)"
by (simp add: mult.commute)
then have " (δ /2) > (b - a) / N"
by (smt (verit, ccfv_SIG) δ_pos a_lt_b divide_less_cancel nonzero_mult_div_cancel_right zero_less_divide_iff)
then show "h < δ / 2"
using h_def by blast
qed
have one_over_N_lt_eta: "1 / N < η"
proof -
have f1: "real N ≥ max (2 * (b - a) / δ - 1) (1 / η)"
unfolding N_def by linarith
have "real N ≥ 1 / η"
unfolding max_def using f1 max.bounded_iff by blast
hence f2: "1 / real N ≤ η"
using η_pos by (smt (verit, ccfv_SIG) divide_divide_eq_right le_divide_eq_1 mult.commute zero_less_divide_1_iff)
then show "1 / real N < η"
using N_defining_properties nle_le by fastforce
qed
have xs_eqs: "xs N = map (λk. a + (real k - 1) * ((b - a) / N)) [0..<N+2]"
using unif_part_def xs_def by presburger
then have xs_els: "⋀k. k ∈ {0..N+1} ⟶ xs N ! k = a + (real k-1) * h"
by (metis (no_types, lifting) Suc_1 add_0 add_Suc_right atLeastAtMost_iff diff_zero h_def linorder_not_le not_less_eq_eq nth_map_upt)
have zeroth_element: "xs N !0 = a-h"
by (simp add: xs_els)
have first_element: "xs N !1 = a"
by (simp add: xs_els)
have last_element: "xs N !(N+1) = b"
proof -
have "xs N !(N+1) = a + N * h"
using xs_els by force
then show ?thesis
by (simp add: N_pos h_def)
qed
have difference_of_terms: "⋀j k . j ∈ {1..N+1} ∧ k ∈ {1..N+1} ∧ j≤ k ⟶ xs N ! k - xs N ! j = h*(real k-j)"
proof(clarify)
fix j k
assume j_type: "j ∈ {1..N + 1}"
assume k_type: "k ∈ {1..N + 1}"
assume j_leq_k: "j ≤ k"
have j_th_el: "xs N ! j = (a + (real j-1) * h)"
using j_type xs_els by auto
have k_th_el: "xs N ! k = (a + (real k-1) * h)"
using k_type xs_els by auto
then show "xs N ! k - xs N ! j = h * (real k - j)"
by (smt (verit, del_insts) j_th_el left_diff_distrib' mult.commute)
qed
then have difference_of_adj_terms: "⋀k . k ∈ {1..N+1} ⟶ xs N ! k - xs N ! (k-1) = h"
proof -
fix k :: nat
have "k = 1 ⟶ k ∈ {1..N + 1} ⟶ xs N ! k - xs N ! (k - 1) = h"
using first_element zeroth_element by auto
then show "k ∈ {1..N + 1} ⟶ xs N ! k - xs N ! (k - 1) = h"
using difference_of_terms le_diff_conv by fastforce
qed
have adj_terms_lt: "⋀k . k ∈ {1..N+1} ⟶ ¦xs N ! k - xs N ! (k - 1)¦ < δ"
proof(clarify)
fix k
assume k_type: "k ∈ {1..N + 1}"
then have "¦xs N ! k - xs N ! (k - 1)¦ = h"
using difference_of_adj_terms h_pos by auto
also have "... < δ /2"
using h_lt_δ_half by auto
also have "... < δ"
by (simp add: δ_pos)
finally show "¦xs N ! k - xs N ! (k - 1)¦ < δ".
qed
from difference_of_terms have list_increasing: "⋀j k . j ∈ {1..N+1} ∧ k ∈ {1..N+1} ∧ j ≤ k ⟶ xs N ! j ≤ xs N !k"
by (smt (verit, ccfv_SIG) h_pos of_nat_eq_iff of_nat_mono zero_less_mult_iff)
have els_in_ab: "⋀k. k ∈ {1..N+1} ⟶ xs N ! k ∈ {a..b}"
using first_element last_element list_increasing by force
from sigmoidal_function N_pos h_pos have "∃ω > 0. ∀w ≥ ω. ∀k < length (xs N).
(∀x. x - xs N !k ≥ h ⟶ ¦σ (w * (x - xs N !k)) - 1¦ < 1/N) ∧
(∀x. x - xs N!k ≤ -h ⟶ ¦σ (w * (x - xs N!k))¦ < 1/N)"
by(subst sigmoidal_uniform_approximation, simp_all)
then obtain ω where ω_pos: "ω > 0"
and ω_prop: "∀w ≥ ω. ∀k < length (xs N).
(∀x. x - xs N !k ≥ h ⟶ ¦σ (w * (x - xs N !k)) - 1¦ < 1/N) ∧
(∀x. x - xs N !k ≤ -h ⟶ ¦σ (w * (x - xs N!k))¦ < 1/N)"
by blast
then obtain w where w_def: "w ≥ ω" and w_prop: "∀k < length (xs N).
(∀x. x - xs N !k ≥ h ⟶ ¦σ (w * (x - xs N !k)) - 1¦ < 1/N) ∧
(∀x. x - xs N !k ≤ -h ⟶ ¦σ (w * (x - xs N!k))¦ < 1/N)"
and w_pos: "w > 0"
by auto
obtain G_Nf where G_Nf_def:
"G_Nf ≡ (λx.
(∑k∈{2..N+1}. (f (xs N ! k) - f (xs N ! (k - 1))) * σ (w * (x - xs N ! k)))
+ f (xs N ! 1) * σ (w * (x - xs N ! 0)))"
by blast
show "∃N w. 0 < w ∧ 0 < N ∧ (∀x∈{a..b}. ¦(∑k = 2..N + 1. (f (xs N ! k) - f (xs N ! (k - 1))) * σ (w * (x - xs N ! k))) + f a * σ (w * (x - xs N ! 0)) - f x¦ < ε)"
proof (intro exI[where x=N] exI[where x=w] conjI allI impI insert w_pos N_pos xs_def, safe)
fix x::real
assume x_in_ab: "x ∈ {a..b}"
have "∃i. i ∈ {1..N} ∧ x ∈ {xs N ! i .. xs N ! (i+1)}"
proof -
have intervals_cover: "{xs N ! 1 .. xs N ! (N+1)} ⊆ (⋃i∈{1..N}. {xs N! i .. xs N! (i+1)})"
proof
fix x::real
assume x_def: "x ∈ {xs N! 1 .. xs N ! (N+1)}"
then have lower_bound: "x ≥ xs N ! 1"
by simp
from x_def have upper_bound: "x ≤ xs N! (N+1)"
by simp
obtain j where j_def: "j = (GREATEST j. xs N ! j ≤ x ∧ j ∈ {1..N+1})"
by blast
have nonempty_definition: "{j ∈ {1..N+1}. xs N ! j ≤ x} ≠ {}"
using lower_bound by force
then have j_exists:"∃j ∈ {1..N+1}. xs N ! j ≤ x"
by blast
then have j_bounds: "j ∈ {1..N+1}"
by (smt (verit) GreatestI_nat atLeastAtMost_iff j_def)
have xs_j_leq_x: "xs N ! j ≤ x"
by (smt (verit, del_insts) GreatestI_ex_nat GreatestI_nat atLeastAtMost_iff ex_least_nat_le j_def j_exists)
show "x ∈ (⋃i ∈ {1..N}. {xs N ! i..xs N ! (i + 1)})"
proof(cases "j = N+1")
show "j = N + 1 ⟹ x ∈ (⋃i ∈ {1..N}. {xs N ! i..xs N ! (i + 1)})"
using N_pos els_in_ab last_element upper_bound xs_j_leq_x by force
next
assume j_not_SucN:"j ≠ N + 1"
then have j_type: "j ∈ {1..N}"
by (metis Suc_eq_plus1 atLeastAtMost_iff j_bounds le_Suc_eq)
then have Suc_j_type: "j + 1 ∈ {2..N+1}"
by (metis Suc_1 Suc_eq_plus1 atLeastAtMost_iff diff_Suc_Suc diff_is_0_eq)
have equal_sets: "{j ∈ {1..N+1}. xs N ! j ≤ x} = {j ∈ {1..N}. xs N ! j ≤ x}"
proof
show "{j ∈ {1..N}. xs N ! j ≤ x} ⊆ {j ∈ {1..N + 1}. xs N ! j ≤ x}"
by auto
show "{j ∈ {1..N + 1}. xs N ! j ≤ x} ⊆ {j ∈ {1..N}. xs N ! j ≤ x}"
by (safe, metis (no_types, lifting) Greatest_equality Suc_eq_plus1 j_not_SucN atLeastAtMost_iff j_def le_Suc_eq)
qed
have xs_j1_not_le_x: "¬ (xs N ! (j+1) ≤ x)"
proof(rule ccontr)
assume BWOC: "¬ ¬ xs N ! (j + 1) ≤ x"
then have Suc_j_type':"j+1 ∈ {1..N}"
using Suc_j_type equal_sets add.commute by auto
from j_def show False
using equal_sets
by (smt (verit, del_insts) BWOC Greatest_le_nat One_nat_def Suc_eq_plus1 Suc_j_type' Suc_n_not_le_n atLeastAtMost_iff mem_Collect_eq)
qed
then have "x ∈ {xs N ! j .. xs N ! (j+1)}"
by (simp add: xs_j_leq_x)
then show ?thesis
using j_type by blast
qed
qed
then show ?thesis
using first_element last_element x_in_ab by fastforce
qed
then obtain i where i_def: "i ∈ {1..N} ∧ x ∈ {xs N ! i .. xs N ! (i+1)}"
by blast
then have i_ge_1: "i ≥ 1"
using atLeastAtMost_iff by blast
have i_leq_N: "i ≤ N"
using i_def by presburger
then have xs_i: "xs N ! i = a + (real i - 1) * h"
using xs_els by force
have xs_Suc_i: "xs N ! (i + 1) = a + real i * h"
proof -
have "(i+1) ∈ {0..N+1} ⟶ xs N ! (i+1) = a + (real (i+1) - 1) * h"
using xs_els by blast
then show ?thesis
using i_leq_N by fastforce
qed
from i_def have x_lower_bound_aux: "x ≥ (xs N ! i)"
using atLeastAtMost_iff by blast
then have x_lower_bound: "x ≥ a + real (i-1) * h"
by (metis xs_i i_ge_1 of_nat_1 of_nat_diff)
from i_def have x_upper_bound_aux: "xs N! (i+1) ≥ x"
using atLeastAtMost_iff by blast
then have x_upper_bound: "a + real i * h ≥ x"
using xs_Suc_i by fastforce
obtain L where L_def:
"⋀i. L i = (if i = 1 ∨ i = 2 then
(λx. f(a) + (f (xs N ! 3) - f (xs N ! 2)) * σ (w * (x - xs N ! 3)) +
(f (xs N ! 2) - f (xs N ! 1)) * σ (w * (x - xs N ! 2)))
else
(λx. (∑k∈{2..i-1}. (f (xs N ! k) - f (xs N ! (k - 1)))) + f(a) +
(f (xs N ! i) - f (xs N ! (i-1))) * σ (w * (x - xs N ! i)) +
(f (xs N ! (i+1)) - f (xs N ! i)) * σ (w * (x - xs N ! (i+1)))))"
by force
obtain I_1 where I_1_def: "⋀i.1 ≤ i ∧ i ≤ N ⟶ I_1 i = (λx. ¦G_Nf x - L i x¦)"
by force
obtain I_2 where I_2_def: "⋀i. 1 ≤ i ∧ i ≤ N ⟶ I_2 i = (λx. ¦L i x - f x¦)"
by force
have triange_inequality_main: "⋀i x. 1 ≤ i ∧ i ≤ N ⟶ ¦G_Nf x - f x¦ ≤ I_1 i x + I_2 i x"
using I_1_def I_2_def by force
have x_minus_xk_ge_h_on_Left_Half:
"∀k. k ∈ {0..i-1} ⟶ x - xs N ! k ≥ h"
proof (clarify)
fix k
assume k_def: "k ∈ {0..i-1}"
then have k_pred_lt_i_pred: "real k- 1 < real i-1"
using i_ge_1 by fastforce
have "x - xs N!k = x - (a + (real k - 1) * h)"
proof(cases "k=0")
show "k = 0 ⟹ x - xs N ! k = x - (a + (real k - 1) * h)"
by (simp add: zeroth_element)
next
assume k_nonzero: "k ≠ 0"
then have k_def2: "k ∈ {1..N+1}"
using i_def k_def less_diff_conv2 by auto
then have "x - xs N ! k = x - (a + (real k - 1) * h)"
by (simp add: xs_els)
then show ?thesis
using k_nonzero by force
qed
also have "... ≥ h"
proof(cases "k=0")
show "k = 0 ⟹ h ≤ x - (a + (real k - 1) * h)"
using x_in_ab by force
next
assume k_nonzero: "k ≠ 0"
then have k_type: "k ∈ {1..N}"
using i_leq_N k_def by fastforce
have difference_of_terms: "(xs N!i) - (a+(real k - 1)*h) = ((real i-1) - (real k-1))*h"
by (simp add: xs_i left_diff_distrib')
then have first_inequality: "x - (a + (real k - 1) * h) ≥ (xs N!i) - (a+(real k - 1)*h)"
using i_def by auto
have second_inequality: "(xs N!i) - (a+(real k - 1)*h) ≥ h"
using difference_of_terms h_pos k_def k_nonzero by force
then show ?thesis
using first_inequality by auto
qed
finally show "h ≤ x - xs N ! k".
qed
have x_minus_xk_le_neg_h_on_Right_Half:
"∀k. k ∈ {i+2..N+1} ⟶ x - xs N ! k ≤ -h"
proof (clarify)
fix k
assume k_def: "k ∈ {i+2..N+1}"
then have i_lt_k_pred: "i < k-1"
by (metis Suc_1 add_Suc_right atLeastAtMost_iff less_diff_conv less_eq_Suc_le)
then have k_nonzero: "k ≠ 0"
by linarith
from i_lt_k_pred have i_minus_k_pred_leq_Minus_One: "i - real (k - 1) ≤ -1"
by simp
have "x - xs N!k = x - (a + (real k - 1) * h)"
proof-
have k_def2: "k ∈ {1..N+1}"
using i_def k_def less_diff_conv2 by auto
then have "x - xs N ! k = x - (a + (real k - 1) * h)"
using xs_els by force
then show ?thesis
using i_lt_k_pred by force
qed
also have "... ≤ -h"
proof -
have x_upper_limit: "(xs N!(i+1)) = (a+(real i)*h)"
using i_def xs_els by fastforce
then have difference_of_terms: "(xs N!(i+1)) - (a+(real k - 1)*h) = ((real i) - (real k-1))*h"
by (smt (verit, ccfv_threshold) diff_is_0_eq i_lt_k_pred left_diff_distrib' nat_less_real_le nle_le of_nat_1 of_nat_diff of_nat_le_0_iff)
then have first_inequality: "x - (a + (real k - 1) * h) ≤ (xs N!(i+1)) - (a+(real k - 1)*h)"
using i_def by fastforce
have second_inequality: "(xs N!(i+1)) - (a+(real k - 1)*h) ≤ -h"
by (metis diff_is_0_eq' difference_of_terms h_pos i_lt_k_pred i_minus_k_pred_leq_Minus_One linorder_not_le mult.left_commute mult.right_neutral mult_minus1_right nle_le not_less_zero of_nat_1 of_nat_diff ordered_comm_semiring_class.comm_mult_left_mono)
then show ?thesis
by (smt (z3) combine_common_factor difference_of_terms first_inequality x_upper_limit)
qed
finally show "x - xs N ! k ≤ -h".
qed
have I1_final_bound: "I_1 i x < (1+ (Sup ((λx. ¦f x¦) ` {a..b}))) * η"
proof -
have I1_decomp:
"I_1 i x ≤ (∑k∈{2..i-1}. ¦f (xs N ! k) - f (xs N ! (k - 1))¦ * ¦σ (w * (x - xs N ! k)) - 1¦)
+ ¦f (a)¦ * ¦σ (w * (x - xs N ! 0)) - 1¦
+ (∑k∈{i+2..N+1}. ¦f (xs N ! k) - f (xs N ! (k - 1))¦ * ¦σ (w * (x - xs N ! k))¦)"
proof (cases "i < 3")
assume i_lt_3: "i < 3"
then have i_is_1_or_2: "i = 1 ∨ i = 2"
using i_ge_1 by linarith
then have empty_summation:
"(∑k = 2..i - 1. ¦f (xs N ! k) - f (xs N ! (k - 1))¦ * ¦σ (w * (x - xs N ! k)) - 1¦) = 0"
by fastforce
have Lix: "L i x = f(a) + (f (xs N ! 3) - f (xs N ! 2)) * σ (w * (x - xs N ! 3)) + (f (xs N ! 2) - f (xs N ! 1)) * σ (w * (x - xs N ! 2))"
using L_def i_is_1_or_2 by presburger
have "I_1 i x = ¦G_Nf x - L i x¦"
by (meson I_1_def i_ge_1 i_leq_N)
also have "... = ¦(∑k∈{2..N+1}. (f (xs N ! k) - f (xs N ! (k - 1))) * σ (w * (x - xs N ! k)))
+ f (xs N ! 1) * σ (w * (x - xs N ! 0))
- f(a)
- (f (xs N ! 3) - f (xs N ! 2)) * σ (w * (x - xs N ! 3))
- (f (xs N ! 2) - f (xs N ! 1)) * σ (w * (x - xs N ! 2))¦"
by (simp add: G_Nf_def Lix)
also have " ... = ¦(∑k∈{3..N+1}. (f (xs N ! k) - f (xs N ! (k - 1))) * σ (w * (x - xs N ! k)))
+ f (xs N ! 1) * σ (w * (x - xs N ! 0))
- f(a)
- (f (xs N ! 3) - f (xs N ! 2)) * σ (w * (x - xs N ! 3))¦"
proof -
from N_pos have "(∑k∈{2..N+1}. (f (xs N ! k) - f (xs N ! (k - 1))) * σ (w * (x - xs N ! k))) =
(f (xs N ! 2) - f (xs N ! 1)) * σ (w * (x - xs N ! 2)) +
(∑k∈{3..N+1}. (f (xs N ! k) - f (xs N ! (k - 1))) * σ (w * (x - xs N ! k)))"
by(subst sum.atLeast_Suc_atMost, auto)
then show ?thesis
by linarith
qed
also have "... = ¦(∑k∈{4..N+1}. (f (xs N ! k) - f (xs N ! (k - 1))) * σ (w * (x - xs N ! k)))
+ f (xs N ! 1) * σ (w * (x - xs N ! 0))
- f(a)¦"
proof -
from N_gt_3 have "(∑k∈{3..N+1}. (f (xs N ! k) - f (xs N ! (k - 1))) * σ (w * (x - xs N ! k))) =
(f (xs N ! 3) - f (xs N ! 2)) * σ (w * (x - xs N ! 3)) +
(∑k∈{4..N+1}. (f (xs N ! k) - f (xs N ! (k - 1))) * σ (w * (x - xs N ! k)))"
by(subst sum.atLeast_Suc_atMost, simp_all)
then show ?thesis
by linarith
qed
also have "... = ¦(∑k∈{4..N+1}. (f (xs N ! k) - f (xs N ! (k - 1))) * σ (w * (x - xs N ! k)))
+ f (a) * (σ (w * (x - xs N ! 0)) - 1)¦"
proof -
have "∀real1 real2 real3. (real1::real) + real2 * real3 - real2 = real1 + real2 * (real3 - 1)"
by (simp add: right_diff_distrib')
then show ?thesis
using first_element by presburger
qed
also have "... ≤ ¦(∑k∈{4..N+1}. (f (xs N ! k) - f (xs N ! (k - 1))) * σ (w * (x - xs N ! k)))¦
+ ¦f (a) * (σ (w * (x - xs N ! 0)) - 1)¦"
by linarith
also have "... ≤ (∑k∈{4..N+1}. ¦(f (xs N ! k) - f (xs N ! (k - 1))) * σ (w * (x - xs N ! k))¦)
+ ¦f (a) * (σ (w * (x - xs N ! 0)) - 1)¦"
using add_mono by blast
also have "... = (∑k∈{4..N+1}. ¦(f (xs N ! k) - f (xs N ! (k - 1)))¦ * ¦σ (w * (x - xs N ! k))¦)
+ ¦f (a)¦ * ¦(σ (w * (x - xs N ! 0)) - 1)¦"
by (simp add: abs_mult)
also have "... ≤ (∑k∈{i+2..N+1}. ¦(f (xs N ! k) - f (xs N ! (k - 1)))¦ * ¦σ (w * (x - xs N ! k))¦)
+ ¦f (a)¦ * ¦(σ (w * (x - xs N ! 0)) - 1)¦"
proof(cases "i=1")
assume i_is_1: "i = 1"
have union: "{i+2} ∪ {4..N+1} = {i+2..N+1}"
proof(safe)
show "⋀n. i + 2 ∈ {i+2..N + 1}"
using N_gt_3 i_is_1 by presburger
show "⋀n. n ∈ {4..N + 1} ⟹ n ∈ {i+2..N + 1}"
using i_is_1 by auto
show "⋀n. n ∈ {i+2..N + 1} ⟹ n ∉ {4..N + 1} ⟹ n ∉ {} ⟹ n = i + 2"
using i_is_1 by presburger
qed
have "(∑k∈{4..N+1}. ¦(f (xs N ! k) - f (xs N ! (k - 1)))¦ * ¦σ (w * (x - xs N ! k))¦)
+ ¦f (a)¦ * ¦(σ (w * (x - xs N ! 0)) - 1)¦ ≤
(∑k∈{i+2}. ¦(f (xs N ! k) - f (xs N ! (k - 1)))¦ * ¦σ (w * (x - xs N ! k))¦)
+
(∑k∈{4..N+1}. ¦(f (xs N ! k) - f (xs N ! (k - 1)))¦ * ¦σ (w * (x - xs N ! k))¦)
+ ¦f (a)¦ * ¦(σ (w * (x - xs N ! 0)) - 1)¦"
by auto
also have "... = (∑k∈{i+2..N+1}. ¦(f (xs N ! k) - f (xs N ! (k - 1)))¦ * ¦σ (w * (x - xs N ! k))¦)
+ ¦f (a)¦ * ¦(σ (w * (x - xs N ! 0)) - 1)¦"
proof -
have "(∑k∈{i+2}. ¦(f (xs N ! k) - f (xs N ! (k - 1)))¦ * ¦σ (w * (x - xs N ! k))¦) +
(∑k∈{4..N+1}. ¦(f (xs N ! k) - f (xs N ! (k - 1)))¦ * ¦σ (w * (x - xs N ! k))¦) =
(∑k∈({i+2} ∪ {4..N+1}). ¦(f (xs N ! k) - f (xs N ! (k - 1)))¦ * ¦σ (w * (x - xs N ! k))¦)"
by (subst sum.union_disjoint, simp_all, simp add: i_is_1)
then show ?thesis
using union by presburger
qed
finally show ?thesis.
next
show "i ≠ 1 ⟹
(∑k = 4..N + 1. ¦f (xs N ! k) - f (xs N ! (k - 1))¦ * ¦σ (w * (x - xs N ! k))¦) + ¦f a¦ * ¦σ (w * (x - xs N ! 0)) - 1¦
≤ (∑k = i + 2..N + 1. ¦f (xs N ! k) - f (xs N ! (k - 1))¦ * ¦σ (w * (x - xs N ! k))¦) + ¦f a¦ * ¦σ (w * (x - xs N ! 0)) - 1¦"
using i_is_1_or_2 by auto
qed
finally show ?thesis
using empty_summation by linarith
next
assume main_case: "¬ i < 3"
then have three_leq_i: "i ≥ 3"
by simp
have disjoint: "{2..i-1} ∩ {i..N+1} = {}"
by auto
have union: "{2..i-1} ∪ {i..N+1} = {2..N+1}"
proof(safe)
show "⋀n. n ∈ {2..i - 1} ⟹ n ∈ {2..N+1}"
using i_leq_N by force
show "⋀n. n∈ {i..N + 1} ⟹ n ∈ {2..N + 1}"
using three_leq_i by force
show "⋀n. n ∈ {2..N + 1} ⟹ n ∉ {i..N + 1} ⟹ n ∈ {2..i - 1}"
by (metis Nat.le_diff_conv2 Suc_eq_plus1 atLeastAtMost_iff i_ge_1 not_less_eq_eq)
qed
have sum_of_terms: "(∑k∈{2..i-1}. (f (xs N ! k) - f (xs N ! (k - 1))) * σ (w * (x - xs N ! k))) +
(∑k∈{i..N+1}. (f (xs N ! k) - f (xs N ! (k - 1))) * σ (w * (x - xs N ! k))) =
(∑k∈{2..N+1}. (f (xs N ! k) - f (xs N ! (k - 1))) * σ (w * (x - xs N ! k)))"
using sum.union_disjoint by (smt (verit, ccfv_threshold) disjoint union finite_atLeastAtMost)
have "I_1 i x = ¦G_Nf x - L i x¦"
using I_1_def i_ge_1 i_leq_N by presburger
also have "... = ¦G_Nf x - ((∑k∈{2..i-1}. (f (xs N ! k) - f (xs N ! (k - 1)))) + f(a) +
(f (xs N ! i) - f (xs N ! (i-1))) * σ (w * (x - xs N ! i)) +
(f (xs N ! (i+1)) - f (xs N ! i)) * σ (w * (x - xs N ! (i+1))))¦"
by (smt (verit, ccfv_SIG) main_case L_def less_add_one nat_1_add_1 numeral_Bit1 numeral_le_iff numerals(1) semiring_norm(70) three_leq_i)
also have "... = ¦(∑k∈{2..i-1}. (f (xs N ! k) - f (xs N ! (k - 1))) * σ (w * (x - xs N ! k))) +
(∑k∈{i..N+1}. (f (xs N ! k) - f (xs N ! (k - 1))) * σ (w * (x - xs N ! k))) + f (xs N ! 1) * σ (w * (x - xs N ! 0)) -
(∑k∈{2..i-1}. (f (xs N ! k) - f (xs N ! (k - 1))) ) - f(a) - (f (xs N ! i) - f (xs N ! (i - 1)))* σ (w * (x - xs N ! i)) -
(f (xs N ! (i+1)) - f (xs N ! i))* σ (w * (x - xs N ! (i+1)))¦"
by (smt (verit, ccfv_SIG) G_Nf_def sum_mono sum_of_terms)
also have "... = ¦((∑k∈{2..i-1}. (f (xs N ! k) - f (xs N ! (k - 1))) * σ (w * (x - xs N ! k)))
-(∑k∈{2..i-1}. (f (xs N ! k) - f (xs N ! (k - 1))) ))+
(∑k∈{i..N+1}. (f (xs N ! k) - f (xs N ! (k - 1))) * σ (w * (x - xs N ! k))) + f (xs N ! 1) * σ (w * (x - xs N ! 0))
- f(a) - (f (xs N ! i) - f (xs N ! (i - 1)))* σ (w * (x - xs N ! i)) -
(f (xs N ! (i+1)) - f (xs N ! i))* σ (w * (x - xs N ! (i+1)))¦"
by linarith
also have "... = ¦(∑k∈{2..i-1}. (f (xs N ! k) - f (xs N ! (k - 1))) * σ (w * (x - xs N ! k))
-(f (xs N ! k) - f (xs N ! (k - 1))) )+
(∑k∈{i..N+1}. (f (xs N ! k) - f (xs N ! (k - 1))) * σ (w * (x - xs N ! k))) + f (xs N ! 1) * σ (w * (x - xs N ! 0))
- f(a) - (f (xs N ! (i)) - f (xs N ! (i - 1)))* σ (w * (x - xs N ! (i))) -
(f (xs N ! (i+1)) - f (xs N ! (i)))* σ (w * (x - xs N ! (i+1)))¦"
by (simp add: sum_subtractf)
also have "... = ¦(∑k∈{2..i-1}. (f (xs N ! k) - f (xs N ! (k - 1))) * (σ (w * (x - xs N ! k)) - 1)) +
(∑k∈{i..N+1}. (f (xs N ! k) - f (xs N ! (k - 1))) * σ (w * (x - xs N ! k))) +
f (xs N ! 1) * σ (w * (x - xs N ! 0)) -
f(a) -
(f (xs N ! (i)) - f (xs N ! (i - 1))) * σ (w * (x - xs N ! (i))) -
(f (xs N ! (i+1)) - f (xs N ! (i))) * σ (w * (x - xs N ! (i+1)))¦"
by (simp add: right_diff_distrib')
also have "... = ¦(∑k∈{2..i-1}. (f (xs N ! k) - f (xs N ! (k - 1))) * (σ (w * (x - xs N ! k)) - 1)) +
(∑k∈{i..N+1}. (f (xs N ! k) - f (xs N ! (k - 1))) * σ (w * (x - xs N ! k))) +
f (a) * σ (w * (x - xs N ! 0)) -
f(a) -
(f (xs N ! (i)) - f (xs N ! (i - 1))) * σ (w * (x - xs N ! (i))) -
(f (xs N ! (i+1)) - f (xs N ! (i))) * σ (w * (x - xs N ! (i+1)))¦"
using first_element by fastforce
also have "... = ¦(∑k∈{2..i-1}. (f (xs N ! k) - f (xs N ! (k - 1))) * (σ (w * (x - xs N ! k)) - 1)) +
(∑k∈{i..N+1}. (f (xs N ! k) - f (xs N ! (k - 1))) * σ (w * (x - xs N ! k))) +
f (a) * (σ (w * (x - xs N ! 0)) -1)
-(f (xs N ! (i)) - f (xs N ! (i - 1))) * σ (w * (x - xs N ! (i)))
-(f (xs N ! (i+1)) - f (xs N ! (i))) * σ (w * (x - xs N ! (i+1)))¦"
by (simp add: add_diff_eq right_diff_distrib')
also have "...= ¦(∑k∈{2..i-1}. (f (xs N ! k) - f (xs N ! (k - 1))) * (σ (w * (x - xs N ! k)) - 1)) +
f (a) * (σ (w * (x - xs N ! 0)) - 1) +
(∑k∈{i+1..N+1}. (f (xs N ! k) - f (xs N ! (k - 1))) * σ (w * (x - xs N ! k)))
- (f (xs N ! (i+1)) - f (xs N ! (i ))) * σ (w * (x - xs N ! (i+1)))¦"
proof -
from i_leq_N have "(∑k∈{i..N+1}. (f (xs N ! k) - f (xs N ! (k - 1))) * σ (w * (x - xs N ! k))) =
(f (xs N ! (i)) - f (xs N ! (i - 1))) * σ (w * (x - xs N ! (i))) +
(∑k∈{i+1..N+1}. (f (xs N ! k) - f (xs N ! (k - 1))) * σ (w * (x - xs N ! k)))"
by(subst sum.atLeast_Suc_atMost, linarith, auto)
then show ?thesis
by linarith
qed
also have "...= ¦(∑k∈{2..i-1}. (f (xs N ! k) - f (xs N ! (k - 1))) * (σ (w * (x - xs N ! k)) - 1)) +
f (a) * (σ (w * (x - xs N ! 0)) - 1) +
(∑k∈{i+2..N+1}. (f (xs N ! k) - f (xs N ! (k - 1))) * σ (w * (x - xs N ! k)))¦"
proof -
from i_leq_N have "(∑k∈{i+1..N+1}. (f (xs N ! k) - f (xs N ! (k - 1))) * σ (w * (x - xs N ! k))) =
(f (xs N ! (i+1)) - f (xs N ! (i))) * σ (w * (x - xs N ! (i+1))) +
(∑k∈{i+2..N+1}. (f (xs N ! k) - f (xs N ! (k - 1))) * σ (w * (x - xs N ! k)))"
by(subst sum.atLeast_Suc_atMost, linarith, auto)
then show ?thesis
by linarith
qed
show ?thesis
proof -
have inequality_pair: "¦∑n = 2..i - 1. (f (xs N ! n) - f (xs N ! (n - 1))) * (σ (w * (x - xs N ! n)) - 1)¦ ≤
(∑n = 2..i - 1. ¦(f (xs N ! n) - f (xs N ! (n - 1))) * (σ (w * (x - xs N ! n)) - 1)¦) ∧
¦f a * (σ (w * (x - xs N ! 0)) - 1)¦ + ¦∑n = i + 2..N + 1. (f (xs N ! n) - f (xs N ! (n - 1))) * σ (w * (x - xs N ! n))¦
≤ ¦f a * (σ (w * (x - xs N ! 0)) - 1)¦ + (∑n = i + 2..N + 1. ¦(f (xs N ! n) - f (xs N ! (n - 1))) * σ (w * (x - xs N ! n))¦)"
using add_le_cancel_left by blast
have "I_1 i x = ¦(∑k∈{2..i-1}. (f (xs N ! k) - f (xs N ! (k - 1))) * (σ (w * (x - xs N ! k)) - 1)) +
f (a) * (σ (w * (x - xs N ! 0)) - 1) +
(∑k = i + 2..N+1. (f (xs N ! k) - f (xs N ! (k - 1))) * σ (w * (x - xs N ! k)))¦"
using ‹¦(∑k = 2..i - 1. (f (xs N ! k) - f (xs N ! (k - 1))) * (σ (w * (x - xs N ! k)) - 1)) + f a * (σ (w * (x - xs N ! 0)) - 1) + (∑k = i + 1..N + 1. (f (xs N ! k) - f (xs N ! (k - 1))) * σ (w * (x - xs N ! k))) - (f (xs N ! (i + 1)) - f (xs N ! i)) * σ (w * (x - xs N ! (i + 1)))¦ = ¦(∑k = 2..i - 1. (f (xs N ! k) - f (xs N ! (k - 1))) * (σ (w * (x - xs N ! k)) - 1)) + f a * (σ (w * (x - xs N ! 0)) - 1) + (∑k = i + 2..N + 1. (f (xs N ! k) - f (xs N ! (k - 1))) * σ (w * (x - xs N ! k)))¦›
calculation by presburger
also have "... ≤¦(∑k∈{2..i-1}. (f (xs N ! k) - f (xs N ! (k - 1))) * (σ (w * (x - xs N ! k)) - 1))¦
+ ¦f (a) * (σ (w * (x - xs N ! 0)) - 1)¦
+¦(∑k∈{i+2..N+1}. (f (xs N ! k) - f (xs N ! (k - 1))) * σ (w * (x - xs N ! k)))¦"
by linarith
also have "...≤ (∑k∈{2..i-1}. ¦(f (xs N ! k) - f (xs N ! (k - 1))) * (σ (w * (x - xs N ! k)) - 1)¦)
+ ¦f (a) * (σ (w * (x - xs N ! 0)) - 1)¦
+ (∑k∈{i+2..N+1}. ¦(f (xs N ! k) - f (xs N ! (k - 1))) * σ (w * (x - xs N ! k))¦)"
using inequality_pair by linarith
also have "...≤ (∑k∈{2..i-1}. ¦(f (xs N ! k) - f (xs N ! (k - 1)))¦ * ¦(σ (w * (x - xs N ! k)) - 1)¦)
+ ¦f (a)¦ * ¦σ (w * (x - xs N ! 0)) - 1¦
+ (∑k∈{i+2..N+1}. ¦(f (xs N ! k) - f (xs N ! (k - 1)))¦ * ¦σ (w * (x - xs N ! k))¦)"
proof -
have f1: "⋀k. k ∈ {2..i-1} ⟶ ¦(f (xs N ! k) - f (xs N ! (k - 1))) * (σ (w * (x - xs N ! k)) - 1)¦ ≤ ¦f (xs N ! k) - f (xs N ! (k - 1))¦ * ¦σ (w * (x - xs N ! k)) - 1¦"
by (simp add: abs_mult)
have f2: "⋀k. k ∈ {i+2..N+1} ⟶ ¦(f (xs N ! k) - f (xs N ! (k - 1))) * σ (w * (x - xs N ! k))¦ ≤ ¦f (xs N ! k) - f (xs N ! (k - 1))¦ * ¦σ (w * (x - xs N ! k))¦"
by (simp add: abs_mult)
have f3: "¦f (a) * (σ (w * (x - xs N ! 0)) - 1)¦ = ¦f (a)¦ * ¦σ (w * (x - xs N ! 0)) - 1¦"
using abs_mult by blast
then show ?thesis
by (smt (verit, best) f1 f2 sum_mono)
qed
finally show ?thesis.
qed
qed
also have "... < (∑k∈{2..i-1}. η * (1/N)) +
¦f (a)¦ * ¦σ (w * (x - xs N ! 0)) - 1¦ +
(∑k∈{i+2..N+1}. η * (1/N))"
proof(cases "i ≥ 3")
assume i_geq_3: "3 ≤ i"
show "(∑k = 2..i - 1. ¦f (xs N ! k) - f (xs N ! (k - 1))¦ * ¦σ (w * (x - xs N ! k)) - 1¦) + ¦f a¦ * ¦σ (w * (x - xs N ! 0)) - 1¦ +
(∑k = i + 2..N + 1. ¦f (xs N ! k) - f (xs N ! (k - 1))¦ * ¦σ (w * (x - xs N ! k))¦)
< (∑k = 2..i - 1. η * (1 / N)) + ¦f a¦ * ¦σ (w * (x - xs N ! 0)) - 1¦ +
(∑k = i + 2..N + 1. η * (1 / N))"
proof(cases "∀k. k ∈ {2..i-1} ⟶ ¦σ (w * (x - xs N ! k)) - 1¦ = 0")
assume all_terms_zero: "∀k. k ∈ {2..i - 1} ⟶ ¦σ (w * (x - xs N ! k)) - 1¦ = 0"
from i_geq_3 have "(∑k∈{2..i-1}. ¦f (xs N ! k) - f (xs N ! (k - 1))¦ * ¦σ (w * (x - xs N ! k)) - 1¦) < (∑k∈{2..i-1}. η * (1/N))"
by (subst sum_strict_mono, force+, (simp add: N_pos η_pos all_terms_zero)+)
show ?thesis
proof(cases "i = N")
assume "i = N"
then show ?thesis
using ‹(∑k = 2..i - 1. ¦f (xs N ! k) - f (xs N ! (k - 1))¦ * ¦σ (w * (x - xs N ! k)) - 1¦) < (∑k = 2..i - 1. η * (1 / N))› by auto
next
assume "i ≠ N"
then have i_lt_N: "i < N"
using i_leq_N le_neq_implies_less by blast
show ?thesis
proof(cases "∀k. k ∈ {i+2..N+1} ⟶ ¦σ (w * (x - xs N ! k))¦ = 0")
assume all_second_terms_zero: "∀k. k ∈ {i + 2..N + 1} ⟶ ¦σ (w * (x - xs N ! k))¦ = (0::real)"
from i_lt_N have "(∑k∈{i+2..N+1}. ¦f (xs N ! k) - f (xs N ! (k - 1))¦ * ¦σ (w * (x - xs N ! k))¦) < (∑k∈{i+2..N+1}. η * (1/N))"
by(subst sum_strict_mono, force+, (simp add: η_pos all_second_terms_zero)+)
then show ?thesis
proof -
show ?thesis
using ‹(∑k = 2..i - 1. ¦f (xs N ! k) - f (xs N ! (k - 1))¦ * ¦σ (w * (x - xs N ! k)) - 1¦) < (∑k = 2..i - 1. η * (1 / N))›
‹(∑k = i + 2..N + 1. ¦f (xs N ! k) - f (xs N ! (k - 1))¦ * ¦σ (w * (x - xs N ! k))¦) < (∑k = i + 2..N + 1. η * (1 / N))› by linarith
qed
next
assume second_terms_not_all_zero: "¬ (∀k. k ∈ {i + 2..N + 1} ⟶ ¦σ (w * (x - xs N ! k))¦ = 0)"
obtain NonZeroTerms where NonZeroTerms_def: "NonZeroTerms = {k ∈ {i + 2..N + 1}. ¦σ (w * (x - xs N ! k))¦ ≠ 0}"
by blast
obtain ZeroTerms where ZeroTerms_def: "ZeroTerms = {k ∈ {i + 2..N + 1}. ¦σ (w * (x - xs N ! k))¦ = 0}"
by blast
have zero_terms_eq_zero: "(∑k ∈ ZeroTerms. ¦f (xs N ! k) - f (xs N ! (k - 1))¦ * ¦σ (w * (x - xs N ! k))¦) = 0"
by (simp add: ZeroTerms_def)
have disjoint: "ZeroTerms ∩ NonZeroTerms = {}"
using NonZeroTerms_def ZeroTerms_def by blast
have union: "ZeroTerms ∪ NonZeroTerms = {i+2..N+1}"
proof(safe)
show "⋀n. n ∈ ZeroTerms ⟹ n ∈ {i + 2..N + 1}"
using ZeroTerms_def by force
show "⋀n. n ∈ NonZeroTerms ⟹ n ∈ {i + 2..N + 1}"
using NonZeroTerms_def by blast
show "⋀n. n ∈ {i + 2..N + 1} ⟹ n ∉ NonZeroTerms ⟹ n ∈ ZeroTerms"
using NonZeroTerms_def ZeroTerms_def by blast
qed
have "(∑k∈{i+2..N+1}. ¦f (xs N ! k) - f (xs N ! (k - 1))¦ * ¦σ (w * (x - xs N ! k))¦) <
(∑k∈{i+2..N+1}. η * ((1::real) / real N))"
proof -
have "(∑k∈{i+2..N+1}. ¦f (xs N ! k) - f (xs N ! (k - 1))¦ * ¦σ (w * (x - xs N ! k))¦) =
(∑k∈NonZeroTerms. ¦f (xs N ! k) - f (xs N ! (k - 1))¦ * ¦σ (w * (x - xs N ! k))¦)"
proof -
have "(∑k∈{i+2..N+1}. ¦f (xs N ! k) - f (xs N ! (k - 1))¦ * ¦σ (w * (x - xs N ! k))¦) =
(∑k∈ZeroTerms. ¦f (xs N ! k) - f (xs N ! (k - 1))¦ * ¦σ (w * (x - xs N ! k))¦)
+ (∑k∈NonZeroTerms. ¦f (xs N ! k) - f (xs N ! (k - 1))¦ * ¦σ (w * (x - xs N ! k))¦)"
by (smt disjoint finite_Un finite_atLeastAtMost union sum.union_disjoint)
then show ?thesis
using zero_terms_eq_zero by linarith
qed
also have "... < (∑k∈NonZeroTerms. η * (1 / N))"
proof(rule sum_strict_mono)
show "finite NonZeroTerms"
by (metis finite_Un finite_atLeastAtMost union)
show "NonZeroTerms ≠ {}"
using NonZeroTerms_def second_terms_not_all_zero by blast
fix y
assume y_subtype: "y ∈ NonZeroTerms"
then have y_type: "y ∈ {i+2..N+1}"
by (metis Un_iff union)
then have y_suptype: "y ∈ {1..N + 1}"
by simp
have parts_lt_eta: "⋀k. k∈{i+2..N+1} ⟶ ¦(f (xs N ! k) - f (xs N ! (k - 1)))¦ < η"
proof(clarify)
fix k
assume k_type: "k ∈ {i + 2..N + 1}"
then have "k - 1 ∈ {i+1..N}"
by force
then have "¦(xs N ! k) - (xs N ! (k - 1))¦ < δ ⟶ ¦f (xs N ! k) - f (xs N ! (k - 1))¦ < η"
using δ_prop atLeastAtMost_iff els_in_ab le_diff_conv by auto
then show "¦f (xs N ! k) - f (xs N ! (k - 1))¦ < η"
using adj_terms_lt i_leq_N k_type by fastforce
qed
then have f_diff_lt_eta: "¦f (xs N ! y) - f (xs N ! (y - 1))¦ < η"
using y_type by blast
have lt_minus_h: "x - xs N!y ≤ -h"
using x_minus_xk_le_neg_h_on_Right_Half y_type by blast
then have sigma_lt_inverseN: "¦σ (w * (x - xs N ! y))¦ < 1 / N"
proof -
have "¬ Suc N < y"
using y_suptype by force
then show ?thesis
by (smt (z3) Suc_1 Suc_eq_plus1 lt_minus_h add.commute add.left_commute diff_zero length_map length_upt not_less_eq w_prop xs_eqs)
qed
show "¦f (xs N ! y) - f (xs N ! (y - 1))¦ * ¦σ (w * (x - xs N ! y))¦ < η * (1 / N)"
using f_diff_lt_eta mult_strict_mono sigma_lt_inverseN by fastforce
qed
also have "... ≤ (∑k∈NonZeroTerms. η * (1 / N)) + (∑k∈ZeroTerms. η * (1 / N))"
using η_pos by force
also have "... = (∑k∈{i+2..N+1}. η * (1 / N))"
by (smt disjoint finite_Un finite_atLeastAtMost union sum.union_disjoint)
finally show ?thesis.
qed
then show ?thesis
using ‹(∑k = 2..i - 1. ¦f (xs N ! k) - f (xs N ! (k - 1))¦ * ¦σ (w * (x - xs N ! k)) - 1¦) < (∑k = 2..i - 1. η * (1 / N))› by linarith
qed
qed
next
assume first_terms_not_all_zero: "¬ (∀k. k ∈ {2..i - 1} ⟶ ¦σ (w * (x - xs N ! k)) - 1¦ = 0)"
obtain BotNonZeroTerms where BotNonZeroTerms_def: "BotNonZeroTerms = {k ∈ {2..i - 1}. ¦σ (w * (x - xs N ! k)) - 1¦ ≠ 0}"
by blast
obtain BotZeroTerms where BotZeroTerms_def: "BotZeroTerms = {k ∈ {2..i - 1}. ¦σ (w * (x - xs N ! k)) - 1¦ = 0}"
by blast
have bot_zero_terms_eq_zero: "(∑k ∈ BotZeroTerms. ¦f (xs N ! k) - f (xs N ! (k - 1))¦ * ¦σ (w * (x - xs N ! k)) -1¦) = 0"
by (simp add: BotZeroTerms_def)
have bot_disjoint: "BotZeroTerms ∩ BotNonZeroTerms = {}"
using BotNonZeroTerms_def BotZeroTerms_def by blast
have bot_union: "BotZeroTerms ∪ BotNonZeroTerms = {2..i - 1}"
proof(safe)
show "⋀n. n ∈ BotZeroTerms ⟹ n ∈ {2..i - 1}"
using BotZeroTerms_def by force
show "⋀n. n ∈ BotNonZeroTerms ⟹ n ∈ {2..i - 1}"
using BotNonZeroTerms_def by blast
show "⋀n. n ∈ {2..i - 1} ⟹ n ∉ BotNonZeroTerms ⟹ n ∈ BotZeroTerms"
using BotNonZeroTerms_def BotZeroTerms_def by blast
qed
have "(∑k∈{2..i - 1}. ¦f (xs N ! k) - f (xs N ! (k - 1))¦ * ¦σ (w * (x - xs N ! k)) -1¦) <
(∑k∈{2..i - 1}. η * (1 / N))"
proof -
have disjoint_sum: "sum (λk. η * (1 / N)) BotNonZeroTerms + sum (λk. η * (1 / N)) BotZeroTerms = sum (λk. η * (1 / N)) {2..i - 1}"
proof -
from bot_disjoint have "sum (λk. η * (1 / real N)) BotNonZeroTerms + sum (λk. η * (1 / N)) BotZeroTerms =
sum (λk. η * (1 / real N)) (BotNonZeroTerms ∪ BotZeroTerms)"
by(subst sum.union_disjoint, (metis(mono_tags) bot_union finite_Un finite_atLeastAtMost)+, auto)
then show ?thesis
by (metis add.commute bot_disjoint bot_union finite_Un finite_atLeastAtMost sum.union_disjoint)
qed
have "(∑k∈{2..i - 1}. ¦f (xs N ! k) - f (xs N ! (k - 1))¦ * ¦σ (w * (x - xs N ! k)) - 1¦) =
(∑k∈BotNonZeroTerms. ¦f (xs N ! k) - f (xs N ! (k - 1))¦ * ¦σ (w * (x - xs N ! k)) - 1¦)"
proof -
have "(∑k∈{2..i - 1}. ¦f (xs N ! k) - f (xs N ! (k - 1))¦ * ¦σ (w * (x - xs N ! k)) -1¦) =
(∑k∈BotZeroTerms. ¦f (xs N ! k) - f (xs N ! (k - 1))¦ * ¦σ (w * (x - xs N ! k)) -1¦)
+ (∑k∈BotNonZeroTerms. ¦f (xs N ! k) - f (xs N ! (k - 1))¦ * ¦σ (w * (x - xs N ! k)) -1¦)"
by (smt bot_disjoint finite_Un finite_atLeastAtMost bot_union sum.union_disjoint)
then show ?thesis
using bot_zero_terms_eq_zero by linarith
qed
also have "... < (∑k∈BotNonZeroTerms. η * (1 / N))"
proof(rule sum_strict_mono)
show "finite BotNonZeroTerms"
by (metis finite_Un finite_atLeastAtMost bot_union)
show "BotNonZeroTerms ≠ {}"
using BotNonZeroTerms_def first_terms_not_all_zero by blast
fix y
assume y_subtype: "y ∈ BotNonZeroTerms"
then have y_type: "y ∈ {2..i - 1}"
by (metis Un_iff bot_union)
then have y_suptype: "y ∈ {1..N + 1}"
using i_leq_N by force
have parts_lt_eta: "⋀k. k∈{2..i - 1} ⟶ ¦(f (xs N ! k) - f (xs N ! (k - 1)))¦ < η"
proof(clarify)
fix k
assume k_type: "k ∈ {2..i - 1}"
then have "¦(xs N ! k) - (xs N ! (k - 1))¦ < δ ⟶ ¦f (xs N ! k) - f (xs N ! (k - 1))¦ < η"
by (metis δ_prop add.commute add_le_imp_le_diff atLeastAtMost_iff diff_le_self dual_order.trans els_in_ab i_leq_N nat_1_add_1 trans_le_add2)
then show "¦f (xs N ! k) - f (xs N ! (k - 1))¦ < η"
using adj_terms_lt i_leq_N k_type by fastforce
qed
then have f_diff_lt_eta: "¦f (xs N ! y) - f (xs N ! (y - 1))¦ < η"
using y_type by blast
have lt_minus_h: "x - xs N!y ≥ h"
using x_minus_xk_ge_h_on_Left_Half y_type by force
then have bot_sigma_lt_inverseN: "¦σ (w * (x - xs N ! y)) -1 ¦ < (1 / N)"
by (smt (z3) Suc_eq_plus1 add_2_eq_Suc' atLeastAtMost_iff diff_zero length_map length_upt less_Suc_eq_le w_prop xs_eqs y_suptype)
then show "¦f (xs N ! y) - f (xs N ! (y - 1))¦ * ¦σ (w * (x - xs N ! y)) - 1¦ < η * (1 / N)"
by (smt (verit, del_insts) f_diff_lt_eta mult_strict_mono)
qed
also have "... ≤ (∑k∈BotNonZeroTerms. η * (1 / N)) + (∑k∈BotZeroTerms. η * (1 / N))"
using η_pos by force
also have "... = (∑k∈{2..i - 1}. η * (1 / N))"
using sum.union_disjoint disjoint_sum by force
finally show ?thesis.
qed
show ?thesis
proof(cases "i = N")
assume "i = N"
then show ?thesis
using ‹(∑k = 2..i - 1. ¦f (xs N ! k) - f (xs N ! (k - 1))¦ * ¦σ (w * (x - xs N ! k)) - 1¦) < (∑k = 2..i - 1. η * (1 / N))› by auto
next
assume "i ≠ N"
then have i_lt_N: "i < N"
using i_leq_N le_neq_implies_less by blast
show ?thesis
proof(cases "∀k. k ∈ {i+2..N+1} ⟶ ¦σ (w * (x - xs N ! k))¦ = 0")
assume all_second_terms_zero: "∀k. k ∈ {i + 2..N + 1} ⟶ ¦σ (w * (x - xs N ! k))¦ = 0"
from i_lt_N have "(∑k∈{i+2..N+1}. ¦f (xs N ! k) - f (xs N ! (k - 1))¦ * ¦σ (w * (x - xs N ! k))¦) < (∑k∈{i+2..N+1}. η * (1/N))"
by (subst sum_strict_mono, fastforce+, (simp add: η_pos all_second_terms_zero)+)
then show ?thesis
using ‹(∑k = 2..i - 1. ¦f (xs N ! k) - f (xs N ! (k - 1))¦ * ¦σ (w * (x - xs N ! k)) - 1¦) < (∑k = 2..i - 1. η * (1 / N))› by linarith
next
assume second_terms_not_all_zero: "¬ (∀k. k ∈ {i + 2..N + 1} ⟶ ¦σ (w * (x - xs N ! k))¦ = 0)"
obtain TopNonZeroTerms where TopNonZeroTerms_def: "TopNonZeroTerms = {k ∈ {i + 2..N + 1}. ¦σ (w * (x - xs N ! k))¦ ≠ 0}"
by blast
obtain TopZeroTerms where TopZeroTerms_def: "TopZeroTerms = {k ∈ {i + 2..N + 1}. ¦σ (w * (x - xs N ! k))¦ = 0}"
by blast
have zero_terms_eq_zero: "(∑k∈TopZeroTerms. ¦f (xs N ! k) - f (xs N ! (k - 1))¦ * ¦σ (w * (x - xs N ! k))¦) = 0"
by (simp add: TopZeroTerms_def)
have disjoint: "TopZeroTerms ∩ TopNonZeroTerms = {}"
using TopNonZeroTerms_def TopZeroTerms_def by blast
have union: "TopZeroTerms ∪ TopNonZeroTerms = {i+2..N+1}"
proof(safe)
show "⋀n. n ∈ TopZeroTerms ⟹ n ∈ {i + 2..N + 1}"
using TopZeroTerms_def by force
show "⋀n. n ∈ TopNonZeroTerms ⟹ n ∈ {i + 2..N + 1}"
using TopNonZeroTerms_def by blast
show "⋀n. n ∈ {i + 2..N + 1} ⟹ n ∉ TopNonZeroTerms ⟹ n ∈ TopZeroTerms"
using TopNonZeroTerms_def TopZeroTerms_def by blast
qed
have "(∑k∈{i+2..N+1}. ¦f (xs N ! k) - f (xs N ! (k - 1))¦ * ¦σ (w * (x - xs N ! k))¦) <
(∑k∈{i+2..N+1}. η * (1 / N))"
proof -
have "(∑k∈{i+2..N+1}. ¦f (xs N ! k) - f (xs N ! (k - 1))¦ * ¦σ (w * (x - xs N ! k))¦) =
(∑k∈TopNonZeroTerms. ¦f (xs N ! k) - f (xs N ! (k - 1))¦ * ¦σ (w * (x - xs N ! k))¦)"
proof -
have "(∑k∈{i+2..N+1}. ¦f (xs N ! k) - f (xs N ! (k - 1))¦ * ¦σ (w * (x - xs N ! k))¦) =
(∑k∈TopZeroTerms. ¦f (xs N ! k) - f (xs N ! (k - 1))¦ * ¦σ (w * (x - xs N ! k))¦)
+ (∑k∈TopNonZeroTerms. ¦f (xs N ! k) - f (xs N ! (k - 1))¦ * ¦σ (w * (x - xs N ! k))¦)"
by (smt disjoint finite_Un finite_atLeastAtMost union sum.union_disjoint)
then show ?thesis
using zero_terms_eq_zero by linarith
qed
also have "... < (∑k∈TopNonZeroTerms. η * (1 / N))"
proof(rule sum_strict_mono)
show "finite TopNonZeroTerms"
by (metis finite_Un finite_atLeastAtMost union)
show "TopNonZeroTerms ≠ {}"
using TopNonZeroTerms_def second_terms_not_all_zero by blast
fix y
assume y_subtype: "y ∈ TopNonZeroTerms"
then have y_type: "y ∈ {i+2..N+1}"
by (metis Un_iff union)
then have y_suptype: "y ∈ {1..N + 1}"
by simp
have parts_lt_eta: "⋀k. k∈{i+2..N+1} ⟶ ¦(f (xs N ! k) - f (xs N ! (k - 1)))¦ < η"
proof(clarify)
fix k
assume k_type: "k ∈ {i + 2..N + 1}"
then have "k - 1 ∈ {i+1..N}"
by force
then have "¦(xs N ! k) - (xs N ! (k - 1))¦ < δ ⟶ ¦f (xs N ! k) - f (xs N ! (k - 1))¦ < η"
using δ_prop atLeastAtMost_iff els_in_ab le_diff_conv by auto
then show "¦f (xs N ! k) - f (xs N ! (k - 1))¦ < η"
using adj_terms_lt i_leq_N k_type by fastforce
qed
then have f_diff_lt_eta: "¦f (xs N ! y) - f (xs N ! (y - 1))¦ < η"
using y_type by blast
have lt_minus_h: "x - xs N!y ≤ -h"
using x_minus_xk_le_neg_h_on_Right_Half y_type by blast
then have sigma_lt_inverseN: "¦σ (w * (x - xs N ! y))¦ < 1 / N"
proof -
have "¬ Suc N < y"
using y_suptype by force
then show ?thesis
by (smt (z3) Suc_1 Suc_eq_plus1 lt_minus_h add.commute add.left_commute diff_zero length_map length_upt not_less_eq w_prop xs_eqs)
qed
then show "¦f (xs N ! y) - f (xs N ! (y - 1))¦ * ¦σ (w * (x - xs N ! y))¦ < η * (1 / N)"
by (smt (verit, best) f_diff_lt_eta mult_strict_mono)
qed
also have "... ≤ (∑k∈TopNonZeroTerms. η * (1 / N)) + (∑k∈TopZeroTerms. η * (1 / N))"
using η_pos by force
also have "... = (∑k∈{i+2..N+1}. η * (1 / N))"
by (smt disjoint finite_Un finite_atLeastAtMost union sum.union_disjoint)
finally show ?thesis.
qed
then show ?thesis
using ‹(∑k = 2..i - 1. ¦f (xs N ! k) - f (xs N ! (k - 1))¦ * ¦σ (w * (x - xs N ! k)) - 1¦) < (∑k = 2..i - 1. η * (1 / N))› by linarith
qed
qed
qed
next
assume "¬ 3 ≤ i"
then have i_leq_2: "i ≤ 2"
by linarith
then have first_empty_sum: "(∑k = 2..i - 1. ¦f (xs N ! k) - f (xs N ! (k - 1))¦ * ¦σ (w * (x - xs N ! k)) - 1¦) = 0"
by force
from i_leq_2 have second_empty_sum: "(∑k = 2..i - 1. η * (1 / N)) = 0"
by force
have i_lt_N: "i < N"
using N_defining_properties i_leq_2 by linarith
have "(∑k = i + 2..N + 1. ¦f (xs N ! k) - f (xs N ! (k - 1))¦ * ¦σ (w * (x - xs N ! k))¦) <
(∑k = i + 2..N + 1. η * (1 / N))"
proof(cases "∀k. k ∈ {i+2..N+1} ⟶ ¦σ (w * (x - xs N ! k))¦ = 0")
assume all_second_terms_zero: "∀k. k ∈ {i + 2..N + 1} ⟶ ¦σ (w * (x - xs N ! k))¦ = 0"
from i_lt_N have "(∑k∈{i+2..N+1}. ¦f (xs N ! k) - f (xs N ! (k - 1))¦ * ¦σ (w * (x - xs N ! k))¦) < (∑k∈{i+2..N+1}. η * (1/N))"
by (subst sum_strict_mono, fastforce+, (simp add: η_pos all_second_terms_zero)+)
then show ?thesis.
next
assume second_terms_not_all_zero: "¬ (∀k. k ∈ {i + 2..N + 1} ⟶ ¦σ (w * (x - xs N ! k))¦ = 0)"
obtain NonZeroTerms where NonZeroTerms_def: "NonZeroTerms = {k ∈ {i + 2..N + 1}. ¦σ (w * (x - xs N ! k))¦ ≠ 0}"
by blast
obtain ZeroTerms where ZeroTerms_def: "ZeroTerms = {k ∈ {i + 2..N + 1}. ¦σ (w * (x - xs N ! k))¦ = 0}"
by blast
have zero_terms_eq_zero: "(∑k∈ZeroTerms. ¦f (xs N ! k) - f (xs N ! (k - 1))¦ * ¦σ (w * (x - xs N ! k))¦) = 0"
by (simp add: ZeroTerms_def)
have disjoint: "ZeroTerms ∩ NonZeroTerms = {}"
using NonZeroTerms_def ZeroTerms_def by blast
have union: "ZeroTerms ∪ NonZeroTerms = {i+2..N+1}"
proof(safe)
show "⋀n. n ∈ ZeroTerms ⟹ n ∈ {i + 2..N + 1}"
using ZeroTerms_def by force
show "⋀n. n ∈ NonZeroTerms ⟹ n ∈ {i + 2..N + 1}"
using NonZeroTerms_def by blast
show "⋀n. n ∈ {i + 2..N + 1} ⟹ n ∉ NonZeroTerms ⟹ n ∈ ZeroTerms"
using NonZeroTerms_def ZeroTerms_def by blast
qed
have "(∑k∈{i+2..N+1}. ¦f (xs N ! k) - f (xs N ! (k - 1))¦ * ¦σ (w * (x - xs N ! k))¦) <
(∑k∈{i+2..N+1}. η * (1 / N))"
proof -
have "(∑k∈{i+2..N+1}. ¦f (xs N ! k) - f (xs N ! (k - 1))¦ * ¦σ (w * (x - xs N ! k))¦) =
(∑k∈NonZeroTerms. ¦f (xs N ! k) - f (xs N ! (k - 1))¦ * ¦σ (w * (x - xs N ! k))¦)"
proof -
have "(∑k∈{i+2..N+1}. ¦f (xs N ! k) - f (xs N ! (k - 1))¦ * ¦σ (w * (x - xs N ! k))¦) =
(∑k∈ZeroTerms. ¦f (xs N ! k) - f (xs N ! (k - 1))¦ * ¦σ (w * (x - xs N ! k))¦)
+ (∑k∈NonZeroTerms. ¦f (xs N ! k) - f (xs N ! (k - 1))¦ * ¦σ (w * (x - xs N ! k))¦)"
by (smt disjoint finite_Un finite_atLeastAtMost union sum.union_disjoint)
then show ?thesis
using zero_terms_eq_zero by linarith
qed
also have "... < (∑k∈NonZeroTerms. η * (1 / N))"
proof(rule sum_strict_mono)
show "finite NonZeroTerms"
by (metis finite_Un finite_atLeastAtMost union)
show "NonZeroTerms ≠ {}"
using NonZeroTerms_def second_terms_not_all_zero by blast
fix y
assume y_subtype: "y ∈ NonZeroTerms"
then have y_type: "y ∈ {i+2..N+1}"
by (metis Un_iff union)
then have y_suptype: "y ∈ {1..N + 1}"
by simp
have parts_lt_eta: "⋀k. k∈{i+2..N+1} ⟶ ¦(f (xs N ! k) - f (xs N ! (k - 1)))¦ < η"
proof(clarify)
fix k
assume k_type: "k ∈ {i + 2..N + 1}"
then have "k - 1 ∈ {i+1..N}"
by force
then have "¦(xs N ! k) - (xs N ! (k - 1))¦ < δ ⟶ ¦f (xs N ! k) - f (xs N ! (k - 1))¦ < η"
using δ_prop atLeastAtMost_iff els_in_ab le_diff_conv by auto
then show "¦f (xs N ! k) - f (xs N ! (k - 1))¦ < η"
using adj_terms_lt i_leq_N k_type by fastforce
qed
then have f_diff_lt_eta: "¦f (xs N ! y) - f (xs N ! (y - 1))¦ < η"
using y_type by blast
have lt_minus_h: "x - xs N!y ≤ -h"
using x_minus_xk_le_neg_h_on_Right_Half y_type by blast
then have sigma_lt_inverseN: "¦σ (w * (x - xs N ! y))¦ < 1 / N"
proof -
have "¬ Suc N < y"
using y_suptype by force
then show ?thesis
by (smt (z3) Suc_1 Suc_eq_plus1 lt_minus_h add.commute add.left_commute diff_zero length_map length_upt not_less_eq w_prop xs_eqs)
qed
show "¦f (xs N ! y) - f (xs N ! (y - 1))¦ * ¦σ (w * (x - xs N ! y))¦ < η * (1 / N)"
using f_diff_lt_eta mult_strict_mono sigma_lt_inverseN by fastforce
qed
also have "... ≤ (∑k∈NonZeroTerms. η * (1 / N)) + (∑k∈ZeroTerms. η * (1 / N))"
using η_pos by force
also have "... = (∑k∈{i+2..N+1}. η * (1 / N))"
by (smt disjoint finite_Un finite_atLeastAtMost union sum.union_disjoint)
finally show ?thesis.
qed
then show ?thesis.
qed
then show ?thesis
using first_empty_sum second_empty_sum by linarith
qed
also have "... = ¦f (a)¦ * ¦σ (w * (x - xs N ! 0)) - 1¦ + (∑k∈{2..i-1}. η * (1/N)) + (∑k∈{i+2..N+1}. η * (1/N))"
by simp
also have "... ≤ ¦f (a)¦ * ¦σ (w * (x - xs N ! 0)) - 1¦ + (∑k∈{2..N+1}. η * (1/N))"
proof -
have "(∑k∈{2..i-1}. η * (1/N)) + (∑k∈{i+2..N+1}. η * (1/N)) ≤ (∑k∈{2..N+1}. η * (1/N))"
proof(cases "i≥ 3")
assume "3 ≤ i"
have disjoint: "{2..i-1} ∩ {i+2..N+1} = {}"
by auto
from i_leq_N have subset: "{2..i-1} ∪ {i+2..N+1} ⊆ {2..N+1}"
by auto
have sum_union: "sum (λk. η * (1 / N)) {2..i-1} + sum (λk. η * (1 / N)) {i+2..N+1} =
sum (λk. η * (1 / N)) ({2..i-1} ∪ {i+2..N+1})"
by (metis disjoint finite_atLeastAtMost sum.union_disjoint)
from subset η_pos have "sum (λk. η * (1 / N)) ({2..i-1} ∪ {i+2..N+1}) ≤ sum (λk. η * (1 / N)) {2..N+1}"
by(subst sum_mono2, simp_all)
then show ?thesis
using sum_union by auto
next
assume "¬ 3 ≤ i"
then have i_leq_2: "i ≤ 2"
by linarith
then have first_term_zero: "(∑k = 2..i - 1. η * (1 / N)) = 0"
by force
from η_pos have "(∑k = i + 2..N + 1. η * (1 / N)) ≤ (∑k = 2..N + 1. η * (1 / N))"
by(subst sum_mono2, simp_all)
then show ?thesis
using first_term_zero by linarith
qed
then show ?thesis
by linarith
qed
also have "... = ¦f (a)¦ * ¦σ (w * (x - xs N ! 0)) - 1¦ + (N * η * (1/N))"
proof -
have "(∑k∈{2..N+1}. η * (1/N)) = (N * η * (1/N))"
by(subst sum_constant, simp)
then show ?thesis
by presburger
qed
also have "... = ¦f (a)¦ * ¦σ (w * (x - xs N ! 0)) - 1¦ + η"
by (simp add: N_pos)
also have "... ≤ ¦f (a)¦ * (1/N) + η"
proof -
have "¦σ (w * (x - xs N ! 0)) - 1¦ < 1/N"
by (smt (z3) Suc_eq_plus1_left ω_prop add_2_eq_Suc' add_gr_0 atLeastAtMost_iff diff_zero
length_map length_upt w_def x_in_ab xs_eqs zero_less_one zeroth_element)
then show ?thesis
by (smt (verit, ccfv_SIG) mult_less_cancel_left)
qed
also have "... ≤ ¦f (a)¦ * η + η"
by (smt (verit, best) mult_left_mono one_over_N_lt_eta)
also have "... = (1 + ¦f (a)¦) * η"
by (simp add: distrib_right)
also have "... ≤ (1+ (SUP x ∈ {a..b}. ¦f x¦)) * η"
proof -
from a_lt_b have "¦f (a)¦ ≤ (SUP x ∈ {a..b}. ¦f x¦)"
by (subst cSUP_upper, simp_all, metis bdd_above_Icc contin_f continuous_image_closed_interval continuous_on_rabs order_less_le)
then show ?thesis
by (simp add: η_pos)
qed
finally show ?thesis.
qed
have x_i_pred_minus_x_lt_delta: "¦xs N !(i-1) - x¦ < δ"
proof -
have "¦xs N !(i-1) - x¦ ≤ ¦xs N !(i-1) - xs N!i¦ + ¦xs N!i - x¦"
by linarith
also have "... ≤ 2*h"
proof -
have first_inequality: "¦xs N !(i-1) - xs N!i¦ ≤ h"
using difference_of_adj_terms h_pos i_ge_1 i_leq_N by fastforce
have second_inequality: "¦xs N!i - x¦ ≤ h"
by (smt (verit) left_diff_distrib' mult_cancel_right1 x_lower_bound_aux x_upper_bound_aux xs_Suc_i xs_i)
show ?thesis
using first_inequality second_inequality by fastforce
qed
also have "... < δ"
using h_lt_δ_half by auto
finally show ?thesis.
qed
have I2_final_bound: "I_2 i x < (2 * (Sup ((λx. ¦σ x¦) ` UNIV)) + 1) * η"
proof(cases "i ≥ 3")
assume three_lt_i: "3 ≤ i"
have telescoping_sum: "sum (λk. f (xs N ! k) - f (xs N ! (k - 1))) {2..i-1} + f a = f (xs N ! (i-1))"
proof(cases "i = 3")
show "i = 3 ⟹ (∑k = 2..i - 1. f (xs N ! k) - f (xs N ! (k - 1))) + f a = f (xs N ! (i - 1))"
using first_element by force
next
assume "i ≠ 3"
then have i_gt_3: "i > 3"
by (simp add: le_neq_implies_less three_lt_i)
have "sum (λk. f (xs N ! k) - f (xs N ! (k - 1))) {2..i-1} = f(xs N!(i-1)) - f(xs N!(2-1))"
proof -
have f1: "1 ≤ i - Suc 1"
using three_lt_i by linarith
have index_shift: "(∑k ∈ {2..i-1}. f (xs N ! (k - 1))) = (∑k ∈ {1..i-2}. f (xs N ! k))"
by (rule sum.reindex_bij_witness[of _ "λj. j +1" "λj. j -1"], simp_all, presburger+)
have "sum (λk. f (xs N ! k) - f (xs N ! (k - 1))) {2..i-1} =
(∑k ∈ {2..i-1}. f (xs N ! k)) - (∑k ∈ {2..i-1}. f (xs N ! (k - 1)))"
by (simp add: sum_subtractf)
also have "... = (∑k ∈ {2..i-1}. f (xs N ! k)) - (∑k ∈ {1..i-2}. f (xs N ! k))"
using index_shift by presburger
also have "... = (∑k ∈ {2..i-1}. f (xs N ! k)) - (f (xs N ! 1) + (∑k ∈ {2..i-2}. f (xs N ! k)))"
using f1 by (metis (no_types) Suc_1 sum.atLeast_Suc_atMost)
also have "... = ((∑k ∈ {2..i-1}. f (xs N ! k)) - (∑k ∈ {2..i-2}. f (xs N ! k))) - f (xs N ! 1)"
by linarith
also have "... = (f (xs N ! (i-1)) + (∑k ∈ {2..i-2}. f (xs N ! k)) - (∑k ∈ {2..i-2}. f (xs N ! k))) - f (xs N ! 1)"
proof -
have disjoint: "{2..i-2} ∩ {i-1} = {}"
by force
have union: "{2..i-2} ∪ {i-1} = {2..i-1}"
proof(safe)
show "⋀n. n ∈ {2..i - 2} ⟹ n ∈ {2..i - 1}"
by fastforce
show "⋀n. i - 1 ∈ {2..i - 1}"
using three_lt_i by force
show "⋀n. n ∈ {2..i - 1} ⟹ n ∉ {2..i - 2} ⟹ n ∉ {} ⟹ n = i - 1"
by presburger
qed
have "(∑k ∈ {2..i-2}. f (xs N ! k)) + f (xs N ! (i-1)) = (∑k ∈ {2..i-2}. f (xs N ! k)) + (∑k ∈ {i-1}. f (xs N ! k))"
by auto
also have "... = (∑k ∈ {2..i-2} ∪ {i-1}. f (xs N ! k))"
using disjoint by force
also have "... = (∑k ∈ {2..i-1}. f (xs N ! k))"
using union by presburger
finally show ?thesis
by linarith
qed
also have "... = f (xs N ! (i-1)) - f (xs N ! 1)"
by auto
finally show ?thesis
by simp
qed
then show ?thesis
using first_element by auto
qed
have I2_decomp: "I_2 i x = ¦L i x - f x¦"
using I_2_def i_ge_1 i_leq_N by presburger
also have "... = ¦ (((∑k∈{2..i-1}. (f (xs N ! k) - f (xs N ! (k - 1)))) + f(a)) +
(f (xs N ! i) - f (xs N ! (i-1))) * σ (w * (x - xs N ! i)) +
(f (xs N ! (i+1)) - f (xs N ! i)) * σ (w * (x - xs N ! (i+1)))) - f x¦"
using L_def three_lt_i by auto
also have "... = ¦ f (xs N ! (i-1)) - f x +
(f (xs N ! i) - f (xs N ! (i-1))) * σ (w * (x - xs N ! i)) +
(f (xs N ! (i+1)) - f (xs N ! i)) * σ (w * (x - xs N ! (i+1)))¦"
using telescoping_sum by fastforce
also have "... ≤ ¦ f (xs N ! (i-1)) - f x¦ +
¦(f (xs N ! i) - f (xs N ! (i-1))) * σ (w * (x - xs N ! i))¦ +
¦(f (xs N ! (i+1)) - f (xs N ! i)) * σ (w * (x - xs N ! (i+1)))¦"
by linarith
also have "... = ¦ f (xs N ! (i-1)) - f x¦ +
¦(f (xs N ! i) - f (xs N ! (i-1)))¦ * ¦ σ (w * (x - xs N ! i))¦ +
¦(f (xs N ! (i+1)) - f (xs N ! i))¦ * ¦σ (w * (x - xs N ! (i+1)))¦"
by (simp add: abs_mult)
also have "... < η + η * ¦ σ (w * (x - xs N ! i))¦ + η * ¦σ (w * (x - xs N ! (i+1)))¦"
proof -
from x_in_ab x_i_pred_minus_x_lt_delta
have first_inequality: "¦f (xs N ! (i-1)) - f x¦ < η"
by(subst δ_prop,
metis Suc_eq_plus1 add_0 add_le_imp_le_diff atLeastAtMost_iff els_in_ab i_leq_N less_imp_diff_less linorder_not_le numeral_3_eq_3 order_less_le three_lt_i,
simp_all)
from els_in_ab i_leq_N le_diff_conv three_lt_i
have second_inequality: "¦(f (xs N ! i) - f (xs N ! (i-1)))¦ < η"
by(subst δ_prop,
simp_all,
metis One_nat_def add.commute atLeastAtMost_iff adj_terms_lt i_ge_1 trans_le_add2)
have third_inequality: "¦(f (xs N ! (i+1)) - f (xs N ! i))¦ < η"
proof(subst δ_prop)
show "xs N ! (i + 1) ∈ {a..b}" and "xs N ! i ∈ {a..b}" and True
using els_in_ab i_ge_1 i_leq_N by auto
show "¦xs N ! (i + 1) - xs N ! i¦ < δ"
using adj_terms_lt
by (metis Suc_eq_plus1 Suc_eq_plus1_left Suc_le_mono add_diff_cancel_left' atLeastAtMost_iff i_leq_N le_add2)
qed
then show ?thesis
by (smt (verit, best) first_inequality mult_right_mono second_inequality)
qed
also have "... = (¦ σ (w * (x - xs N ! i))¦ + ¦σ (w * (x - xs N ! (i+1)))¦ + 1) * η"
by (simp add: mult.commute ring_class.ring_distribs(1))
also have "... ≤ (2* (Sup ((λx. ¦σ x¦) ` UNIV)) + 1) * η"
proof -
from bounded_sigmoidal have first_inequality: "¦ σ (w * (x - xs N ! i))¦ ≤ (Sup ((λx. ¦σ x¦) ` UNIV))"
by (metis UNIV_I bounded_function_def cSUP_upper2 dual_order.refl)
from bounded_sigmoidal have second_inequality: "¦ σ (w * (x - xs N ! (i+1)))¦ ≤ (Sup ((λx. ¦σ x¦) ` UNIV))"
unfolding bounded_function_def
by (subst cSUP_upper, simp_all)
then show ?thesis
using η_pos first_inequality by auto
qed
finally show ?thesis.
next
assume "¬ 3 ≤ i"
then have i_is_1_or_2: "i = 1 ∨ i = 2"
using i_ge_1 by linarith
have x_near_a: "¦a - x¦ < δ"
proof(cases "i = 1")
show "i = 1 ⟹ ¦a - x¦ < δ"
using first_element h_pos x_i_pred_minus_x_lt_delta x_lower_bound_aux zeroth_element by auto
show "i ≠ 1 ⟹ ¦a - x¦ < δ"
using first_element i_is_1_or_2 x_i_pred_minus_x_lt_delta by auto
qed
have Lix: "L i x = f(a) + (f (xs N ! 3) - f (xs N ! 2)) * σ (w * (x - xs N ! 3)) + (f (xs N ! 2) - f (xs N ! 1)) * σ (w * (x - xs N ! 2))"
using L_def i_is_1_or_2 by presburger
have "I_2 i x = ¦L i x - f x¦"
using I_2_def i_ge_1 i_leq_N by presburger
also have "... = ¦(f a - f x) + (f (xs N ! 3) - f (xs N ! 2)) * σ (w * (x - xs N ! 3)) + (f (xs N ! 2) - f (xs N ! 1)) * σ (w * (x - xs N ! 2))¦"
using Lix by linarith
also have "... ≤ ¦(f a - f x)¦ + ¦(f (xs N ! 3) - f (xs N ! 2)) * σ (w * (x - xs N ! 3))¦ + ¦(f (xs N ! 2) - f (xs N ! 1)) * σ (w * (x - xs N ! 2))¦"
by linarith
also have "... ≤ ¦(f a - f x)¦ + ¦f (xs N ! 3) - f (xs N ! 2)¦ * ¦σ (w * (x - xs N ! 3))¦ + ¦f (xs N ! 2) - f (xs N ! 1)¦ * ¦σ (w * (x - xs N ! 2))¦"
by (simp add: abs_mult)
also have "... < η + η * ¦ σ (w * (x - xs N ! 3))¦ + ¦f (xs N ! 2) - f (xs N ! 1)¦ * ¦σ (w * (x - xs N ! 2))¦"
proof -
from x_in_ab x_near_a have first_inequality: "¦f a - f x¦ < η"
by(subst δ_prop, auto)
have second_inequality: "¦f (xs N ! 3) - f (xs N ! 2)¦ < η"
proof(subst δ_prop, safe)
show "xs N ! 3 ∈ {a..b}"
using N_gt_3 els_in_ab by force
show "xs N ! 2 ∈ {a..b}"
using N_gt_3 els_in_ab by force
from N_gt_3 have "xs N ! 3 - xs N ! 2 = h"
by(subst xs_els, auto, smt (verit, best) h_pos i_is_1_or_2 mult_cancel_right1 nat_1_add_1 of_nat_1 of_nat_add xs_Suc_i xs_i)
then show "¦xs N ! 3 - xs N ! 2¦ < δ"
using adj_terms_lt first_element zeroth_element by fastforce
qed
then show ?thesis
by (smt (verit, best) first_inequality mult_right_mono)
qed
also have "... ≤ η + η * ¦ σ (w * (x - xs N ! 3))¦ + η * ¦σ (w * (x - xs N ! 2))¦"
proof -
have third_inequality: "¦f (xs N ! 2) - f (xs N ! 1)¦ < η"
proof(subst δ_prop, safe)
show "xs N ! 2 ∈ {a..b}"
using N_gt_3 els_in_ab by force
show "xs N ! 1 ∈ {a..b}"
using N_gt_3 els_in_ab by force
from N_pos first_element have "xs N ! 2 - xs N ! 1 = h"
by(subst xs_els, auto)
then show "¦xs N ! 2 - xs N ! 1¦ < δ"
using adj_terms_lt first_element zeroth_element by fastforce
qed
show ?thesis
by (smt (verit, best) mult_right_mono third_inequality)
qed
also have "... = (¦ σ (w * (x - xs N ! 3))¦ + ¦σ (w * (x - xs N ! 2))¦ + 1)*η"
by (simp add: mult.commute ring_class.ring_distribs(1))
also have "... ≤ (2*(Sup ((λx. ¦σ x¦) ` UNIV)) + 1) * η"
proof -
from bounded_sigmoidal have first_inequality: "¦ σ (w * (x - xs N ! 3))¦ ≤ Sup ((λx. ¦σ x¦) ` UNIV)"
unfolding bounded_function_def
by (subst cSUP_upper, simp_all)
from bounded_sigmoidal have second_inequality: "¦ σ (w * (x - xs N ! 2))¦ ≤ Sup ((λx. ¦σ x¦) ` UNIV)"
unfolding bounded_function_def
by (subst cSUP_upper, simp_all)
then show ?thesis
using η_pos first_inequality by force
qed
finally show ?thesis.
qed
have "¦(∑k = 2..N + 1. (f (xs N ! k) - f (xs N ! (k - 1))) * σ (w * (x - xs N ! k))) + f a * σ (w * (x - xs N ! 0)) - f x¦ ≤ I_1 i x + I_2 i x"
using G_Nf_def i_ge_1 i_leq_N triange_inequality_main first_element by blast
also have "... < (1+ (Sup ((λx. ¦f x¦) ` {a..b}))) * η + (2 * (Sup ((λx. ¦σ x¦) ` UNIV)) + 1) * η"
using I1_final_bound I2_final_bound by linarith
also have "... = ((Sup ((λx. ¦f x¦) ` {a..b})) + 2*(Sup ((λx. ¦σ x¦) ` UNIV)) + 2)* η"
by (simp add: distrib_right)
also have "... = ε"
using η_def η_pos by force
finally show "¦(∑k = 2..N + 1. (f (xs N ! k) - f (xs N ! (k - 1))) * σ (w * (x - xs N ! k))) + f a * σ (w * (x - xs N ! 0)) - f x¦ < ε".
qed
qed
end