Theory Lemma_1_8_Defs

theory Lemma_1_8_Defs
  imports Main "../MPoly_Utils/More_More_MPoly_Type" Bit_Counting
          Utils Multinomial
begin

subsection ‹Expressing polynomial solutions in terms of carry counting›

subsubsection ‹Preliminary definitions›

locale Lemma_1_8_Defs =
  fixes P :: "int mpoly" 
    and ℬ :: nat
    and L :: int
    and z :: "nat list"
begin 
  
abbreviation σ where "σ ≡ count_bits"
abbreviation τ where "τ ≡ count_carries"

definition δ::nat where "δ = total_degree P"
definition ν::nat where "ν = max_vars P"
definition b::nat where "b ≡ ℬ div 2"
definition n::"nat ⇒ nat" where "n j = (δ+1)^j"

definition X::"int mpoly" where "X = Var 0"

text ‹The are assignments of variables, used to evaluate (multivariable) polynomials.›
definition z_assign where "z_assign = ((!⇩0) (map int z))"
definition ℬ_assign where "ℬ_assign = (λi. (int ℬ) when i = 0)"

text ‹We will often use this set as indices of sums.›
definition δ_tuples :: "(nat list) set" where
  "δ_tuples ≡ {i. length i = ν + 1 ∧ sum_list i ≤ δ}"

(* 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))"

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))"
text ‹This is really a univariate polynomial›
definition D::"int mpoly" where
  "D ≡ ∑i∈δ_tuples. of_int (D_precoeff i * P_coeff i) * X^(D_exponent i)"

text ‹This is really a univariate polynomial›
definition c::"int mpoly" where 
  "c ≡ (∑i≤ν. of_nat (z!i) * X^(n i))"

text ‹Definition of the constant K›
definition R::"int mpoly" where "R ≡ (1+c)^δ * D"
definition S::"nat" where "S ≡ (∑i≤(2*δ+1) * n ν. b * ℬ^i)"
definition K::int where "K ≡ insertion ℬ_assign R + int S"

text ‹Some more notation used in the proofs :
  (e j) is the coefficient of $X^j$ in R›
definition e::"nat ⇒ int" 
  where "e j = coeff R (Poly_Mapping.single 0 j)"

end

end