Theory Lemma_1_8_Coding

theory Lemma_1_8_Coding                                 
  imports Lemma_1_8_Defs
begin

subsubsection ‹Bounds on the defined variables›

locale K_Nonnegative = Lemma_1_8_Defs +
  assumes δ_pos: "δ > 0"
      and L_pos: "L > 0"
      and L_lower_bound: "L ≥ max_coeff P"
      and len_z: "length z = ν+1"
      and ℬ_even: "2 dvd ℬ"
      and ℬ_lower_bound: "ℬ > 2 * fact δ * (nat L) * (1 + sum_list z)^δ"   
begin

text ‹This is for convenience in proofs, but the following lemma is strictly stronger.›
lemma ℬ_ge_1[simp]: "ℬ ≥ 1" 
  using ℬ_lower_bound δ_pos L_pos by auto

lemma ℬ_gt_2[simp]: "ℬ > 2" 
  using ℬ_lower_bound
  by (smt (verit, ccfv_threshold) L_pos ℬ_ge_1 fact_gt_zero less_2_cases less_numeral_extra(3)
      less_one linorder_neqE_nat mult_eq_0_iff nat_1_eq_mult_iff nat_le_iff_add not_one_le_zero 
      power_not_zero zero_less_nat_eq)

text ‹Also for convenience.›
lemma ℬ_ge_2[simp]: "ℬ ≥ 2" 
  using ℬ_gt_2 by linarith

lemma b_def_reverse: "2 * b = ℬ" using ℬ_even b_def by simp

lemma b_ge_1[simp]: "b ≥ 1" 
  using b_def_reverse ℬ_ge_1 by fastforce

lemma n_ge_1[simp]: "n j ≥ 1" 
  unfolding n_def by auto

lemma L_lower_bound_specialize: "L ≥ abs (P_coeff i)" 
proof cases
  assume assm: "P_coeff i ≠ 0"
  hence "P_coeff i ∈ coeffs P"
    unfolding P_coeff_def coeffs_def by (simp add: coeff_def coeff_keys)
  hence 0: "abs (P_coeff i) ∈ abs ` coeffs P"
    by auto

  have "L ≥ Max (abs ` coeffs P)"
    using L_lower_bound max_coeff_def by metis
  thus ?thesis
    using 0 by (meson Max_ge finite_coeffs finite_imageI order_trans)
next 
  assume "¬ P_coeff i ≠ 0"
  hence "P_coeff i = 0" by auto
  thus ?thesis using L_pos by auto
qed

lemma δ_tuples_finite[simp]: "finite δ_tuples"
proof -
  have stronger: "finite {i::nat list. length i = n ∧ sum_list i ≤ K }" 
    (is "finite (?S n)") for n K
  proof (induction n)
    case 0 thus ?case by auto
  next
    case (Suc n)
    { fix i assume assm_i: "i ∈ ?S (Suc n)"
      then obtain j0 j where i_def: "i = j0#j"
        by (smt (verit, best) Suc_length_conv mem_Collect_eq)
      hence "(j0, j) ∈ ({..K} × ?S n)" using assm_i by auto
      hence "i ∈ (λ(j0, j). j0#j) ` ({..K} × ?S n)" using i_def by auto }
    hence "?S (Suc n) ⊆ (λ(j0, j). j0#j) ` ({..K} × ?S n)" 
     by blast
    moreover have "finite ((λ(j0, j). j0#j) ` ({..K} × ?S n))" 
      using Suc.IH by blast
    ultimately have "finite (?S (Suc n))" 
      by (meson finite_subset)
    thus ?case .
  qed
  thus ?thesis unfolding δ_tuples_def .
qed

lemma P_z_insertion: "insertion z_assign P = (∑i∈δ_tuples. P_coeff i * mpow z i)"
proof -
  have mpow_eq: "i∈δ_tuples ⟹ (∏s≤ν. (z_assign s)^(i!s)) = mpow z i" for i
  proof -
    assume i_def: "i∈δ_tuples" 
    have 0: "s < length z ⟹ z_assign s = int (z!s)" for s
    proof -
      assume "s < length z"
      hence "s < length (map int z)" 
        using length_map by simp
      hence "z_assign s = (map int z) ! s"
        unfolding z_assign_def using nth0_nth by blast
      also have "... = int (z ! s)"
        using `s < length z` nth_map by blast
      finally show ?thesis .
    qed

    have z_i_length: "min (length z) (length i) = length z"
      using δ_tuples_def len_z i_def by auto
    
    have "(∏s≤ν. (z_assign s)^(i!s)) = (∏s<length z. (z_assign s)^(i!s))"
      using Suc_eq_plus1 len_z lessThan_Suc_atMost by presburger  
    also have "... = (∏s<length z. (int (z!s))^(i!s))"
      using 0 by simp
    finally show "(∏s≤ν. (z_assign s)^(i!s)) = int (mpow z i)"
      unfolding mpow_def using z_i_length by auto
  qed
 
  have "P = (∑i∈δ_tuples. of_int (P_coeff i) * (∏s=0..ν. (Var s)^(i!s)))"
    unfolding δ_tuples_def ν_def δ_def of_int_Const P_coeff_def 
    using mpoly_multivariate_expansion by auto
  hence "insertion z_assign P = (∑i∈δ_tuples. insertion z_assign (of_int (P_coeff i)) * 
    insertion z_assign (∏s≤ν. (Var s)^(i!s)))"
    using insertion_sum insertion_mult δ_tuples_finite
    by (smt (verit, del_insts) sum.cong atLeast0AtMost)
  also have "... = (∑i∈δ_tuples. P_coeff i * insertion z_assign (∏s≤ν. (Var s)^(i!s)))"
    using of_int_Const by simp
  also have "... = (∑i∈δ_tuples. P_coeff i * mpow z i)" 
    by (simp add: mpow_eq)
  finally show ?thesis .
qed


text ‹This is essentially an instance of the multinomial theorem.›
lemma c_delta_expansion:
  "(1+c)^δ = (∑i∈δ_tuples. of_nat ((δ mchoose i) * mpow z i) * X^(∑s≤ν. i!s * n s))"
proof -
  define F::"(int mpoly) list" where 
    "F = map (λs. of_nat (z!(nat s)) * X^(n (nat s))) [0..ν]"   
  
  have F_length: "length F = ν+1" 
    unfolding F_def by simp

  have F_get: "s < length F ⟹ F!s = of_nat (z!s) * X^(n s)" for s 
    unfolding F_def using F_length by simp

  have F_mpow: "length i = ν + 1 ⟹
    mpow F i = of_nat (mpow z i) * X ^ (∑s<ν + 1. i ! s * n s)" for i
  proof -
    assume "length i = ν + 1"
    hence F_i_length: "min (length F) (length i) = ν + 1" using F_length by auto
    have "mpow F i = (∏s<ν+1. (of_nat (z!s) * X^(n s)) ^ i!s)" 
      using F_i_length by (simp add: mpow_def F_get)
    also have "... = (∏s<ν+1. (of_nat (z!s))^ i!s) * (∏s<ν+1. (X^(n s)) ^ i!s)"
     by (simp add: power_mult_distrib prod.distrib)   
    also have "... = of_nat (mpow z i) * (∏s<ν+1. (X^(n s)) ^ i!s)" 
      unfolding mpow_def using len_z F_i_length by auto
    also have "... = of_nat (mpow z i) * (∏s<ν+1. X^(i!s * n s))"
      by (metis mult.commute power_mult)
    also have "... = of_nat (mpow z i) * X^(∑s<ν+1. i!s * n s)" 
      by (smt (verit, ccfv_SIG) power_sum prod.cong)
    finally show ?thesis .
  qed

  have "(1 + c)^δ = (1 + (∑s≤ν. F!s))^δ" 
    by (simp add : c_def F_get F_length)
  also have "... = (1 + sum_list F)^δ" 
    using F_length by (metis Suc_eq_plus1 atLeastLessThanSuc_atLeastAtMost sum_list_sum_nth 
                       atLeast0AtMost)
  also have "... = (∑i | length i = length F ∧ sum_list i ≤ δ. of_nat (δ mchoose i) * mpow F i)" 
    by (simp only: multinomial_ring_alt)
  also have "... = (∑i∈δ_tuples. of_nat (δ mchoose i) * mpow F i)" 
    unfolding δ_tuples_def by (simp add: F_length)
  also have "... = (∑i∈δ_tuples. of_nat (δ mchoose i) * 
    of_nat (mpow z i) * X^(∑s≤ν. i!s * n s))"
    by (auto simp add: algebra_simps F_mpow δ_tuples_def lessThan_Suc_atMost)
  finally show ?thesis by auto
qed

lemma n_νp1_ge_sum: "i∈δ_tuples ⟹ n (ν+1) ≥ (∑s≤ν. i!s * n s)"
proof - 
  assume i_def: "i∈δ_tuples"

  { fix s assume "s ∈ {..ν}" 
    hence "i!s * n s ≤ i!s * n ν" 
      unfolding n_def by (simp add: power_increasing) }
  note 0 = this

  have "(∑s≤ν. i!s * n s) ≤ (∑s≤ν. i!s * n ν)"
    using 0 by (meson atLeastAtMost_iff atMost_iff sum_mono zero_le)
  also have "... = n ν * (∑s≤ν. i!s)"
    using sum_distrib_right by (metis mult.commute)
  also have "... = n ν * (∑s<length i. i!s)"
    using i_def unfolding δ_tuples_def using lessThan_Suc_atMost by force
  also have "... = n ν * sum_list i"
    by (simp add: sum_list_sum_nth atLeast0LessThan)
  also have "... ≤ n ν * δ"
    using i_def unfolding δ_tuples_def by simp
  also have "... ≤ n (ν+1)"
    unfolding n_def by auto
  finally show ?thesis .
qed

lemma D_exponent_inj: "inj_on D_exponent δ_tuples"
proof
  have digit: "i ∈ δ_tuples ⟹ 
    nth_digit (∑s≤ν. i!s * (δ+1)^s) s (δ+1) = (if s ≤ ν then i!s else 0)" for i s
  proof -
    assume i_def: "i ∈ δ_tuples"
    have "s ≤ ν ⟹ i!s < δ+1" for s
    proof -
      assume "s ≤ ν" 
      hence "s < length i" using i_def δ_tuples_def by auto
      hence "i!s ≤ sum_list i" using elem_le_sum_list by auto
      thus ?thesis using i_def δ_tuples_def by auto
    qed 
    hence "nth_digit (∑s=0..ν. i!s * (δ+1)^s) s (δ+1) = (if s ≤ ν then i!s else 0)"
      using nth_digit_gen_power_series_general[of "δ+1" ν] δ_pos by simp
    thus ?thesis
      using atMost_atLeast0 by presburger
  qed

  fix i j assume i_def: "i∈δ_tuples" and j_def: "j∈δ_tuples" 
    and "D_exponent i = D_exponent j"
  hence "(∑s≤ν. i!s * (δ+1)^s) = (∑s≤ν. j!s * (δ+1)^s)"
    unfolding D_exponent_def using n_νp1_ge_sum n_def
    by (metis (no_types, lifting) diff_diff_cancel sum.cong)
  hence "s ≤ ν ⟹ i!s = j!s" for s
    using digit i_def j_def by (metis (full_types))
  hence "s < length i ⟹ i!s = j!s" for s  
    using i_def unfolding δ_tuples_def by auto
  thus "i = j" 
    apply (simp add: List.list_eq_iff_nth_eq)
    using δ_tuples_def i_def j_def by force
qed

definition R_exponent :: "nat list ⇒ nat list ⇒ nat" where 
  "R_exponent i j = D_exponent j + (∑s≤ν. i!s * n s)"

lemma R_expansion:
  "R = (∑i∈δ_tuples. (∑j∈δ_tuples. 
    of_int ((δ mchoose i) * mfact j * fact (δ - sum_list j) * mpow z i * P_coeff j) *
    X^(R_exponent i j)))"
proof -
  define A::"nat list ⇒ int mpoly" where "A = (λi. of_nat ((δ mchoose i) * mpow z i))" 
  define B::"nat list ⇒ int mpoly" where "B = (λi. of_int (D_precoeff i * P_coeff i))" 
  
  have AB_rewrite: "A i * B j = of_int ((δ mchoose i) * mfact j * 
    fact (δ - sum_list j) * mpow z i * P_coeff j)" for i j
  using A_def B_def D_precoeff_def by simp

  have "R = (1+c)^δ * D" by (simp add: R_def)
  also have "... = (∑i∈δ_tuples. A i * X^(∑s≤ν. i!s * n s)) *
    (∑j∈δ_tuples. B j * X^(D_exponent j))"
    by (simp add: D_def c_delta_expansion A_def B_def)
  also have "... = (∑i∈δ_tuples. (∑j∈δ_tuples. 
    A i * X^(∑s≤ν. i!s * n s) * (B j * X^(D_exponent j))))"
    using sum_product by simp
  also have "... = (∑i∈δ_tuples. (∑j∈δ_tuples. 
    (A i * B j) * (X^(∑s≤ν. i!s * n s) * X^(D_exponent j))))"
    by (simp add: algebra_simps)
  also have "... = (∑i∈δ_tuples. (∑j∈δ_tuples. 
    A i * B j * X^(R_exponent i j)))"
    unfolding R_exponent_def by (simp add: mult.commute power_add)
  finally show ?thesis by (simp add: AB_rewrite)
qed

lemma c_degree_bound: "degree c 0 ≤ n ν"
proof -
  have 0: "s∈{..ν} ⟹ degree (of_nat (z!s) * X^(n s)) 0 ≤ n ν" for s
  proof -
    assume Hs: "s ∈ {..ν}"
    have "degree (of_nat (z!s) * X^(n s)) 0 ≤ degree (X^(n s)) 0"
      using degree_mult degree_Const of_nat_Const by (metis add_0)
    also have "... ≤ n s * degree X 0"
      using degree_pow by auto
    also have "... = n s" 
      unfolding X_def using degree_Var by (metis nat_mult_1_right) 
    also have "... ≤ n ν"
      unfolding n_def using Hs
      by (simp add: power_increasing)
    finally show ?thesis .
  qed

  have "degree c 0 ≤ Max (insert 0 ((λs. degree (of_nat (z!s) * X^(n s)) 0) ` {..ν}))"
    unfolding c_def using degree_sum by blast
  also have "... ≤ n ν" 
    by (simp add: 0)
  finally show ?thesis .
qed

lemma D_degree_bound: "degree D 0 ≤ n (ν+1)"
proof -
  have 0: "i∈δ_tuples ⟹  
    degree (of_int (D_precoeff i * P_coeff i) * X^(D_exponent i)) 0 ≤ n (ν+1)" for i
  proof -
    assume "i∈δ_tuples"
    have "degree (of_int (D_precoeff i * P_coeff i) * X^(D_exponent i)) 0 ≤ 
      degree (X^(D_exponent i)) 0" 
      using degree_mult degree_Const of_int_Const by (metis add_0)
    also have "... ≤ D_exponent i"
      unfolding X_def using degree_pow degree_Var by (metis mult.right_neutral)
    also have "... ≤ n (ν+1)"
      unfolding D_exponent_def by auto
    finally show ?thesis .
  qed

  have "degree D 0 ≤ Max (insert 0 (
    (λi. degree (of_int (D_precoeff i * P_coeff i) * X^(D_exponent i)) 0) ` δ_tuples))"
    unfolding D_def using degree_sum δ_tuples_finite by blast
  also have "... ≤ n (ν+1)"
    using 0 by auto
  finally show ?thesis .
qed

lemma R_degree_bound: "degree R 0 ≤ (2*δ+1) * n ν"
proof - 
  have c_1_deg: "degree (1 + c) 0 ≤ degree c 0"
  proof cases
    assume "degree c 0 ≥ 1"
    thus ?thesis using degree_add degree_one by (metis max_def zero_le)
  next
    assume "¬ 1 ≤ degree c 0"
    hence "degree c 0 = 0" by auto
    moreover have "degree (1 + c) 0 ≤ 0"
      by (metis degree_add MPoly_Type.degree_one calculation max_0L) 
    ultimately show ?thesis by auto
  qed

  have "degree R 0 ≤ degree ((1+c)^δ) 0 + degree D 0"
    unfolding R_def by (simp add: degree_mult)
  also have "... ≤ δ * degree (1+c) 0 + degree D 0"
    by (simp add: degree_pow)
  also have "... ≤ δ * degree c 0 + degree D 0" 
    by (simp add: c_1_deg)
  also have "... ≤ δ * n ν + n (ν+1)"
    using c_degree_bound D_degree_bound by (simp add: add_le_mono)
  finally show ?thesis unfolding n_def by auto
qed  


lemma R_univariate: "vars R ⊆ {0}"
proof -
  define x where "x = (λi j. of_int 
    (int ((δ mchoose i) * mfact j * fact (δ - sum_list j) * mpow z i) * P_coeff j) 
    * X ^ R_exponent i j)"
  have vars_0: "vars (x i j) ⊆ {0}" for i j 
  proof -
    have "vars (x i j) ⊆ vars (X^R_exponent i j)"
      using vars_Const vars_mult of_int_Const x_def by fastforce
    also have "... ⊆ vars X"
      using vars_pow by auto
    also have "... = {0}"
      using vars_Var X_def by metis
    finally show ?thesis .
  qed

  have "vars R ⊆ (⋃i∈δ_tuples. vars (∑j∈δ_tuples. x i j))" 
    unfolding R_expansion x_def using vars_setsum δ_tuples_finite by blast
  also have "... ⊆ (⋃i∈δ_tuples. (⋃j∈δ_tuples. vars (x i j)))"
    using vars_setsum δ_tuples_finite by fast
  also have "... ⊆ (⋃i∈δ_tuples. (⋃j∈δ_tuples. {0}))"
    using vars_0 by auto
  also have "... ⊆ {0}"
    by auto
  finally show ?thesis .
qed

lemma R_sum_e: "R = (∑i≤(2*δ+1) * n ν. (of_int (e i)) * X^i)"
proof -
  have 0: "i ∉ {..(2*δ+1) * n ν} ⟹ of_int (e i) * X^i = 0" for i
  proof -
    assume "i∉{..(2*δ+1) * n ν}"
    hence "i > (2*δ+1) * n ν" 
      by auto
    hence "i > degree R 0" 
      using R_degree_bound by auto
    hence "i ∉ ((λm. lookup m 0) ` keys (mapping_of R))"
      unfolding degree_def by auto
    hence "Poly_Mapping.single 0 i ∉ keys (mapping_of R)"
      by (metis lookup_single_eq rev_image_eqI)
    hence "e i = 0" 
      unfolding e_def coeff_def by (simp add: in_keys_iff)
    thus ?thesis by auto
  qed

  have "R = Sum_any (λi. monom (Poly_Mapping.single 0 i) (e i))"
    using mpoly_univariate_expansion R_univariate e_def by auto
  also have "... = Sum_any (λi. Const (e i) * monom (Poly_Mapping.single 0 i) 1)"
    using cst_poly_times_monom_one by (metis (mono_tags, lifting) Const.abs_eq)
  also have "... = Sum_any (λi. of_int (e i) * X^i)"
    unfolding of_int_Const e_def X_def
    by (metis (no_types, lifting) Var.abs_eq Var⇩0_def monom.abs_eq monom_pow mult_1 power_one)
  also have "... = Sum_any (λi. if i∈{..(2*δ+1) * n ν} then of_int (e i) * X^i else 0)"
    using 0 by meson
  also have "... = (∑i∈{..(2*δ+1) * n ν}. of_int (e i) * X^i)"
    by (simp add: Sum_any.conditionalize)
  finally show ?thesis .
qed


lemma e_expression:
  "e p = (∑i∈δ_tuples. (∑j∈δ_tuples ∩ {j. R_exponent i j = p}.
    (δ mchoose i) * mfact j * fact (δ - sum_list j) * P_coeff j * mpow z i))"
proof -
  define m where "m = Poly_Mapping.single (0::nat) p"
  define c where "c = (λi j. 
    (δ mchoose i) * mfact j * fact (δ - sum_list j) * mpow z i * P_coeff j)"

  { fix i j
    have "X^(R_exponent i j) = monom (Poly_Mapping.single 0 (R_exponent i j)) 1"
      unfolding X_def
      by (metis Var.abs_eq Var⇩0_def monom.abs_eq monom_pow nat_mult_1 power_one)
    hence "of_int (c i j) * X^(R_exponent i j) = monom (Poly_Mapping.single 0 (R_exponent i j)) (c i j)"
      unfolding of_int_Const using cst_poly_times_monom_one by (metis Const.abs_eq)
    hence "coeff (of_int (c i j) * X^(R_exponent i j)) m =
      coeff (monom (Poly_Mapping.single 0 (R_exponent i j)) (c i j)) m"
      by simp
    also have "... = (c i j when m = Poly_Mapping.single 0 (R_exponent i j))"
      using More_MPoly_Type.coeff_monom by blast
    also have "... = (c i j when R_exponent i j = p)"
      unfolding m_def by (smt (verit, best) lookup_single_eq)
    finally have "coeff (of_int (c i j) * X^(R_exponent i j)) m = 
      (c i j when R_exponent i j = p)" . }
  note coeff_interior = this

  have 0: "(∑j∈δ_tuples. (c i j when R_exponent i j = p)) =
     (∑j∈δ_tuples ∩ {j. R_exponent i j = p}. c i j)" for i
     using δ_tuples_finite
     by (smt (verit, ccfv_SIG) mem_Collect_eq sum.cong sum.inter_restrict when_def)

   have "e p = coeff (∑i∈δ_tuples. (∑j∈δ_tuples. of_int (c i j) * X^(R_exponent i j))) m"
    unfolding e_def m_def c_def using R_expansion by simp
  also have "... = (∑i∈δ_tuples. (∑j∈δ_tuples. coeff (of_int (c i j) * X^(R_exponent i j)) m))"
    using coeff_sum δ_tuples_finite by (smt (verit, best) sum.cong)
  also have "... = (∑i∈δ_tuples. (∑j∈δ_tuples. (c i j when R_exponent i j = p)))"
    using coeff_interior by simp
  also have "... = (∑i∈δ_tuples. (∑j∈δ_tuples ∩ {j. R_exponent i j = p}. c i j))"
    using 0 by simp
  finally show ?thesis unfolding c_def
    by (smt (verit, ccfv_SIG) ab_semigroup_mult_class.mult_ac(1) 
        mult.commute of_nat_mult sum.cong)  
qed

text ‹This is a key step of the proof.›
lemma e_n_ν1_expression: "e (n (ν+1)) = fact δ * insertion z_assign P"
proof -
  have simp_indices: "i∈δ_tuples ⟹ δ_tuples ∩ {j. R_exponent i j = n (ν+1)} = {i}" 
    (is "_ ⟹ ?S i = {i}") for i
  proof -
    assume i_def: "i∈δ_tuples"
    have 0: "i ∈ ?S i"
      unfolding R_exponent_def D_exponent_def using n_νp1_ge_sum i_def by simp
    have 1: "j1 ∈ ?S i ⟹ j2 ∈ ?S i ⟹ j1 = j2" for j1 j2
      unfolding R_exponent_def using D_exponent_inj
      by (simp add: inj_on_def)   
    
    have "{i} ⊆ ?S i" using 0 by auto
    moreover have "card (?S i) ≤ 1" using 1 by (simp add: card_le_Suc0_iff_eq)
    ultimately show ?thesis
      by (metis One_nat_def δ_tuples_finite card.empty card.insert
          card_seteq empty_iff finite.emptyI finite_Int)
  qed

  have simp_coeff: "i∈δ_tuples ⟹ (δ mchoose i) * mfact i * fact (δ - sum_list i) = fact δ" for i
    unfolding δ_tuples_def multinomial_def multinomial'_def using mchoose_dvd by fastforce
   
  have "e (n (ν+1)) = (∑i∈δ_tuples. (∑j∈δ_tuples ∩ {j. R_exponent i j = n (ν+1)}.
    (δ mchoose i) * mfact j * fact (δ - sum_list j) * P_coeff j * mpow z i))"
    by (simp add: e_expression)
  also have "... = (∑i∈δ_tuples.
    (δ mchoose i) * mfact i * fact (δ - sum_list i) * P_coeff i * mpow z i)"
    using simp_indices by auto
  also have "... = (∑i∈δ_tuples. fact δ * P_coeff i * mpow z i)"
    using simp_coeff by auto
  also have "... = fact δ * (∑i∈δ_tuples. P_coeff i * mpow z i)"
    using sum_distrib_left
    by (smt (verit) ab_semigroup_mult_class.mult_ac(1) sum.cong)
  also have "... = fact δ * insertion z_assign P"
    using P_z_insertion by simp
  finally show ?thesis .
qed

lemma abs_int[simp]: "abs (int x) = int x" 
  using abs_of_nat by auto

text ‹This is a key step of the proof.›
lemma e_upper_bound:
  "abs (e p) ≤ fact δ * L * (1 + sum_list z)^δ"
proof -
  { 
    fix i assume "i∈δ_tuples"
    define S_i where "S_i = δ_tuples ∩ {j. R_exponent i j = p}"

    have "finite S_i" unfolding S_i_def using δ_tuples_finite by simp
    
    { fix j1 j2 assume "j1 ∈ S_i" and "j2 ∈ S_i" 
      hence "D_exponent j1 = D_exponent j2" 
        unfolding S_i_def R_exponent_def by auto
      hence "j1 = j2" 
        using `j1 ∈ S_i` `j2 ∈ S_i` D_exponent_inj unfolding S_i_def
        by (meson IntD1 inj_on_contraD) }
    hence "card S_i ≤ 1" by (simp add: `finite S_i` card_le_Suc0_iff_eq)
 
    have 0: "(∑j∈S_i. mfact j * fact (δ - sum_list j) * abs (P_coeff j)) ≤ 
      fact δ * L * card S_i"
    proof -
      have "j∈S_i ⟹ mfact j * fact (δ - sum_list j) ≤ fact δ" for j
        unfolding S_i_def δ_tuples_def using mchoose_le by blast
      hence "j∈S_i ⟹ mfact j * fact (δ - sum_list j) * abs (P_coeff j) ≤ fact δ * L" for j
        using L_lower_bound_specialize
        by (metis abs_ge_zero mult_mono' of_nat_0_le_iff of_nat_fact zle_int)
      thus ?thesis by (simp add: mult.commute sum_bounded_above)
    qed

    have "abs (∑j∈S_i. (δ mchoose i) * mfact j * fact (δ - sum_list j) * P_coeff j * mpow z i)
      ≤ (∑j∈S_i. abs ((δ mchoose i) * mfact j * fact (δ - sum_list j) * P_coeff j * mpow z i))"
      using sum_abs by simp
    also have "... = (∑j∈S_i. (δ mchoose i) * 
      mfact j * fact (δ - sum_list j) * abs (P_coeff j) * mpow z i)"
      using abs_mult abs_int by (metis (no_types, opaque_lifting))
    also have "... = (∑j∈S_i. int (δ mchoose i) * mpow z i * 
      (mfact j * fact (δ - sum_list j) * abs (P_coeff j)))"
      by (simp add: algebra_simps)
    also have "... = int (δ mchoose i) * mpow z i *
      (∑j∈S_i. mfact j * fact (δ - sum_list j) * abs (P_coeff j))"
      by (simp only: sum_distrib_left) 
    also have "... ≤ int (δ mchoose i) * mpow z i * (fact δ * L * card S_i)"
      using 0 by (simp add: mult_left_mono)
    also have "... ≤ fact δ * L * int (δ mchoose i) * mpow z i"
      using `card S_i ≤ 1` L_pos order_le_less by fastforce
    finally have "abs (∑j∈S_i. (δ mchoose i) * mfact j * fact (δ - sum_list j) *
      P_coeff j * mpow z i) ≤ fact δ * L * int (δ mchoose i) * mpow z i" .
  } note bound_coeff = this
    
  have "abs (e p) ≤ (∑i∈δ_tuples. abs (∑j∈δ_tuples ∩ {j. R_exponent i j = p}. 
    (δ mchoose i) * mfact j * fact (δ - sum_list j) * P_coeff j * mpow z i))"
    using sum_abs e_expression by simp
  also have "... ≤ (∑i∈δ_tuples. fact δ * L * (int (δ mchoose i) * mpow z i))"
    using bound_coeff
    by (simp add: ab_semigroup_mult_class.mult_ac(1) sum_mono)
  also have "... = fact δ * L * (∑i∈δ_tuples. int (δ mchoose i) * mpow z i)" 
    by (simp only: sum_distrib_left)
  also have "... = fact δ * L * int (∑i∈δ_tuples. (δ mchoose i) * mpow z i)"
    using int_sum by simp
  also have "... = fact δ * L * int ((1 + sum_list z)^δ)"
    unfolding δ_tuples_def
    by (simp only: multinomial_ring_alt len_z of_nat_id)
   finally show ?thesis by simp
qed

lemma e_b_bound: shows "0 < e j + b" and "e j + b < ℬ"
proof -
  have 0: "abs (e j) < b"
  proof -
    have "2 * abs (e j) ≤ 2 * fact δ * L * (1 + sum_list z)^δ"
      using e_upper_bound by (simp add: algebra_simps)
    also have "... = int ( 2 * fact δ * (nat L) * (1 + sum_list z)^δ)" 
      using int_ops L_pos by auto
    also have "... < int ℬ" using ℬ_lower_bound
      by presburger
    finally show ?thesis using b_def_reverse by auto
  qed

  have "e j < b" using 0 by linarith
  thus "e j + b < ℬ" using b_def_reverse by linarith
  
  have "- e j < b" using 0 by linarith
  thus "0 < e j + b" by linarith
qed 

text ‹This is a key step of the proof.›
lemma K_expression: "K = (∑i≤(2*δ+1) * n ν. (e i + int b) * ℬ^i)"
proof -
  have 0: "insertion ℬ_assign R = (∑i≤(2*δ+1) * n ν. (e i) * ℬ^i)"
  proof -
    have "insertion ℬ_assign R = (∑i≤(2*δ+1) * n ν. (e i) * (insertion ℬ_assign X)^i)"
      by (simp add: R_sum_e)
    also have "... = (∑i≤(2*δ+1) * n ν. (e i) * ℬ^i)"
      unfolding X_def ℬ_assign_def by simp
    finally show ?thesis .  
  qed

  have "K = insertion ℬ_assign R + S" 
    by (simp add: K_def)
  also have "... = (∑i≤(2*δ+1) * n ν. e i * ℬ^i) + (∑i≤(2*δ+1) * n ν. b * ℬ^i)"
    by (simp add: S_def 0)
  also have "... = (∑i≤(2*δ+1) * n ν. (e i + int b) * ℬ^i)"
    by (simp add: sum.distrib algebra_simps)
  finally show ?thesis .
qed

lemma δ_n_positive: "0 < (2*δ+1) * n ν"
  using n_ge_1
  by (metis add_gr_0 mult_pos_pos not_gr0 not_one_le_zero zero_less_one)

lemma K_lower_bound: "K > int ℬ^((2*δ+1) * n ν)"
proof -
  from δ_n_positive have "(∑i=0..<(2*δ+1) * n ν. ℬ^i) = 1 + (∑i=1..<(2*δ+1) * n ν. ℬ^i)" 
    using sum.atLeast_Suc_lessThan power_0 by (metis One_nat_def)
  hence 0: "(∑i<(2*δ+1) * n ν. ℬ^i) > 0"
    by (metis Suc_eq_plus1 add.commute atLeast0LessThan zero_less_Suc)
   
  have "j ∈ {..(2*δ+1) * n ν} ⟹ 1 ≤ e j + b" for j
    using int_one_le_iff_zero_less e_b_bound by blast  
  hence 1: "j ∈ {..(2*δ+1) * n ν} ⟹ ℬ^j ≤ (e j + b) * ℬ^j" for j
    using ℬ_ge_1 by simp

  have "int ℬ^((2*δ+1) * n ν) < int (∑i<(2*δ+1) * n ν. ℬ^i) + ℬ^((2*δ+1) * n ν)" 
    using 0 by (simp add: nat_int_comparison(2))
  also have "... = (∑i<(2*δ+1) * n ν. int ℬ^i) + ℬ^((2*δ+1) * n ν)"
    using Int.int_sum by simp
  also have "... = (∑i≤(2*δ+1) * n ν. int ℬ^i)"
    by (metis lessThan_Suc_atMost of_nat_eq_of_nat_power_cancel_iff sum.lessThan_Suc)
  also have "... ≤ K" unfolding K_expression
    using sum_mono 1 by (metis (no_types, lifting) of_nat_power)
  finally show ?thesis .
qed

corollary K_gt_0: "K > 0"
  using ℬ_gt_2 δ_n_positive K_lower_bound
  by (smt (verit) of_nat_zero_less_power_iff power_eq_0_iff zero_less_power2)

end

end