Theory Coding_Theorem_Definitions

theory Coding_Theorem_Definitions
  imports "../Coding/Multinomial" "../Coding/Bit_Counting" "Digit_Expansions.Bits_Digits"
          "../MPoly_Utils/More_More_MPoly_Type" "../MPoly_Utils/Poly_Extract"
          "../MPoly_Utils/Total_Degree_Env" "../MPoly_Utils/Poly_Degree"
begin

section ‹The Coding Theorem›

lemma series_bound:
  fixes b :: int
  assumes "b ≥ 2"
  shows "(∀k≤q. f k < b) ⟹ (∑k = 0..q. f k * b ^ k) < b^(Suc q)"
proof (induct q)
  case 0
  then show ?case
    by simp
next
  case (Suc q)
  hence f_le_bound: "∀k≤Suc q. f k ≤ b-1" using assms
    by auto
  
  from Suc show ?case
  proof -
    assume "∀k≤q. f k < b ⟹ (∑k = 0..q. f k * b ^ k) < b ^ Suc q"
    with Suc have asm: "(∑k = 0..q. f k * b ^ k) < b ^ Suc q"
      by auto

    have "(∑k = 0..q. f k * b ^ k) + f (Suc q) * (b * b ^ q)
          ≤ (∑k = 0..q. f k * b ^ k) + (b-1) * (b * b ^ q)"
      using f_le_bound assms by auto
    also have "... < b^(Suc q) + (b-1) * (b * b ^ q)"
      using asm by auto
    also have "... ≤ b * b * b^q"
      by (simp add: left_diff_distrib)
    finally show ?thesis
      using asm by auto
  qed 
qed

subsection ‹Definition of polynomials required in the Coding Theorem›

locale coding_variables =
  fixes P :: "int mpoly"
    and a :: int
    and f :: int
begin

text ‹Notation for working with P›

definition δ :: nat where "δ ≡ total_degree P"
definition ν :: nat where "ν ≡ max_vars P"

(* Beware : we can't use Abs_poly_mapping ((!) i) *)
definition P_coeff :: "nat list ⇒ int" where
  "P_coeff i ≡ coeff P (Abs_poly_mapping ((!⇩0) i))"

text ‹Notation used in the proofs›
definition n :: "nat ⇒ nat" where "n i ≡ (δ+1)^i"
definition δ_tuples :: "(nat list) set" where
  "δ_tuples ≡ {i. length i = ν + 1 ∧ sum_list i ≤ δ}"

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
  
abbreviation σ where "σ ≡ count_bits"
abbreviation τ where "τ ≡ count_carries"

text ‹The variables of Definition 2.2›

text ‹This is not the same ‹ℒ› as in Lemma 1.8›
definition ℒ :: nat where "ℒ ≡ nat (∑i∈δ_tuples. abs (P_coeff i))"
text ‹We have to use Inf instead of Min to define r because the set is infinite›
definition r :: nat where "r ≡ Inf {y. 4^y > 2 * fact δ * ℒ * (ν + 3)^δ}"
definition β :: nat where "β ≡ 4^r"
definition γ :: nat where "γ ≡ β^(n ν)"
definition α :: nat where "α ≡ δ * n ν + 1"

lemma α_gt_0: "α > 0" unfolding α_def by auto
lemma γ_gt_0: "γ > 0" unfolding γ_def β_def n_def by auto

definition b :: "int" where 
  "b ≡ 1 + 3*(2*a + 1) * f"
definition ℬ :: "int" where
  "ℬ ≡ (of_nat β) * b^δ"
definition N0 :: "int" where 
  "N0 ≡ ℬ^((δ+1)^ν + 1)"
definition N1 :: "int" where 
  "N1 ≡ 4 * ℬ^((2*δ+1) * (δ+1)^ν + 1)"
definition N :: "int" where 
  "N ≡ N0 * N1"
definition c :: "int ⇒ int" where 
  "c g ≡ 1 + a*ℬ + g"

poly_extract b
poly_degree b_poly

poly_extract ℬ
poly_degree ℬ_poly

poly_extract N0
poly_extract N1
poly_extract N
poly_extract c
poly_degree c_poly


text ‹The M polynomial.›
definition m :: "nat ⇒ int" where 
  "m j ≡ (if j ∈ n ` {1..ν} then ℬ - b else ℬ - 1)"
definition M :: "int" where 
  "M ≡ (∑j=0..n ν. m j * ℬ^j)"

definition m_poly :: "nat ⇒ int mpoly" where
  "m_poly j = (if j ∈ n ` {1..ν} then ℬ_poly - b_poly else ℬ_poly - 1)"

definition M_poly :: "int mpoly" where 
  "M_poly ≡ (∑ j=0..n ν. m_poly j * ℬ_poly ^ j)"

lemma m_correct: "insertion fn (m_poly j) = coding_variables.m P (fn 0) (fn (Suc 0)) j"
  unfolding coding_variables.m_def coding_variables.m_poly_def
  by (cases "j ∈ n ` {1..ν}", simp_all add: ℬ_correct b_correct) 

lemma m_poly_degree_env_correct: "total_degree_env ctxt (m_poly j)
   ≤ max (total_degree_env ctxt ℬ_poly) (total_degree_env ctxt b_poly)"
  unfolding m_poly_def by (auto simp: le_trans[OF total_degree_env_diff])

lemma M_correct:
  "insertion fn (coding_variables.M_poly P) = coding_variables.M P (fn 0) (fn 1)"
  unfolding M_poly_def coding_variables.M_def apply simp
  unfolding ℬ_correct m_correct by auto

(* This lemma relies on poly_degree having been called on ℬ_poly and b_poly
    within the locale where they are defined *)
lemma m_poly_degree_correct: 
  shows "δ > 0 ⟹ total_degree (m_poly j) ≤ 2*δ"
  unfolding total_degree_env_id[symmetric]
  apply (rule le_trans[OF coding_variables.m_poly_degree_env_correct])
  apply (unfold total_degree_env_id, simp, intro conjI)
  using coding_variables.ℬ_poly_degree_correct[unfolded coding_variables.ℬ_poly_degree_def]
  using coding_variables.b_poly_degree_correct[unfolded coding_variables.b_poly_degree_def]
  by (auto simp add: mult_2)

lemma M_poly_degree_correct:
  assumes asm: "δ > 0"
  shows "total_degree M_poly ≤ (1+(δ+1)^ν) * 2*δ"
proof -
  have fin0: "finite {0..(δ + 1)^ν}" by simp
  {
    fix a
    assume "a ∈ {0..Suc δ^ν}"
    hence a: "a ≤ (δ+1)^ν" by auto
    have "total_degree (coding_variables.m_poly P a * ℬ_poly ^ a)
            ≤ total_degree (coding_variables.m_poly P a) + a * total_degree ℬ_poly"
      apply (rule le_trans[OF total_degree_mult add_mono])
      by (auto simp: le_trans total_degree_mult total_degree_pow)
    also have "... ≤ 2*δ + (δ+1)^ν * (2*δ)"
      apply (rule add_mono, simp add: m_poly_degree_correct[OF asm])
      apply (rule mult_mono, simp_all add: a[unfolded Suc_eq_plus1[symmetric]])
      using coding_variables.ℬ_poly_degree_correct[unfolded coding_variables.ℬ_poly_degree_def]
      by (auto simp add: mult_2)
    finally have "total_degree (coding_variables.m_poly P a * ℬ_poly ^ a)
                  ≤ 2*δ + (δ+1)^ν * (2*δ)".
  } note h0 = this

  show ?thesis
    unfolding coding_variables.M_poly_def coding_variables.n_def
    apply (rule le_trans[OF total_degree_sum[OF fin0]], simp)
    using h0 by (auto simp: mult.assoc)
qed 


definition D_exponent :: "nat list ⇒ nat" where
  "D_exponent i ≡ n (ν+1) - (∑s≤ν. i!s * n s)"
definition D_precoeff :: "nat list ⇒ int" where
  "D_precoeff i ≡ int (mfact i * fact (δ - sum_list i))"
definition D :: "int" where
  "D ≡ ∑i∈δ_tuples. of_int (D_precoeff i * P_coeff i) * ℬ^(D_exponent i)"

definition D_poly :: "int mpoly" where 
  "D_poly ≡ ∑i∈δ_tuples. Const (D_precoeff i * P_coeff i) * ℬ_poly ^ (D_exponent i)"

lemma D_correct: 
  "insertion fn (coding_variables.D_poly P) = coding_variables.D P (fn 0) (fn 1)"
  unfolding D_poly_def coding_variables.D_def apply simp
  using insertion_sum[OF δ_tuples_finite, of fn] apply simp
  unfolding ℬ_correct by auto

lemma D_poly_degree_env_correct:
  shows "total_degree_env fv D_poly ≤ n (ν+1) * total_degree_env fv ℬ_poly"
proof -
  {
    fix a
    assume "a ∈ δ_tuples"
    hence d: "D_exponent a ≤ n (ν+1)"
      unfolding D_exponent_def by simp
    have "total_degree_env fv (Const (D_precoeff a * P_coeff a) * ℬ_poly ^ D_exponent a)
            ≤ D_exponent a * total_degree_env fv (ℬ_poly)"
      by (metis add_0 le_trans total_degree_env_Const total_degree_env_mult total_degree_env_pow)
    with d have "total_degree_env fv (Const (D_precoeff a * P_coeff a) * ℬ_poly ^ D_exponent a)
            ≤ n (ν+1) * total_degree_env fv (ℬ_poly)"
      by (simp add: le_trans)
  } note h0 = this

  show ?thesis
    unfolding D_poly_def
    apply (rule le_trans[OF total_degree_env_sum[OF δ_tuples_finite]])
    using h0 by simp
qed

lemma D_poly_degree_correct: "total_degree (coding_variables.D_poly P) ≤ (δ+1)^(ν+1) * (2*δ)"
  unfolding total_degree_env_id[symmetric]
  apply (rule le_trans[OF D_poly_degree_env_correct], unfold total_degree_env_id n_def)
  apply (rule mult_le_mono)
  using ℬ_poly_degree_correct[unfolded ℬ_poly_degree_def] by auto


(* The K polynomial. I would have preferred to write something like "ℬ / 2"
  instead of "of_nat (β div 2) * b^δ", but there is nothing quite like this: 
  "sdiv 2 ℬ" is not what we want since it divides each coefficient. *)
definition K :: "int ⇒ int" where 
  "K g ≡ (c g)^δ * D + (∑i=0..(2*δ+1)*n ν. of_nat (β div 2) * b^δ * ℬ^i)"

definition K_poly :: "int mpoly" where
  "K_poly ≡ c_poly^δ * D_poly + (∑i=0..(2*δ+1)*n ν. of_nat (β div 2) * b_poly^δ * ℬ_poly^i)"

lemma K_correct: 
  "insertion fn (coding_variables.K_poly P) = coding_variables.K P (fn 0) (fn 1) (fn 2)"
  unfolding K_poly_def coding_variables.K_def apply simp
  unfolding c_correct D_correct b_correct ℬ_correct by auto

lemma K_poly_degree_correct:
  shows "total_degree (coding_variables.K_poly P)
  ≤ max (δ*(1+2*δ) + (δ+1)^(ν+1) * 2*δ) ((1 + (2*δ+1)*(δ+1)^ν) * 2*δ)"
proof -
  have fin0: "finite {0..(2 * δ + 1) * n ν}" by simp

  {
    fix a
    assume "a∈{0..Suc δ ^ ν + 2 * δ * Suc δ ^ ν}"
    hence a: "a ≤ Suc δ ^ ν + 2 * δ * Suc δ ^ ν" by simp
    have "total_degree (of_nat (β div 2) * b_poly ^ δ * ℬ_poly ^ a)
       ≤ 2*δ + (Suc δ ^ ν + 2 * (δ * Suc δ ^ ν)) * (2*δ)"
      apply (rule le_trans[OF total_degree_mult add_mono])
      subgoal
        apply (rule le_trans[OF total_degree_mult], simp add: of_nat_Const)
        apply (rule le_trans[OF total_degree_pow])
        using b_poly_degree_correct[unfolded b_poly_degree_def] 
        by simp
      subgoal
        apply (rule le_trans[OF total_degree_pow], rule mult_le_mono)
        using ℬ_poly_degree_correct[unfolded ℬ_poly_degree_def]
        using a by simp_all
      done
  } note h0 = this

  show ?thesis
    unfolding K_poly_def
    apply (rule le_trans[OF total_degree_add max.mono]
        | rule le_trans[OF total_degree_diff max.mono]
        | rule le_trans[OF total_degree_mult add_mono]
        | rule le_trans[OF total_degree_pow mult_le_mono2])+
    subgoal using c_poly_degree_correct[unfolded c_poly_degree_def] by simp
    subgoal unfolding mult.assoc by (rule D_poly_degree_correct)
    apply (rule le_trans[OF total_degree_sum[OF fin0]])
    using h0 by (simp add: n_def algebra_simps) 
qed


definition T where "T ≡ M + (ℬ-2) * ℬ^((δ+1)^(ν+1)) * N0"
definition S :: "int ⇒ int" where "S g ≡ g + 2 * K g * N0"
definition R :: "int ⇒ int" where "R g ≡ (S g + T + 1)*N + T + 1"
definition X :: "int ⇒ int" where "X g ≡ (N-1) * R g"
definition Y :: "int" where "Y ≡ N^2"

poly_extract T
poly_extract S
poly_extract R
poly_extract X
poly_extract Y


text ‹These are the statements that make up theorem I.›
definition statement1_weak where 
  "statement1_weak y ≡ (y 0 = a) ∧ (∀i. 0 ≤ y i ∧ y i < b) ∧ insertion y P = 0"
definition statement1_strong where 
  "statement1_strong y ≡ statement1_weak y ∧ (∃i∈{1..ν}. y i ≠ 0)"
text ‹We evaluate Y in 0 because it doesn't depend on g.›
definition statement2_strong where 
  "statement2_strong g ≡ b ≤ g ∧ g < (int γ) * b^α ∧ Y dvd (2 * nat (X g) choose nat (X g))"
definition statement2_weak where 
  "statement2_weak g ≡ 0 ≤ g ∧ g < 2 * (int γ) * b^α ∧ Y dvd (2 * nat (X g) choose nat (X g))"

lemma δ_tuples_nonempty: "δ_tuples ≠ {}"
proof -
  define i where "i ≡ replicate (ν+1) (0::nat)"
  have "i ∈ δ_tuples"
    unfolding δ_tuples_def i_def
    by (smt (verit, best) in_set_replicate length_replicate less_eq_nat.simps(1) 
        mem_Collect_eq sum_list_eq_0_iff) 
  thus ?thesis by auto
qed

corollary x_series_bound:
  assumes "0 < δ"
  assumes "x ∈ δ_tuples"
  shows "(∑s≤ν. x ! s * Suc δ ^ s) ≤ (δ+1)^(ν+1)"
proof -
  from assms have "2 ≤ int (Suc δ)"
    by auto
  from assms have "length x = Suc ν"
    unfolding δ_tuples_def by simp
  have x_bound: "∀s≤ν. (x ! s) < Suc δ"
    using assms unfolding δ_tuples_def
    by simp (smt (verit) elem_le_sum_list le_imp_less_Suc order_trans)
  hence x_bound2: "∀k≤ν. int (x ! k) < int (Suc δ)"
    by auto
  show ?thesis
    using series_bound[of "Suc δ" ν "(!) x", OF ‹2 ≤ int (Suc δ)› x_bound2]
    apply (subst atMost_atLeast0, subst less_imp_le, simp_all)
    apply (subst nat_int_comparison(2))
    by auto (smt (verit, del_insts) of_nat_Suc of_nat_add of_nat_mult
                 of_nat_power times_nat.simps(2))
qed

lemma D_exponent_injective:
  assumes "0 < δ"
  shows "inj_on D_exponent δ_tuples"
proof -
  from assms have "1 < δ + 1"
    by auto

  {
    fix x y
    assume a1: "x ∈ δ_tuples" and a2: "y ∈ δ_tuples"
    hence l1: "length x = Suc ν" and l2: "length y = Suc ν"
      unfolding δ_tuples_def by auto
    from a1 a2 have l3: "∀s≤ν. x ! s < δ + 1" and l4: "∀s≤ν. y ! s < δ + 1" 
      unfolding δ_tuples_def using l1 l2 elem_le_sum_list
      by (metis (no_types, lifting) Suc_eq_plus1 le_imp_less_Suc mem_Collect_eq order_trans)+
    
    assume "(∑s≤ν. x ! s * (δ + 1) ^ s) = (∑s≤ν. y ! s * (δ + 1) ^ s)"
    hence "x = y"
      apply (subst (asm) digit_wise_gen_equiv[OF ‹1 < δ + 1›])
      apply (subst (asm) atMost_atLeast0)+
      apply (subst (asm) nth_digit_gen_power_series_general[OF ‹1 < δ + 1› l3])
      apply (subst (asm) nth_digit_gen_power_series_general[OF ‹1 < δ + 1› l4])
      using l1 l2 l3 l4 by (metis less_Suc_eq_le nth_equalityI)
  }

  then show ?thesis
    unfolding inj_on_def D_exponent_def n_def
    using x_series_bound[OF ‹0 < δ›]
  proof -
    { fix nns :: "nat list" and nnsa :: "nat list"
      have ff1: "⋀ns. ns ∉ δ_tuples ∨ (∑n≤ν. ns ! n * Suc δ ^ n) ≤ Suc δ ^ Suc ν"
        using ‹⋀x. x ∈ δ_tuples ⟹ (∑s≤ν. x ! s * Suc δ ^ s) ≤ (δ + 1) ^ (ν + 1)› by force
      have "∀n na. ∃nb. ¬ (na::nat) ≤ n ∨ na + nb = n"
        using le_Suc_ex by blast
      then obtain nn :: "nat ⇒ nat ⇒ nat" where
        ff2: "⋀n na. ¬ n ≤ na ∨ n + nn na n = na"
        by metis
      then have ff3: "⋀n na. ¬ n ≤ na ∨ na - nn na n = n"
        by (metis (no_types) add_diff_cancel_right')
      { assume "(∑n≤ν. nnsa ! n * Suc δ ^ n) ≤ Suc δ ^ Suc ν ∧ (∑n≤ν. nns ! n * Suc δ ^ n) ≠ (∑n≤ν. nnsa ! n * Suc δ ^ n)"
        then have "(∑n≤ν. nns ! n * Suc δ ^ n) ≤ Suc δ ^ Suc ν ⟶ (∑n≤ν. nns ! n * Suc δ ^ n) ≤ Suc δ ^ Suc ν ∧ Suc δ ^ Suc ν - nn (Suc δ ^ Suc ν) (∑n≤ν. nnsa ! n * Suc δ ^ n) ≠ (∑n≤ν. nns ! n * Suc δ ^ n)"
          using ff3 by (smt (z3))
        then have "(∑n≤ν. nnsa ! n * Suc δ ^ n) ≤ Suc δ ^ Suc ν ∧ (∑n≤ν. nns ! n * Suc δ ^ n) ≤ Suc δ ^ Suc ν ⟶ nns ∉ δ_tuples ∨ nnsa ∉ δ_tuples ∨ nns = nnsa ∨ (δ + 1) ^ (ν + 1) - (∑n≤ν. nns ! n * (δ + 1) ^ n) ≠ (δ + 1) ^ (ν + 1) - (∑n≤ν. nnsa ! n * (δ + 1) ^ n)"
          using ff2 by fastforce
        then have "(∑n≤ν. nnsa ! n * Suc δ ^ n) ≤ Suc δ ^ Suc ν ⟶ nns ∉ δ_tuples ∨ nnsa ∉ δ_tuples ∨ nns = nnsa ∨ (δ + 1) ^ (ν + 1) - (∑n≤ν. nns ! n * (δ + 1) ^ n) ≠ (δ + 1) ^ (ν + 1) - (∑n≤ν. nnsa ! n * (δ + 1) ^ n)"
          using ff1 by blast }
      then have "nns ∉ δ_tuples ∨ nnsa ∉ δ_tuples ∨ nns = nnsa ∨ (δ + 1) ^ (ν + 1) - (∑n≤ν. nns ! n * (δ + 1) ^ n) ≠ (δ + 1) ^ (ν + 1) - (∑n≤ν. nnsa ! n * (δ + 1) ^ n)"
        using ff1 by (metis (no_types) Suc_eq_plus1 ‹⋀y x. ⟦x ∈ δ_tuples; y ∈ δ_tuples; (∑s≤ν. x ! s * (δ + 1) ^ s) = (∑s≤ν. y ! s * (δ + 1) ^ s)⟧ ⟹ x = y›) }
    then show "∀ns∈δ_tuples. ∀nsa∈δ_tuples. (δ + 1) ^ (ν + 1) - (∑n≤ν. ns ! n * (δ + 1) ^ n) = (δ + 1) ^ (ν + 1) - (∑n≤ν. nsa ! n * (δ + 1) ^ n) ⟶ ns = nsa"
      by blast
  qed
qed

corollary D_exponent_injective': "0 < δ ⟹ inj_on D_exponent (δ_tuples - {x})"
  using D_exponent_injective by (rule inj_on_diff)

lemma D_precoeff_bound:
  assumes "0 < sum_list i" and "sum_list i ≤ δ"
  shows "¦D_precoeff i¦ ≤ fact δ"
proof -
  have "δ mchoose i ≥ 1"
    using assms unfolding multinomial_def multinomial'_def
    by simp (metis dvd_mult_div_cancel fact_ge_Suc_0_nat mchoose_dvd mult.commute one_le_mult_iff)
  thus ?thesis
    using assms unfolding D_precoeff_def multinomial_def multinomial'_def
    by (metis abs_of_nat mchoose_le of_nat_fact of_nat_le_iff)
qed

text ‹We later assume that ‹δ > 0› i.e. P is not the zero polynomial›
lemma P_coeffs_not_all_zero:
  assumes "δ > 0"
  shows "∃i∈δ_tuples. P_coeff i ≠ 0"
proof -
  have "¬ (∀i∈δ_tuples. P_coeff i = 0)"
  proof
    assume coeffs_zero: "∀i∈δ_tuples. P_coeff i = 0"
    { fix m assume assm: "m ∈ keys (mapping_of P)"
      then obtain i where "m = Abs_poly_mapping ((!⇩0) i)" and "i∈δ_tuples"
        using mpoly_keys_subset unfolding δ_tuples_def δ_def ν_def by auto
      hence "P_coeff i ≠ 0" 
        using assm P_coeff_def by (simp add: coeff_keys)
      hence "False" 
        using coeffs_zero ‹i∈δ_tuples› by auto }
    hence "keys (mapping_of P) = {}"
      by blast
    hence "P = 0"
      by (metis keys_eq_empty mapping_of_inverse zero_mpoly.abs_eq)
    thus "False"
       using ‹δ > 0› δ_def by simp
  qed
  thus ?thesis by auto
qed

lemma ℒ_pos:
  assumes "δ > 0"
  shows "ℒ > 0"
proof -
  have "¬ ℒ = 0"
  proof 
    assume "ℒ = 0"
    hence "(∑i∈δ_tuples. abs (P_coeff i)) = 0"
      unfolding ℒ_def by (metis int_ops(1) nat_0_le sum_abs_ge_zero)
    hence "i∈δ_tuples ⟹ abs (P_coeff i) = 0" for i
      using sum_nonneg_eq_0_iff[OF δ_tuples_finite] by (metis (full_types) abs_ge_zero)
    hence "i∈δ_tuples ⟹ P_coeff i = 0" for i
      by auto
    thus "False" 
      using P_coeffs_not_all_zero[OF ‹δ > 0›] by auto 
  qed
  thus ?thesis by auto
qed

lemma ℒ_ge_P_coeff: "i∈δ_tuples ⟹ abs (P_coeff i) ≤ int ℒ" for i
proof -
  assume "i∈δ_tuples"
  hence "abs (P_coeff i) ≤ (∑i∈δ_tuples. abs (P_coeff i))"
    by (meson δ_tuples_finite abs_ge_zero sum_nonneg_leq_bound)
  also have "... = int ℒ"
    unfolding ℒ_def by auto
  finally show ?thesis .
qed

lemma ℒ_ge_max_coeff:
  assumes "δ > 0"
  shows "max_coeff P ≤ int ℒ"
proof -
  have "lookup (mapping_of P) i ∈ (P_coeff ` δ_tuples) ∪ {0}" for i
  proof (cases "lookup (mapping_of P) i = 0")
    case True thus ?thesis by simp
  next
    case False
    hence "i∈keys (mapping_of P)" 
      by (simp add: in_keys_iff)
    thus ?thesis 
      using mpoly_keys_subset unfolding P_coeff_def MPoly_Type.coeff_def δ_tuples_def δ_def ν_def 
      by auto
  qed
  hence 1: "coeffs P ⊆ P_coeff ` δ_tuples" 
    unfolding coeffs_def range_def by auto

  have 2: "coeffs P ≠ {}"
  proof 
    assume "coeffs P = {}"
    hence "δ = 0"
      unfolding δ_def using coeffs_empty_iff[of "P"] by simp
    thus "False"
      using ‹δ > 0› by auto
  qed

  from ℒ_ge_P_coeff 1 2 show ?thesis
    unfolding max_coeff_def by auto
qed

lemma β_lower_bound: "β > 2 * fact δ * ℒ * (ν+3)^δ"
proof -
  define S where "S ≡ {y. 4^y > 2 * fact δ * ℒ * (ν + 3)^δ}"
 
  have "2 * fact δ * ℒ * (ν + 3)^δ ∈ S"
    unfolding S_def using power_gt_expt by auto
  hence "S ≠ {}"
    by auto
  hence "Inf S ∈ S"
    by (simp add: Inf_nat_def1)
  hence "r ∈ S"
    using r_def S_def by simp
  thus ?thesis 
    unfolding S_def β_def by simp
qed

corollary r_pos:
  assumes "δ > 0"
  shows "r > 0"
  using β_lower_bound β_def ℒ_pos[OF ‹δ > 0›] zero_less_iff_neq_zero by fastforce


lemma marcos_state: 
  fixes i 
  shows "total_degree_env 
  (λm. total_degree_env (λ_. Suc 0) ([Var 0, Var 1, Var 2] !⇩0 m)) 
  ([Var 0, Var 1, Var 2] !⇩0 i) ≤ 1"
proof -
  have 1: "[Var 0, Var 1, Var 2] !⇩0 m = map Var [0, 1, 2] !⇩0 m" for m 
    apply auto done

  have aux: "(λm. total_degree_env (λ_. Suc 0) (map Var [0, 1, 2] !⇩0 m)) = 
        (λm. if m < length [0, 1, 2] then 1 else 0)" 
    by (metis One_nat_def length_Cons list.size(3) total_degree_env_Var_list)

  show ?thesis
    apply (rule le_trans[of _ "total_degree_env (λm. if m < length [0, 1, 2] then 1 else 0) ([Var 0, Var 1, Var 2] !⇩0 i)"])
    subgoal 
      apply simp
      using aux
      by (smt (z3) "1" Suc_1 Suc_eq_plus1 dual_order.refl le_less_Suc_eq less_2_cases 
          linorder_not_less list.size(3,4) nth0_0
          nth0_Cons_0 nth0_Cons_Suc total_degree_env_Var total_degree_env_zero)
    subgoal 
      by (smt (verit, del_insts) One_nat_def Suc_leI Suc_le_mono add.right_neutral add_Suc_right antisym_conv1
          bot_nat_0.not_eq_extremum list.size(3,4) nth0_0 nth0_Cons_0 nth0_Cons_Suc total_degree_env_Var
          total_degree_env_zero)
    done
qed

end

end