Theory Zeta5_Inner_Range
theory Zeta5_Inner_Range
imports Zeta5_Small_Primes Zeta5_Pole_Distribution Polynomial_Taylor_Shift Unimodular_Determinants
begin
section ‹The inner range: Proposition 4.1›
text ‹Section 4.1 of the paper: the inner basis,
extraction of powers of ‹p› from ‹g(c + p z)›, the
entry bounds (4.2) and (4.3), and the unimodularity of the inner Gram matrix (Proposition 4.1,
@{text DeltaK_vpGge_inner}). Lean theories @{text Section4}, @{text InnerBasis},
@{text InnerEntries},
@{text InnerFinal}.›
subsection ‹Section 4.1 The inner range›
text ‹(4.1): the inner range.›
definition InnerHyp :: "nat ⇒ nat ⇒ nat ⇒ bool" where
"InnerHyp K M p ⟷ 40 ≤ M ∧ 40 dvd K ∧ 0 < K ∧
200 * M ^ 2 ≤ K ∧ K < p * M ∧ 3 * p ≤ K"
text ‹Under (4.1): @{text "p > 200M"} and @{text "p^2 > 5K"}.›
lemma innerHyp_bounds:
assumes "InnerHyp K M p"
shows "200 * M < p ∧ 5 * K < p ^ 2"
proof -
have hM: "40 ≤ M" and hK: "200 * M ^ 2 ≤ K" and hp: "K < p * M"
using assms by (auto simp: InnerHyp_def)
have "200 * M * M < p * M" using le_less_trans[OF hK hp]
by (simp only: power2_eq_square mult.assoc)
hence h1: "200 * M < p" using hM by simp
have "5 * K < p * (5 * M)" using hp by simp
also have "… ≤ p * p" using h1 by (auto intro: mult_le_mono2)
finally show ?thesis using h1 by (simp add: power2_eq_square)
qed
text ‹(4.4): @{text "0 ≤ E < m"} and @{text "mT + E = h - L_0 + 3(N - m_N)"}.›
lemma TE_spec:
assumes "prime p" "InnerHyp K M p"
shows "0 ≤ Ein K M p ∧ Ein K M p < int (mHalf p) ∧
int (mHalf p) * Tin K M p + Ein K M p = rhs44 K M p"
proof -
have "8000 < p" using innerHyp_bounds[OF assms(2)] assms(2) by (auto simp: InnerHyp_def)
hence "0 < mHalf p" by (simp add: mHalf_def)
hence "0 < int (mHalf p)" by simp
thus ?thesis unfolding Ein_def Tin_def using pos_mod_sign pos_mod_bound mult_div_mod_eq
by presburger
qed
text ‹(4.8): @{text "γ_p^in"} is an integer (twice a sum of half-integers).›
lemma two_wIn_Ints: "2 * wIn K M p a i ∈ (ℤ :: rat set)"
proof (cases "a = 0")
case True
define S where "S = insert (2 * of_nat i + 6 * of_nat (Nof K div p) - of_nat (K div p) + 1 /
2 :: rat)
((λc. of_int (Zin K M p c) - (of_nat (ell p K c) + 4) / 2) ` {1..mHalf p})"
have wS: "wIn K M p a i = Min S" using True by (simp add: wIn_def S_def)
have "Min S ∈ S" unfolding S_def by (rule Min_in) auto
moreover have "2 * y ∈ ℤ" if "y ∈ S" for y
proof -
from that consider "y = 2 * of_nat i + 6 * of_nat (Nof K div p) - of_nat (K div p) + 1 / 2"
| c where "y = of_int (Zin K M p c) - (of_nat (ell p K c) + 4) / 2"
unfolding S_def by auto
thus ?thesis
proof cases
case 1
have "2 * y = of_int (4 * int i + 12 * int (Nof K div p) - 2 * int (K div p) + 1)"
using 1 by (simp add: algebra_simps)
thus ?thesis by (metis Ints_of_int)
next
case (2 c)
have "2 * y = of_int (2 * Zin K M p c - int (ell p K c) - 4)"
using 2 by (simp add: field_simps)
thus ?thesis by (metis Ints_of_int)
qed
qed
ultimately show ?thesis using wS by simp
next
case False
have "2 * wIn K M p a i = of_int (2 * int i + 2 * bIn K p a - int (ell p K a) - 4)"
using False by (simp add: wIn_def field_simps)
thus ?thesis by (metis Ints_of_int)
qed
lemma gammaIn_isInt: "∃n::int. gammaIn K M p = of_int n"
proof -
have "gammaIn K M p ∈ ℤ"
unfolding gammaIn_def sum_distrib_left by (intro Ints_sum two_wIn_Ints)
thus ?thesis by (auto elim: Ints_cases)
qed
text ‹Section 4.1: the dimensions @{text "L_a"} are nonnegative and
@{text "L_0 + ∑_{a≥1} L_a = h"}.›
lemma card_cong_class_le:
assumes "0 < p" "A ⊆ {..N}" "⋀x y. x ∈ A ⟹
y ∈ A ⟹ x mod p = y mod p"
shows "card A ≤ N div p + 1"
proof -
have inj: "inj_on (λj. j div p) A"
proof (rule inj_onI)
fix x y assume xy: "x ∈ A" "y ∈ A" "x div p = y div p"
have "x = x div p * p + x mod p" by simp
also have "… = y div p * p + y mod p" using xy assms(3)[OF xy(1,2)] by simp
also have "… = y" by simp
finally show "x = y" .
qed
have "(λj. j div p) ` A ⊆ {..N div p}" using assms(2)
by (auto intro: div_le_mono)
hence "card ((λj. j div p) ` A) ≤ card {..N div p}" by (intro card_mono) auto
thus ?thesis using card_image[OF inj] by simp
qed
lemma ell_le:
assumes "0 < p"
shows "ell p N a ≤ 2 * (N div p) + 2"
proof -
define A1 where "A1 = {j ∈ {1..N}. j mod p = a mod p}"
define A2 where "A2 = {j ∈ {1..N}. (j + a) mod p = 0}"
have "ell p N a = card (A1 ∪ A2)" unfolding ell_def A1_def A2_def
by (rule arg_cong[where f = card]) auto
also have "… ≤ card A1 + card A2" by (rule card_Un_le)
also have "card A1 ≤ N div p + 1"
by (rule card_cong_class_le[OF assms]) (auto simp: A1_def)
also have "card A2 ≤ N div p + 1"
proof (rule card_cong_class_le[OF assms])
show "A2 ⊆ {..N}" by (auto simp: A2_def)
next
fix x y assume "x ∈ A2" "y ∈ A2"
hence "[x + a = y + a] (mod p)" by (simp add: A2_def cong_def)
hence "[x = y] (mod p)" by (rule cong_add_rcancel_nat[THEN iffD1])
thus "x mod p = y mod p" by (simp only: cong_def)
qed
finally show ?thesis by simp
qed
lemma Lin_nonneg: "prime p ⟹ InnerHyp K M p ⟹
a ≤ mHalf p ⟹ 0 ≤ Lin K M p a"
proof -
assume "prime p" and H: "InnerHyp K M p" and "a ≤ mHalf p"
show "0 ≤ Lin K M p a"
proof (cases "a = 0")
case True
thus ?thesis by (simp add: Lin_def)
next
case False
from H have M40: "40 ≤ M" and K40: "40 dvd K" and KM: "200 * M ^ 2 ≤ K"
and pK: "3 * p ≤ K" by (auto simp: InnerHyp_def)
obtain k where k: "K = 40 * k" using K40 by (elim dvdE)
have hk: "hof K = 37 * k" and Nk: "Nof K = 3 * k" unfolding k hof_def Nof_def by simp_all
have p8: "8000 < p" using innerHyp_bounds[OF H] M40 by linarith
define m where "m = mHalf p"
define q where "q = Nof K div p"
have m0: "0 < m" using p8 by (simp add: m_def mHalf_def)
have m2: "2 * m ≤ p" by (simp add: m_def mHalf_def)
have "q * p ≤ 3 * k" unfolding q_def Nk[symmetric] by (rule div_times_less_eq_dividend)
hence qp: "p * q ≤ 3 * k" by (simp add: mult.commute)
have "2 * m * q ≤ p * q" using m2 by (rule mult_le_mono1)
hence mq: "2 * (m * q) ≤ p * q" by (simp add: mult.assoc)
have MM: "40 * M ≤ M * M" using M40 by (rule mult_le_mono1)
have kM: "200 * (M * M) ≤ 40 * k" using KM k by (simp add: power2_eq_square)
have qq: "q ≤ p * q" using p8 by simp
have "6 * (m * (q + 1)) + 4 * M + 10 + 3 * q ≤ 46 * k"
proof (cases "q = 0")
case True
have e: "m * (q + 1) = m" using True by simp
show ?thesis unfolding e using True m2 pK k MM kM M40 by linarith
next
case False
have e: "m * (q + 1) = m * q + m" by simp
have e2: "6 * (m * q + m) = 6 * (m * q) + 6 * m" by (rule add_mult_distrib2)
have pq: "p ≤ p * q" using False by simp
have "6 * (m * q) ≤ 9 * k" using mq qp by linarith
moreover have "6 * m ≤ 9 * k" using m2 pq qp by linarith
moreover have "3 * q ≤ 9 * k" using qq qp by linarith
moreover have "4 * M + 10 ≤ 19 * k" using MM kM M40 by linarith
ultimately show ?thesis unfolding e e2 by linarith
qed
hence "int (6 * (m * (q + 1)) + 4 * M + 10 + 3 * q) ≤ int (46 * k)"
by (simp only: of_nat_le_iff)
hence r: "int (6 * (q + 1)) * int m ≤ rhs44 K M p"
unfolding rhs44_def q_def[symmetric] unfolding hk Nk L0_def
by (simp add: algebra_simps)
have T: "int (6 * (q + 1)) ≤ Tin K M p"
proof -
have "int (6 * (q + 1)) = (int (6 * (q + 1)) * int m) div int m" using m0 by simp
also have "… ≤ rhs44 K M p div int m" by (rule zdiv_mono1[OF r]) (use m0 in simp)
finally show ?thesis by (simp add: Tin_def m_def)
qed
have e: "0 ≤ epsIn K M p a" by (simp add: epsIn_def)
have l: "ell p (Nof K) a ≤ 2 * q + 2" unfolding q_def using p8 by (intro ell_le) simp
show ?thesis using False T e l by (simp add: Lin_def bIn_def)
qed
qed
lemma card_multiples_upto:
assumes "0 < p"
shows "card {j ∈ {1..N}. p dvd j} = N div p"
proof -
have "{j ∈ {1..N}. p dvd j} = (λi. p * i) ` {1..N div p}"
proof (intro equalityI subsetI)
fix j assume "j ∈ {j ∈ {1..N}. p dvd j}"
then obtain i where j: "j = p * i" "1 ≤ p * i" "p * i ≤ N" by (auto elim!: dvdE)
have "1 ≤ i" using j(2) by (cases i) auto
moreover have "i ≤ N div p" using div_le_mono[OF j(3), of p] assms by simp
ultimately show "j ∈ (λi. p * i) ` {1..N div p}" using j(1) by auto
next
fix j assume "j ∈ (λi. p * i) ` {1..N div p}"
then obtain i where "i ∈ {1..N div p}" "j = p * i" by blast
hence i: "j = p * i" "1 ≤ i" "i ≤ N div p" by auto
have "p * i ≤ N" using mult_le_mono2[OF i(3), of p] times_div_less_eq_dividend[of p N]
by linarith
moreover have "1 ≤ p * i" using i(2) assms by simp
ultimately show "j ∈ {j ∈ {1..N}. p dvd j}" using i(1) by auto
qed
moreover have "inj_on (λi. p * i) {1..N div p}" using assms by (auto intro: inj_onI)
ultimately show ?thesis by (simp add: card_image)
qed
lemma sum_ell:
assumes "prime p" "2 < p"
shows "(∑ a = 1..mHalf p. ell p N a) = N - N div p"
proof -
define m where "m = mHalf p"
have p0: "0 < p" using assms by simp
have "odd p" using assms by (metis prime_odd_nat)
hence m2: "2 * m = p - 1" unfolding m_def mHalf_def by (auto elim!: oddE)
define C where "C a = {j ∈ {1..N}. j mod p = a ∨ j mod p = p - a}" for a
have Ceq: "{j ∈ {1..N}. j mod p = a mod p ∨ (j + a) mod p = 0} = C a"
if a: "a ∈ {1..m}" for a
proof -
have ap: "0 < a" "a < p" using a m2 by auto
have "(j + a) mod p = 0 ⟷ j mod p = p - a" for j
proof -
have r: "j mod p < p" using p0 by simp
have "(j + a) mod p = (j mod p + a) mod p" by (simp add: mod_add_left_eq)
also have "… = 0 ⟷ j mod p + a = p"
proof
assume h: "(j mod p + a) mod p = 0"
have "j mod p + a < 2 * p" using r ap by linarith
moreover have "p dvd j mod p + a" using h by (simp add: mod_eq_0_iff_dvd)
then obtain t where t: "j mod p + a = p * t" by (elim dvdE)
ultimately have "t < 2" by simp
moreover have "t ≠ 0"
proof
assume "t = 0"
hence "j mod p + a = 0" using t by simp
thus False using ap by simp
qed
ultimately show "j mod p + a = p" using t by (cases t) auto
qed simp
finally show ?thesis using ap by linarith
qed
thus ?thesis using ap by (auto simp: C_def)
qed
have "(∑ a = 1..m. ell p N a) = (∑ a = 1..m. card (C a))"
proof (rule sum.cong)
fix a assume a: "a ∈ {1..m}"
show "ell p N a = card (C a)" unfolding ell_def Ceq[OF a] ..
qed simp
also have "… = card (⋃ a ∈ {1..m}. C a)"
proof (rule card_UN_disjoint[symmetric])
show "∀i ∈ {1..m}. ∀j ∈ {1..m}. i ≠ j ⟶
C i ∩ C j = {}"
using m2 by (auto simp: C_def)
qed (auto simp: C_def)
also have "(⋃ a ∈ {1..m}. C a) = {1..N} - {j ∈ {1..N}. p dvd j}"
proof (intro equalityI subsetI)
fix j assume "j ∈ (⋃ a ∈ {1..m}. C a)"
then obtain a where a: "a ∈ {1..m}" "j ∈ C a" by auto
hence "j mod p ≠ 0" using m2 by (auto simp: C_def)
thus "j ∈ {1..N} - {j ∈ {1..N}. p dvd j}" using a by (auto simp: C_def dvd_eq_mod_eq_0)
next
fix j assume j: "j ∈ {1..N} - {j ∈ {1..N}. p dvd j}"
hence r0: "j mod p ≠ 0" by (auto simp: dvd_eq_mod_eq_0)
have rp: "j mod p < p" using p0 by simp
show "j ∈ (⋃ a ∈ {1..m}. C a)"
proof (cases "j mod p ≤ m")
case True
thus ?thesis using j r0 by (auto simp: C_def intro!: bexI[of _ "j mod p"])
next
case False
hence "p - j mod p ∈ {1..m}" using rp m2 by auto
moreover have "j ∈ C (p - j mod p)" using j rp by (auto simp: C_def)
ultimately show ?thesis by blast
qed
qed
also have "card ({1..N} - {j ∈ {1..N}. p dvd j}) = N - N div p"
by (subst card_Diff_subset) (use card_multiples_upto[OF p0, of N] in auto)
finally show ?thesis by (simp add: m_def)
qed
lemma rank_props:
fixes r :: "'a ⇒ 'a ⇒ bool"
assumes A: "finite A" and irr: "⋀x. ¬ r x x" and tr: "⋀x y z. r x y
⟹ r y z ⟹ r x z"
and tot: "⋀x y. x ∈ A ⟹ y ∈ A ⟹
x ≠ y ⟹ r x y ∨ r y x"
defines "rk ≡ λx. card {c ∈ A. r c x}"
shows "⋀x y. x ∈ A ⟹ y ∈ A ⟹
rk x < rk y ⟷ r x y"
and "bij_betw rk A {..<card A}"
proof -
have mono: "rk x < rk y" if "x ∈ A" "y ∈ A" "r x y" for x y
proof -
have "{c ∈ A. r c x} ⊂ {c ∈ A. r c y}"
using that irr tr by blast
thus ?thesis unfolding rk_def by (rule psubset_card_mono[rotated]) (use A in simp)
qed
show "rk x < rk y ⟷ r x y" if "x ∈ A" "y ∈ A" for x y
proof
assume "rk x < rk y"
thus "r x y" using mono[OF that(2,1)] tot[OF that] by (cases "x = y") auto
qed (rule mono[OF that])
have inj: "inj_on rk A"
proof (rule inj_onI)
fix x y assume "x ∈ A" "y ∈ A" "rk x = rk y"
thus "x = y" using mono tot by (metis less_irrefl)
qed
have sub: "rk ` A ⊆ {..<card A}"
proof
fix i assume "i ∈ rk ` A"
then obtain x where x: "x ∈ A" "i = rk x" by auto
have "{c ∈ A. r c x} ⊆ A - {x}" using irr by auto
hence "rk x ≤ card (A - {x})" unfolding rk_def by (intro card_mono) (use A in auto)
also have "… < card A" by (rule card_Diff1_less[OF A x(1)])
finally show "i ∈ {..<card A}" using x by simp
qed
have "rk ` A = {..<card A}"
by (rule card_subset_eq) (use sub card_image[OF inj] in auto)
thus "bij_betw rk A {..<card A}" using inj by (simp add: bij_betw_def)
qed
lemma sum_epsIn:
assumes "prime p" "InnerHyp K M p"
shows "(∑ a = 1..mHalf p. epsIn K M p a) = Ein K M p"
proof -
define m where "m = mHalf p"
define A where "A = {1..m}"
define r where "r c a ⟷ ell p K a < ell p K c ∨
(ell p K c = ell p K a ∧ c < a)" for c a
have rk: "defaultPos K p a = card {c ∈ A. r c a}" for a
by (simp add: defaultPos_def A_def m_def r_def)
have irr: "⋀x. ¬ r x x" and tr: "⋀x y z. r x y ⟹
r y z ⟹ r x z"
and tot: "⋀x y. x ∈ A ⟹ y ∈ A ⟹
x ≠ y ⟹ r x y ∨ r y x"
unfolding r_def by auto
note RP = rank_props[of A r, OF _ irr tr tot, folded rk]
have cA: "card A = m" by (simp add: A_def)
have iff: "x ∈ A ⟹ y ∈ A ⟹
defaultPos K p x < defaultPos K p y ⟷ r x y" for x y
using RP(1) by (simp add: A_def)
have bij: "bij_betw (defaultPos K p) A {..<m}" using RP(2) cA by (simp add: A_def)
have TE: "0 ≤ Ein K M p" "Ein K M p < int m" using TE_spec[OF assms] by (auto simp: m_def)
define E where "E = nat (Ein K M p)"
have E: "Ein K M p = int E" "E ≤ m" using TE by (auto simp: E_def)
have eps: "epsIn K M p a = (if defaultPos K p a < E then 1 else 0)" if a: "a ∈ A" for a
proof -
have "{c ∈ {1..mHalf p}. defaultPos K p c < defaultPos K p a} = {c ∈ A. r c a}"
using iff[OF _ a] by (auto simp: A_def m_def)
thus ?thesis by (simp add: epsIn_def rk[symmetric] E)
qed
have "(∑ a = 1..mHalf p. epsIn K M p a) = (∑ a ∈ A.
if defaultPos K p a < E then 1 else 0)"
unfolding A_def m_def by (rule sum.cong) (simp_all add: eps[unfolded A_def m_def])
also have "… = int (card {a ∈ A. defaultPos K p a < E})"
by (simp add: sum.If_cases A_def Int_def)
also have "card {a ∈ A. defaultPos K p a < E} = card {..<E}"
proof -
have inj: "inj_on (defaultPos K p) {a ∈ A. defaultPos K p a < E}"
using bij by (auto simp: bij_betw_def intro: inj_on_subset)
have "defaultPos K p ` {a ∈ A. defaultPos K p a < E} = {..<E}"
proof (intro equalityI subsetI)
fix i assume "i ∈ {..<E}"
hence "i ∈ {..<m}" using E by auto
hence "i ∈ defaultPos K p ` A" using bij by (simp add: bij_betw_def)
then obtain a where "a ∈ A" "defaultPos K p a = i" by blast
thus "i ∈ defaultPos K p ` {a ∈ A. defaultPos K p a < E}"
using ‹i ∈ {..<E}› by auto
qed auto
thus ?thesis using card_image[OF inj] by simp
qed
finally show ?thesis using E by simp
qed
lemma sum_Lin: "prime p ⟹ InnerHyp K M p ⟹
(∑ a ≤ mHalf p. Lin K M p a) = int (hof K)"
proof -
assume p: "prime p" and H: "InnerHyp K M p"
define m where "m = mHalf p"
have p8: "8000 < p" using innerHyp_bounds[OF H] H by (auto simp: InnerHyp_def)
have "{..m} = insert 0 {1..m}" by auto
hence "(∑ a ≤ m. Lin K M p a) = Lin K M p 0 + (∑ a = 1..m. Lin K M p a)" by simp
also have "(∑ a = 1..m. Lin K M p a)
= (∑ a = 1..m. Tin K M p - 3 * int (ell p (Nof K) a) + epsIn K M p a)"
by (rule sum.cong) (auto simp: Lin_def bIn_def)
also have "… = int m * Tin K M p - 3 * int (∑ a = 1..m. ell p (Nof K) a) + (∑ a =
1..m. epsIn K M p a)"
by (simp add: sum.distrib sum_subtractf sum_distrib_left of_nat_sum)
also have "(∑ a = 1..m. ell p (Nof K) a) = Nof K - Nof K div p"
unfolding m_def by (rule sum_ell[OF p]) (use p8 in simp)
also have "(∑ a = 1..m. epsIn K M p a) = Ein K M p"
unfolding m_def by (rule sum_epsIn[OF p H])
finally have "(∑ a ≤ m. Lin K M p a)
= int (L0 M) + (int m * Tin K M p + Ein K M p) - 3 * int (Nof K - Nof K div p)"
by (simp add: Lin_def)
also have "int m * Tin K M p + Ein K M p = rhs44 K M p" using TE_spec[OF p H] by (simp add: m_def)
also have "int (Nof K - Nof K div p) = int (Nof K) - int (Nof K div p)" by (simp add: of_nat_diff)
finally show "(∑ a ≤ mHalf p. Lin K M p a) = int (hof K)" by (simp add: rhs44_def m_def)
qed
lemma length_inner_idx: "prime p ⟹ InnerHyp K M p ⟹
length (inner_idx K M p) = hof K"
proof -
assume p: "prime p" and H: "InnerHyp K M p"
have "length (inner_idx K M p) = (∑ a ∈ set [0..<mHalf p + 1]. nat (Lin K M p a))"
unfolding inner_idx_def length_concat map_map
by (simp add: o_def sum_list_distinct_conv_sum_set)
also have "set [0..<mHalf p + 1] = {..mHalf p}" by auto
also have "(∑ a ≤ mHalf p. nat (Lin K M p a)) = hof K"
proof -
have "int (∑ a ≤ mHalf p. nat (Lin K M p a)) = (∑ a ≤ mHalf p. Lin K M p a)"
unfolding of_nat_sum by (rule sum.cong) (use Lin_nonneg[OF p H] in auto)
also have "… = int (hof K)" by (rule sum_Lin[OF p H])
finally show ?thesis by (simp only: of_nat_eq_iff)
qed
finally show "length (inner_idx K M p) = hof K" .
qed
text ‹(4.5): the inner basis is @{text "ℤ_p"}-unimodular: the coefficient matrix of the
basis
polynomials has a determinant that is a @{text p}-adic unit (CRT basis lemma over
@{text "ℤ/pℤ"}).›
text ‹The index list is lexicographically ordered: an earlier position has a smaller class,
or the same class
and a smaller exponent.›
lemma inner_idx_sorted:
"sorted_wrt (λu v. fst u < fst v ∨ (fst u = fst v ∧ snd u < snd v))
(concat (map (λa. map (λi. (a, i)) [0..<f a]) [0..<n]))"
proof (induction n)
case 0
show ?case by simp
next
case (Suc n)
have "sorted_wrt (λu v. fst u < fst v ∨ (fst u = fst v ∧
snd u < snd v)) (map (λi. (n, i)) [0..<f n])"
unfolding sorted_wrt_map by (simp add: sorted_wrt_upt)
with Suc show ?case by (auto simp: sorted_wrt_append)
qed
lemma inner_idx_lex:
assumes "y < x" "x < length (inner_idx K M p)"
shows "fst (inner_idx K M p ! y) < fst (inner_idx K M p ! x) ∨
(fst (inner_idx K M p ! y) = fst (inner_idx K M p ! x) ∧
snd (inner_idx K M p ! y) < snd (inner_idx K M p ! x))"
using sorted_wrt_nth_less[OF inner_idx_sorted assms(1) assms(2)[unfolded inner_idx_def]]
unfolding inner_idx_def .
lemma vpGge_innerBasis: "prime p ⟹ vpGge p (innerBasis K M p x) 0"
proof -
assume p: "prime p"
have f: "vpGge p (pX + [:of_nat c ^ 2:]) 0" for c
proof -
have "vge p (of_nat c ^ 2) 0" using vge_pow[OF p vge_of_int[OF p, of "int c"]] by simp
thus ?thesis by (intro vpGge_add[OF p vpGge_pX vpGge_C])
qed
have fp: "vpGge p ((pX + [:of_nat c ^ 2:]) ^ n) 0" for c n using vpGge_pow[OF p f[of c], of n]
by simp
have pr: "vpGge p (∏ c ∈ {0..mHalf p} - {fst x}. (pX +
[:of_nat c ^ 2:]) ^ nat (Lin K M p c)) 0"
using vpGge_prod[OF p, of "{0..mHalf p} - {fst x}" "λc. (pX +
[:of_nat c ^ 2:]) ^ nat (Lin K M p c)" "λ_. 0"] fp
by simp
show ?thesis unfolding innerBasis_def using vpGge_mul[OF p pr fp] by simp
qed
text ‹Shapes of pulled-back numerators (Lean: @{text FarGood}, @{text Decomp}).›
definition FarGood :: "nat ⇒ rat poly ⇒ bool" where
"FarGood p F ⟷ vpGge p F 0 ∧ (∀d. 1 ≤ d ⟶
vge p (Polynomial.coeff F d) 1)"
definition Decomp :: "nat ⇒ nat ⇒ nat ⇒ rat poly ⇒
bool" where
"Decomp p e n Q ⟷ (∃N F. Q = [:of_nat p ^ e:] * N * F ∧
vpGge p N 0 ∧ degree N ≤ n ∧ FarGood p F)"
text ‹The number of @{text p}'s in
@{text "j^2 - (c + p z)^2 = (j - c - p z)(j + c + p z)"}.›
definition omg :: "nat ⇒ nat ⇒ nat ⇒ nat" where
"omg p c j = (if int p dvd (int j - int c) then 1 else 0) + (if int p dvd (int j +
int c) then 1 else 0)"
text ‹The exponent of @{text p} extracted from the pulled-back numerator at the class
@{text c}.›
definition eNum :: "nat ⇒ nat ⇒ nat set ⇒ (nat ⇒
nat) ⇒ nat" where
"eNum p c J k = 5 * (if int p dvd int c then 1 else 0) + (∑ j ∈ J. k j * omg p c j)"
text ‹The near poles of the class @{text c}: @{text "r ∈ ±[1, K]"} with
@{text "r ≡ c (mod p)"}.›
definition nearCount :: "nat ⇒ nat ⇒ nat ⇒ nat" where
"nearCount p K c = card {r ∈ signedPoles {1..K}. int p dvd (r - int c)}"
subsection ‹Extracting powers of @{text p} from @{text "g(c + p z)"}›
lemma FarGood_one: "FarGood p 1"
unfolding FarGood_def by (auto simp: vpGge_one vge_zero)
lemma FarGood_mult: "prime p ⟹ FarGood p F ⟹
FarGood p G ⟹ FarGood p (F * G)"
proof -
assume p: "prime p" and F: "FarGood p F" and G: "FarGood p G"
have F0: "⋀i. vge p (Polynomial.coeff F i) 0" and G0: "⋀i. vge p (Polynomial.coeff G i)
0"
using F G unfolding FarGood_def vpGge_iff by auto
have F1: "⋀i. 1 ≤ i ⟹ vge p (Polynomial.coeff F i) 1"
and G1: "⋀i. 1 ≤ i ⟹ vge p (Polynomial.coeff G i) 1"
using F G unfolding FarGood_def by auto
have "vpGge p (F * G) 0" using vpGge_mul[OF p, of F 0 G 0] F G unfolding FarGood_def by simp
moreover have "vge p (Polynomial.coeff (F * G) d) 1" if d: "1 ≤ d" for d
unfolding coeff_mult
proof (rule vge_sum[OF p])
show "finite {..d}" by simp
next
fix i assume i: "i ∈ {..d}"
show "vge p (Polynomial.coeff F i * Polynomial.coeff G (d - i)) 1"
proof (cases "i = 0")
case True
have "vge p (Polynomial.coeff F i * Polynomial.coeff G (d - i)) (0 + 1)"
by (rule vge_mul[OF p F0 G1]) (use True d in simp)
thus ?thesis by simp
next
case False
have "vge p (Polynomial.coeff F i * Polynomial.coeff G (d - i)) (1 + 0)"
by (rule vge_mul[OF p F1 G0]) (use False in simp)
thus ?thesis by simp
qed
qed
ultimately show ?thesis unfolding FarGood_def by blast
qed
lemma Decomp_one: "Decomp p 0 0 1"
unfolding Decomp_def by (rule exI[of _ 1], rule exI[of _ 1]) (simp add: vpGge_one FarGood_one)
lemma Decomp_mult:
"prime p ⟹ Decomp p e n Q ⟹ Decomp p e' n' Q' ⟹
Decomp p (e + e') (n + n') (Q * Q')"
proof -
assume p: "prime p" and D1: "Decomp p e n Q" and D2: "Decomp p e' n' Q'"
obtain N F where Q: "Q = [:of_nat p ^ e:] * N * F" and N: "vpGge p N 0" and dN: "degree N ≤ n"
and F: "FarGood p F" using D1 unfolding Decomp_def by blast
obtain N' F' where Q': "Q' = [:of_nat p ^ e':] * N' *
F'" and N': "vpGge p N' 0" and dN': "degree N' ≤ n'"
and F': "FarGood p F'" using D2 unfolding Decomp_def by blast
have "Q * Q' = [:of_nat p ^ (e + e'):] * (N * N') * (F * F')"
unfolding Q Q' power_add by (simp add: mult_ac)
moreover have "vpGge p (N * N') 0" using vpGge_mul[OF p N N'] by simp
moreover have "degree (N * N') ≤ n + n'" using degree_mult_le[of N N'] dN dN' by linarith
moreover have "FarGood p (F * F')" by (rule FarGood_mult[OF p F F'])
ultimately show ?thesis unfolding Decomp_def by blast
qed
lemma Decomp_pow: "prime p ⟹ Decomp p e n Q ⟹
Decomp p (k * e) (k * n) (Q ^ k)"
proof (induction k)
case 0
show ?case using Decomp_one by simp
next
case (Suc k)
have "Decomp p (k * e + e) (k * n + n) (Q ^ k * Q)"
by (rule Decomp_mult[OF Suc.prems(1) Suc.IH[OF Suc.prems] Suc.prems(2)])
thus ?case by (simp add: ac_simps)
qed
lemma Decomp_C_unit: "prime p ⟹ Decomp p e n Q ⟹
vge p u 0 ⟹ Decomp p e n ([:u:] * Q)"
proof -
assume p: "prime p" and D: "Decomp p e n Q" and u: "vge p u 0"
obtain N F where Q: "Q = [:of_nat p ^ e:] * N * F" and N: "vpGge p N 0" and dN: "degree N ≤ n"
and F: "FarGood p F" using D unfolding Decomp_def by blast
have e: "[:u:] * Q = [:of_nat p ^ e:] * N * ([:u:] * F)" unfolding Q by (simp add: mult_ac)
have "vpGge p ([:u:] * F) 0" using vpGge_mul[OF p vpGge_C[OF u], of F 0] F unfolding FarGood_def
by simp
moreover have "vge p (Polynomial.coeff ([:u:] * F) d) 1" if d: "1 ≤ d" for d
proof -
have "vge p (u * Polynomial.coeff F d) (0 + 1)"
by (rule vge_mul[OF p u]) (use F d in ‹simp add: FarGood_def›)
thus ?thesis by simp
qed
ultimately have "FarGood p ([:u:] * F)" unfolding FarGood_def by blast
thus ?thesis using e N dN unfolding Decomp_def by blast
qed
text ‹A linear factor @{text "α + σ p z"} (@{text "σ = ±1"})
is @{text "p ⋅ (near)"} if @{text "p | α"}, and far-good otherwise.›
lemma Decomp_linear:
assumes "prime p" "σ = 1 ∨ σ = - 1"
shows "Decomp p (if int p dvd α then 1 else 0) (if int p dvd α then 1 else 0)
[:of_int α, of_int (σ * int p):]"
proof (cases "int p dvd α")
case True
then obtain β where b: "α = int p * β" by (elim dvdE)
have e: "[:of_int α, of_int (σ * int p):] =
[:of_nat p ^ 1:] * [:of_int β, of_int σ:] * (1 :: rat poly)"
unfolding b by (simp add: mult.commute)
have N: "vpGge p [:of_int β, of_int σ :: rat:] 0" unfolding vpGge_iff
by (auto simp: coeff_pCons vge_of_int[OF assms(1)] vge_zero split: nat.split)
have dN: "degree [:of_int β, of_int σ :: rat:] ≤ 1"
using degree_pCons_le[of "of_int β" "[:of_int σ :: rat:]"] by simp
have "Decomp p 1 1 [:of_int α, of_int (σ * int p):]"
unfolding Decomp_def by (rule exI[of _ "[:of_int β, of_int σ:]"],
rule exI[of _ 1]) (intro conjI e N dN FarGood_one)
thus ?thesis using True by simp
next
case False
have vp1: "vge p (of_nat p) 1" using qmultiplicity_power_int[OF assms(1), of 1]
by (simp add: vge_def vp_def)
have vp1': "vge p (- of_nat p) 1" by (rule vge_neg[OF vp1])
have vp0: "vge p (of_nat p) 0" and vp0': "vge p (- of_nat p) 0"
by (rule vge_mono[OF vp1], simp, rule vge_mono[OF vp1'], simp)
have FG: "FarGood p [:of_int α, of_int (σ * int p) :: rat:]"
unfolding FarGood_def vpGge_iff
using assms(2) by (auto simp: coeff_pCons vge_of_int[OF assms(1)] vge_zero vp1 vp1' vp0 vp0'
split: nat.split)
have e: "[:of_int α, of_int (σ * int p):] =
[:of_nat p ^ 0:] * 1 * [:of_int α, of_int (σ * int p) :: rat:]"
by simp
have "Decomp p 0 0 [:of_int α, of_int (σ * int p):]"
unfolding Decomp_def by (rule exI[of _ 1], rule exI[of _ "[:of_int α,
of_int (σ * int p):]"]) (intro conjI e vpGge_one FG, simp)
thus ?thesis using False by simp
qed
lemma Decomp_prod:
"prime p ⟹ finite J ⟹ (⋀j. j ∈ J ⟹
Decomp p (e j) (e j) (f j)) ⟹
Decomp p (∑ j ∈ J. e j) (∑ j ∈ J. e j) (∏ j ∈ J. f j)"
proof -
assume p: "prime p" and J: "finite J" and D: "⋀j. j ∈ J ⟹
Decomp p (e j) (e j) (f j)"
show ?thesis using J D
proof (induction J rule: finite_induct)
case empty
show ?case using Decomp_one by simp
next
case (insert a J)
have "Decomp p (e a + (∑ j ∈ J. e j)) (e a + (∑ j ∈
J. e j)) (f a * (∏ j ∈ J. f j))"
by (rule Decomp_mult[OF p]) (use insert in auto)
thus ?case unfolding sum.insert[OF insert.hyps] prod.insert[OF insert.hyps] .
qed
qed
text ‹The pulled-back numerator @{text "ε x^5 ∏_j (j^2 - x^2)^{k_j}"} at
@{text "x = c + p z"}: every factor
@{text "j^2 - (c + p z)^2 = (j - c - p z)(j + c + p z)"} contributes @{text "omg p c j"} powers of
@{text p}.›
lemma decomp_pullback:
assumes p: "prime p" and J: "finite J" and ε: "vge p ε 0"
shows "Decomp p (eNum p c J k) (eNum p c J k)
(pcompose ([:ε:] * pX ^ 5 * pcompose (∏ j ∈
J. (pX + [:of_nat j ^ 2:]) ^ k j) (- (pX ^ 2)))
([:of_nat c:] + [:of_nat p:] * pX))"
proof -
define L where "L = [:of_nat c:] + [:of_nat p:] * (pX :: rat poly)"
have Leq: "L = [:of_int (int c), of_int (1 * int p):]"
unfolding L_def by (simp add: monom_Suc)
have fac: "⋀j. pcompose (pcompose (pX + [:of_nat j ^ 2:]) (- (pX ^ 2))) L =
[:of_int (int j - int c), of_int (- 1 * int p):] * [:of_int (int j + int c),
of_int (1 * int p):]"
proof -
fix j :: nat
have e: "poly (pcompose (pcompose (pX + [:of_nat j ^ 2:]) (- (pX ^ 2))) L) x =
poly ([:of_int (int j - int c), of_int (- 1 * int p):] * [:of_int (int j + int c),
of_int (1 * int p):]) x" for x :: rat
unfolding L_def by (simp add: poly_pcompose poly_monom algebra_simps power2_eq_square)
show "pcompose (pcompose (pX + [:of_nat j ^ 2:]) (- (pX ^ 2))) L =
[:of_int (int j - int c), of_int (- 1 * int p):] * [:of_int (int j + int c),
of_int (1 * int p):]"
by (rule poly_eq_of_eval_nat) (rule e)
qed
have Q: "pcompose ([:ε:] * pX ^ 5 * pcompose (∏ j ∈
J. (pX + [:of_nat j ^ 2:]) ^ k j) (- (pX ^ 2))) L =
[:ε:] * (L ^ 5 * (∏ j ∈
J. ([:of_int (int j - int c), of_int (- 1 * int p):] *
[:of_int (int j + int c), of_int (1 * int p):]) ^ k j))"
unfolding pcompose_mult pcompose_prod pcompose_power_left pcompose_pX pcompose_const fac
by (simp only: mult.assoc)
have L5: "Decomp p (5 * (if int p dvd int c then 1 else 0)) (5 *
(if int p dvd int c then 1 else 0)) (L ^ 5)"
unfolding Leq by (rule Decomp_pow[OF p Decomp_linear[OF p, of 1 "int c"]]) simp
have Pr: "Decomp p (∑ j ∈ J. k j * omg p c j) (∑ j ∈ J. k j * omg p c j)
(∏ j ∈ J. ([:of_int (int j - int c), of_int (- 1 * int p):] *
[:of_int (int j + int c), of_int (1 * int p):]) ^ k j)"
proof (rule Decomp_prod[OF p J])
fix j assume "j ∈ J"
show "Decomp p (k j * omg p c j) (k j * omg p c j)
(([:of_int (int j - int c), of_int (- 1 * int p):] * [:of_int (int j + int c),
of_int (1 * int p):]) ^ k j)"
unfolding omg_def by (rule Decomp_pow[OF p Decomp_mult[OF p Decomp_linear[OF p]
Decomp_linear[OF p]]]) simp_all
qed
show ?thesis
unfolding L_def[symmetric] Q eNum_def
by (rule Decomp_C_unit[OF p _ ε]) (rule Decomp_mult[OF p L5 Pr])
qed
lemma tauExt_tr_C_mul: "tauExt_tr p Y ([:a:] * U) S M = [:a:] * tauExt_tr p Y U S M"
proof -
have d: "([:a:] * U) div qPoleProd S = Polynomial.smult a (U div qPoleProd S)"
by (simp add: div_smult_left)
have t: "tauK (Polynomial.smult a P) = a * tauK P" for P by (simp add: tauK_eq_tau tau_smult)
have r: "qRes S ([:a:] * U) s = a * qRes S U s" for s by (simp add: qRes_def)
show ?thesis unfolding tauExt_tr_def d t r by (simp add: smult_add_right smult_sum_right)
qed
lemma vpGge_Yp_tr: "prime p ⟹ 7 ≤ p ⟹ vpGge p (Yp_tr p M) 0"
proof -
assume p: "prime p" and p7: "7 ≤ p"
have v: "vge p (of_nat p) 0" using vge_of_int[OF p, of "int p"] by simp
have a: "vpGge p ([:of_nat p ^ 5:] * pX) 0"
using vpGge_mul[OF p vpGge_C[OF vge_pow[OF p v]] vpGge_pX] by simp
have b: "vpGge p [:Cp_tr p M:] 0" by (rule vpGge_C[OF vge_mono[OF Cp_tr_vge[OF p p7]]]) simp
show ?thesis unfolding Yp_tr_def by (rule vpGge_add[OF p a b])
qed
lemma coeff_high_vge:
assumes "prime p" "vpGge p N 0" "FarGood p F" "degree N < d"
shows "vge p (Polynomial.coeff (N * F) d) 1"
proof -
have N0: "⋀i. vge p (Polynomial.coeff N i) 0" using assms(2) unfolding vpGge_iff by blast
have F1: "⋀i. 1 ≤ i ⟹ vge p (Polynomial.coeff F i) 1" using assms(3)
unfolding FarGood_def by blast
have "vge p (∑ i ≤ d. Polynomial.coeff N i * Polynomial.coeff F (d - i)) 1"
proof (rule vge_sum[OF assms(1)])
show "finite {..d}" by simp
next
fix i assume "i ∈ {..d}"
show "vge p (Polynomial.coeff N i * Polynomial.coeff F (d - i)) 1"
proof (cases "degree N < i")
case True
thus ?thesis by (simp add: coeff_eq_0 vge_zero)
next
case False
hence "1 ≤ d - i" using assms(4) by linarith
from vge_mul[OF assms(1) N0 F1[OF this]] show ?thesis by simp
qed
qed
thus ?thesis unfolding coeff_mult .
qed
text ‹One summand of (3.7). If @{text "P(c + p z) = p^e N F"} (@{text Decomp}) with
@{text "e ≤ p + 1"},
the class-@{text c} summand has valuation @{text "≥ e - #{near poles}"},
for every truncation length
@{text "M ≥ deg P"}.›
theorem summand_bound_tr:
assumes p: "prime p" and p7: "7 ≤ p" and K1: "2 * K < p ^ 2" and K2: "K + p < p ^ 2"
and S: "finite S" and hS: "⋀r. r ∈ S ⟹
¦r¦ ≤ int K" and c: "c < p"
and D: "Decomp p e e (pcompose P ([:of_nat c:] + [:of_nat p:] * pX))" and e: "e ≤ p + 1"
and dP: "degree P ≤ M"
shows "vpGge p (tauExt_tr p (Yp_tr p M) (distribNum p S P c) (distribPoles p S c) M)
(of_int (int e - int (card {r ∈ S. int p dvd (r - int c)})))"
proof -
define L where "L = [:of_nat c:] + [:of_nat p:] * (pX :: rat poly)"
obtain N F where Q: "pcompose P L = [:of_nat p ^ e:] * N * F" and N0: "vpGge p N 0"
and Nd: "degree N ≤ e" and FG: "FarGood p F"
using D unfolding Decomp_def L_def by blast
have p0: "(of_nat p :: rat) ≠ 0" using p by (simp add: prime_gt_0_nat)
define Sn where "Sn = {r ∈ S. int p dvd (r - int c)}"
define Sf where "Sf = {r ∈ S. ¬ int p dvd (r - int c)}"
define near :: "int set" where "near = (λr. (r - int c) div int p) ` Sn"
define far :: "rat set" where "far = (λr. (of_int r - of_nat c) / of_nat p) ` Sf"
have finSn: "finite Sn" and finSf: "finite Sf" and finnear: "finite near" and finfar: "finite far"
by (simp_all add: Sn_def Sf_def near_def far_def S)
have inj: "inj_on (λr. (of_int r - of_nat c) / (of_nat p :: rat)) S"
by (rule inj_on_subset[OF distrib_inj subset_UNIV]) (simp add: prime_gt_0_nat p)
have cardfar: "card far = card Sf"
unfolding far_def by (rule card_image) (use inj in ‹auto simp: Sf_def inj_on_def›)
have cardS: "card S = card Sn + card Sf"
proof -
have SU: "S = Sn ∪ Sf" by (auto simp: Sn_def Sf_def)
show ?thesis unfolding SU by (rule card_Un_disjoint[OF finSn finSf]) (auto simp: Sn_def Sf_def)
qed
have poles: "distribPoles p S c = of_int ` near ∪ far"
proof -
have SU: "S = Sn ∪ Sf" by (auto simp: Sn_def Sf_def)
have e1: "(λr. (of_int r - of_nat c) / (of_nat p :: rat)) ` Sn = of_int ` near"
unfolding near_def image_image
proof (rule image_cong[OF refl])
fix r assume "r ∈ Sn"
hence "int p dvd (r - int c)" by (simp add: Sn_def)
then obtain q where q: "r - int c = int p * q" by (elim dvdE)
have qd: "(r - int c) div int p = q" unfolding q using p by (simp add: prime_gt_0_nat)
have "(of_int r - of_nat c) / (of_nat p :: rat) = of_int (r - int c) / of_nat p" by simp
also have "… = of_int q" unfolding q using p0 by simp
finally show "(of_int r - of_nat c) / of_nat p = (of_int ((r - int c) div int p) :: rat)"
unfolding qd .
qed
show ?thesis unfolding distribPoles_def SU image_Un e1 far_def ..
qed
have hT: "⋀r s. r ∈ near ⟹ s ∈ near ⟹
r ≠ s ⟹ ¬ int p dvd (r - s)"
proof -
fix r s assume r: "r ∈ near" and s: "s ∈ near" and rs: "r ≠ s"
obtain r0 where r0: "r0 ∈ Sn" "r = (r0 - int c) div int p" using r unfolding near_def
by blast
obtain s0 where s0: "s0 ∈ Sn" "s = (s0 - int c) div int p" using s unfolding near_def
by blast
have r0S: "r0 ∈ S" and s0S: "s0 ∈ S" using r0(1) s0(1) by (simp_all add: Sn_def)
have "int p dvd (r0 - int c)" using r0(1) by (simp add: Sn_def)
hence dr: "r0 - int c = int p * r" unfolding r0(2) by simp
have "int p dvd (s0 - int c)" using s0(1) by (simp add: Sn_def)
hence ds: "s0 - int c = int p * s" unfolding s0(2) by simp
have "int (2 * K) < int (p ^ 2)" using K1 by (simp only: of_nat_less_iff)
hence K1': "2 * int K < int p ^ 2" by simp
show "¬ int p dvd (r - s)"
proof
assume "int p dvd (r - s)"
then obtain t where t: "r - s = int p * t" by (elim dvdE)
have "r0 - s0 = (r0 - int c) - (s0 - int c)" by simp
also have "… = int p * (r - s)" unfolding dr ds by (simp add: right_diff_distrib)
also have "… = int p ^ 2 * t" unfolding t by (simp add: power2_eq_square)
finally have e: "r0 - s0 = int p ^ 2 * t" .
have dv: "int p ^ 2 dvd (r0 - s0)" unfolding e by simp
have "¦r0 - s0¦ ≤ ¦r0¦ + ¦s0¦" by (rule abs_triangle_ineq4)
hence bnd: "¦r0 - s0¦ < int p ^ 2" using hS[OF r0S] hS[OF s0S] K1' by linarith
have "r0 - s0 = 0"
proof (rule ccontr)
assume "r0 - s0 ≠ 0"
from dvd_imp_le_int[OF this dv] bnd show False by simp
qed
hence "r = s" using r0(2) s0(2) by simp
with rs show False ..
qed
qed
have hd: "⋀r. r ∈ near ⟹ dIdx r < p"
proof -
fix r assume r: "r ∈ near"
obtain r0 where r0: "r0 ∈ Sn" "r = (r0 - int c) div int p" using r unfolding near_def
by blast
have r0S: "r0 ∈ S" using r0(1) by (simp add: Sn_def)
have "int p dvd (r0 - int c)" using r0(1) by (simp add: Sn_def)
hence dr: "r0 - int c = int p * r" unfolding r0(2) by simp
have ab: "¦r0¦ ≤ int K" by (rule hS[OF r0S])
have "int (K + p) < int (p ^ 2)" using K2 by (simp only: of_nat_less_iff)
hence K2': "int K + int p < int p * int p" by (simp add: power2_eq_square)
have pp: "0 < int p" using p by (simp add: prime_gt_0_nat)
have ci: "int c < int p" using c by simp
have up: "int p * r < int p * int p" using dr ab K2' ci unfolding abs_le_iff by linarith
have lo: "int p * (- int p) < int p * r" using dr ab K2' ci unfolding abs_le_iff by linarith
have "r < int p" using up pp by (simp add: mult_less_cancel_left)
moreover have "- int p < r"
proof (rule ccontr)
assume "¬ - int p < r"
hence "r ≤ - int p" by simp
hence "int p * r ≤ int p * (- int p)" using pp by (intro mult_left_mono) simp_all
thus False using lo by linarith
qed
ultimately show "dIdx r < p" unfolding dIdx_def by (simp add: nat_less_iff)
qed
have hFv: "⋀s. s ∈ far ⟹ vp p s = - 1"
proof -
fix s assume "s ∈ far"
then obtain r0 where r0: "r0 ∈ Sf" "s = (of_int r0 - of_nat c) / of_nat p"
unfolding far_def by blast
have nd: "¬ int p dvd (r0 - int c)" using r0(1) by (simp add: Sf_def)
have "s = of_int (r0 - int c) / of_nat p" unfolding r0(2) by simp
thus "vp p s = - 1" using vp_int_div_p[OF p nd] by simp
qed
have U0: "vpGge p (N * F) 0" using FG
by (intro vpGge_mul[OF p N0, of _ 0, simplified]) (simp add: FarGood_def)
have U1: "⋀d. p + 1 < d ⟹ vge p (Polynomial.coeff (N * F) d) 1"
by (rule coeff_high_vge[OF p N0 FG]) (use Nd e in simp)
have dU: "degree (N * F) ≤ M"
proof -
have Le: "L = [:of_nat c, of_nat p:]" unfolding L_def by (simp add: monom_Suc)
have "degree L = 1" unfolding Le using p0 by simp
hence "degree (pcompose P L) = degree P" by (simp add: degree_pcompose)
moreover have "degree (pcompose P L) = degree (N * F)" unfolding Q using p0
by (simp add: mult.assoc)
ultimately show ?thesis using dP by simp
qed
have num: "distribNum p S P c = [:of_nat p powi (int e - int (card Sn)) * (- 1) ^ card Sf:] *
([:(- of_nat p) powi (- int (card far)):] * (N * F))"
proof -
have pp: "(of_nat p :: rat) powi (int e - int (card Sn)) * of_nat p powi (- int (card Sf)) =
of_nat p powi (- int (card S)) * of_nat p ^ e"
proof -
have "(of_nat p :: rat) powi (int e - int (card Sn)) * of_nat p powi (- int (card Sf)) =
of_nat p powi (int e - int (card Sn) + - int (card Sf))"
by (rule power_int_add[symmetric]) (use p0 in simp)
also have "… = of_nat p powi (- int (card S) + int e)"
by (rule arg_cong[where f = "λk. (of_nat p :: rat) powi k"]) (use cardS in simp)
also have "… = of_nat p powi (- int (card S)) * of_nat p powi (int e)"
by (rule power_int_add) (use p0 in simp)
also have "… = of_nat p powi (- int (card S)) * of_nat p ^ e"
by (simp add: power_int_of_nat)
finally show ?thesis .
qed
have mm: "((- 1 :: rat) ^ card Sf) * (- 1) ^ card Sf = 1"
by (simp add: power_mult_distrib[symmetric])
have ng: "(- (of_nat p :: rat)) powi (- int (card Sf)) =
(- 1) ^ card Sf * of_nat p powi (- int (card Sf))"
proof -
have i1: "inverse ((- 1 :: rat) ^ card Sf) = (- 1) ^ card Sf"
by (cases "even (card Sf)") (simp_all add: neg_one_even_power neg_one_odd_power)
show ?thesis unfolding power_int_minus power_int_of_nat power_minus[of "of_nat p :: rat"]
inverse_mult_distrib i1 ..
qed
have k: "of_nat p powi (- int (card S)) * of_nat p ^ e =
(of_nat p powi (int e - int (card Sn)) * (- 1) ^ card Sf) *
((- of_nat p) powi (- int (card far)) :: rat)"
proof -
have "(of_nat p powi (int e - int (card Sn)) * (- 1) ^ card Sf) *
((- of_nat p) powi (- int (card far)) :: rat) =
((- 1) ^ card Sf * (- 1) ^ card Sf) * (of_nat p powi (int e - int (card Sn)) *
of_nat p powi (- int (card Sf)))"
unfolding cardfar ng by (simp only: mult_ac)
also have "… = of_nat p powi (- int (card S)) * of_nat p ^ e" unfolding mm pp by simp
finally show ?thesis by (rule sym)
qed
have g1: "[:x:] * ([:y:] * N * F) = Polynomial.smult (x * y) (N * F)" for x y :: rat
by (simp add: mult_ac)
have g2: "[:x:] * ([:y:] * (N * F)) = Polynomial.smult (x * y) (N * F)" for x y :: rat
by (simp add: mult.commute)
show ?thesis unfolding distribNum_def L_def[symmetric] Q g1 g2 k ..
qed
have ext: "vpGge p (tauExt_tr p (Yp_tr p M) ([:(- of_nat p) powi (- int (card far)):] * (N *
F)) (of_int ` near ∪ far) M) 0"
by (rule tauX_far_pole_valuation[OF p p7 finnear finfar hT hd hFv vpGge_Yp_tr[OF p p7] U0 U1
dU])
have cv: "vge p (of_nat p powi (int e - int (card Sn)) * (- 1) ^ card Sf) (of_int (int e -
int (card Sn)))"
proof -
have v1: "vge p (of_nat p powi (int e - int (card Sn))) (of_int (int e - int (card Sn)))"
by (simp add: vge_def vp_def qmultiplicity_power_int[OF p])
have v2: "vge p ((- 1) ^ card Sf) 0" using vge_of_int[OF p, of "(- 1) ^ card Sf"] by simp
from vge_mul[OF p v1 v2] show ?thesis by simp
qed
show ?thesis
unfolding poles num tauExt_tr_C_mul[where a =
"of_nat p powi (int e - int (card Sn)) * (- 1) ^ card Sf"] Sn_def[symmetric]
using vpGge_mul[OF p vpGge_C[OF cv] ext] by simp
qed
lemma finite_signedPoles: "finite S ⟹ finite (signedPoles S)"
by (simp add: signedPoles_def)
lemma signedPoles_abs_le: "r ∈ signedPoles {1..K} ⟹ ¦r¦ ≤ int K"
by (auto simp: signedPoles_def)
lemma nearCount_eq_card: "nearCount p K c = card {r ∈
signedPoles {1..K}. int p dvd (r - int c)}"
by (simp add: nearCount_def)
text ‹The inner-range entry bound, generic form (Lean: @{text entry_generic}):
if every class @{text c}
gives @{text "B + 4 ≤ e_c - n_c"} with @{text "e_c ≤ p + 1"}, then
@{text "v_p^G(mu_X(∏(t + j^2)^{k_j} / D_K)) ≥ B"}. Uses (3.1),
Lemma 3.2 and the summand bounds.›
theorem entry_generic:
assumes p: "prime p" and p7: "7 ≤ p" and K1: "2 * K < p ^ 2" and K2: "K + p <
p ^ 2" and J: "finite J"
and hB: "⋀c. c < p ⟹
B + 4 ≤ of_nat (eNum p c J k) - of_nat (nearCount p K c)"
and hdeg: "⋀c. c < p ⟹ eNum p c J k ≤ p + 1"
shows "vpGge p (muX {1..K} (∏ j ∈ J. (pX + [:of_nat j ^ 2:]) ^ k j)) B"
proof -
define S where "S = signedPoles {1..K}"
define P where "P = [:(- 1) ^ card {1..K}:] * pX ^ 5 * pcompose (∏ j ∈
J. (pX + [:of_nat j ^ 2:]) ^ k j) (- (pX ^ 2))"
have finS: "finite S" by (simp add: S_def finite_signedPoles)
have pb: "muX {1..K} (∏ j ∈ J. (pX + [:of_nat j ^ 2:]) ^ k j) = tauX S P"
unfolding S_def P_def by (rule pullback) auto
have ε: "vge p ((- 1) ^ card {1..K}) 0"
using vge_of_int[OF p, of "(- 1) ^ card {1..K}"] by simp
obtain M0 where M0: "⋀M. M0 ≤ M ⟹
vpGge p (tauX S P - [:of_nat p powi (- 4):] *
(∑ a < p. tauExt_tr p (Yp_tr p M) (distribNum p S P a) (distribPoles p S a) M))
B"
using tauX_distribution_formula[OF p p7 finS, of P B] by blast
define M where "M = max M0 (degree P)"
have summand: "⋀c. c < p ⟹
vpGge p (tauExt_tr p (Yp_tr p M) (distribNum p S P c) (distribPoles p S c) M) (B + 4)"
proof -
fix c assume c: "c < p"
have "vpGge p (tauExt_tr p (Yp_tr p M) (distribNum p S P c) (distribPoles p S c) M)
(of_int (int (eNum p c J k) - int (card {r ∈ S. int p dvd (r - int c)})))"
unfolding P_def
by (rule summand_bound_tr[OF p p7 K1 K2 finS _ c decomp_pullback[OF p J ε] hdeg[OF
c]])
(use signedPoles_abs_le in ‹auto simp: S_def M_def P_def›)
thus "vpGge p (tauExt_tr p (Yp_tr p M) (distribNum p S P c) (distribPoles p S c) M) (B + 4)"
proof (rule vpGge_mono)
show "B + 4 ≤ of_int (int (eNum p c J k) - int (card {r ∈ S. int p dvd (r - int c)}))"
using hB[OF c] unfolding nearCount_eq_card S_def by simp
qed
qed
have sumv: "vpGge p ([:of_nat p powi (- 4):] *
(∑ a < p. tauExt_tr p (Yp_tr p M) (distribNum p S P a) (distribPoles p S a) M)) B"
proof -
have c4: "vpGge p [:of_nat p powi (- 4):] (- 4)"
by (rule vpGge_C) (simp add: vge_def vp_def qmultiplicity_power_int[OF p])
have "vpGge p (∑ a < p. tauExt_tr p (Yp_tr p M) (distribNum p S P a) (distribPoles p S a)
M) (B + 4)"
by (rule vpGge_sum[OF p]) (use summand in auto)
from vpGge_mul[OF p c4 this] show ?thesis by simp
qed
have "vpGge p (tauX S P) B"
using vpGge_add[OF p M0[of M] sumv] by (simp add: M_def)
thus ?thesis by (simp only: pb)
qed
subsection ‹The inner entry bounds (4.2)/(4.3)›
text ‹The class of a residue: @{text "cls p j = min(j mod p, p - j mod p)"}.›
definition cls :: "nat ⇒ nat ⇒ nat" where "cls p j =
min (j mod p) (p - j mod p)"
text ‹Exponent of @{text "t + j^2"} in the inner row @{text "E_x"}.›
definition nu :: "nat ⇒ nat ⇒ nat ⇒ nat ×
nat ⇒ nat ⇒ nat" where
"nu K M p x j = (if j ≤ mHalf p then (if j = fst x then snd x else nat (Lin K M p j)) else 0)"
text ‹The index set and the exponents of the numerator @{text "D_N^6 E_x E_y"}.›
definition Jset :: "nat ⇒ nat ⇒ nat set" where "Jset K p =
{1..Nof K} ∪ {..mHalf p}"
definition kexp :: "nat ⇒ nat ⇒ nat ⇒ nat ×
nat ⇒ nat × nat ⇒ nat ⇒ nat" where
"kexp K M p x y j = 6 * (if j ∈ {1..Nof K} then 1 else 0) + nu K M p x j + nu K M p y j"
text ‹Multiplicity of a class: 2 for the zero class, 1 otherwise.›
definition mult :: "nat ⇒ nat" where "mult c = (if c = 0 then 2 else 1)"
lemma mem_inner_idx:
"x ∈ set (inner_idx K M p) ⟷ fst x ≤ mHalf p ∧
snd x < nat (Lin K M p (fst x))"
by (cases x) (auto simp: inner_idx_def image_iff simp del: upt_Suc)
lemma innerBasis_eq_prod:
assumes "fst x ≤ mHalf p"
shows "innerBasis K M p x = (∏ j ≤ mHalf p. (pX + [:of_nat j ^ 2:]) ^ nu K M p x j)"
proof -
have a: "fst x ∈ {..mHalf p}" using assms by simp
have n: "nu K M p x (fst x) = snd x" using assms by (simp add: nu_def)
have c: "(∏ j ∈ {..mHalf p} - {fst x}. (pX + [:of_nat j ^ 2:]) ^ nu K M p x j) =
(∏ c ∈ {0..mHalf p} - {fst x}. (pX + [:of_nat c ^ 2:]) ^ nat (Lin K M p c))"
by (rule prod.cong) (auto simp: nu_def)
show ?thesis unfolding innerBasis_def prod.remove[OF finite_atMost a] n c by (rule mult.commute)
qed
lemma numerator_eq:
assumes "fst x ≤ mHalf p" "fst y ≤ mHalf p"
shows "Dm (Nof K) ^ 6 * innerBasis K M p x * innerBasis K M p y =
(∏ j ∈ Jset K p. (pX + [:of_nat j ^ 2:]) ^ kexp K M p x y j)"
proof -
have fin: "finite (Jset K p)" by (simp add: Jset_def)
have e1: "(∏ j ∈ Jset K p. (pX + [:of_nat j ^ 2:]) ^ (6 * (if j ∈
{1..Nof K} then 1 else 0))) = Dm (Nof K) ^ 6"
proof -
have "(∏ j ∈ Jset K p. (pX + [:of_nat j ^ 2:]) ^ (6 * (if j ∈
{1..Nof K} then 1 else 0))) =
(∏ j = 1..Nof K. (pX + [:of_nat j ^ 2:]) ^ 6)"
by (rule prod.mono_neutral_cong_right[OF fin]) (auto simp: Jset_def)
also have "… = Dm (Nof K) ^ 6" unfolding Dm_def by (rule prod_power_distrib[symmetric])
finally show ?thesis .
qed
have e2: "(∏ j ∈ Jset K p. (pX + [:of_nat j ^ 2:]) ^ nu K M p z j) =
innerBasis K M p z" if "fst z ≤ mHalf p" for z
proof -
have "(∏ j ∈ Jset K p. (pX + [:of_nat j ^ 2:]) ^ nu K M p z j) = (∏ j ≤
mHalf p. (pX + [:of_nat j ^ 2:]) ^ nu K M p z j)"
by (rule prod.mono_neutral_cong_right[OF fin]) (auto simp: Jset_def nu_def)
also have "… = innerBasis K M p z" by (rule innerBasis_eq_prod[OF that, symmetric])
finally show ?thesis .
qed
have "(∏ j ∈ Jset K p. (pX + [:of_nat j ^ 2:]) ^ kexp K M p x y j) =
(∏ j ∈ Jset K p. (pX + [:of_nat j ^ 2:]) ^ (6 * (if j ∈
{1..Nof K} then 1 else 0))) *
(∏ j ∈ Jset K p. (pX + [:of_nat j ^ 2:]) ^ nu K M p x j) * (∏ j ∈
Jset K p. (pX + [:of_nat j ^ 2:]) ^ nu K M p y j)"
unfolding kexp_def power_add prod.distrib ..
thus ?thesis unfolding e1 e2[OF assms(1)] e2[OF assms(2)] by (rule sym)
qed
lemma cls_le: "odd p ⟹ cls p j ≤ mHalf p"
proof -
assume "odd p"
then obtain m where pm: "p = 2 * m + 1" by (elim oddE)
have "j mod p < p" using pm by simp
thus ?thesis unfolding cls_def mHalf_def pm by (auto simp: min_def)
qed
lemma cls_small: "odd p ⟹ j ≤ mHalf p ⟹ cls p j = j"
proof -
assume "odd p" and j: "j ≤ mHalf p"
then obtain m where pm: "p = 2 * m + 1" by (elim oddE)
have "j ≤ m" using j unfolding mHalf_def pm by simp
thus ?thesis unfolding cls_def pm by (simp add: min_def)
qed
lemma mod_add_zero_iff_aux:
fixes r c p :: nat
assumes "r < p" "c < p"
shows "(r + c) mod p = 0 ⟷ r + c = 0 ∨ r + c = p"
proof (cases "r + c < p")
case True
thus ?thesis by simp
next
case False
hence "(r + c) mod p = (r + c - p) mod p" by (simp add: le_mod_geq)
also have "… = r + c - p" using assms by simp
finally show ?thesis using False by auto
qed
lemma cls_eq_iff:
assumes "odd p" "a ≤ mHalf p"
shows "cls p j = a ⟷ j mod p = a ∨ j mod p + a = p"
proof -
obtain m where pm: "p = 2 * m + 1" using assms(1) by (elim oddE)
have "j mod p < p" using pm by simp
moreover have "a ≤ m" using assms(2) unfolding mHalf_def pm by simp
ultimately show ?thesis unfolding cls_def pm by (auto simp: min_def)
qed
lemma omg_eq:
assumes "odd p" "c < p"
shows "omg p c j = (if cls p j = cls p c then mult c else 0)"
proof -
have p0: "0 < p" using assms(2) by simp
define r where "r = j mod p"
have r: "r < p" using p0 by (simp add: r_def)
have d1: "int p dvd (int j - int c) ⟷ r = c"
proof -
have "int p dvd (int j - int c) ⟷ int j mod int p = int c mod int p"
by (simp add: mod_eq_dvd_iff)
also have "… ⟷ j mod p = c mod p"
by (simp only: of_nat_mod[symmetric] of_nat_eq_iff)
finally show ?thesis using assms(2) by (simp add: r_def)
qed
have d2: "int p dvd (int j + int c) ⟷ r + c = 0 ∨ r + c = p"
proof -
have "int p dvd (int j + int c) ⟷ p dvd (j + c)"
by (metis int_dvd_int_iff of_nat_add)
also have "… ⟷ (r + c) mod p = 0"
by (simp add: r_def dvd_eq_mod_eq_0 mod_add_left_eq)
also have "… ⟷ r + c = 0 ∨ r + c = p"
by (rule mod_add_zero_iff_aux[OF r assms(2)])
finally show ?thesis .
qed
have np: "c + c ≠ p" using assms(1) by presburger
have cj: "cls p j = min r (p - r)" by (simp add: cls_def r_def)
have cc: "cls p c = min c (p - c)" using assms(2) by (simp add: cls_def)
show ?thesis unfolding omg_def d1 d2 cj cc mult_def using r assms(2) np by (auto simp: min_def)
qed
lemma sum_omg:
assumes "odd p" "c < p"
shows "(∑ j = 1..A. omg p c j) = mult c * ell p A (cls p c)"
proof -
have p0: "0 < p" using assms(2) by simp
define a where "a = cls p c"
have am: "a ≤ mHalf p" unfolding a_def by (rule cls_le[OF assms(1)])
have ap: "a < p" using am p0 by (simp add: mHalf_def)
have m2: "(j + a) mod p = 0 ⟷ j mod p + a = 0 ∨ j mod p + a = p" for j
using mod_add_zero_iff_aux[OF _ ap, of "j mod p"] p0 by (simp add: mod_add_left_eq)
have S: "{j ∈ {1..A}. cls p j = a} = {j ∈ {1..A}. j mod p = a mod p ∨
(j + a) mod p = 0}"
using cls_eq_iff[OF assms(1) am] m2 ap by auto
have "(∑ j = 1..A. omg p c j) = (∑ j ∈ {j ∈ {1..A}. cls p j = a}. mult c)"
unfolding omg_eq[OF assms] a_def sum.inter_filter[OF finite_atLeastAtMost] ..
also have "… = mult c * card {j ∈ {1..A}. cls p j = a}" by simp
also have "… = mult c * ell p A (cls p c)" unfolding S unfolding ell_def a_def ..
finally show ?thesis .
qed
lemma nearCount_eq:
assumes "prime p"
shows "nearCount p K c = (∑ j = 1..K. omg p c j)"
proof -
have n: "int p dvd (- int j - int c) ⟷ int p dvd (int j + int c)" for j
proof -
have eq: "- int j - int c = - (int j + int c)" by simp
show ?thesis unfolding eq dvd_minus_iff ..
qed
have U: "{r ∈ int ` {1..K} ∪ (λj. - int j) ` {1..K}. int p dvd (r - int c)} =
int ` {j ∈ {1..K}. int p dvd (int j - int c)} ∪ (λj. - int j) ` {j ∈
{1..K}. int p dvd (int j + int c)}"
using n by auto
have c1: "card (int ` {j ∈ {1..K}. P j}) = card {j ∈ {1..K}. P j}" for P
by (rule card_image) (simp add: inj_on_def)
have c2: "card ((λj. - int j) ` {j ∈ {1..K}. P j}) = card {j ∈ {1..K}. P j}" for P
by (rule card_image) (simp add: inj_on_def)
have ind: "(∑ j ∈ {1..K}. (if P j then 1 else 0 :: nat)) = card {j ∈ {1..K}. P j}"
for P
by (simp add: sum.inter_filter[OF finite_atLeastAtMost, symmetric])
have "nearCount p K c = card (int ` {j ∈ {1..K}. int p dvd (int j - int c)} ∪
(λj. - int j) ` {j ∈ {1..K}. int p dvd (int j + int c)})"
unfolding nearCount_def signedPoles_def U ..
also have "… = card (int ` {j ∈ {1..K}. int p dvd (int j - int c)}) +
card ((λj. - int j) ` {j ∈ {1..K}. int p dvd (int j + int c)})"
by (rule card_Un_disjoint; force+)
also have "… = card {j ∈ {1..K}. int p dvd (int j - int c)} + card {j ∈
{1..K}. int p dvd (int j + int c)}"
unfolding c1 c2 ..
also have "… = (∑ j = 1..K. omg p c j)" unfolding omg_def sum.distrib ind ..
finally show ?thesis .
qed
lemma cls_zero: "cls p 0 = 0"
by (simp add: cls_def)
lemma cls_pos: "c ≠ 0 ⟹ c < p ⟹ 1 ≤ cls p c"
by (simp add: cls_def)
lemma ell_zero_eq: "0 < p ⟹ ell p A 0 = A div p"
proof -
assume p: "0 < p"
have e: "{j ∈ {1..A}. j mod p = 0 mod p ∨ (j + 0) mod p = 0} = {j ∈ {1..A}. p dvd j}"
by (auto simp: dvd_eq_mod_eq_0)
show ?thesis unfolding ell_def e by (rule card_multiples_upto[OF p])
qed
lemma eNum_eq:
assumes "odd p" "c < p"
shows "eNum p c (Jset K p) (kexp K M p x y) =
5 * (if c = 0 then 1 else 0) +
mult c * (6 * ell p (Nof K) (cls p c) + nu K M p x (cls p c) + nu K M p y (cls p c))"
proof -
have fin: "finite (Jset K p)" by (simp add: Jset_def)
have dc: "int p dvd int c ⟷ c = 0" using assms(2) by (auto dest: dvd_imp_le)
have s1: "(∑ j ∈ Jset K p. (if j ∈ {1..Nof K} then 1 else 0) * omg p c j) =
mult c * ell p (Nof K) (cls p c)"
proof -
have "(∑ j ∈ Jset K p. (if j ∈ {1..Nof K} then 1 else 0) * omg p c j) = (∑ j =
1..Nof K. omg p c j)"
by (rule sum.mono_neutral_cong_right[OF fin]) (auto simp: Jset_def)
also have "… = mult c * ell p (Nof K) (cls p c)" by (rule sum_omg[OF assms])
finally show ?thesis .
qed
have s2: "(∑ j ∈ Jset K p. nu K M p z j * omg p c j) = nu K M p z (cls p c) * mult c"
for z
proof -
have "(∑ j ∈ Jset K p. nu K M p z j * omg p c j) = (∑ j ≤ mHalf p.
if j = cls p c then nu K M p z j * mult c else 0)"
by (rule sum.mono_neutral_cong_right[OF fin]) (auto simp: Jset_def nu_def omg_eq[OF assms]
cls_small[OF assms(1)])
also have "… = nu K M p z (cls p c) * mult c" using cls_le[OF assms(1), of c] by simp
finally show ?thesis .
qed
have "eNum p c (Jset K p) (kexp K M p x y) = 5 * (if int p dvd int c then 1 else 0) +
(6 * (∑ j ∈ Jset K p. (if j ∈ {1..Nof K} then 1 else 0) * omg p c j) +
(∑ j ∈ Jset K p. nu K M p x j * omg p c j) + (∑ j ∈
Jset K p. nu K M p y j * omg p c j))"
unfolding eNum_def kexp_def by (simp add: sum.distrib sum_distrib_left algebra_simps)
also have "… = 5 * (if c = 0 then 1 else 0) +
mult c * (6 * ell p (Nof K) (cls p c) + nu K M p x (cls p c) + nu K M p y (cls p c))"
unfolding s1 s2 dc by (simp add: algebra_simps)
finally show ?thesis .
qed
lemma count_mod_ge: "0 < p ⟹ 1 ≤ r ⟹ r < p ⟹
A div p ≤ card {j ∈ {1..A}. j mod p = r}"
proof -
assume p: "0 < p" and r1: "1 ≤ r" and rp: "r < p"
have sub: "(λt. t * p + r) ` {..<A div p} ⊆ {j ∈ {1..A}. j mod p = r}"
proof
fix j assume "j ∈ (λt. t * p + r) ` {..<A div p}"
then obtain t where t: "t < A div p" "j = t * p + r" by blast
have "Suc t * p ≤ A div p * p" using t(1) by (intro mult_le_mono1) simp
also have "… ≤ A" by (rule div_times_less_eq_dividend)
finally have "t * p + p ≤ A" by simp
thus "j ∈ {j ∈ {1..A}. j mod p = r}" using t r1 rp by simp
qed
have inj: "inj_on (λt. t * p + r) {..<A div p}" using p by (auto intro: inj_onI)
have "card ((λt. t * p + r) ` {..<A div p}) ≤ card {j ∈ {1..A}. j mod p = r}"
by (rule card_mono[OF _ sub]) simp
thus ?thesis using card_image[OF inj] by simp
qed
lemma count_mod_le: "0 < p ⟹ 1 ≤ r ⟹ r < p ⟹
card {j ∈ {1..A}. j mod p = r} ≤ A div p + 1"
proof -
assume p: "0 < p"
show ?thesis by (rule card_cong_class_le[OF p]) auto
qed
lemma ell_bounds:
assumes "odd p" "1 ≤ a" "a ≤ mHalf p"
shows "2 * (A div p) ≤ ell p A a ∧ ell p A a ≤ 2 * (A div p) + 2"
proof -
have p0: "0 < p" using assms(1) by (rule odd_pos)
have ap: "a < p" using assms(3) p0 by (simp add: mHalf_def)
have np: "a ≠ p - a" using assms(1) ap by presburger
have m: "(j + a) mod p = 0 ⟷ j mod p = p - a" for j
proof -
have r: "j mod p < p" using p0 by simp
have "(j + a) mod p = 0 ⟷ j mod p + a = 0 ∨ j mod p + a = p"
using mod_add_zero_iff_aux[OF r ap] by (simp add: mod_add_left_eq)
thus ?thesis using assms(2) ap r by auto
qed
have e: "{j ∈ {1..A}. j mod p = a mod p ∨ (j + a) mod p = 0} =
{j ∈ {1..A}. j mod p = a} ∪ {j ∈ {1..A}. j mod p = p - a}"
using m ap by auto
have "ell p A a = card {j ∈ {1..A}. j mod p = a} + card {j ∈ {1..A}. j mod p = p - a}"
unfolding ell_def e by (rule card_Un_disjoint) (use np in auto)
moreover have "A div p ≤ card {j ∈ {1..A}. j mod p = a}"
by (rule count_mod_ge[OF p0 assms(2) ap])
moreover have "A div p ≤ card {j ∈ {1..A}. j mod p = p - a}"
by (rule count_mod_ge[OF p0]) (use assms(2) ap in auto)
moreover have "card {j ∈ {1..A}. j mod p = a} ≤ A div p + 1"
by (rule count_mod_le[OF p0 assms(2) ap])
moreover have "card {j ∈ {1..A}. j mod p = p - a} ≤ A div p + 1"
by (rule count_mod_le[OF p0]) (use assms(2) ap in auto)
ultimately show ?thesis by linarith
qed
lemma hyp_facts:
assumes "prime p" "InnerHyp K M p"
shows "7 ≤ p ∧ odd p ∧ 2 * mHalf p + 1 = p ∧ K div p < M ∧
Nof K div p < M"
proof -
have b: "200 * M < p" using innerHyp_bounds[OF assms(2)] by blast
have H: "40 ≤ M" "K < p * M" using assms(2) by (auto simp: InnerHyp_def)
have p7: "7 ≤ p" using b H by linarith
have o: "odd p" using prime_odd_nat[OF assms(1)] p7 by simp
have mp: "2 * mHalf p + 1 = p" using o unfolding mHalf_def by (auto elim: oddE)
have kd: "K div p < M" using H(2) p7 by (simp add: div_less_iff_less_mult mult.commute)
have "Nof K div p ≤ K div p" by (rule div_le_mono) (simp add: Nof_def)
hence "Nof K div p < M" using kd by linarith
with p7 o mp kd show ?thesis by simp
qed
lemma Tin_le:
assumes "prime p" "InnerHyp K M p"
shows "Tin K M p ≤ 4 * int M"
proof -
have T0: "0 ≤ Ein K M p" and Em: "int (mHalf p) * Tin K M p + Ein K M p = rhs44 K M p"
using TE_spec[OF assms] by blast+
have H: "40 ≤ M" "40 dvd K" "200 * M ^ 2 ≤ K" "K < p * M" using assms(2)
by (auto simp: InnerHyp_def)
obtain k where Kk: "K = 40 * k" using H(2) by (elim dvdE)
have hk: "hof K = 37 * k" and Nk: "Nof K = 3 * k" unfolding Kk hof_def Nof_def by simp_all
have r44: "rhs44 K M p ≤ 46 * int k" unfolding rhs44_def hk Nk L0_def by simp
have mp: "2 * mHalf p + 1 = p" using hyp_facts[OF assms] by blast
define m where "m = int (mHalf p)"
have m0: "0 ≤ m" by (simp add: m_def)
have ip: "int p = 2 * m + 1" unfolding m_def using mp by linarith
have pM: "int p * int M = 2 * (m * int M) + int M" unfolding ip by (simp add: algebra_simps)
have "int K < int (p * M)" using H(4) by (simp only: of_nat_less_iff)
hence KpM: "40 * int k < int p * int M" unfolding Kk by simp
have "M ≤ M * M" by (rule le_square)
hence "M ≤ k" using H(3) Kk unfolding power2_eq_square by linarith
hence kM: "int M ≤ int k" by simp
show ?thesis
proof (rule ccontr)
assume "¬ Tin K M p ≤ 4 * int M"
hence "4 * int M + 1 ≤ Tin K M p" by simp
hence "m * (4 * int M + 1) ≤ m * Tin K M p" using m0 by (rule mult_left_mono)
hence "4 * (m * int M) + m ≤ m * Tin K M p" by (simp add: algebra_simps)
moreover have "m * Tin K M p ≤ 46 * int k" using Em T0 r44 unfolding m_def by linarith
ultimately show False using pM KpM kM m0 by linarith
qed
qed
lemma Lin_le:
assumes "prime p" "InnerHyp K M p" "a ≤ mHalf p"
shows "Lin K M p a ≤ 4 * int M + 10"
proof (cases "a = 0")
case True
thus ?thesis by (simp add: Lin_def L0_def)
next
case False
have "epsIn K M p a ≤ 1" by (simp add: epsIn_def)
moreover have "0 ≤ bIn K p a" by (simp add: bIn_def)
moreover have "Lin K M p a = Tin K M p - bIn K p a + epsIn K M p a" using False
by (simp add: Lin_def)
ultimately show ?thesis using Tin_le[OF assms(1,2)] by linarith
qed
lemma nu_le:
assumes "prime p" "InnerHyp K M p" "x ∈ set (inner_idx K M p)"
shows "nu K M p x j ≤ 4 * M + 10"
proof -
have m: "fst x ≤ mHalf p" "snd x < nat (Lin K M p (fst x))" using assms(3)
by (simp_all add: mem_inner_idx)
have l: "nat (Lin K M p a) ≤ 4 * M + 10" if "a ≤ mHalf p" for a
using Lin_le[OF assms(1,2) that] by (simp add: nat_le_iff)
show ?thesis unfolding nu_def using m l[of "fst x"] l[of j] by auto
qed
lemma ellN_le:
assumes "prime p" "InnerHyp K M p" "1 ≤ a" "a ≤ mHalf p"
shows "ell p (Nof K) a ≤ M"
proof -
have o: "odd p" using hyp_facts[OF assms(1,2)] by blast
have b: "ell p (Nof K) a ≤ 2 * (Nof K div p) + 2"
using ell_bounds[OF o assms(3,4), of "Nof K"] by blast
have H: "40 ≤ M" "K < p * M" using assms(2) by (auto simp: InnerHyp_def)
have N: "40 * Nof K ≤ 3 * K" by (simp add: Nof_def)
have q: "Nof K div p * p ≤ Nof K" by (rule div_times_less_eq_dividend)
have "p * (40 * (Nof K div p)) < p * (3 * M)"
proof -
have "p * (40 * (Nof K div p)) = 40 * (Nof K div p * p)" by (simp add: ac_simps)
also have "… ≤ 40 * Nof K" using q by simp
also have "… ≤ 3 * K" by (rule N)
also have "… < 3 * (p * M)" using H(2) by simp
also have "… = p * (3 * M)" by (simp add: ac_simps)
finally show ?thesis .
qed
hence "0 < p ∧ 40 * (Nof K div p) < 3 * M" by (simp only: mult_less_cancel1)
hence "40 * (Nof K div p) < 3 * M" by simp
thus ?thesis using b H(1) by linarith
qed
lemma eps_key:
assumes "prime p" "InnerHyp K M p" "a ∈ {1..mHalf p}" "b ∈ {1..mHalf p}"
shows "2 * (epsIn K M p a - epsIn K M p b) ≤ 2 + int (ell p K a) - int (ell p K b)"
proof -
define r where "r = (λx y. ell p K y < ell p K x ∨ (ell p K x = ell p K y ∧
x < y))"
have rk: "defaultPos K p x = card {c ∈ {1..mHalf p}. r c x}" for x
by (simp add: defaultPos_def r_def)
have irr: "⋀x. ¬ r x x" by (simp add: r_def)
have tr: "⋀x y z. r x y ⟹ r y z ⟹ r x z" unfolding r_def
by auto
have tot: "⋀x y. x ∈ {1..mHalf p} ⟹
y ∈ {1..mHalf p} ⟹ x ≠ y ⟹ r x y ∨ r y x"
unfolding r_def by auto
have iff: "defaultPos K p x < defaultPos K p y ⟷ r x y"
if "x ∈ {1..mHalf p}" "y ∈ {1..mHalf p}" for x y
unfolding rk using rank_props(1)[OF finite_atLeastAtMost irr tr tot that] .
have cnt: "card {c ∈ {1..mHalf p}. defaultPos K p c < defaultPos K p x} = defaultPos K p x"
if "x ∈ {1..mHalf p}" for x
proof -
have "{c ∈ {1..mHalf p}. defaultPos K p c < defaultPos K p x} = {c ∈
{1..mHalf p}. r c x}" using iff that by auto
thus ?thesis using rk[of x] by simp
qed
have ea: "epsIn K M p a = (if int (defaultPos K p a) < Ein K M p then 1 else 0)"
unfolding epsIn_def cnt[OF assms(3)] ..
have eb: "epsIn K M p b = (if int (defaultPos K p b) < Ein K M p then 1 else 0)"
unfolding epsIn_def cnt[OF assms(4)] ..
have o: "odd p" using hyp_facts[OF assms(1,2)] by blast
have ba: "2 * (K div p) ≤ ell p K a ∧ ell p K a ≤ 2 * (K div p) + 2"
using ell_bounds[OF o, of a K] assms(3) by auto
have bb: "2 * (K div p) ≤ ell p K b ∧ ell p K b ≤ 2 * (K div p) + 2"
using ell_bounds[OF o, of b K] assms(4) by auto
show ?thesis
proof (cases "int (defaultPos K p a) < Ein K M p ∧
¬ int (defaultPos K p b) < Ein K M p")
case True
hence "defaultPos K p a < defaultPos K p b" by linarith
hence "r a b" using iff assms(3,4) by blast
hence "ell p K b ≤ ell p K a" unfolding r_def by auto
hence "int (ell p K b) ≤ int (ell p K a)" by simp
thus ?thesis unfolding ea eb using True by simp
next
case False
thus ?thesis unfolding ea eb using ba bb by auto
qed
qed
text ‹Half-weight at an ordinary source @{text b}.›
lemma half_ord:
assumes "prime p" "InnerHyp K M p" "x ∈ set (inner_idx K M p)" "1 ≤ b" "b ≤ mHalf p"
shows "wInIdx K M p x ≤ of_nat (nu K M p x b) + 3 * of_nat (ell p (Nof K) b) -
(of_nat (ell p K b) + 4) / 2"
proof -
obtain a i where x: "x = (a, i)" by (cases x)
have m: "a ≤ mHalf p" "i < nat (Lin K M p a)" using assms(3) unfolding x
by (simp_all add: mem_inner_idx)
have bnz: "b ≠ 0" using assms(4) by simp
have "Lin K M p b = Tin K M p - bIn K p b + epsIn K M p b" using bnz by (simp add: Lin_def)
moreover have "0 ≤ Lin K M p b" by (rule Lin_nonneg[OF assms(1,2,5)])
ultimately have ratLb: "(of_nat (nat (Lin K M p b)) :: rat) =
of_int (Tin K M p) - 3 * of_nat (ell p (Nof K) b) + of_int (epsIn K M p b)"
by (simp add: bIn_def)
show ?thesis
proof (cases "a = 0")
case True
have "wInIdx K M p x ≤ of_int (Zin K M p b) - (of_nat (ell p K b) + 4) / 2"
unfolding wInIdx_def x fst_conv snd_conv wIn_def if_P[OF True]
by (rule Min_le) (use assms(4,5) in auto)
moreover have "(of_nat (nu K M p x b) :: rat) =
of_int (Tin K M p) - 3 * of_nat (ell p (Nof K) b) + of_int (epsIn K M p b)"
unfolding x nu_def using True assms(5) bnz ratLb by simp
moreover have "(of_int (Zin K M p b) :: rat) = of_int (Tin K M p) + of_int (epsIn K M p b)"
by (simp add: Zin_def)
ultimately show ?thesis by linarith
next
case False
show ?thesis
proof (cases "a = b")
case True
show ?thesis unfolding wInIdx_def x fst_conv snd_conv wIn_def using True bnz
by (simp add: bIn_def nu_def assms(5))
next
case ab: False
have a1: "a ∈ {1..mHalf p}" using False m(1) by simp
have b1: "b ∈ {1..mHalf p}" using assms(4,5) by simp
have La: "Lin K M p a = Tin K M p - bIn K p a + epsIn K M p a" using False
by (simp add: Lin_def)
have "int i + 1 ≤ Lin K M p a" using m(2) by arith
hence r1: "rat_of_int (int i + 1) ≤ rat_of_int (Tin K M p - bIn K p a + epsIn K M p a)"
unfolding La by (simp only: of_int_le_iff)
have "2 * (epsIn K M p a - epsIn K M p b) ≤ 2 + int (ell p K a) - int (ell p K b)"
by (rule eps_key[OF assms(1,2) a1 b1])
hence r2: "rat_of_int (2 * (epsIn K M p a - epsIn K M p b)) ≤
rat_of_int (2 + int (ell p K a) - int (ell p K b))"
by (simp only: of_int_le_iff)
have w: "wInIdx K M p x = of_nat i + 3 * of_nat (ell p (Nof K) a) - (of_nat (ell p K a) + 4) /
2"
unfolding wInIdx_def x fst_conv snd_conv wIn_def using False by (simp add: bIn_def)
have nb: "(of_nat (nu K M p x b) :: rat) =
of_int (Tin K M p) - 3 * of_nat (ell p (Nof K) b) + of_int (epsIn K M p b)"
unfolding x nu_def using ab assms(5) ratLb by simp
have "of_nat i + 1 ≤ (of_int (Tin K M p) - 3 * of_nat (ell p (Nof K) a) +
of_int (epsIn K M p a) :: rat)"
using r1 by (simp add: bIn_def)
moreover have "2 * (of_int (epsIn K M p a) - of_int (epsIn K M p b)) ≤
(2 + of_nat (ell p K a) - of_nat (ell p K b) :: rat)"
using r2 by simp
ultimately show ?thesis unfolding w nb
by (simp only: distrib_left right_diff_distrib add_divide_distrib diff_divide_distrib;
linarith)
qed
qed
qed
text ‹Half-weight at the zero source.›
lemma half_zero:
assumes "prime p" "InnerHyp K M p" "x ∈ set (inner_idx K M p)"
shows "wInIdx K M p x ≤ 2 * of_nat (nu K M p x 0) + 6 * of_nat (Nof K div p) -
of_nat (K div p) + 1 / 2"
proof -
obtain a i where x: "x = (a, i)" by (cases x)
have m: "a ≤ mHalf p" "i < nat (Lin K M p a)" using assms(3) unfolding x
by (simp_all add: mem_inner_idx)
show ?thesis
proof (cases "a = 0")
case True
have w: "wInIdx K M p x ≤ 2 * of_nat i + 6 * of_nat (Nof K div p) - of_nat (K div p) + 1 /
2"
unfolding wInIdx_def x fst_conv snd_conv wIn_def if_P[OF True] by (rule Min_le) auto
have n: "nu K M p x 0 = i" unfolding x nu_def using True by simp
show ?thesis using w unfolding n .
next
case False
have Tl: "Tin K M p ≤ 4 * int M" by (rule Tin_le[OF assms(1,2)])
have e: "epsIn K M p a ≤ 1" by (simp add: epsIn_def)
have L: "Lin K M p a = Tin K M p - bIn K p a + epsIn K M p a" using False by (simp add: Lin_def)
have iL: "int i + 1 ≤ Lin K M p a" using m(2) by arith
have n0: "nu K M p x 0 = 4 * M + 10" unfolding x nu_def using False
by (simp add: Lin_def L0_def)
have Kq: "K div p < M" using hyp_facts[OF assms(1,2)] by blast
have w: "wInIdx K M p x = of_nat i + of_int (bIn K p a) - (of_nat (ell p K a) + 4) / 2"
unfolding wInIdx_def x fst_conv snd_conv wIn_def using False by simp
have r1: "rat_of_int (int i + 1) ≤ rat_of_int (Tin K M p - bIn K p a + epsIn K M p a)"
using iL unfolding L by (simp only: of_int_le_iff)
have r2: "rat_of_int (Tin K M p) ≤ rat_of_int (4 * int M)" using Tl
by (simp only: of_int_le_iff)
have r3: "rat_of_int (epsIn K M p a) ≤ rat_of_int 1" using e by (simp only: of_int_le_iff)
have r4: "(of_nat (K div p) :: rat) ≤ of_nat M" using Kq by simp
have r5: "(0 :: rat) ≤ of_nat (ell p K a)" "(0 :: rat) ≤ of_nat (Nof K div p)"
by simp_all
have c4: "(of_nat (4 * M + 10) :: rat) = 4 * of_nat M + 10" by simp
have r6: "(0 :: rat) ≤ of_nat M" "(0 :: rat) ≤ of_nat i" by simp_all
show ?thesis unfolding w n0 c4 using r1 r2 r3 r4 r5 r6
by (simp only: of_int_add of_int_diff of_int_mult of_int_of_nat_eq of_int_1 of_int_numeral
distrib_left right_diff_distrib add_divide_distrib diff_divide_distrib; linarith)
qed
qed
text ‹(4.2)/(4.3): every entry of the inner Gram matrix satisfies the weights.›
theorem innerGram_entry_bound:
assumes p: "prime p" and H: "InnerHyp K M p" and x: "x < length (inner_idx K M p)" and y: "y <
length (inner_idx K M p)"
shows "vpGge p (innerGram K M p $$ (x, y))
(wInIdx K M p (inner_idx K M p ! x) + wInIdx K M p (inner_idx K M p ! y))"
proof -
define ix where "ix = inner_idx K M p ! x"
define iy where "iy = inner_idx K M p ! y"
have ixs: "ix ∈ set (inner_idx K M p)" and iys: "iy ∈ set (inner_idx K M p)"
by (simp_all add: ix_def iy_def x y)
obtain p7: "7 ≤ p" and oddp: "odd p" and NpM: "Nof K div p < M"
using hyp_facts[OF p H] by blast
have K1: "2 * K < p ^ 2" and K2: "K + p < p ^ 2"
proof -
have b: "200 * M < p ∧ 5 * K < p ^ 2" by (rule innerHyp_bounds[OF H])
have KM: "K < p * M" using H by (simp add: InnerHyp_def)
have "p * (M + 1) ≤ p * p" using b by (intro mult_le_mono2) linarith
moreover have "p * (M + 1) = p * M + p" by simp
ultimately have "K + p < p * p" using KM by linarith
thus "K + p < p ^ 2" by (simp add: power2_eq_square)
show "2 * K < p ^ 2" using b by linarith
qed
have entry: "innerGram K M p $$ (x, y) = muX {1..K} (∏ j ∈
Jset K p. (pX + [:of_nat j ^ 2:]) ^ kexp K M p ix iy j)"
using x y numerator_eq[of ix p iy K M] mem_inner_idx[of ix K M p] mem_inner_idx[of iy K M p] ixs
iys
by (simp add: innerGram_def Let_def ix_def iy_def mult.assoc)
define B where "B = wInIdx K M p ix + wInIdx K M p iy"
have hB: "⋀c. c < p ⟹
B + 4 ≤ of_nat (eNum p c (Jset K p) (kexp K M p ix iy)) - of_nat (nearCount p K c)"
proof -
fix c assume c: "c < p"
have nc: "nearCount p K c = mult c * ell p K (cls p c)"
by (simp only: nearCount_eq[OF p] sum_omg[OF oddp c])
show "B + 4 ≤ of_nat (eNum p c (Jset K p) (kexp K M p ix iy)) - of_nat (nearCount p K c)"
proof (cases "c = 0")
case True
have hx: "wInIdx K M p ix ≤ 2 * of_nat (nu K M p ix 0) + 6 * of_nat (Nof K div p) -
of_nat (K div p) + 1 / 2"
and hy: "wInIdx K M p iy ≤ 2 * of_nat (nu K M p iy 0) + 6 * of_nat (Nof K div p) -
of_nat (K div p) + 1 / 2"
by (rule half_zero[OF p H ixs]) (rule half_zero[OF p H iys])
have e: "of_nat (eNum p c (Jset K p) (kexp K M p ix iy)) - of_nat (nearCount p K c) =
(5 + 2 * (6 * of_nat (Nof K div p) + of_nat (nu K M p ix 0) + of_nat (nu K M p iy 0)) -
2 * of_nat (K div p) :: rat)"
unfolding eNum_eq[OF oddp c] nc using True
by (simp add: cls_zero mult_def ell_zero_eq[OF prime_gt_0_nat[OF p]])
show ?thesis unfolding B_def e using hx hy
by (simp only: distrib_left right_diff_distrib add_divide_distrib diff_divide_distrib;
linarith)
next
case False
have cls_ge1: "1 ≤ cls p c" using cls_pos[OF False c] .
have cls_le_half: "cls p c ≤ mHalf p" using cls_le[OF oddp] .
have hx: "wInIdx K M p ix ≤ of_nat (nu K M p ix (cls p c)) + 3 *
of_nat (ell p (Nof K) (cls p c)) - (of_nat (ell p K (cls p c)) + 4) / 2"
and hy: "wInIdx K M p iy ≤ of_nat (nu K M p iy (cls p c)) + 3 *
of_nat (ell p (Nof K) (cls p c)) - (of_nat (ell p K (cls p c)) + 4) / 2"
by (rule half_ord[OF p H ixs cls_ge1 cls_le_half]) (rule half_ord[OF p H iys cls_ge1
cls_le_half])
have e: "of_nat (eNum p c (Jset K p) (kexp K M p ix iy)) - of_nat (nearCount p K c) =
(6 * of_nat (ell p (Nof K) (cls p c)) + of_nat (nu K M p ix (cls p c)) +
of_nat (nu K M p iy (cls p c))
- of_nat (ell p K (cls p c)) :: rat)"
unfolding eNum_eq[OF oddp c] nc using False by (simp add: mult_def)
show ?thesis unfolding B_def e using hx hy
by (simp only: distrib_left right_diff_distrib add_divide_distrib diff_divide_distrib;
linarith)
qed
qed
have hdeg: "⋀c. c < p ⟹ eNum p c (Jset K p) (kexp K M p ix iy) ≤ p + 1"
proof -
fix c assume c: "c < p"
have b: "200 * M < p" using innerHyp_bounds[OF H] by blast
have M40: "40 ≤ M" using H by (simp add: InnerHyp_def)
have nx: "nu K M p ix (cls p c) ≤ 4 * M + 10" by (rule nu_le[OF p H ixs])
have ny: "nu K M p iy (cls p c) ≤ 4 * M + 10" by (rule nu_le[OF p H iys])
have el: "ell p (Nof K) (cls p c) ≤ M"
proof (cases "c = 0")
case True
thus ?thesis using NpM by (simp add: cls_zero ell_zero_eq[OF prime_gt_0_nat[OF p]])
next
case False
show ?thesis by (rule ellN_le[OF p H cls_pos[OF False c] cls_le[OF oddp]])
qed
show "eNum p c (Jset K p) (kexp K M p ix iy) ≤ p + 1"
proof (cases "c = 0")
case True
have "eNum p c (Jset K p) (kexp K M p ix iy) =
5 + 2 * (6 * ell p (Nof K) (cls p c) + nu K M p ix (cls p c) + nu K M p iy (cls p c))"
unfolding eNum_eq[OF oddp c] using True by (simp add: mult_def)
thus ?thesis using nx ny el b M40 by fastforce
next
case False
have "eNum p c (Jset K p) (kexp K M p ix iy) =
6 * ell p (Nof K) (cls p c) + nu K M p ix (cls p c) + nu K M p iy (cls p c)"
unfolding eNum_eq[OF oddp c] using False by (simp add: mult_def)
thus ?thesis using nx ny el b M40 by arith
qed
qed
show ?thesis
unfolding entry ix_def[symmetric] iy_def[symmetric] B_def[symmetric]
by (rule entry_generic[OF p p7 K1 K2 _ hB hdeg]) (simp add: Jset_def)
qed
text ‹Multiplying by a @{text p}-adic unit does not change Gauss-valuation bounds.›
lemma vpGge_of_unit_mul:
assumes "prime p" "u ≠ 0" "vp p u = 0" "vpGge p ([:u:] * P) b"
shows "vpGge p P b"
proof -
have "prime (int p)" using assms(1) by (simp add: prime_nat_int_transfer)
hence pr: "prime_elem (int p)" by (rule prime_imp_prime_elem)
show ?thesis unfolding vpGge_def
proof (intro allI impI)
fix i assume c: "Polynomial.coeff P i ≠ 0"
have ne: "u * Polynomial.coeff P i ≠ 0" using assms(2) c by simp
have co: "Polynomial.coeff ([:u:] * P) i = u * Polynomial.coeff P i" by simp
have l: "b ≤ of_int (vp p (u * Polynomial.coeff P i))" using assms(4) ne
unfolding vpGge_def co[symmetric] by blast
have e: "vp p (u * Polynomial.coeff P i) = vp p (Polynomial.coeff P i)"
using qmultiplicity_mult[OF pr assms(2) c] assms(3) by (simp add: vp_def)
show "b ≤ of_int (vp p (Polynomial.coeff P i))" using l unfolding e .
qed
qed
text ‹@{text "∑_i (w (σ i) + w i) = 2 ∑_i w i"}
for a permutation @{text σ} of @{text "{0..<n}"}.›
lemma sum_permute_add:
assumes "σ permutes {0..<n}"
shows "(∑ i = 0..<n. w (σ i) + w i) = 2 * (∑ i = 0..<n. (w i :: rat))"
proof -
have "(∑ i = 0..<n. w (σ i)) = (∑ i = 0..<n. w i)"
using sum.permute[OF assms, of w] unfolding o_def by (rule sym)
thus ?thesis unfolding sum.distrib mult_2 by simp
qed
text ‹The Gram matrix of a basis @{text B} (rows =
coefficient vectors) is @{text "B G B^T"}, and its
determinant is @{text "det(B)^2 det(G)"};
a Gauss bound on the Gram determinant transfers to @{text "det G"}
when @{text "det B"} is a @{text p}-adic unit.›
lemma det_gram_transfer:
assumes p: "prime p" and G: "G ∈ carrier_mat n n" and B: "B ∈ carrier_mat n n"
and dB: "Determinant.det B ≠ 0" "vp p (Determinant.det B) = 0"
and gram: "vpGge p (Determinant.det (map_mat (λq. [:q:]) B * G *
transpose_mat (map_mat (λq. [:q:]) B))) b"
shows "vpGge p (Determinant.det G) b"
proof -
have "Determinant.det (map_mat (λq. [:q:]) B * G *
transpose_mat (map_mat (λq. [:q:]) B)) =
[:Determinant.det B ^ 2:] * Determinant.det G"
proof -
have Bp: "map_mat (λq. [:q:]) B ∈ carrier_mat n n" using B by simp
have Tc: "transpose_mat (map_mat (λq. [:q:]) B) ∈ carrier_mat n n" using Bp by simp
have BG: "map_mat (λq. [:q:]) B * G ∈ carrier_mat n n" using Bp G
by (rule mult_carrier_mat)
show ?thesis unfolding det_mult[OF BG Tc] det_mult[OF Bp G] det_transpose[OF Bp]
det_map_mat_C[OF B]
by (simp add: power2_eq_square mult_ac)
qed
thus ?thesis using gram vpGge_of_unit_mul[OF p, of "Determinant.det B ^ 2"] dB
by (metis power_not_zero dB(1) dB(2) vp_power_rat[OF p dB(1), of 2] mult_zero_right)
qed
text ‹@{text "γ_p^in = 2 ∑_{x ∈ idx} w_x"},
the double sum written over the index list.›
lemma sum_list_concat_aux: "sum_list (concat xss) =
sum_list (map sum_list (xss :: 'a :: monoid_add list list))"
by (induction xss) simp_all
lemma gammaIn_eq_sum_idx:
"gammaIn K M p = 2 * (∑ x < length (inner_idx K M p). wInIdx K M p (inner_idx K M p ! x))"
proof -
have "sum_list (map (wInIdx K M p) (inner_idx K M p)) =
(∑ x < length (inner_idx K M p). wInIdx K M p (inner_idx K M p ! x))"
by (simp add: sum_list_sum_nth atLeast0LessThan)
moreover have "sum_list (map (wInIdx K M p) (inner_idx K M p)) = (∑ a ≤
mHalf p. ∑ i < nat (Lin K M p a). wIn K M p a i)"
unfolding inner_idx_def map_concat sum_list_concat_aux map_map
by (simp add: o_def wInIdx_def interv_sum_list_conv_sum_set_nat atLeast0LessThan
lessThan_Suc_atMost del: upt_Suc)
ultimately show ?thesis unfolding gammaIn_def by simp
qed
lemma degree_innerBasis_lt:
assumes "prime p" "InnerHyp K M p" "x ∈ set (inner_idx K M p)"
shows "degree (innerBasis K M p x) < hof K"
proof -
obtain a i where x: "x = (a, i)" by (cases x)
have a: "a ≤ mHalf p" and i: "i < nat (Lin K M p a)" using assms(3) unfolding x
by (simp_all add: mem_inner_idx)
have tot: "(∑ c ≤ mHalf p. nat (Lin K M p c)) = hof K"
proof -
have "int (∑ c ≤ mHalf p. nat (Lin K M p c)) = (∑ c ≤ mHalf p. Lin K M p c)"
unfolding of_nat_sum by (rule sum.cong) (use Lin_nonneg[OF assms(1,2)] in auto)
also have "… = int (hof K)" by (rule sum_Lin[OF assms(1,2)])
finally show ?thesis by (simp only: of_nat_eq_iff)
qed
have rem: "(∑ c ≤ mHalf p. nat (Lin K M p c)) = nat (Lin K M p a) + (∑ c ∈
{0..mHalf p} - {a}. nat (Lin K M p c))"
proof -
have e: "{..mHalf p} = {0..mHalf p}" by auto
show ?thesis unfolding e using a by (simp add: sum.remove)
qed
have d1: "degree (∏ c ∈ {0..mHalf p} - {a}. (pX +
[:of_nat c ^ 2:]) ^ nat (Lin K M p c)) ≤
(∑ c ∈ {0..mHalf p} - {a}. nat (Lin K M p c))"
proof -
have "degree (∏ c ∈ {0..mHalf p} - {a}. (pX +
[:of_nat c ^ 2:]) ^ nat (Lin K M p c)) ≤
(∑ c ∈ {0..mHalf p} - {a}. degree ((pX + [:of_nat c ^ 2:]) ^ nat (Lin K M p c)))"
using degree_prod_sum_le[of "{0..mHalf p} - {a}" "λc. (pX +
[:of_nat c ^ 2:]) ^ nat (Lin K M p c)"]
by (simp add: o_def)
also have "… ≤ (∑ c ∈ {0..mHalf p} - {a}. nat (Lin K M p c))"
proof (rule sum_mono)
fix c
show "degree ((pX + [:of_nat c ^ 2:]) ^ nat (Lin K M p c)) ≤ nat (Lin K M p c)"
using degree_power_le[of "pX + [:of_nat c ^ 2:]" "nat (Lin K M p c)"]
unfolding degree_pX_plus_const by simp
qed
finally show ?thesis .
qed
have d2: "degree ((pX + [:of_nat a ^ 2:]) ^ i) ≤ i"
using degree_power_le[of "pX + [:of_nat a ^ 2:]" i] unfolding degree_pX_plus_const by simp
have "degree (innerBasis K M p x) ≤ (∑ c ∈
{0..mHalf p} - {a}. nat (Lin K M p c)) + i"
unfolding innerBasis_def x fst_conv snd_conv using degree_mult_le d1 d2
by (meson add_le_mono order_trans)
thus ?thesis using tot rem i by linarith
qed
text ‹The inner Gram matrix is @{text "B G_K B^T"}
for the coefficient matrix @{text B} of the inner basis.›
lemma innerGram_eq_conj:
assumes p: "prime p" and H: "InnerHyp K M p"
defines "B ≡ Matrix.mat (hof K) (hof K) (λ(x,
d). Polynomial.coeff (innerBasis K M p (inner_idx K M p ! x)) d)"
shows "innerGram K M p = map_mat (λq. [:q:]) B * GK K *
transpose_mat (map_mat (λq. [:q:]) B)"
proof -
let ?h = "hof K" and ?idx = "inner_idx K M p"
let ?Q = "map_mat (λq. [:q:]) B"
have len: "length ?idx = ?h" by (rule length_inner_idx[OF p H])
have dB: "dim_row B = ?h" "dim_col B = ?h" by (simp_all add: B_def)
have dG: "dim_row (GK K) = ?h" "dim_col (GK K) = ?h" by (simp_all add: GK_def)
have sm: "muX S (Polynomial.smult a P) = Polynomial.smult a (muX S P)" for S a P
using muX_C_mul[of S a P] by simp
have qe: "innerBasis K M p (?idx ! x) = (∑ k < ?h. Polynomial.smult (B $$ (x, k)) (pX ^ k))"
if x: "x < ?h" for x
proof -
have dg: "degree (innerBasis K M p (?idx ! x)) ≤ ?h - 1"
using degree_innerBasis_lt[OF p H, of "?idx ! x"] x len by simp
have e: "{..?h - 1} = {..<?h}" using x by auto
have "innerBasis K M p (?idx ! x) =
(∑ k ≤ ?h - 1. Polynomial.monom (Polynomial.coeff (innerBasis K M p (?idx ! x)) k)
k)"
by (rule sym[OF poly_as_sum_of_monoms'[OF dg]])
also have "… = (∑ k < ?h. Polynomial.monom (Polynomial.coeff (innerBasis K M p (?idx
! x)) k) k)"
unfolding e ..
also have "… = (∑ k < ?h. Polynomial.smult (B $$ (x, k)) (pX ^ k))"
by (rule sum.cong[OF refl]) (use x in ‹unfold pX_pow_monom smult_monom,
simp add: B_def›)
finally show ?thesis .
qed
have pq: "Dm (Nof K) ^ 6 * innerBasis K M p (?idx ! x) * innerBasis K M p (?idx ! y) =
(∑ k < ?h. ∑ l < ?h. Polynomial.smult (B $$ (x, k) * B $$ (y,
l)) (Dm (Nof K) ^ 6 * pX ^ (k + l)))"
if x: "x < ?h" and y: "y < ?h" for x y
proof -
have pq0: "innerBasis K M p (?idx ! x) * innerBasis K M p (?idx ! y) = (∑ k <
?h. ∑ l < ?h.
Polynomial.smult (B $$ (x, k)) (pX ^ k) * Polynomial.smult (B $$ (y, l)) (pX ^ l))"
unfolding qe[OF x] qe[OF y] by (rule sum_product)
have "Dm (Nof K) ^ 6 * innerBasis K M p (?idx ! x) * innerBasis K M p (?idx ! y) =
Dm (Nof K) ^ 6 * (innerBasis K M p (?idx ! x) * innerBasis K M p (?idx ! y))"
by (simp only: mult.assoc)
also have "… = (∑ k < ?h. ∑ l <
?h. Polynomial.smult (B $$ (x, k) * B $$ (y, l)) (Dm (Nof K) ^ 6 * pX ^ (k + l)))"
unfolding pq0 sum_distrib_left by (intro sum.cong refl) (simp add: power_add mult_ac)
finally show ?thesis .
qed
have entry: "innerGram K M p $$ (x, y) = (?Q * GK K * transpose_mat ?Q) $$ (x, y)"
if x: "x < ?h" and y: "y < ?h" for x y
proof -
have "innerGram K M p $$ (x, y) =
muX {1..K} (Dm (Nof K) ^ 6 * innerBasis K M p (?idx ! x) * innerBasis K M p (?idx ! y))"
using x y len by (simp add: innerGram_def Let_def)
also have "… = (∑ k < ?h. ∑ l <
?h. [:B $$ (x, k):] * GK K $$ (k, l) * [:B $$ (y, l):])"
unfolding pq[OF x y] muX_sum sm by (intro sum.cong refl) (simp add: GK_def mult_ac)
also have "… = (?Q * GK K * transpose_mat ?Q) $$ (x, y)"
proof -
have m: "(?Q * GK K * transpose_mat ?Q) $$ (x, y) =
(∑ l < ?h. (∑ k < ?h. [:B $$ (x, k):] * GK K $$ (k, l)) * [:B $$ (y, l):])"
using x y by (simp add: scalar_prod_def dB dG atLeast0LessThan)
show ?thesis unfolding m sum_distrib_right by (rule sum.swap)
qed
finally show ?thesis .
qed
show ?thesis
proof (rule eq_matI)
fix x y
assume x: "x < dim_row (?Q * GK K * transpose_mat ?Q)" and y: "y <
dim_col (?Q * GK K * transpose_mat ?Q)"
have xh: "x < ?h" and yh: "y < ?h" using x y by (simp_all add: dB)
show "innerGram K M p $$ (x, y) = (?Q * GK K * transpose_mat ?Q) $$ (x, y)"
by (rule entry[OF xh yh])
qed (simp_all add: innerGram_def Let_def len dB dG)
qed
text ‹(4.5): the inner basis is @{text "ℤ_p"}-unimodular: the coefficient matrix of the
basis
polynomials has a determinant that is a @{text p}-adic unit. Proof by the Taylor-matrix criterion
(@{text "unimodular_criterion"}): expanding row @{text "E_{a,j}"} at the point @{text "-c^2"} to
order @{text i}
gives an upper triangular matrix with the units @{text "∏_{c ≠ a} (c^2 - a^2)^{L_c}"}
on the diagonal.›
theorem innerBasis_unimodular:
assumes p: "prime p" and H: "InnerHyp K M p"
defines "B ≡ Matrix.mat (hof K) (hof K) (λ(x,
d). Polynomial.coeff (innerBasis K M p (inner_idx K M p ! x)) d)"
shows "Determinant.det B ≠ 0 ∧ vp p (Determinant.det B) = 0"
proof -
define h where "h = hof K"
define idx where "idx = inner_idx K M p"
define rt where "rt = (λy. - (of_nat (fst (idx ! y)) ^ 2) :: rat)"
define od where "od = (λy. snd (idx ! y))"
define V where "V = Matrix.mat h h (λ(d, y). tay (pX ^ d) (rt y) (od y))"
define T where "T = B * V"
have len: "length idx = h" by (simp add: idx_def h_def length_inner_idx[OF p H])
have Bc: "B ∈ carrier_mat h h" and Vc: "V ∈ carrier_mat h h"
by (simp_all add: B_def V_def h_def)
have mp: "2 * mHalf p + 1 = p" using hyp_facts[OF p H] by blast
have mem: "⋀x. x < h ⟹ idx ! x ∈ set idx" by (simp add: len)
have cls_le: "⋀x. x < h ⟹ fst (idx ! x) ≤ mHalf p"
using mem_inner_idx mem by (auto simp: idx_def)
have Tentry: "⋀x y. x < h ⟹ y < h ⟹
T $$ (x, y) = tay (innerBasis K M p (idx ! x)) (rt y) (od y)"
proof -
fix x y assume x: "x < h" and y: "y < h"
have dg: "degree (innerBasis K M p (idx ! x)) < h"
using degree_innerBasis_lt[OF p H, of "idx ! x"] mem[OF x] by (simp add: idx_def h_def)
have "dim_row B = h" "dim_col B = h" "dim_row V = h" "dim_col V = h" using Bc Vc by auto
with x y have "T $$ (x, y) = (∑ d ∈ {0..<h}. B $$ (x, d) * V $$ (d, y))"
by (simp add: T_def scalar_prod_def)
also have "… = (∑ d < h. Polynomial.coeff (innerBasis K M p (idx ! x)) d *
tay (pX ^ d) (rt y) (od y))"
by (rule sum.cong) (use x y in ‹auto simp: B_def V_def idx_def h_def›)
also have "… = tay (innerBasis K M p (idx ! x)) (rt y) (od y)"
by (rule tay_eq_sum[OF dg, symmetric])
finally show "T $$ (x, y) = tay (innerBasis K M p (idx ! x)) (rt y) (od y)" .
qed
have below: "⋀x y. y < x ⟹ x < h ⟹ T $$ (x, y) = 0"
proof -
fix x y assume yx: "y < x" and x: "x < h"
have y: "y < h" using yx x by simp
obtain a j where ax: "idx ! x = (a, j)" by (cases "idx ! x")
obtain c i where cy: "idx ! y = (c, i)" by (cases "idx ! y")
have my: "c ≤ mHalf p" "i < nat (Lin K M p c)" using mem[OF y] cy
by (simp_all add: idx_def mem_inner_idx)
have mx: "a ≤ mHalf p" using mem[OF x] ax by (simp add: idx_def mem_inner_idx)
have lex: "c < a ∨ (c = a ∧ i < j)"
using inner_idx_lex[of y x K M p] yx x len ax cy by (simp add: idx_def)
have rr: "pX + [:of_nat c ^ 2:] = pX - [:rt y:]" unfolding rt_def cy by simp
have T: "T $$ (x, y) = tay (innerBasis K M p (a, j)) (rt y) i"
using Tentry[OF x y] unfolding ax by (simp add: od_def cy)
show "T $$ (x, y) = 0"
proof (cases "c < a")
case True
have cin: "c ∈ {0..mHalf p} - {a}" using True mx by simp
have E: "innerBasis K M p (a, j) = (pX - [:rt y:]) ^ nat (Lin K M p c) *
((∏ c' ∈ {0..mHalf p} - {a} - {c}. (pX +
[:of_nat c' ^ 2:]) ^ nat (Lin K M p c')) * (pX + [:of_nat a ^ 2:]) ^ j)"
unfolding innerBasis_def fst_conv snd_conv prod.remove[OF finite_Diff[OF
finite_atLeastAtMost] cin] rr
by (simp only: mult.assoc)
show ?thesis unfolding T E by (rule tay_pow_mult_lt[OF my(2)])
next
case False
hence ca: "c = a" and ij: "i < j" using lex by auto
have E: "innerBasis K M p (a, j) = (pX - [:rt y:]) ^ j *
(∏ c' ∈ {0..mHalf p} - {a}. (pX + [:of_nat c' ^ 2:]) ^ nat (Lin K M p c'))"
unfolding innerBasis_def fst_conv snd_conv rr[unfolded ca] by (rule mult.commute)
show ?thesis unfolding T E by (rule tay_pow_mult_lt[OF ij])
qed
qed
have diag: "⋀x. x < h ⟹ T $$ (x, x) =
(∏ c ∈ {0..mHalf p} - {fst (idx ! x)}. (of_nat c ^ 2 -
of_nat (fst (idx ! x)) ^ 2) ^ nat (Lin K M p c))"
proof -
fix x assume x: "x < h"
obtain a j where ax: "idx ! x = (a, j)" by (cases "idx ! x")
have rr: "pX + [:of_nat a ^ 2:] = pX - [:rt x:]" unfolding rt_def ax by simp
have E: "innerBasis K M p (a, j) = (pX - [:rt x:]) ^ j *
(∏ c ∈ {0..mHalf p} - {a}. (pX + [:of_nat c ^ 2:]) ^ nat (Lin K M p c))"
unfolding innerBasis_def fst_conv snd_conv rr by (rule mult.commute)
have "T $$ (x, x) = tay (innerBasis K M p (a, j)) (rt x) j"
using Tentry[OF x x] unfolding ax by (simp add: od_def ax)
also have "… = tay (∏ c ∈
{0..mHalf p} - {a}. (pX + [:of_nat c ^ 2:]) ^ nat (Lin K M p c)) (rt x) 0"
unfolding E using tay_pow_mult[of "rt x" j "∏ c ∈
{0..mHalf p} - {a}. (pX + [:of_nat c ^ 2:]) ^ nat (Lin K M p c)" 0]
by simp
also have "… = poly (∏ c ∈
{0..mHalf p} - {a}. (pX + [:of_nat c ^ 2:]) ^ nat (Lin K M p c)) (rt x)"
by (rule tay_0_eq_poly)
also have "… = (∏ c ∈
{0..mHalf p} - {fst (idx ! x)}. (of_nat c ^ 2 -
of_nat (fst (idx ! x)) ^ 2) ^ nat (Lin K M p c))"
unfolding ax rt_def by (simp add: poly_prod poly_monom)
finally show "T $$ (x, x) =
(∏ c ∈ {0..mHalf p} - {fst (idx ! x)}. (of_nat c ^ 2 -
of_nat (fst (idx ! x)) ^ 2) ^ nat (Lin K M p c))" .
qed
have unit: "⋀x. x < h ⟹ T $$ (x, x) ≠ 0 ∧ vp p (T $$ (x, x)) = 0"
proof -
fix x assume x: "x < h"
define a where "a = fst (idx ! x)"
have am: "a ≤ mHalf p" using cls_le[OF x] by (simp add: a_def)
have pr: "prime (int p)" using p by (simp add: prime_nat_int_transfer)
have fac: "(of_nat c ^ 2 - of_nat a ^ 2 :: rat) ≠ 0 ∧
vp p (of_nat c ^ 2 - of_nat a ^ 2) = 0"
if c: "c ∈ {0..mHalf p} - {a}" for c
proof -
have cm: "c ≤ mHalf p" "c ≠ a" using c by auto
define z :: int where "z = (int c - int a) * (int c + int a)"
have zq: "(of_nat c ^ 2 - of_nat a ^ 2 :: rat) = of_int z"
by (simp add: z_def power2_eq_square algebra_simps)
have "¬ int p dvd (int c - int a)"
proof
assume d: "int p dvd (int c - int a)"
have "int c - int a ≠ 0" using cm by simp
from dvd_imp_le_int[OF this d] have "int p ≤ ¦int c - int a¦" by simp
thus False using cm am mp by arith
qed
moreover have "¬ int p dvd (int c + int a)"
proof
assume d: "int p dvd (int c + int a)"
have "int c + int a ≠ 0" using cm by simp
from dvd_imp_le_int[OF this d] have "int p ≤ ¦int c + int a¦" by simp
thus False using cm am mp by arith
qed
ultimately have nz: "¬ int p dvd z" unfolding z_def using prime_dvd_mult_iff[OF pr]
by blast
hence "z ≠ 0" by auto
thus ?thesis unfolding zq using nz
by (simp add: vp_def qmultiplicity_of_int not_dvd_imp_multiplicity_0)
qed
have d: "T $$ (x, x) = (∏ c ∈
{0..mHalf p} - {a}. (of_nat c ^ 2 - of_nat a ^ 2) ^ nat (Lin K M p c))"
using diag[OF x] by (simp add: a_def)
have ne: "(∏ c ∈ {0..mHalf p} - {a}. (of_nat c ^ 2 -
of_nat a ^ 2 :: rat) ^ nat (Lin K M p c)) ≠ 0"
using fac by (simp add: prod_zero_iff)
have "vp p (∏ c ∈ {0..mHalf p} - {a}. (of_nat c ^ 2 -
of_nat a ^ 2 :: rat) ^ nat (Lin K M p c)) =
(∑ c ∈ {0..mHalf p} - {a}. vp p ((of_nat c ^ 2 -
of_nat a ^ 2) ^ nat (Lin K M p c)))"
by (rule vp_prod_rat[OF p]) (use fac in auto)
also have "… = 0" using fac by (simp add: vp_power_rat[OF p])
finally show "T $$ (x, x) ≠ 0 ∧ vp p (T $$ (x, x)) = 0" unfolding d using ne by simp
qed
have Bi: "⋀x d. x < h ⟹ d < h ⟹ vge p (B $$ (x, d)) 0"
using vpGge_innerBasis[OF p] by (auto simp: B_def h_def vpGge_iff)
have Vi: "⋀d y. d < h ⟹ y < h ⟹ vge p (V $$ (d, y)) 0"
proof -
fix d y assume d: "d < h" and y: "y < h"
have P: "vpGge p (pX ^ d) 0" using vpGge_pow[OF p vpGge_pX, of d] by simp
have "vge p (of_nat (fst (idx ! y)) ^ 2) 0"
using vge_pow[OF p vge_of_int[OF p, of "int (fst (idx ! y))"]] by simp
hence r: "vge p (rt y) 0" unfolding rt_def by (rule vge_neg)
show "vge p (V $$ (d, y)) 0" using vge_tay[OF p P r, of "od y"] d y by (simp add: V_def)
qed
show ?thesis
unfolding h_def[symmetric]
by (rule unimodular_criterion[OF p Bc Vc Bi Vi])
(use below unit in ‹simp_all add: T_def[symmetric] vge_zero›)
qed
text ‹Proposition 4.1 from the entry bounds (unimodular change of basis +
@{text "vpGge_det_of_terms"}).›
theorem DeltaK_vpGge_inner_of_entries:
assumes p: "prime p" and H: "InnerHyp K M p"
and ent: "⋀x y. x < length (inner_idx K M p) ⟹
y < length (inner_idx K M p) ⟹
vpGge p (innerGram K M p $$ (x, y))
(wInIdx K M p (inner_idx K M p ! x) + wInIdx K M p (inner_idx K M p ! y))"
shows "vpGge p (DeltaK K) (gammaIn K M p)"
proof -
define h where "h = hof K"
define B where "B = Matrix.mat (hof K) (hof K) (λ(x,
d). Polynomial.coeff (innerBasis K M p (inner_idx K M p ! x)) d)"
define w where "w = (λx. wInIdx K M p (inner_idx K M p ! x))"
have len: "length (inner_idx K M p) = h" by (simp add: h_def length_inner_idx[OF p H])
have Bc: "B ∈ carrier_mat h h" and Gc: "GK K ∈
carrier_mat h h" and IGc: "innerGram K M p ∈ carrier_mat h h"
by (simp_all add: B_def GK_def innerGram_def h_def len Let_def)
have uni: "Determinant.det B ≠ 0 ∧ vp p (Determinant.det B) = 0"
unfolding B_def by (rule innerBasis_unimodular[OF p H])
have gramv: "vpGge p (Determinant.det (innerGram K M p)) (2 * (∑ i = 0..<h. w i))"
proof (rule vpGge_det_of_terms[OF p IGc])
fix σ assume σ: "σ permutes {0..<h}"
have "vpGge p (∏ i = 0..<h. innerGram K M p $$ (i, σ i)) (∑ i =
0..<h. w i + w (σ i))"
proof (rule vpGge_prod[OF p])
show "finite {0..<h}" by simp
next
fix i assume i: "i ∈ {0..<h}"
have si: "σ i < h" using permutes_in_image[OF σ] i by simp
show "vpGge p (innerGram K M p $$ (i, σ i)) (w i + w (σ i))"
unfolding w_def by (rule ent) (use i si len in auto)
qed
thus "vpGge p (∏ i = 0..<h. innerGram K M p $$ (i, σ i)) (2 * (∑ i =
0..<h. w i))"
using sum_permute_add[OF σ, of w] by (simp add: add.commute)
qed
have "vpGge p (DeltaK K) (2 * (∑ i = 0..<h. w i))"
unfolding DeltaK_def
by (rule det_gram_transfer[OF p Gc Bc conjunct1[OF uni] conjunct2[OF uni]])
(use gramv innerGram_eq_conj[OF p H] in ‹simp add: B_def›)
thus ?thesis
using gammaIn_eq_sum_idx[of K M p] by (simp add: w_def len atLeast0LessThan)
qed
text ‹Proposition 4.1: under (4.1), @{text "v_p^G(Δ_K) ≥ γ_p^in"}.›
theorem DeltaK_vpGge_inner: "prime p ⟹ InnerHyp K M p ⟹
vpGge p (DeltaK K) (gammaIn K M p)"
by (rule DeltaK_vpGge_inner_of_entries, assumption+, rule innerGram_entry_bound)
end