Theory Complex_Lattices
section ‹Complex lattices›
theory Complex_Lattices
imports "HOL-Complex_Analysis.Complex_Analysis" Parallelogram_Paths
begin
lemmas [simp del] = div_mult_self1 div_mult_self2 div_mult_self3 div_mult_self4
subsection ‹Basic definitions and useful lemmas›
text ‹
We define a complex lattice with two generators $\omega_1, \omega_2\in\mathbb{C}$ as the set
$\Lambda(\omega_1, \omega_2) = \omega_1\mathbb{Z} + \omega_2\mathbb{Z}$.
For now, we make no restrictions on the generators, but for most of our results we will require
that they be independent (i.e.\ neither is a multiple of the other, or, in terms of complex
numbers, their quotient is not real).
›
locale pre_complex_lattice =
fixes ω1 ω2 :: complex
begin
text ‹
The following function convergs from lattice coordinates into cartesian coordinates.
›
definition of_ω12_coords :: "real × real ⇒ complex" where
"of_ω12_coords = (λ(x,y). of_real x * ω1 + of_real y * ω2)"
sublocale of_ω12_coords: linear of_ω12_coords
unfolding of_ω12_coords_def by (auto simp: linear_iff algebra_simps scaleR_conv_of_real)
sublocale of_ω12_coords: bounded_linear of_ω12_coords
using of_ω12_coords.linear_axioms linear_conv_bounded_linear by auto
lemmas [continuous_intros] = of_ω12_coords.continuous_on of_ω12_coords.continuous
lemmas [tendsto_intros] = of_ω12_coords.tendsto
lemmas [simp] = of_ω12_coords.add of_ω12_coords.diff of_ω12_coords.neg of_ω12_coords.scaleR
lemma of_ω12_coords_fst [simp]: "of_ω12_coords (a, 0) = of_real a * ω1"
and of_ω12_coords_snd [simp]: "of_ω12_coords (0, a) = of_real a * ω2"
and of_ω12_coords_scaleR': "of_ω12_coords (c *⇩R z) = of_real c * of_ω12_coords z"
by (simp_all add: of_ω12_coords_def algebra_simps case_prod_unfold
scaleR_prod_def scaleR_conv_of_real)
text ‹
The following is our lattice as a set of lattice points.
›
definition lattice :: "complex set" ("Λ") where
"lattice = of_ω12_coords ` (ℤ × ℤ)"
definition lattice0 :: "complex set" ("Λ⇧*") where
"lattice0 = lattice - {0}"
lemma countable_lattice [intro]: "countable lattice"
unfolding lattice_def by (intro countable_image countable_SIGMA countable_int)
lemma latticeI: "of_ω12_coords (x, y) = z ⟹ x ∈ ℤ ⟹ y ∈ ℤ ⟹ z ∈ Λ"
by (auto simp: lattice_def)
lemma latticeE:
assumes "z ∈ Λ"
obtains x y where "z = of_ω12_coords (of_int x, of_int y)"
using assms unfolding lattice_def Ints_def by auto
lemma lattice0I [intro]: "z ∈ Λ ⟹ z ≠ 0 ⟹ z ∈ Λ⇧*"
by (auto simp: lattice0_def)
lemma lattice0E [elim]: "⋀P. z ∈ Λ⇧* ⟹ (z ∈ Λ ⟹ z ≠ 0 ⟹ P) ⟹ P"
by (auto simp: lattice0_def)
lemma in_lattice0_iff: "z ∈ Λ⇧* ⟷ z ∈ Λ ∧ z ≠ 0"
by (auto simp: lattice0_def)
named_theorems lattice_intros
lemma zero_in_lattice [lattice_intros, simp]: "0 ∈ lattice"
by (rule latticeI[of 0 0]) (auto simp: of_ω12_coords_def)
lemma generator_in_lattice [lattice_intros, simp]: "ω1 ∈ lattice" "ω2 ∈ lattice"
by (auto intro: latticeI[of 0 1] latticeI[of 1 0] simp: of_ω12_coords_def)
lemma uminus_in_lattice [lattice_intros]: "z ∈ Λ ⟹ -z ∈ Λ"
proof -
assume "z ∈ Λ"
then obtain x y where "z = of_ω12_coords (of_int x, of_int y)"
by (elim latticeE)
thus ?thesis
by (intro latticeI[of "-x" "-y"]) (auto simp: of_ω12_coords_def)
qed
lemma uminus_in_lattice_iff: "-z ∈ Λ ⟷ z ∈ Λ"
using uminus_in_lattice minus_minus by metis
lemma uminus_in_lattice0_iff: "-z ∈ Λ⇧* ⟷ z ∈ Λ⇧*"
by (auto simp: lattice0_def uminus_in_lattice_iff)
lemma add_in_lattice [lattice_intros]: "z ∈ Λ ⟹ w ∈ Λ ⟹ z + w ∈ Λ"
proof -
assume "z ∈ Λ" "w ∈ Λ"
then obtain a b c d
where "z = of_ω12_coords (of_int a, of_int b)" "w = of_ω12_coords (of_int c, of_int d)"
by (elim latticeE)
thus ?thesis
by (intro latticeI[of "a + c" "b + d"]) (auto simp: of_ω12_coords_def algebra_simps)
qed
lemma lattice_lattice0: "Λ = insert 0 Λ⇧*"
by (auto simp: lattice0_def)
lemma mult_of_nat_left_in_lattice [lattice_intros]: "z ∈ Λ ⟹ of_nat n * z ∈ Λ"
by (induction n) (auto intro!: lattice_intros simp: ring_distribs)
lemma mult_of_nat_right_in_lattice [lattice_intros]: "z ∈ Λ ⟹ z * of_nat n ∈ Λ"
using mult_of_nat_left_in_lattice[of z n] by (simp add: mult.commute)
lemma mult_of_int_left_in_lattice [lattice_intros]: "z ∈ Λ ⟹ of_int n * z ∈ Λ"
using mult_of_nat_left_in_lattice[of z "nat n"]
uminus_in_lattice[OF mult_of_nat_left_in_lattice[of z "nat (-n)"]]
by (cases "n ≥ 0") auto
lemma mult_of_int_right_in_lattice [lattice_intros]: "z ∈ Λ ⟹ z * of_int n ∈ Λ"
using mult_of_int_left_in_lattice[of z n] by (simp add: mult.commute)
lemma diff_in_lattice [lattice_intros]: "z ∈ Λ ⟹ w ∈ Λ ⟹ z - w ∈ Λ"
using add_in_lattice[OF _ uminus_in_lattice, of z w] by simp
lemma diff_in_lattice_commute: "z - w ∈ Λ ⟷ w - z ∈ Λ"
using uminus_in_lattice_iff[of "z - w"] by simp
lemma of_ω12_coords_in_lattice [lattice_intros]: "ab ∈ ℤ × ℤ ⟹ of_ω12_coords ab ∈ Λ"
unfolding lattice_def by auto
lemma lattice_plus_right_cancel [simp]: "y ∈ Λ ⟹ x + y ∈ Λ ⟷ x ∈ Λ"
by (metis add_diff_cancel_right' add_in_lattice diff_in_lattice)
lemma lattice_plus_left_cancel [simp]: "x ∈ Λ ⟹ x + y ∈ Λ ⟷ y ∈ Λ"
by (metis add.commute lattice_plus_right_cancel)
lemma lattice_induct [consumes 1, case_names zero gen1 gen2 add uminus]:
assumes "z ∈ Λ"
assumes zero: "P 0"
assumes gens: "P ω1" "P ω2"
assumes plus: "⋀w z. P w ⟹ P z ⟹ P (w + z)"
assumes uminus: "⋀w. P w ⟹ P (-w)"
shows "P z"
proof -
from assms(1) obtain a b where z_eq: "z = of_ω12_coords (of_int a, of_int b)"
by (elim latticeE)
have nat1: "P (of_ω12_coords (of_nat n, 0))" for n
by (induction n) (auto simp: of_ω12_coords_def ring_distribs intro: zero plus gens)
have int1: "P (of_ω12_coords (of_int n, 0))" for n
using nat1[of "nat n"] uminus[OF nat1[of "nat (-n)"]]
by (cases "n ≥ 0") (auto simp: of_ω12_coords_def)
have nat2: "P (of_ω12_coords (of_int a, of_nat n))" for a n
proof (induction n)
case 0
thus ?case
using int1[of a] by simp
next
case (Suc n)
from plus[OF Suc gens(2)] show ?case
by (simp add: of_ω12_coords_def algebra_simps)
qed
have int2: "P (of_ω12_coords (of_int a, of_int b))" for a b
using nat2[of a "nat b"] uminus[OF nat2[of "-a" "nat (-b)"]]
by (cases "b ≥ 0") (auto simp: of_ω12_coords_def)
from this[of a b] and z_eq show ?thesis
by simp
qed
text ‹
The following equivalence relation equates two points if they differ by a lattice point.
›
definition rel :: "complex ⇒ complex ⇒ bool" where
"rel x y ⟷ (x - y) ∈ Λ"
lemma rel_refl [simp, intro]: "rel x x"
by (auto simp: rel_def)
lemma relE:
assumes "rel x y"
obtains z where "z ∈ Λ" "y = x + z"
using assms unfolding rel_def using pre_complex_lattice.uminus_in_lattice by force
lemma rel_symI: "rel x y ⟹ rel y x"
by (auto simp: rel_def diff_in_lattice_commute)
lemma rel_sym: "rel x y ⟷ rel y x"
by (auto simp: rel_def diff_in_lattice_commute)
lemma rel_0_right_iff: "rel x 0 ⟷ x ∈ Λ"
by (simp add: rel_def)
lemma rel_0_left_iff: "rel 0 x ⟷ x ∈ Λ"
by (simp add: rel_def uminus_in_lattice_iff)
lemma rel_trans [trans]: "rel x y ⟹ rel y z ⟹ rel x z"
using add_in_lattice rel_def by fastforce
lemma rel_minus [lattice_intros]: "rel a b ⟹ rel (-a) (-b)"
unfolding rel_def by (simp add: diff_in_lattice_commute)
lemma rel_minus_iff: "rel (-a) (-b) ⟷ rel a b"
by (auto simp: rel_def diff_in_lattice_commute)
lemma rel_add [lattice_intros]: "rel a b ⟹ rel c d ⟹ rel (a + c) (b + d)"
unfolding rel_def by (simp add: add_diff_add add_in_lattice)
lemma rel_diff [lattice_intros]: "rel a b ⟹ rel c d ⟹ rel (a - c) (b - d)"
by (metis rel_add rel_minus uminus_add_conv_diff)
lemma rel_mult_of_nat_left [lattice_intros]: "rel a b ⟹ rel (of_nat n * a) (of_nat n * b)"
by (induction n) (auto intro!: lattice_intros simp: ring_distribs)
lemma rel_mult_of_nat_right [lattice_intros]: "rel a b ⟹ rel (a * of_nat n) (b * of_nat n)"
by (induction n) (auto intro!: lattice_intros simp: ring_distribs)
lemma rel_mult_of_int_left [lattice_intros]: "rel a b ⟹ rel (of_int n * a) (of_int n * b)"
by (induction n) (auto intro!: lattice_intros simp: ring_distribs)
lemma rel_mult_of_int_right [lattice_intros]: "rel a b ⟹ rel (a * of_int n) (b * of_int n)"
by (induction n) (auto intro!: lattice_intros simp: ring_distribs)
lemma rel_sum [lattice_intros]:
"(⋀i. i ∈ A ⟹ rel (f i) (g i)) ⟹ rel (∑i∈A. f i) (∑i∈A. g i)"
by (induction A rule: infinite_finite_induct) (auto intro!: lattice_intros)
lemma rel_sum_list [lattice_intros]:
"list_all2 rel xs ys ⟹ rel (sum_list xs) (sum_list ys)"
by (induction rule: list_all2_induct) (auto intro!: lattice_intros)
lemma rel_lattice_trans_left [trans]: "x ∈ Λ ⟹ rel x y ⟹ y ∈ Λ"
using rel_0_left_iff rel_trans by blast
lemma rel_lattice_trans_right [trans]: "rel x y ⟹ y ∈ Λ ⟹ x ∈ Λ"
using rel_lattice_trans_left rel_sym by blast
end
text ‹
Exchanging the two generators clearly does not change the underlying lattice.
›
locale pre_complex_lattice_swap = pre_complex_lattice
begin
sublocale swap: pre_complex_lattice ω2 ω1 .
lemma swap_of_ω12_coords [simp]: "swap.of_ω12_coords = of_ω12_coords ∘ prod.swap"
by (auto simp: fun_eq_iff swap.of_ω12_coords_def of_ω12_coords_def add_ac)
lemma swap_lattice [simp]: "swap.lattice = lattice"
unfolding swap.lattice_def lattice_def swap_of_ω12_coords image_comp [symmetric] product_swap ..
lemma swap_lattice0 [simp]: "swap.lattice0 = lattice0"
unfolding swap.lattice0_def lattice0_def swap_lattice ..
lemma swap_rel [simp]: "swap.rel = rel"
unfolding swap.rel_def rel_def swap_lattice ..
end
text ‹
A pair ‹(ω⇩1, ω⇩2)› of complex numbers with ‹ω⇩2 / ω⇩1 ∉ ℝ› is called a ∗‹fundamental pair›.
Two such pairs are called ∗‹equivalent› if
›
definition fundpair :: "complex × complex ⇒ bool" where
"fundpair = (λ(a, b). b / a ∉ ℝ)"
lemma fundpair_swap: "fundpair ab ⟷ fundpair (prod.swap ab)"
unfolding fundpair_def prod.swap_def case_prod_unfold fst_conv snd_conv
by (metis Un_insert_right collinear_iff_Reals insert_is_Un)
lemma fundpair_cnj_iff [simp]: "fundpair (cnj a, cnj b) = fundpair (a, b)"
by (auto simp: fundpair_def complex_is_Real_iff simp flip: complex_cnj_divide)
lemma fundpair_altdef: "fundpair = (λ(a,b). a / b ∉ ℝ)"
proof
fix ab :: "complex × complex"
show "fundpair ab = (case ab of (a, b) ⇒ a / b ∉ ℝ)"
using fundpair_swap[of ab] by (auto simp: fundpair_def)
qed
lemma
assumes "fundpair (a, b)"
shows fundpair_imp_nonzero [dest]: "a ≠ 0" "b ≠ 0"
and fundpair_imp_neq: "a ≠ b" "b ≠ a"
using assms unfolding fundpair_def by (auto split: if_splits)
lemma fundpair_imp_independent:
assumes "fundpair (ω1, ω2)"
shows "independent {ω1, ω2}"
proof
assume "dependent {ω1, ω2}"
then obtain a b where ab: "a *⇩R ω1 + b *⇩R ω2 = 0" and "a ≠ 0 ∨ b ≠ 0"
by (subst (asm) real_vector.dependent_finite) (use assms in ‹auto dest: fundpair_imp_neq›)
with assms have [simp]: "a ≠ 0" "b ≠ 0"
by auto
from ab have "ω2 / ω1 = of_real (-a / b)"
using assms by (auto simp: field_simps scaleR_conv_of_real add_eq_0_iff)
also have "… ∈ ℝ"
by simp
finally show False
using assms by (auto simp: fundpair_def)
qed
lemma fundpair_imp_basis:
assumes "fundpair (ω1, ω2)"
shows "span {ω1, ω2} = UNIV"
proof -
have "dim (span {ω1, ω2}) = card {ω1, ω2}"
using fundpair_imp_independent[OF assms] by (rule dim_span_eq_card_independent)
hence "dim (span {ω1, ω2}) = DIM(complex)"
using fundpair_imp_neq(1)[OF assms] by simp
thus ?thesis
using dim_eq_full span_span by blast
qed
text ‹
We now introduce the assumption that the generators be independent. This makes
$\{\omega_1,\omega_2\}$ a basis of $\mathbb{C}$ (in the sense of an $\mathbb{R}$-vector space),
and we define a few functions to help us convert between these two views.
›
locale complex_lattice = pre_complex_lattice +
assumes fundpair: "fundpair (ω1, ω2)"
begin
lemma ω1_neq_ω2 [simp]: "ω1 ≠ ω2" and ω2_neq_ω1 [simp]: "ω2 ≠ ω1"
using fundpair fundpair_imp_neq by blast+
lemma ω1_nonzero [simp]: "ω1 ≠ 0" and ω2_nonzero [simp]: "ω2 ≠ 0"
using fundpair by auto
lemma lattice0_nonempty [simp]: "lattice0 ≠ {}"
proof -
have "ω1 ∈ lattice0"
by auto
thus ?thesis
by blast
qed
lemma ω12_independent': "independent {ω1, ω2}"
using fundpair by (rule fundpair_imp_independent)
lemma span_ω12: "span {ω1, ω2} = UNIV"
using fundpair by (rule fundpair_imp_basis)
text ‹
The following converts complex numbers into lattice coordinates, i.e.\ as a linear
combination of the two generators.
›
definition ω1_coord :: "complex ⇒ real" where
"ω1_coord z = representation {ω1, ω2} z ω1"
definition ω2_coord :: "complex ⇒ real" where
"ω2_coord z = representation {ω1, ω2} z ω2"
definition ω12_coords :: "complex ⇒ real × real" where
"ω12_coords z = (ω1_coord z, ω2_coord z)"
sublocale ω1_coord: bounded_linear ω1_coord
unfolding ω1_coord_def using ω12_independent' span_ω12
by (rule bounded_linear_representation)
sublocale ω2_coord: bounded_linear ω2_coord
unfolding ω2_coord_def using ω12_independent' span_ω12
by (rule bounded_linear_representation)
sublocale ω12_coords: linear ω12_coords
unfolding ω12_coords_def
by (auto simp: linear_iff ω1_coord.add ω2_coord.add ω1_coord.scaleR ω2_coord.scaleR)
sublocale ω12_coords: bounded_linear ω12_coords
using ω12_coords.linear_axioms linear_conv_bounded_linear by auto
lemmas [continuous_intros] =
ω1_coord.continuous_on ω1_coord.continuous
ω2_coord.continuous_on ω2_coord.continuous
ω12_coords.continuous_on ω12_coords.continuous
lemmas [tendsto_intros] = ω1_coord.tendsto ω2_coord.tendsto ω12_coords.tendsto
lemma ω1_coord_ω1 [simp]: "ω1_coord ω1 = 1"
and ω1_coord_ω2 [simp]: "ω1_coord ω2 = 0"
and ω2_coord_ω1 [simp]: "ω2_coord ω1 = 0"
and ω2_coord_ω2 [simp]: "ω2_coord ω2 = 1"
unfolding ω1_coord_def ω2_coord_def using ω1_neq_ω2
by (simp_all add: ω12_independent' representation_basis)
lemma ω12_coords_ω1 [simp]: "ω12_coords ω1 = (1, 0)"
and ω12_coords_ω2 [simp]: "ω12_coords ω2 = (0, 1)"
by (simp_all add: ω12_coords_def)
lemma ω12_coords_of_ω12_coords [simp]: "ω12_coords (of_ω12_coords z) = z"
by (simp add: of_ω12_coords_def case_prod_unfold ω12_coords.add ω12_coords.scaleR
flip: scaleR_conv_of_real)
lemma ω1_coord_of_ω12_coords [simp]: "ω1_coord (of_ω12_coords z) = fst z"
and ω2_coord_of_ω12_coords [simp]: "ω2_coord (of_ω12_coords z) = snd z"
using ω12_coords_of_ω12_coords[of z]
by (auto simp del: ω12_coords_of_ω12_coords simp add: ω12_coords_def prod_eq_iff)
lemma of_ω12_coords_ω12_coords [simp]: "of_ω12_coords (ω12_coords z) = z"
proof -
have "(∑b∈{ω1, ω2}. representation {ω1, ω2} z b *⇩R b) = z"
by (rule real_vector.sum_representation_eq) (use ω12_independent' span_ω12 in simp_all)
thus ?thesis
by (simp add: ω12_coords_def of_ω12_coords_def scaleR_conv_of_real
ω1_coord_def ω2_coord_def ω1_neq_ω2)
qed
lemma ω12_coords_eqI:
assumes "of_ω12_coords a = b"
shows "ω12_coords b = a"
unfolding assms[symmetric] by auto
lemmas [simp] = ω1_coord.scaleR ω2_coord.scaleR ω12_coords.scaleR
lemma ω12_coords_times_ω1 [simp]: "ω12_coords (of_real a * ω1) = (a, 0)"
and ω12_coords_times_ω2 [simp]: "ω12_coords (of_real a * ω2) = (0, a)"
and ω12_coords_times_ω1' [simp]: "ω12_coords (ω1 * of_real a) = (a, 0)"
and ω12_coords_times_ω2' [simp]: "ω12_coords (ω2 * of_real a) = (0, a)"
and ω12_coords_mult_of_real [simp]: "ω12_coords (of_real c * z) = c *⇩R ω12_coords z"
and ω12_coords_mult_of_int [simp]: "ω12_coords (of_int i * z) = of_int i *⇩R ω12_coords z"
and ω12_coords_mult_of_nat [simp]: "ω12_coords (of_nat n * z) = of_nat n *⇩R ω12_coords z"
and ω12_coords_divide_of_real [simp]: "ω12_coords (z / of_real c) = ω12_coords z /⇩R c"
and ω12_coords_mult_numeral [simp]: "ω12_coords (numeral num * z) = numeral num *⇩R ω12_coords z"
and ω12_coords_divide_numeral [simp]: "ω12_coords (z / numeral num) = ω12_coords z /⇩R numeral num"
by (rule ω12_coords_eqI; simp add: scaleR_conv_of_real field_simps; fail)+
lemma of_ω12_coords_eq_iff: "of_ω12_coords z1 = of_ω12_coords z2 ⟷ z1 = z2"
using ω12_coords_eqI by blast
lemma ω12_coords_eq_iff: "ω12_coords z1 = ω12_coords z2 ⟷ z1 = z2"
by (metis of_ω12_coords_ω12_coords)
lemma of_ω12_coords_eq_0_iff [simp]: "of_ω12_coords z = 0 ⟷ z = (0,0)"
unfolding zero_prod_def [symmetric]
by (metis ω12_coords.zero ω12_coords_eqI of_ω12_coords_ω12_coords)
lemma ω12_coords_eq_0_0_iff [simp]: "ω12_coords x = (0, 0) ⟷ x = 0"
by (metis ω12_coords.zero ω12_coords_eq_iff zero_prod_def)
lemma bij_of_ω12_coords: "bij of_ω12_coords"
proof -
have "∃z'. z = of_ω12_coords z'" for z
by (rule exI[of _ "ω12_coords z"]) auto
hence "surj of_ω12_coords"
by blast
thus ?thesis
unfolding bij_def by (auto intro!: injI simp: of_ω12_coords_eq_iff)
qed
lemma bij_betw_lattice: "bij_betw of_ω12_coords (ℤ × ℤ) lattice"
unfolding lattice_def using bij_of_ω12_coords unfolding bij_betw_def inj_on_def by blast
lemma bij_betw_lattice0: "bij_betw of_ω12_coords (ℤ × ℤ - {(0,0)}) lattice0"
unfolding lattice0_def by (intro bij_betw_DiffI bij_betw_singletonI bij_betw_lattice) auto
lemma bij_betw_lattice': "bij_betw (of_ω12_coords ∘ map_prod of_int of_int) UNIV lattice"
by (rule bij_betw_trans[OF _ bij_betw_lattice]) (auto simp: Ints_def bij_betw_def inj_on_def)
lemma bij_betw_lattice0': "bij_betw (of_ω12_coords ∘ map_prod of_int of_int) (-{(0,0)}) lattice0"
by (rule bij_betw_trans[OF _ bij_betw_lattice0]) (auto simp: Ints_def bij_betw_def inj_on_def)
lemma infinite_lattice: "¬finite lattice"
proof -
have "finite (UNIV :: (int × int) set) ⟷ finite lattice"
by (rule bij_betw_finite[OF bij_betw_lattice'])
moreover have "¬finite (UNIV :: (int × int) set)"
by (simp add: finite_prod)
ultimately show ?thesis
by blast
qed
lemma ω12_coords_image_eq: "ω12_coords ` X = of_ω12_coords -` X"
using bij_of_ω12_coords image_iff by fastforce
lemma of_ω12_coords_image_eq: "of_ω12_coords ` X = ω12_coords -` X"
by (metis UNIV_I ω12_coords_eqI ω12_coords_image_eq bij_betw_imp_surj_on
bij_of_ω12_coords rangeI subsetI subset_antisym surj_image_vimage_eq)
lemma of_ω12_coords_linepath:
"of_ω12_coords (linepath a b x) = linepath (of_ω12_coords a) (of_ω12_coords b) x"
by (simp add: linepath_def scaleR_prod_def scaleR_conv_of_real
of_ω12_coords_def algebra_simps case_prod_unfold)
lemma of_ω12_coords_linepath':
"of_ω12_coords o (linepath a b) =
linepath (of_ω12_coords a) (of_ω12_coords b)"
unfolding comp_def using of_ω12_coords_linepath
by auto
lemma ω12_coords_linepath:
"ω12_coords (linepath a b x) = linepath (ω12_coords a) (ω12_coords b) x"
by (rule ω12_coords_eqI) (simp add: of_ω12_coords_linepath)
lemma of_ω12_coords_in_lattice_iff:
"of_ω12_coords z ∈ Λ ⟷ fst z ∈ ℤ ∧ snd z ∈ ℤ"
proof
assume "of_ω12_coords z ∈ Λ"
then obtain m n where mn: "of_ω12_coords z = of_ω12_coords (of_int m, of_int n)"
by (elim latticeE)
hence "z = (of_int m, of_int n)"
by (simp only: of_ω12_coords_eq_iff)
thus "fst z ∈ ℤ ∧ snd z ∈ ℤ"
by auto
next
assume "fst z ∈ ℤ ∧ snd z ∈ ℤ"
thus "of_ω12_coords z ∈ Λ"
by (simp add: latticeI of_ω12_coords_def split_def)
qed
lemma of_ω12_coords_in_lattice [simp, intro]:
"fst z ∈ ℤ ⟹ snd z ∈ ℤ ⟹ of_ω12_coords z ∈ Λ"
by (subst of_ω12_coords_in_lattice_iff) auto
lemma in_lattice_conv_ω12_coords: "z ∈ Λ ⟷ ω12_coords z ∈ ℤ × ℤ"
using of_ω12_coords_in_lattice_iff[of "ω12_coords z"] by (auto simp: mem_Times_iff)
lemma ω12_coords_in_Z_times_Z: "z ∈ Λ ⟹ ω12_coords z ∈ ℤ × ℤ"
by (subst (asm) in_lattice_conv_ω12_coords) auto
lemma half_periods_notin_lattice [simp]:
"ω1 / 2 ∉ Λ" "ω2 / 2 ∉ Λ" "(ω1 + ω2) / 2 ∉ Λ"
by (auto simp: in_lattice_conv_ω12_coords ω12_coords.add)
end
locale complex_lattice_swap = complex_lattice
begin
sublocale pre_complex_lattice_swap ω1 ω2 .
sublocale swap: complex_lattice ω2 ω1
proof
show "fundpair (ω2, ω1)"
using fundpair by (subst (asm) fundpair_swap) auto
qed
lemma swap_ω12_coords [simp]: "swap.ω12_coords = prod.swap ∘ ω12_coords"
by (metis (no_types, lifting) ext comp_apply of_ω12_coords_ω12_coords
pre_complex_lattice_swap.swap_of_ω12_coords swap.ω12_coords_eqI)
lemma swap_ω1_coord [simp]: "swap.ω1_coord = ω2_coord"
and swap_ω2_coord [simp]: "swap.ω2_coord = ω1_coord"
using swap_ω12_coords unfolding swap.ω12_coords_def[abs_def] ω12_coords_def[abs_def]
by (auto simp: fun_eq_iff)
end
subsection ‹Period parallelograms›
context pre_complex_lattice
begin
text ‹
The period parallelogram at a vertex ‹z› is the parallelogram with the vertices
‹z›, ‹z + ω⇩1›, ‹z + ω⇩2›, and ‹z + ω⇩1 + ω⇩2›. For convenience, we define the parallelogram to
be contain only two of its four sides, so that one can obtain an exact covering of the complex
plane with period parallelograms.
We will occasionally need the full parallelogram with all four sides, or the interior of the
parallelogram without its four sides, but these are easily obtained from this using the
\<^const>‹closure› and \<^const>‹interior› operators, while the border itself (which is of interest
for integration) is obtained with the \<^const>‹frontier› operator.
›
definition period_parallelogram :: "complex ⇒ complex set" where
"period_parallelogram z = (+) z ` of_ω12_coords ` ({0..<1} × {0..<1})"
text ‹
The following is a path along the border of a period parallelogram, starting
at the vertex ‹z› and going in direction ‹ω1›.
›
definition period_parallelogram_path :: "complex ⇒ real ⇒ complex" where
"period_parallelogram_path z ≡ parallelogram_path z ω1 ω2"
lemma bounded_period_parallelogram [intro]: "bounded (period_parallelogram z)"
unfolding period_parallelogram_def
by (rule bounded_translation bounded_linear_image bounded_Times)+
(auto intro: of_ω12_coords.bounded_linear_axioms)
lemma convex_period_parallelogram [intro]:
"convex (period_parallelogram z)"
unfolding period_parallelogram_def
by (intro convex_translation convex_linear_image of_ω12_coords.linear_axioms convex_Times) auto
lemma closure_period_parallelogram:
"closure (period_parallelogram z) = (+) z ` of_ω12_coords ` (cbox (0,0) (1,1))"
proof -
have "closure (period_parallelogram z) = (+) z ` closure (of_ω12_coords ` ({0..<1} × {0..<1}))"
unfolding period_parallelogram_def by (subst closure_translation) auto
also have "closure (of_ω12_coords ` ({0..<1} × {0..<1})) =
of_ω12_coords ` (closure ({0..<1} × {0..<1}))"
by (rule closure_bounded_linear_image [symmetric])
(auto intro: bounded_Times of_ω12_coords.linear_axioms)
also have "closure ({0..<1::real} × {0..<1::real}) = {0..1} × {0..1}"
by (simp add: closure_Times)
also have "… = cbox (0,0) (1,1)"
by auto
finally show ?thesis .
qed
lemma compact_closure_period_parallelogram [intro]: "compact (closure (period_parallelogram z))"
unfolding closure_period_parallelogram
by (intro compact_translation compact_continuous_image continuous_intros compact_Times) auto
lemma vertex_in_period_parallelogram [simp, intro]: "z ∈ period_parallelogram z"
unfolding period_parallelogram_def image_image
by (rule image_eqI[of _ _ "(0,0)"]) auto
lemma nonempty_period_parallelogram: "period_parallelogram z ≠ {}"
using vertex_in_period_parallelogram[of z] by blast
end
lemma (in pre_complex_lattice_swap)
swap_period_parallelogram [simp]: "swap.period_parallelogram = period_parallelogram"
unfolding swap.period_parallelogram_def period_parallelogram_def swap_of_ω12_coords
image_comp [symmetric] product_swap ..
context complex_lattice
begin
lemma simple_path_parallelogram: "simple_path (parallelogram_path z ω1 ω2)"
unfolding parallelogram_path_altdef
proof (rule simple_path_continuous_image)
let ?h = "λw. z + Re w *⇩R ω1 + Im w *⇩R ω2"
show "simple_path (rectpath 0 (1 + 𝗂))"
by (intro simple_path_rectpath) auto
show "continuous_on (path_image (rectpath 0 (1 + 𝗂))) ?h"
by (intro continuous_intros)
show "inj_on ?h (path_image (rectpath 0 (1 + 𝗂)))"
proof
fix x y assume "?h x = ?h y"
hence "of_ω12_coords (Re x, Im x) = of_ω12_coords (Re y, Im y)"
by (simp add: of_ω12_coords_def scaleR_conv_of_real)
thus "x = y"
by (intro complex_eqI) (simp_all add: of_ω12_coords_eq_iff)
qed
qed
lemma (in -) image_plus_conv_vimage_plus:
fixes c :: "'a :: group_add"
shows "(+) c ` A = (+) (-c) -` A"
proof safe
fix z assume "-c + z ∈ A"
thus "z ∈ (+) c ` A"
by (intro image_eqI[of _ _ "-c + z"]) (auto simp: algebra_simps)
qed auto
lemma period_parallelogram_altdef:
"period_parallelogram z = {w. ω12_coords (w - z) ∈ {0..<1} × {0..<1}}"
unfolding period_parallelogram_def of_ω12_coords_image_eq image_plus_conv_vimage_plus
by auto
lemma interior_period_parallelogram:
"interior (period_parallelogram z) = (+) z ` of_ω12_coords ` box (0,0) (1,1)"
proof -
have bij: "bij of_ω12_coords"
by (simp add: bij_of_ω12_coords)
have "interior (period_parallelogram z) = (+) z ` interior (of_ω12_coords ` ({0..<1} × {0..<1}))"
unfolding period_parallelogram_def by (subst interior_translation) auto
also have "interior (of_ω12_coords ` ({0..<1} × {0..<1})) =
of_ω12_coords ` (interior ({0..<1} × {0..<1}))"
using of_ω12_coords.linear_axioms bij
by (rule interior_bijective_linear_image)
also have "interior ({0..<1::real} × {0..<1::real}) = {0<..<1} × {0<..<1}"
by (subst interior_Times) simp_all
finally show ?thesis by (auto simp: box_prod)
qed
lemma path_image_parallelogram_path':
"path_image (parallelogram_path z ω1 ω2) =
(+) z ` of_ω12_coords ` (cbox (0,0) (1,1) - box (0,0) (1,1))"
proof -
define f where "f = (λx. (Re x, Im x))"
have "bij f"
by (rule bij_betwI[of _ _ _ "λ(x,y). Complex x y"]) (auto simp: f_def)
hence "inj f" "surj f"
using bij_is_inj bij_is_surj by auto
have "path_image (parallelogram_path z ω1 ω2) =
(λw. z + Re w *⇩R ω1 + Im w *⇩R ω2) ` (cbox 0 (1 + 𝗂) - box 0 (1 + 𝗂))"
(is "_ = _ ` ?S")
unfolding parallelogram_path_altdef period_parallelogram_altdef path_image_compose
by (subst path_image_rectpath_cbox_minus_box) auto
also have "(λw. z + Re w *⇩R ω1 + Im w *⇩R ω2) = (+) z ∘ of_ω12_coords ∘ f"
by (auto simp: of_ω12_coords_def fun_eq_iff scaleR_conv_of_real f_def)
also have "… ` (cbox 0 (1 + 𝗂) - box 0 (1 + 𝗂)) =
(+) z ` of_ω12_coords ` f ` ((cbox 0 (1 + 𝗂) - box 0 (1 + 𝗂)))"
by (simp add: image_image)
also have "f ` ((cbox 0 (1 + 𝗂) - box 0 (1 + 𝗂))) = f ` cbox 0 (1 + 𝗂) - f ` box 0 (1 + 𝗂)"
by (rule image_set_diff[OF ‹inj f›])
also have "cbox 0 (1 + 𝗂) = f -` cbox (0,0) (1,1)"
by (auto simp: f_def cbox_complex_eq)
also have "f ` … = cbox (0,0) (1,1)"
by (rule surj_image_vimage_eq[OF ‹surj f›])
also have "box 0 (1 + 𝗂) = f -` box (0,0) (1,1)"
by (auto simp: f_def box_complex_eq box_prod)
also have "f ` … = box (0,0) (1,1)"
by (rule surj_image_vimage_eq[OF ‹surj f›])
finally show ?thesis .
qed
lemma fund_period_parallelogram_in_lattice_iff:
assumes "z ∈ period_parallelogram 0"
shows "z ∈ Λ ⟷ z = 0"
proof
assume "z ∈ Λ"
then obtain m n where mn: "z = of_ω12_coords (of_int m, of_int n)"
by (elim latticeE)
show "z = 0"
using assms unfolding mn period_parallelogram_altdef by auto
qed auto
lemma path_image_parallelogram_path:
"path_image (parallelogram_path z ω1 ω2) = frontier (period_parallelogram z)"
unfolding frontier_def closure_period_parallelogram interior_period_parallelogram
path_image_parallelogram_path'
by (subst image_set_diff) (auto intro!: inj_onI simp: of_ω12_coords_eq_iff)
lemma path_image_parallelogram_subset_closure:
"path_image (parallelogram_path z ω1 ω2) ⊆ closure (period_parallelogram z)"
unfolding path_image_parallelogram_path' closure_period_parallelogram by (intro image_mono) auto
lemma path_image_parallelogram_disjoint_interior:
"path_image (parallelogram_path z ω1 ω2) ∩ interior (period_parallelogram z) = {}"
unfolding path_image_parallelogram_path' interior_period_parallelogram
by (auto simp: of_ω12_coords_eq_iff box_prod)
lemma winding_number_parallelogram_outside:
assumes "w ∉ closure (period_parallelogram z)"
shows "winding_number (parallelogram_path z ω1 ω2) w = 0"
by (rule winding_number_zero_outside[OF _ _ _ assms])
(use path_image_parallelogram_subset_closure[of z] in auto)
text ‹
The path we take around the period parallelogram is clearly a simple path, and its orientation
depends on the angle between our generators.
›
lemma winding_number_parallelogram_inside:
assumes "w ∈ interior (period_parallelogram z)"
shows "winding_number (parallelogram_path z ω1 ω2) w = sgn (Im (ω2 / ω1))"
proof -
let ?P = "parallelogram_path z ω1 ω2"
have w: "w ∉ path_image ?P"
using assms unfolding interior_period_parallelogram path_image_parallelogram_path'
by (auto simp: of_ω12_coords_eq_iff box_prod)
define ind where "ind = (λa b. winding_number (linepath (z + a) (z +b)) w)"
define u where "u = w - z"
define x y where "x = ω1_coord u" and "y = ω2_coord u"
have u_eq: "u = of_ω12_coords (x, y)"
by (simp_all add: x_def y_def flip: ω12_coords_def)
have xy: "x ∈ {0<..<1}" "y ∈ {0<..<1}" using assms(1)
unfolding interior_period_parallelogram image_plus_conv_vimage_plus of_ω12_coords_image_eq
by (auto simp: x_def y_def ω12_coords_def u_def box_prod)
have w_eq: "w = z + of_ω12_coords (x, y)"
using u_eq by (simp add: u_def algebra_simps)
define W where "W = winding_number (parallelogram_path z ω1 ω2) w"
have Re_W_eq: "Re W = Re (ind 0 ω1) + Re (ind ω1 (ω1 + ω2)) + Re (ind (ω1 + ω2) ω2) + Re (ind ω2 0)"
using w unfolding W_def parallelogram_path_def
by (simp add: winding_number_join ind_def path_image_join add_ac)
show ?thesis
proof (cases "Im (ω2 / ω1)" "0::real" rule: linorder_cases)
case equal
hence False
using fundpair complex_is_Real_iff by (auto simp: fundpair_def)
thus ?thesis ..
next
case greater
have "W = 1"
unfolding W_def
proof (rule simple_closed_path_winding_number_pos; (fold W_def)?)
from greater have neg: "Im (ω1 * cnj ω2) < 0"
by (subst (asm) Im_complex_div_gt_0) (auto simp: mult_ac)
have pos1: "Re (ind 0 ω1) > 0"
proof -
have "Im ((z + ω1 - (z + 0)) * cnj (z + ω1 - w)) = y * (-Im (ω1 * cnj ω2))"
by (simp add: w_eq algebra_simps of_ω12_coords_def)
also have "… > 0"
using neg xy by (intro mult_pos_pos) auto
finally show ?thesis
unfolding ind_def by (rule winding_number_linepath_pos_lt)
qed
have pos2: "Re (ind ω1 (ω1 + ω2)) > 0"
proof -
have "Im ((z + (ω1 + ω2) - (z + ω1)) * cnj (z + (ω1 + ω2) - w)) =
(1 - x) * (-Im (ω1 * cnj ω2))"
by (simp add: w_eq algebra_simps of_ω12_coords_def)
also have "… > 0"
using neg xy by (intro mult_pos_pos) auto
finally show ?thesis
unfolding ind_def by (rule winding_number_linepath_pos_lt)
qed
have pos3: "Re (ind (ω1 + ω2) ω2) > 0"
proof -
have "Im ((z + ω2 - (z + (ω1 + ω2))) * cnj (z + ω2 - w)) =
(1 - y) * (-Im (ω1 * cnj ω2))"
by (simp add: w_eq algebra_simps of_ω12_coords_def)
also have "… > 0"
using neg xy by (intro mult_pos_pos) auto
finally show ?thesis
unfolding ind_def by (rule winding_number_linepath_pos_lt)
qed
have pos4: "Re (ind ω2 0) > 0"
proof -
have "Im ((z + 0 - (z + ω2)) * cnj (z + 0 - w)) =
x * (-Im (ω1 * cnj ω2))"
by (simp add: w_eq algebra_simps of_ω12_coords_def)
also have "… > 0"
using neg xy by (intro mult_pos_pos) auto
finally show ?thesis
unfolding ind_def by (rule winding_number_linepath_pos_lt)
qed
show "Re W > 0"
using pos1 pos2 pos3 pos4 unfolding Re_W_eq by linarith
qed (use w in ‹auto intro: simple_path_parallelogram›)
thus ?thesis
using greater by (simp add: W_def)
next
case less
have "W = -1"
unfolding W_def
proof (rule simple_closed_path_winding_number_neg; (fold W_def)?)
from less have neg: "Im (ω2 * cnj ω1) < 0"
by (simp add: Im_complex_div_lt_0)
have neg1: "Re (ind 0 ω1) < 0"
proof -
have "Im ((z + 0 - (z + ω1)) * cnj (z + 0 - w)) = y * (-Im (ω2 * cnj ω1))"
by (simp add: w_eq algebra_simps of_ω12_coords_def)
also have "… > 0"
using neg xy by (intro mult_pos_pos) auto
finally show ?thesis
unfolding ind_def by (rule winding_number_linepath_neg_lt)
qed
have neg2: "Re (ind ω1 (ω1 + ω2)) < 0"
proof -
have "Im ((z + ω1 - (z + (ω1 + ω2))) * cnj (z + ω1 - w)) =
(1 - x) * (-Im (ω2 * cnj ω1))"
by (simp add: w_eq algebra_simps of_ω12_coords_def)
also have "… > 0"
using neg xy by (intro mult_pos_pos) auto
finally show ?thesis
unfolding ind_def by (rule winding_number_linepath_neg_lt)
qed
have neg3: "Re (ind (ω1 + ω2) ω2) < 0"
proof -
have "Im ((z + (ω1 + ω2) - (z + ω2)) * cnj (z + (ω1 + ω2) - w)) =
(1 - y) * (-Im (ω2 * cnj ω1))"
by (simp add: w_eq algebra_simps of_ω12_coords_def)
also have "… > 0"
using neg xy by (intro mult_pos_pos) auto
finally show ?thesis
unfolding ind_def by (rule winding_number_linepath_neg_lt)
qed
have neg4: "Re (ind ω2 0) < 0"
proof -
have "Im ((z + ω2 - (z + 0)) * cnj (z + ω2 - w)) =
x * (-Im (ω2 * cnj ω1))"
by (simp add: w_eq algebra_simps of_ω12_coords_def)
also have "… > 0"
using neg xy by (intro mult_pos_pos) auto
finally show ?thesis
unfolding ind_def by (rule winding_number_linepath_neg_lt)
qed
show "Re W < 0"
using neg1 neg2 neg3 neg4 unfolding Re_W_eq by linarith
qed (use w in ‹auto intro: simple_path_parallelogram›)
thus ?thesis
using less by (simp add: W_def)
qed
qed
end
subsection ‹Canonical representatives and the fundamental parallelogram›
context complex_lattice
begin
text ‹
The following function maps any complex number ‹z› to its canonical representative ‹z'›
in the fundamental period parallelogram.
›
definition to_fund_parallelogram :: "complex ⇒ complex" where
"to_fund_parallelogram z =
(case ω12_coords z of (a, b) ⇒ of_ω12_coords (frac a, frac b))"
lemma to_fund_parallelogram_in_parallelogram [intro]:
"to_fund_parallelogram z ∈ period_parallelogram 0"
unfolding to_fund_parallelogram_def
by (auto simp: period_parallelogram_altdef case_prod_unfold frac_lt_1)
lemma ω1_coord_to_fund_parallelogram [simp]: "ω1_coord (to_fund_parallelogram z) = frac (ω1_coord z)"
and ω2_coord_to_fund_parallelogram [simp]: "ω2_coord (to_fund_parallelogram z) = frac (ω2_coord z)"
by (auto simp: to_fund_parallelogram_def case_prod_unfold ω12_coords_def)
lemma to_fund_parallelogramE:
obtains m n where "to_fund_parallelogram z = z + of_int m * ω1 + of_int n * ω2"
proof -
define m where "m = floor (fst (ω12_coords z))"
define n where "n = floor (snd (ω12_coords z))"
have "z - of_int m * ω1 - of_int n * ω2 =
of_ω12_coords (ω12_coords z) - of_int m * ω1 - of_int n * ω2"
by (simp add: m_def n_def)
also have "… = to_fund_parallelogram z"
unfolding of_ω12_coords_def
by (simp add: case_prod_unfold to_fund_parallelogram_def frac_def
m_def n_def of_ω12_coords_def algebra_simps)
finally show ?thesis
by (intro that[of "-m" "-n"]) auto
qed
lemma rel_to_fund_parallelogram_left: "rel (to_fund_parallelogram z) z"
proof -
obtain m n where "to_fund_parallelogram z = z + of_int m * ω1 + of_int n * ω2"
by (elim to_fund_parallelogramE)
hence "to_fund_parallelogram z - z = of_int m * ω1 + of_int n * ω2"
by Groebner_Basis.algebra
also have "… = of_ω12_coords (of_int m, of_int n)"
by (simp add: of_ω12_coords_def)
also have "… ∈ Λ"
by (rule of_ω12_coords_in_lattice) auto
finally show ?thesis
by (simp add: rel_def)
qed
lemma rel_to_fund_parallelogram_right: "rel z (to_fund_parallelogram z)"
using rel_to_fund_parallelogram_left[of z] by (simp add: rel_sym)
lemma rel_to_fund_parallelogram_left_iff [simp]: "rel (to_fund_parallelogram z) w ⟷ rel z w"
using rel_sym rel_to_fund_parallelogram_right rel_trans by blast
lemma rel_to_fund_parallelogram_right_iff [simp]: "rel z (to_fund_parallelogram w) ⟷ rel z w"
using rel_sym rel_to_fund_parallelogram_left rel_trans by blast
lemma to_fund_parallelogram_in_lattice_iff [simp]:
"to_fund_parallelogram z ∈ lattice ⟷ z ∈ lattice"
using pre_complex_lattice.rel_0_left_iff rel_to_fund_parallelogram_right_iff by blast
lemma to_fund_parallelogram_in_lattice [lattice_intros]:
"z ∈ lattice ⟹ to_fund_parallelogram z ∈ lattice"
by simp
text ‹
\<^const>‹to_fund_parallelogram› is a bijective map from any period parallelogram to
the standard period parallelogram:
›
lemma bij_betw_to_fund_parallelogram:
"bij_betw to_fund_parallelogram (period_parallelogram orig) (period_parallelogram 0)"
proof -
have "bij_betw (of_ω12_coords ∘ map_prod frac frac ∘ ω12_coords)
(period_parallelogram orig) (period_parallelogram 0)"
proof (intro bij_betw_trans)
show "bij_betw of_ω12_coords ({0..<1}×{0..<1}) (period_parallelogram 0)"
by (rule bij_betwI[of _ _ _ ω12_coords]) (auto simp: period_parallelogram_altdef)
next
define a b where "a = ω1_coord orig" "b = ω2_coord orig"
have orig_eq: "orig = of_ω12_coords (a, b)"
by (auto simp: a_b_def simp flip: ω12_coords_def)
show "bij_betw ω12_coords (period_parallelogram orig)
({ω1_coord orig..<ω1_coord orig+1} × {ω2_coord orig..<ω2_coord orig+1})"
proof (rule bij_betwI[of _ _ _ of_ω12_coords])
show "ω12_coords
∈ period_parallelogram orig →
{ω1_coord orig..<ω1_coord orig + 1} × {ω2_coord orig..<ω2_coord orig + 1}"
by (auto simp: orig_eq period_parallelogram_def period_parallelogram_altdef ω12_coords.add)
next
show "of_ω12_coords ∈ {ω1_coord orig..<ω1_coord orig + 1} × {ω2_coord orig..<ω2_coord orig + 1} →
period_parallelogram orig"
proof safe
fix c d :: real
assume c: "c ∈ {ω1_coord orig..<ω1_coord orig + 1}"
assume d: "d ∈ {ω2_coord orig..<ω2_coord orig + 1}"
have "of_ω12_coords (c, d) = of_ω12_coords (a, b) + of_ω12_coords (c - a, d - b)"
by (simp add: of_ω12_coords_def algebra_simps)
moreover have "(c - a, d - b) ∈ {0..<1} × {0..<1}"
using c d unfolding a_b_def [symmetric] by auto
ultimately show "of_ω12_coords (c, d) ∈ period_parallelogram orig"
unfolding period_parallelogram_def period_parallelogram_altdef orig_eq image_image
by auto
qed
qed auto
next
show "bij_betw (map_prod frac frac)
({ω1_coord orig..<ω1_coord orig + 1} × {ω2_coord orig..<ω2_coord orig + 1})
({0..<1} × {0..<1})"
by (intro bij_betw_map_prod bij_betw_frac)
qed
also have "of_ω12_coords ∘ map_prod frac frac ∘ ω12_coords =
to_fund_parallelogram"
by (auto simp: o_def to_fund_parallelogram_def fun_eq_iff case_prod_unfold map_prod_def)
finally show ?thesis .
qed
text ‹
There exists a bijection between any two period parallelograms that always maps points to
equivalent points.
›
lemma bij_betw_period_parallelograms:
obtains f where
"bij_betw f (period_parallelogram orig) (period_parallelogram orig')"
"⋀z. rel (f z) z"
proof -
define h where "h = inv_into (period_parallelogram orig') to_fund_parallelogram"
show ?thesis
proof (rule that[of "h ∘ to_fund_parallelogram"])
show "bij_betw (h ∘ to_fund_parallelogram)
(period_parallelogram orig) (period_parallelogram orig')"
unfolding h_def
using bij_betw_to_fund_parallelogram bij_betw_inv_into[OF bij_betw_to_fund_parallelogram]
by (rule bij_betw_trans)
next
fix z :: complex
have "rel (to_fund_parallelogram (h (to_fund_parallelogram z))) (h (to_fund_parallelogram z))"
by auto
also have "to_fund_parallelogram (h (to_fund_parallelogram z)) = to_fund_parallelogram z"
unfolding h_def using bij_betw_to_fund_parallelogram[of orig']
by (subst f_inv_into_f[of _ to_fund_parallelogram])
(simp_all add: bij_betw_def to_fund_parallelogram_in_parallelogram)
finally have *: "rel (to_fund_parallelogram z) (h (to_fund_parallelogram z))" .
have "rel ((to_fund_parallelogram z - z)) (to_fund_parallelogram z - h (to_fund_parallelogram z))"
using * diff_in_lattice rel_def rel_to_fund_parallelogram_left by blast
thus "rel ((h ∘ to_fund_parallelogram) z) z"
using * pre_complex_lattice.rel_sym by force
qed
qed
lemma to_fund_parallelogram_0 [simp]: "to_fund_parallelogram 0 = 0"
by (simp add: to_fund_parallelogram_def zero_prod_def)
lemma to_fund_parallelogram_lattice [simp]: "z ∈ Λ ⟹ to_fund_parallelogram z = 0"
by (auto simp: to_fund_parallelogram_def in_lattice_conv_ω12_coords)
lemma to_fund_parallelogram_eq_iff [simp]:
"to_fund_parallelogram u = to_fund_parallelogram v ⟷ rel u v"
proof
assume "rel u v"
then obtain z where z: "z ∈ Λ" "v = u + z"
by (elim relE)
from this(1) obtain m n where mn: "z = of_ω12_coords (of_int m, of_int n)"
by (elim latticeE)
show "to_fund_parallelogram u = to_fund_parallelogram v" unfolding z(2)
by (simp add: to_fund_parallelogram_def ω12_coords.add in_lattice_conv_ω12_coords mn case_prod_unfold)
next
assume "to_fund_parallelogram u = to_fund_parallelogram v"
thus "rel u v"
by (metis rel_to_fund_parallelogram_right rel_to_fund_parallelogram_right_iff)
qed
lemma to_fund_parallelogram_eq_0_iff [simp]: "to_fund_parallelogram u = 0 ⟷ u ∈ Λ"
using to_fund_parallelogram_eq_iff[of u 0]
by (simp del: to_fund_parallelogram_eq_iff add: rel_0_right_iff)
lemma to_fund_parallelogram_of_fund_parallelogram:
"z ∈ period_parallelogram 0 ⟹ to_fund_parallelogram z = z"
unfolding to_fund_parallelogram_def period_parallelogram_def
by (auto simp: of_ω12_coords_eq_iff frac_eq_id)
lemma to_fund_parallelogram_idemp [simp]:
"to_fund_parallelogram (to_fund_parallelogram z) = to_fund_parallelogram z"
by (rule to_fund_parallelogram_of_fund_parallelogram) auto
lemma to_fund_parallelogram_unique:
assumes "rel z z'" "z' ∈ period_parallelogram 0"
shows "to_fund_parallelogram z = z'"
using assms by (metis to_fund_parallelogram_eq_iff to_fund_parallelogram_of_fund_parallelogram)
lemma to_fund_parallelogram_unique':
assumes "rel z z'" "z ∈ period_parallelogram 0" "z' ∈ period_parallelogram 0"
shows "z = z'"
using assms
by (metis to_fund_parallelogram_eq_iff to_fund_parallelogram_of_fund_parallelogram)
text ‹
The following is the ``left half'' of the fundamental parallelogram. The bottom border is
contained, the top border is not. Of the frontier of this parallelogram only the upper half
is
›
definition (in pre_complex_lattice) half_fund_parallelogram where
"half_fund_parallelogram =
of_ω12_coords ` {(x,y). x ∈ {0..1/2} ∧ y ∈ {0..<1} ∧ (x ∈ {0, 1/2} ⟶ y ≤ 1/2)}"
lemma half_fund_parallelogram_altdef:
"half_fund_parallelogram = ω12_coords -` {(x,y). x ∈ {0..1/2} ∧ y ∈ {0..<1} ∧ (x ∈ {0, 1/2} ⟶ y ≤ 1/2)}"
unfolding half_fund_parallelogram_def by (meson of_ω12_coords_image_eq)
lemma zero_in_half_fund_parallelogram [simp, intro]: "0 ∈ half_fund_parallelogram"
by (auto simp: half_fund_parallelogram_altdef zero_prod_def)
lemma half_fund_parallelogram_in_lattice_iff:
assumes "z ∈ half_fund_parallelogram"
shows "z ∈ Λ ⟷ z = 0"
proof
assume "z ∈ Λ"
then obtain m n where z_eq: "z = of_ω12_coords (of_int m, of_int n)"
by (elim latticeE)
thus "z = 0"
using assms unfolding z_eq half_fund_parallelogram_altdef by auto
qed auto
definition to_half_fund_parallelogram :: "complex ⇒ complex" where
"to_half_fund_parallelogram z =
(let (x,y) = map_prod frac frac (ω12_coords z);
(x',y') = (if x > 1/2 ∨ (x ∈ {0, 1/2} ∧ y > 1 / 2) then (if x = 0 then 0 else 1 - x, if y = 0 then 0 else 1 - y) else (x, y))
in of_ω12_coords (x',y'))"
lemma in_Ints_conv_floor: "x ∈ ℤ ⟷ x = of_int (floor x)"
by (metis Ints_of_int of_int_floor)
lemma (in complex_lattice) rel_to_half_fund_parallelogram:
"rel z (to_half_fund_parallelogram z) ∨ rel z (-to_half_fund_parallelogram z)"
unfolding rel_def in_lattice_conv_ω12_coords to_half_fund_parallelogram_def Let_def
ω1_coord.diff ω2_coord.diff ω1_coord.add ω2_coord.add ω1_coord.neg ω2_coord.neg
case_prod_unfold Let_def ω12_coords_def frac_def map_prod_def
by (simp flip: in_Ints_conv_floor)
lemma (in complex_lattice) to_half_fund_parallelogram_in_half_fund_parallelogram [intro]:
"to_half_fund_parallelogram z ∈ half_fund_parallelogram"
unfolding half_fund_parallelogram_altdef to_half_fund_parallelogram_def to_half_fund_parallelogram_def Let_def
ω1_coord.diff ω2_coord.diff ω1_coord.add ω2_coord.add ω1_coord.neg ω2_coord.neg
case_prod_unfold Let_def ω12_coords_def frac_def map_prod_def
apply simp
apply linarith
done
lemma (in complex_lattice) half_fund_parallelogram_subset_period_parallelogram:
"half_fund_parallelogram ⊆ period_parallelogram 0"
proof -
have "of_ω12_coords ` {(x, y). x ∈ {0..1 / 2} ∧ y ∈ {0..<1} ∧ (x ∈ {0,1/2} ⟶ y ≤ 1 / 2)} ⊆
of_ω12_coords ` ({0..<1} × {0..<1})"
by (intro image_mono) (auto simp: not_less)
also have "… = (+) 0 ` (of_ω12_coords ` ({0..<1} × {0..<1}))"
by simp
finally show ?thesis
unfolding period_parallelogram_def half_fund_parallelogram_def .
qed
lemma to_half_fund_parallelogram_in_lattice_iff [simp]: "to_half_fund_parallelogram z ∈ Λ ⟷ z ∈ Λ"
by (metis rel_lattice_trans_left rel_sym rel_to_half_fund_parallelogram uminus_in_lattice_iff)
lemma rel_in_half_fund_parallelogram_imp_eq:
assumes "rel z w ∨ rel z (-w)" "z ∈ half_fund_parallelogram" "w ∈ half_fund_parallelogram"
shows "z = w"
using assms(1)
proof
assume "rel z w"
moreover from assms have "z ∈ period_parallelogram 0" "w ∈ period_parallelogram 0"
using half_fund_parallelogram_subset_period_parallelogram by blast+
ultimately show "z = w"
by (metis to_fund_parallelogram_eq_iff
to_fund_parallelogram_of_fund_parallelogram)
next
assume "rel z (-w)"
hence "rel (-w) z"
by (rule rel_symI)
then obtain m n where z_eq: "z = -w + of_ω12_coords (of_int m, of_int n)"
by (elim relE latticeE) auto
define x y where "x = ω1_coord w" "y = ω2_coord w"
have w_eq: "w = of_ω12_coords (x, y)"
unfolding x_y_def ω12_coords_def [symmetric] by simp
have 1: "x ≥ 0" "y ≥ 0" "x ≤ 1/2" "y < 1" "x = 0 ∨ x = 1/2 ⟹ y ≤ 1/2"
using assms(3) unfolding half_fund_parallelogram_altdef w_eq by auto
have 2: "of_int m - x ≥ 0" "of_int n - y ≥ 0" "of_int m - x ≤ 1/2" "of_int n - y < 1"
"of_int m - x = 0 ∨ of_int m - x = 1/2 ⟹ of_int n - y ≤ 1/2"
using assms(2) unfolding half_fund_parallelogram_altdef z_eq w_eq
by (auto simp: ω12_coords.diff)
have "m ∈ {0,1}" "n ∈ {0,1}"
using 1 2 by auto
hence "real_of_int m = 2 * x ∧ real_of_int n = 2 * y"
using 1 2 by auto
hence "ω12_coords z = ω12_coords w"
unfolding z_eq w_eq ω12_coords.add ω12_coords.diff ω12_coords.neg ω12_coords_of_ω12_coords
by simp
thus ?thesis
by (metis of_ω12_coords_ω12_coords)
qed
lemma to_half_fund_parallelogram_of_half_fund_parallelogram:
assumes "z ∈ half_fund_parallelogram"
shows "to_half_fund_parallelogram z = z"
by (metis assms rel_to_half_fund_parallelogram to_half_fund_parallelogram_in_half_fund_parallelogram rel_in_half_fund_parallelogram_imp_eq)
lemma to_half_fund_parallelogram_idemp [simp]:
"to_half_fund_parallelogram (to_half_fund_parallelogram z) = to_half_fund_parallelogram z"
by (rule to_half_fund_parallelogram_of_half_fund_parallelogram) auto
lemma to_half_fund_parallelogram_unique:
assumes "rel z z' ∨ rel z (-z')" "z' ∈ half_fund_parallelogram"
shows "to_half_fund_parallelogram z = z'"
proof (rule rel_in_half_fund_parallelogram_imp_eq)
show "rel (to_half_fund_parallelogram z) z' ∨ rel (to_half_fund_parallelogram z) (- z')"
using rel_to_half_fund_parallelogram[of z] assms rel_sym rel_trans rel_minus minus_minus
by metis
qed (use to_half_fund_parallelogram_in_half_fund_parallelogram assms in auto)
lemma to_half_fund_parallelogram_eq_iff:
"to_half_fund_parallelogram z = to_half_fund_parallelogram w ⟷ rel z w ∨ rel z (-w)"
proof
assume eq: "to_half_fund_parallelogram z = to_half_fund_parallelogram w"
define u where "u = to_half_fund_parallelogram w"
have "rel z u ∨ rel z (-u)" "rel w u ∨ rel w (-u)"
using rel_to_half_fund_parallelogram[of z] rel_to_half_fund_parallelogram[of w] eq unfolding u_def by auto
hence "rel z w ∨ (rel z u ∧ rel w (-u) ∨ rel z (-u) ∧ rel w u)"
using rel_trans rel_sym by blast
moreover have "rel z (-w)" if "rel z u ∧ rel w (-u) ∨ rel z (-u) ∧ rel w u"
using that by (metis minus_minus pre_complex_lattice.rel_minus rel_sym rel_trans)
ultimately show "rel z w ∨ rel z (-w)" by blast
next
assume *: "rel z w ∨ rel z (-w)"
define u where "u = to_half_fund_parallelogram w"
show "to_half_fund_parallelogram z = u"
proof (rule to_half_fund_parallelogram_unique)
have "rel w u ∨ rel w (-u)"
unfolding u_def using rel_to_half_fund_parallelogram[of w] by blast
with * have "rel z u ∨ (rel (-w) (-u) ∧ rel z (-w) ∨ rel w (-u) ∧ rel z w)"
using rel_trans rel_sym rel_minus[of w "-u"] rel_minus[of z "-w"] rel_minus[of w u]
unfolding minus_minus by blast
thus "rel z u ∨ rel z (-u)"
using rel_trans rel_sym by blast
qed (auto simp: u_def)
qed
lemma in_half_fund_parallelogram_imp_half_lattice:
assumes "z ∈ half_fund_parallelogram" "to_fund_parallelogram (-z) ∈ half_fund_parallelogram"
shows "2 * z ∈ Λ"
using assms
by (metis rel_in_half_fund_parallelogram_imp_eq diff_minus_eq_add mult_2
pre_complex_lattice.rel_def rel_to_fund_parallelogram_left)
end
subsection ‹Equivalence of fundamental pairs›
text ‹
Two fundamental pairs are called ∗‹equivalent› if they generate the same complex lattice.
›
definition equiv_fundpair :: "complex × complex ⇒ complex × complex ⇒ bool" where
"equiv_fundpair = (λ(ω1, ω2) (ω1', ω2').
pre_complex_lattice.lattice ω1 ω2 = pre_complex_lattice.lattice ω1' ω2')"
lemma equiv_fundpair_iff_aux:
fixes p :: int
assumes "p * c + q * a = 0" "p * d + q * b = 1"
"r * c + s * a = 1" "r * d + s * b = 0"
shows "¦a * d - b * c¦ = 1"
proof -
have "r * b * c + s * a * b = b"
by (metis assms(3) distrib_left mult.left_commute mult.right_neutral)
moreover have "r * a * d + s * a * b = 0"
by (metis assms(4) distrib_left mult.commute mult.left_commute mult_zero_right)
ultimately have "r dvd b"
by (metis mult.assoc dvd_0_right dvd_add_right_iff dvd_triv_left)
have "p * r * d + p * s * b = 0"
by (metis assms(4) distrib_left mult.commute mult.left_commute mult_zero_right)
moreover have "p * r * d + q * r * b = r"
by (metis assms(2) int_distrib(2) mult.assoc mult.left_commute mult.right_neutral)
ultimately have "b dvd r"
by (metis dvd_0_right mult.commute zdvd_reduce)
have "r * c * d + s * b * c = 0"
by (metis assms(4) distrib_left mult.commute mult.left_commute mult_zero_right)
moreover have "r * c * d + s * a * d = d"
by (metis assms(3) distrib_left mult.commute mult.right_neutral)
ultimately have "s dvd d"
by (metis dvd_0_right dvd_add_times_triv_right_iff mult.assoc mult.commute)
have "q * r * d + q * s * b = 0"
by (metis mult.assoc assms(4) int_distrib(2) mult_not_zero)
moreover have "p * s * d + q * s * b = s"
by (metis assms(2) int_distrib(2) mult.assoc mult.left_commute mult.right_neutral)
ultimately have "d dvd s"
by (metis add.commute dvd_0_right mult.commute zdvd_reduce)
have "¦b¦ = ¦r¦" "¦d¦ = ¦s¦"
by (meson ‹b dvd r› ‹r dvd b› ‹d dvd s› ‹s dvd d› zdvd_antisym_abs)+
then show ?thesis
by (smt (verit, best) assms(3,4) mult.commute mult_cancel_left mult_eq_0_iff mult_minus_left)
qed
text ‹
The following fact is Theorem 1.2 in Apostol's book: two fundamental pairs are equivalent
iff there exists a unimodular transformation that maps one to the other.
›
theorem equiv_fundpair_iff:
fixes ω1 ω2 ω1' ω2' :: complex
assumes "fundpair (ω1, ω2)" "fundpair (ω1', ω2')"
shows "equiv_fundpair (ω1, ω2) (ω1', ω2') ⟷
(∃a b c d. ¦a*d - b*c¦ = 1 ∧
ω2' = of_int a * ω2 + of_int b * ω1 ∧ ω1' = of_int c * ω2 + of_int d * ω1)"
(is "?lhs = ?rhs")
proof -
interpret gl: complex_lattice ω1 ω2
by standard fact
interpret gl': complex_lattice ω1' ω2'
by standard fact
show ?thesis
proof
assume L: ?lhs
hence lattices_eq: "gl.lattice = gl'.lattice"
by (simp add: equiv_fundpair_def)
have "ω1' ∈ gl'.lattice" "ω2' ∈ gl'.lattice"
by auto
hence "ω1' ∈ gl.lattice" "ω2' ∈ gl.lattice"
by (simp_all add: lattices_eq)
then obtain a b c d
where ab: "ω2' = of_int b * ω1 + of_int a * ω2"
and cd: "ω1' = of_int d * ω1 + of_int c * ω2"
by (elim gl.latticeE) (auto simp: gl.of_ω12_coords_def scaleR_conv_of_real)
have "ω1 ∈ gl.lattice" "ω2 ∈ gl.lattice"
by auto
hence "ω1 ∈ gl'.lattice" "ω2 ∈ gl'.lattice"
by (simp_all add: lattices_eq)
then obtain p q r s
where pq: "ω1 = of_int p * ω1' + of_int q * ω2'" and
rs: "ω2 = of_int r * ω1' + of_int s * ω2'"
by (elim gl'.latticeE) (auto simp: gl'.of_ω12_coords_def scaleR_conv_of_real)
have "ω1 = p * (c * ω2 + d * ω1) + q * (a * ω2 + b * ω1)"
using pq cd ab add.commute by metis
also have "... = (p * c + q * a) * ω2 + (p * d + q * b) * ω1"
by (simp add: algebra_simps)
finally have "gl.of_ω12_coords (1, 0) = gl.of_ω12_coords (p*d+q*b, p*c+q*a)"
by (simp_all add: gl.of_ω12_coords_def add_ac)
hence pc: "(p * c + q * a) = 0 ∧ p * d + q * b = 1"
unfolding gl.of_ω12_coords_eq_iff prod.case prod.inject by linarith
have "ω2 = r * (c * ω2 + d * ω1) + s * (a * ω2 + b * ω1)"
using cd rs ab add.commute by metis
also have "... = (r * c + s * a) * ω2 + (r * d + s * b) * ω1"
by (simp add: algebra_simps)
finally have "gl.of_ω12_coords (0, 1) = gl.of_ω12_coords (r*d+s*b, r*c+s*a)"
by (simp_all add: gl.of_ω12_coords_def add_ac)
hence rc: "r * c + s * a = 1 ∧ r * d + s * b = 0"
unfolding gl.of_ω12_coords_eq_iff prod.case prod.inject by linarith
with pc have "¦a*d - b*c¦ = 1"
by (meson equiv_fundpair_iff_aux)
hence "¦a*d - b*c¦ = 1 ∧
ω2' = of_int a * ω2 + of_int b * ω1 ∧ ω1' = of_int c * ω2 + of_int d * ω1"
using cd ab by auto
thus ?rhs
by blast
next
assume ?rhs
then obtain a b c d :: int where 1: "¦a * d - b * c¦ = 1"
and eq: "ω2' = of_int a * ω2 + of_int b * ω1" "ω1' = of_int c * ω2 + of_int d * ω1"
by blast
define det where "det = a * d - b * c"
define a' b' c' d' where "a' = det * d" "b' = -det * b" "c' = -det * c" "d' = det * a"
have "¦det¦ = 1"
using 1 by (simp add: det_def)
hence det_square: "det ^ 2 = 1"
using abs_square_eq_1 by blast
have eq': "ω2 = of_int a' * ω2' + of_int b' * ω1'" "ω1 = of_int c' * ω2' + of_int d' * ω1'"
proof -
have "of_int a' * ω2' + of_int b' * ω1' = det^2 * ω2"
by (simp add: eq algebra_simps det_def a'_b'_c'_d'_def power2_eq_square)
thus "ω2 = of_int a' * ω2' + of_int b' * ω1'"
by (simp add: det_square)
next
have "of_int c' * ω2' + of_int d' * ω1' = det^2 * ω1"
by (simp add: eq algebra_simps det_def a'_b'_c'_d'_def power2_eq_square)
thus "ω1 = of_int c' * ω2' + of_int d' * ω1'"
by (simp add: det_square)
qed
have "gl'.lattice ⊆ gl.lattice"
by (safe elim!: gl'.latticeE, unfold gl'.of_ω12_coords_def)
(auto simp: eq ring_distribs intro!: gl'.lattice_intros)
moreover have "gl.lattice ⊆ gl'.lattice"
by (safe elim!: gl.latticeE, unfold gl.of_ω12_coords_def)
(auto simp: eq' ring_distribs intro!: gl.lattice_intros)
ultimately show ?lhs
unfolding equiv_fundpair_def by auto
qed
qed
text ‹
We will now look at the triangle spanned by the origin and the generators.
We will prove that the only points that lie in or on this triangle are its three vertices.
Moreover, we shall prove that for any lattice ‹Λ›, if we have two points ‹ω⇩1', ω⇩2' ∈ Λ›
then these two points generate ‹Λ› if and only if the triangle spanned by ‹0›, ‹ω⇩1'›, and ‹ω⇩2'›
contains no other lattice points except ‹0›, ‹ω⇩1'›, and ‹ω⇩2'›.
›
context complex_lattice
begin
lemma in_triangle_iff:
fixes x
defines "a ≡ ω1_coord x" and "b ≡ ω2_coord x"
shows "x ∈ convex hull {0, ω1, ω2} ⟷ a ≥ 0 ∧ b ≥ 0 ∧ a + b ≤ 1"
proof
assume "x ∈ convex hull {0, ω1, ω2}"
then obtain t u where tu: "u ≥ 0" "t ≥ 0" "u + t ≤ 1" "x = of_ω12_coords (u, t)"
unfolding convex_hull_3_alt by (auto simp: of_ω12_coords_def scaleR_conv_of_real)
have "a = u" "b = t"
by (auto simp: a_def b_def tu(4))
with tu show "a ≥ 0 ∧ b ≥ 0 ∧ a + b ≤ 1"
by auto
next
assume ab: "a ≥ 0 ∧ b ≥ 0 ∧ a + b ≤ 1"
have "x = of_ω12_coords (a, b)"
by (auto simp: a_def b_def simp flip: ω12_coords_def)
hence "x = 0 + a *⇩R (ω1 - 0) + b *⇩R (ω2 - 0)" "0 ≤ a ∧ 0 ≤ b ∧ a + b ≤ 1"
using ab by (auto simp: a_def b_def of_ω12_coords_def scaleR_conv_of_real)
thus "x ∈ convex hull {0, ω1, ω2}"
unfolding convex_hull_3_alt by blast
qed
text ‹
The only lattice points inside the fundamental triangle are the generators and the origin.
›
lemma lattice_Int_triangle: "convex hull {0, ω1, ω2} ∩ Λ = {0, ω1, ω2}"
proof (intro equalityI subsetI)
fix x assume x: "x ∈ convex hull {0, ω1, ω2} ∩ Λ"
then obtain a b :: real where ab: "a ≥ 0" "b ≥ 0" "a + b ≤ 1" "x = of_ω12_coords (a, b)"
unfolding convex_hull_3_alt by (auto simp: of_ω12_coords_def scaleR_conv_of_real)
from ab(4) and x have "a ∈ ℤ" "b ∈ ℤ"
by (auto simp: of_ω12_coords_in_lattice_iff)
with ab(1-3) have "(a, b) ∈ {(0, 0), (0, 1), (1, 0)}"
by (auto elim!: Ints_cases)
with ab show "x ∈ {0, ω1, ω2}"
by auto
qed (auto intro: hull_inc)
text ‹
The following fact is Theorem~1.1 in Apostol's book: given a fixed lattice ‹Λ›, a pair of
non-collinear period vectors $\omega_1$, $\omega_2$ is fundamental (i.e.\ generates ‹Λ›) iff the
triangle spanned by $0$, $\omega_1$, $\omega_2$ contains no lattice points other than its
three vertices.
›
lemma equiv_fundpair_iff_triangle:
assumes "fundpair (ω1', ω2')" "ω1' ∈ Λ" "ω2' ∈ Λ"
shows "equiv_fundpair (ω1, ω2) (ω1', ω2') ⟷ convex hull {0, ω1', ω2'} ∩ Λ = {0, ω1', ω2'}"
proof -
interpret lattice': complex_lattice ω1' ω2'
by standard fact
show ?thesis
proof
assume "equiv_fundpair (ω1, ω2) (ω1', ω2')"
thus "convex hull {0, ω1', ω2'} ∩ Λ = {0, ω1', ω2'}"
using lattice'.lattice_Int_triangle by (simp add: equiv_fundpair_def)
next
assume triangle: "convex hull {0, ω1', ω2'} ∩ Λ = {0, ω1', ω2'}"
show "equiv_fundpair (ω1, ω2) (ω1', ω2')"
unfolding equiv_fundpair_def prod.case
proof
show "lattice'.lattice ⊆ Λ"
by (intro subsetI, elim lattice'.latticeE)
(auto simp: lattice'.of_ω12_coords_def intro!: lattice_intros assms)
next
show "Λ ⊆ lattice'.lattice"
proof
fix x assume x: "x ∈ Λ"
define y where "y = lattice'.to_fund_parallelogram x"
have y: "y ∈ Λ"
proof -
obtain a b where y_eq: "y = x + of_int a * ω1' + of_int b * ω2'"
using lattice'.to_fund_parallelogramE[of x] unfolding y_def by blast
show ?thesis by (auto simp: y_eq intro!: lattice_intros assms x)
qed
have "y ∈ lattice'.lattice"
proof (cases "y ∈ convex hull {0, ω1', ω2'}")
case True
hence "y ∈ convex hull {0, ω1', ω2'} ∩ Λ"
using y by auto
also note triangle
finally show ?thesis
by auto
next
case False
define y' where "y' = ω1' + ω2' - y"
have y_conv_y': "y = ω1' + ω2' - y'"
by (simp add: y'_def)
define a b where "a = lattice'.ω1_coord x" and "b = lattice'.ω2_coord x"
have [simp]: "lattice'.ω1_coord y = frac a" "lattice'.ω2_coord y = frac b"
by (simp_all add: y_def a_def b_def)
from False have "frac a + frac b > 1"
by (auto simp: lattice'.in_triangle_iff y'_def)
hence "y' ∈ convex hull {0, ω1', ω2'}"
by (auto simp: lattice'.in_triangle_iff y'_def less_imp_le[OF frac_lt_1]
lattice'.ω1_coord.add lattice'.ω2_coord.add
lattice'.ω1_coord.diff lattice'.ω2_coord.diff)
hence "y' ∈ convex hull {0, ω1', ω2'} ∩ Λ"
using y assms by (auto simp: y'_def intro!: lattice_intros)
also note triangle
finally have "y' ∈ {0, ω1', ω2'}" .
thus ?thesis
by (auto simp: y_conv_y' intro!: lattice'.lattice_intros)
qed
thus "x ∈ lattice'.lattice"
by (simp add: y_def)
qed
qed
qed
qed
end
subsection ‹Additional useful facts›
context complex_lattice
begin
text ‹
The following partitions the lattice into countably many ``layers'', starting from the origin,
which is the 0-th layer. The $k$-th layer consists of precisely those points in the lattice
whose lattice coordinates $(m,n)$ satisfy $\max(|m|,|n|) = k$.
›
definition lattice_layer :: "nat ⇒ complex set" where
"lattice_layer k =
of_ω12_coords ` map_prod of_int of_int `
({int k, -int k} × {-int k..int k} ∪ {-int k..int k} × {-int k, int k})"
lemma in_lattice_layer_iff:
"z ∈ lattice_layer k ⟷
ω12_coords z ∈ ℤ × ℤ ∩ ({int k, -int k} × {-int k..int k} ∪ {-int k..int k} × {-int k, int k})"
(is "?lhs = ?rhs")
proof
assume ?lhs
thus ?rhs
unfolding lattice_layer_def of_ω12_coords_image_eq by (auto simp: case_prod_unfold)
next
assume ?rhs
thus ?lhs unfolding lattice_layer_def image_Un map_prod_image of_ω12_coords_image_eq
by (auto elim!: Ints_cases)
qed
lemma of_ω12_coords_of_int_in_lattice_layer:
"of_ω12_coords (of_int a, of_int b) ∈ lattice_layer (nat (max ¦a¦ ¦b¦))"
unfolding in_lattice_layer_iff by (auto simp flip: of_int_minus simp: max_def)
lemma lattice_layer_covers: "Λ = (⋃k. lattice_layer k)"
proof -
have "(⋃k. lattice_layer k) = of_ω12_coords ` map_prod real_of_int real_of_int `
(⋃k. ({int k, - int k} × {- int k..int k} ∪ {- int k..int k} × {- int k, int k}))"
(is "_ = _ ` _ ` (⋃k. ?A k)") unfolding lattice_layer_def by blast
also have "(⋃k. ?A k) = UNIV"
proof safe
fix a b :: int
have "(a, b) ∈ ?A (nat (max ¦a¦ ¦b¦))"
unfolding max_def by simp linarith
thus "(a, b) ∈ (⋃k. ?A k)"
by blast
qed blast+
also have "range (map_prod real_of_int real_of_int) = ℤ × ℤ"
by (auto elim!: Ints_cases)
finally show ?thesis
by (simp add: lattice_def)
qed
lemma finite_lattice_layer: "finite (lattice_layer k)"
unfolding lattice_layer_def by auto
lemma lattice_layer_0: "lattice_layer 0 = {0}"
by (auto simp: lattice_layer_def)
lemma zero_in_lattice_layer_iff [simp]: "0 ∈ lattice_layer k ⟷ k = 0"
by (auto simp: in_lattice_layer_iff zero_prod_def)
lemma lattice_layer_disjoint:
assumes "m ≠ n"
shows "lattice_layer m ∩ lattice_layer n = {}"
using assms by (auto simp: lattice_layer_def of_ω12_coords_eq_iff)
lemma lattice0_conv_layers: "Λ⇧* = (⋃i∈{0<..}. lattice_layer i)" (is "?lhs = ?rhs")
proof -
have "Λ⇧* = (⋃i∈UNIV. lattice_layer i) - lattice_layer 0"
by (simp add: lattice0_def lattice_layer_covers lattice_layer_0)
also have "… = (⋃i∈UNIV-{0}. lattice_layer i)"
using lattice_layer_disjoint by blast
also have "UNIV-{0::nat} = {0<..}"
by auto
finally show ?thesis .
qed
lemma card_lattice_layer:
assumes "k > 0"
shows "card (lattice_layer k) = 8 * k"
proof -
define f where "f = of_ω12_coords ∘ map_prod real_of_int real_of_int"
have "lattice_layer k = f ` ({int k, - int k} × {- int k..int k} ∪ {- int k..int k} × {- int k, int k})"
(is "_ = _ ` ?A") unfolding lattice_layer_def f_def image_image o_def ..
also have "card … = card ?A"
by (intro card_image)
(auto simp: inj_on_def of_ω12_coords_eq_iff f_def map_prod_def case_prod_unfold)
also have "?A = {int k, -int k} × {-int k..int k} ∪ {-int k+1..int k-1} × {-int k, int k}"
by auto
also have "card … = 8 * k" using ‹k > 0›
by (subst card_Un_disjoint)
(auto simp: nat_diff_distrib nat_add_distrib nat_mult_distrib Suc_diff_Suc)
finally show ?thesis .
qed
lemma lattice_layer_nonempty: "lattice_layer k ≠ {}"
by (auto simp: lattice_layer_def)
definition lattice_layer_path :: "complex set" where
"lattice_layer_path = of_ω12_coords ` ({1, -1} × {-1..1} ∪ {-1..1} × {-1, 1})"
lemma in_lattice_layer_path_iff:
"z ∈ lattice_layer_path ⟷ ω12_coords z ∈ ({1, -1} × {-1..1} ∪ {-1..1} × {-1, 1})"
unfolding lattice_layer_path_def of_ω12_coords_image_eq by blast
lemma lattice_layer_path_nonempty: "lattice_layer_path ≠ {}"
proof -
have "ω1 ∈ lattice_layer_path"
by (auto simp: in_lattice_layer_path_iff)
thus ?thesis by blast
qed
lemma compact_lattice_layer_path [intro]: "compact lattice_layer_path"
unfolding lattice_layer_path_def of_ω12_coords_def case_prod_unfold
by (intro compact_continuous_image continuous_intros compact_Un compact_Times) auto
lemma lattice_layer_subset: "lattice_layer k ⊆ (*) (of_nat k) ` lattice_layer_path"
proof
fix x
assume "x ∈ lattice_layer k"
then obtain m n where x: "x = of_ω12_coords (of_int m, of_int n)"
"(m, n) ∈ ({int k, -int k} × {-int k..int k} ∪ {-int k..int k} × {-int k, int k})"
unfolding lattice_layer_def by blast
show "x ∈ (*) (of_nat k) ` lattice_layer_path"
proof (cases "k > 0")
case True
have "x = of_nat k * of_ω12_coords (of_int m / of_int k, of_int n / of_int k)"
"(of_int m / of_int k, of_int n / of_int k) ∈ {1::real, -1} × {-1..1} ∪ {-1..1} × {-1::real, 1}"
using x True by (auto simp: divide_simps of_ω12_coords_def)
thus ?thesis
unfolding lattice_layer_path_def by blast
qed (use x in ‹auto simp: lattice_layer_path_def image_iff
intro!: exI[of _ "ω1"] bexI[of _ "(1, 0)"]›)
qed
text ‹
The shortest and longest distance of any point on the first layer from the origin,
respectively.
›
definition Inf_para :: real where
"Inf_para ≡ Inf (norm ` lattice_layer_path)"
lemma Inf_para_pos: "Inf_para > 0"
proof -
have "compact (norm ` lattice_layer_path)"
by (intro compact_continuous_image continuous_intros) auto
hence "Inf_para ∈ norm ` lattice_layer_path"
unfolding Inf_para_def
by (intro closed_contains_Inf)
(use lattice_layer_path_nonempty in ‹auto simp: compact_imp_closed bdd_below_norm_image›)
moreover have "∀x∈norm ` lattice_layer_path. x > 0"
by (auto simp: in_lattice_layer_path_iff zero_prod_def)
ultimately show ?thesis
by blast
qed
lemma Inf_para_nonzero [simp]: "Inf_para ≠ 0"
using Inf_para_pos by linarith
lemma Inf_para_le:
assumes "z ∈ lattice_layer_path"
shows "Inf_para ≤ norm z"
unfolding Inf_para_def by (rule cInf_lower) (use assms bdd_below_norm_image in auto)
lemma lattice_layer_le_norm:
assumes "ω ∈ lattice_layer k"
shows "k * Inf_para ≤ norm ω"
proof -
obtain z where z: "z ∈ lattice_layer_path" "ω = of_nat k * z"
using lattice_layer_subset[of k] assms by auto
have "real k * Inf_para ≤ real k * norm z"
by (intro mult_left_mono Inf_para_le z) auto
also have "… = norm ω"
by (simp add: z norm_mult)
finally show ?thesis .
qed
corollary Inf_para_le_norm:
assumes "ω ∈ Λ⇧*"
shows "Inf_para ≤ norm ω"
proof -
from assms obtain k where ω: "ω ∈ lattice_layer k" and "k ≠ 0"
unfolding lattice0_def by (metis DiffE UN_iff lattice_layer_0 lattice_layer_covers)
with Inf_para_pos have "Inf_para ≤ real k * Inf_para"
by auto
then show ?thesis
using ω lattice_layer_le_norm by force
qed
text ‹
One easy corollary is now that our lattice is discrete in the sense that there is a positive
real number that bounds the distance between any two points from below.
›
lemma Inf_para_le_dist:
assumes "x ∈ Λ" "y ∈ Λ" "x ≠ y"
shows "dist x y ≥ Inf_para"
proof -
have "x - y ∈ Λ" "x - y ≠ 0"
using assms by (auto intro: diff_in_lattice)
hence "x - y ∈ Λ⇧*"
by auto
hence "Inf_para ≤ norm (x - y)"
by (rule Inf_para_le_norm)
thus ?thesis
by (simp add: dist_norm)
qed
definition Sup_para :: real where
"Sup_para ≡ Sup (norm ` lattice_layer_path)"
lemma Sup_para_ge:
assumes "z ∈ lattice_layer_path"
shows "Sup_para ≥ norm z"
unfolding Sup_para_def
proof (rule cSup_upper)
show "bdd_above (norm ` lattice_layer_path)"
unfolding bdd_above_norm by (rule compact_imp_bounded) auto
qed (use assms in auto)
lemma Sup_para_pos: "Sup_para > 0"
proof -
have "0 < norm ω1"
using ω1_nonzero by auto
also have "… ≤ Sup_para"
by (rule Sup_para_ge) (auto simp: in_lattice_layer_path_iff)
finally show ?thesis .
qed
lemma Sup_para_nonzero [simp]: "Sup_para ≠ 0"
using Sup_para_pos by linarith
lemma lattice_layer_ge_norm:
assumes "ω ∈ lattice_layer k"
shows "norm ω ≤ k * Sup_para"
proof -
obtain z where z: "z ∈ lattice_layer_path" "ω = of_nat k * z"
using lattice_layer_subset[of k] assms by auto
have "norm ω = real k * norm z"
by (simp add: z norm_mult)
also have "… ≤ real k * Sup_para"
by (intro mult_left_mono Sup_para_ge z) auto
finally show ?thesis .
qed
text ‹
We can now easily show that our lattice is a sparse set (i.e. it has no limit points).
This also implies that it is closed.
›
lemma not_islimpt_lattice: "¬z islimpt Λ"
proof (rule discrete_imp_not_islimpt[of Inf_para])
fix x y assume "x ∈ Λ" "y ∈ Λ" "dist x y < Inf_para"
with Inf_para_le_dist[of x y] show "x = y"
by (cases "x = y") auto
qed (fact Inf_para_pos)
lemma closed_lattice: "closed lattice"
unfolding closed_limpt by (auto simp: not_islimpt_lattice)
lemma lattice_sparse: "Λ sparse_in UNIV"
using not_islimpt_lattice sparse_in_def by blast
text ‹
Any non-empty set of lattice points has one lattice point that is closer to the origin
than all others.
›
lemma shortest_lattice_vector_exists:
assumes "X ⊆ Λ" "X ≠ {}"
obtains x where "x ∈ X" "⋀y. y ∈ X ⟹ norm x ≤ norm y"
proof -
obtain x0 where x0: "x0 ∈ X"
using assms by auto
have "¬z islimpt X" for z
using not_islimpt_lattice assms(1) islimpt_subset by blast
hence "finite (cball 0 (norm x0) ∩ X)"
by (intro finite_not_islimpt_in_compact) auto
moreover have "x0 ∈ cball 0 (norm x0) ∩ X"
using x0 by auto
ultimately obtain x where x: "is_arg_min norm (λx. x ∈ cball 0 (norm x0) ∩ X) x"
using ex_is_arg_min_if_finite[of "cball 0 (norm x0) ∩ X" norm] by blast
thus ?thesis
by (intro that[of x]) (auto simp: is_arg_min_def)
qed
text ‹
If $x$ is a non-zero lattice point then there exists another lattice point that is
not collinear with $x$, i.e.\ that does not lie on the line through $0$ and $x$.
›
lemma noncollinear_lattice_point_exists:
assumes "x ∈ Λ⇧*"
obtains y where "y ∈ Λ⇧*" "y / x ∉ ℝ"
proof -
from assms obtain m n where x: "x = of_ω12_coords (of_int m, of_int n)" and "x ≠ 0"
by (elim latticeE lattice0E DiffE) auto
define y where "y = of_ω12_coords (of_int (-n), of_int m)"
have "y ∈ Λ"
by (auto simp: y_def)
moreover have "y ≠ 0"
using ‹x ≠ 0› by (auto simp: x y_def of_ω12_coords_eq_0_iff prod_eq_iff)
moreover have "y / x ∉ ℝ"
proof
assume "y / x ∈ ℝ"
then obtain a where "y / x = of_real a"
by (elim Reals_cases)
hence y: "y = a *⇩R x"
using assms ‹x ≠ 0› by (simp add: field_simps scaleR_conv_of_real)
have "of_ω12_coords (-real_of_int n, real_of_int m) =
of_ω12_coords (a * real_of_int m, a * real_of_int n)"
using y by (simp add: x y_def algebra_simps flip: of_ω12_coords.scaleR)
hence eq: "-real_of_int n = a * real_of_int m" "real_of_int m = a * real_of_int n"
unfolding of_ω12_coords_eq_iff prod_eq_iff fst_conv snd_conv by blast+
have "m ≠ 0 ∨ n ≠ 0"
using ‹x ≠ 0› by (auto simp: x)
with eq[symmetric] have nz: "m ≠ 0" "n ≠ 0"
by auto
have "a ^ 2 * real_of_int m = a * (a * real_of_int m)"
by (simp add: power2_eq_square algebra_simps)
also have "… = (-1) * real_of_int m"
by (simp flip: eq)
finally have "a ^ 2 = -1"
using ‹m ≠ 0› by (subst (asm) mult_right_cancel) auto
moreover have "a ^ 2 ≥ 0"
by simp
ultimately show False
by linarith
qed
ultimately show ?thesis
by (intro that) auto
qed
text ‹
We can always easily find a period parallelogram whose border does not touch any given set
of points we want to avoid, as long as that set is sparse.
›
lemma shifted_period_parallelogram_avoid:
assumes "countable avoid"
obtains orig where "path_image (parallelogram_path orig ω1 ω2) ∩ avoid = {}"
proof -
define avoid' where "avoid' = ω12_coords ` avoid"
define avoid1 where "avoid1 = fst ` avoid'"
define avoid2 where "avoid2 = snd ` avoid'"
define avoid''
where "avoid'' = (avoid1 ∪ (λx. x - 1) ` avoid1) × UNIV ∪ UNIV × (avoid2 ∪ (λx. x - 1) ` avoid2)"
obtain orig where orig: "orig ∉ avoid''"
proof -
have *: "avoid1 ∪ (λx. x - 1) ` avoid1 ∈ null_sets lborel"
"avoid2 ∪ (λx. x - 1) ` avoid2 ∈ null_sets lborel"
by (rule null_sets.Un; rule countable_imp_null_set_lborel;
use assms in ‹force simp: avoid1_def avoid2_def avoid'_def›)+
have "avoid'' ∈ null_sets lborel"
unfolding lborel_prod[symmetric] avoid''_def using * by (intro null_sets.Un) auto
hence "AE z in lborel. z ∉ avoid''"
using AE_not_in by blast
from eventually_happens[OF this] show ?thesis using that
by (auto simp: ae_filter_eq_bot_iff)
qed
have *: "(λx. x - 1) ` X = ((+) 1) -` X" for X :: "real set"
by force
have fst_orig: "fst z ∉ {fst orig, fst orig + 1}" if "z ∈ avoid'" for z
proof
assume "fst z ∈ {fst orig, fst orig + 1}"
hence "orig ∈ (avoid1 ∪ (λx. x - 1) ` avoid1) × UNIV"
using that unfolding avoid1_def * by (cases orig; cases z) force
thus False using orig
by (auto simp: avoid''_def)
qed
have snd_orig: "snd z ∉ {snd orig, snd orig + 1}" if "z ∈ avoid'" for z
proof
assume "snd z ∈ {snd orig, snd orig + 1}"
hence "orig ∈ UNIV × (avoid2 ∪ (λx. x - 1) ` avoid2)"
using that unfolding avoid2_def * by (cases orig; cases z) force
thus False using orig
by (auto simp: avoid''_def)
qed
show ?thesis
proof (rule that[of "of_ω12_coords orig"], safe)
fix z assume z: "z ∈ path_image (parallelogram_path (of_ω12_coords orig) ω1 ω2)" "z ∈ avoid"
have "ω12_coords z ∈ ω12_coords `path_image (parallelogram_path (of_ω12_coords orig) ω1 ω2)"
using z(1) by blast
thus "z ∈ {}" using z(2) fst_orig[of "ω12_coords z"] snd_orig[of "ω12_coords z"]
unfolding path_image_parallelogram_path'
by (auto simp: avoid'_def ω12_coords.add box_prod)
qed
qed
text ‹
We can also prove a rule that allows us to prove a property about period parallelograms while
assuming w.l.o.g.\ that the border of the parallelogram does not touch an arbitrary sparse
set of points we want to avoid and the property we want to prove is invariant under shifting
the parallelogram by an arbitrary amount.
This will be useful later for the use case of showing that any period parallelograms contain
the same number of zeros as poles, which is proven by integrating along the border of a period
parallelogram that is assume w.l.o.g.\ not to have any zeros or poles on its border.
›
lemma shifted_period_parallelogram_avoid_wlog [consumes 1, case_names shift avoid]:
assumes "⋀z. ¬z islimpt avoid"
assumes "⋀orig d. finite (closure (period_parallelogram orig) ∩ avoid) ⟹
finite (closure (period_parallelogram (orig + d)) ∩ avoid) ⟹
P orig ⟹ P (orig + d)"
assumes "⋀orig. finite (closure (period_parallelogram orig) ∩ avoid) ⟹
path_image (parallelogram_path orig ω1 ω2) ∩ avoid = {} ⟹
P orig"
shows "P orig"
proof -
from assms have countable: "countable avoid"
using no_limpt_imp_countable by blast
from shifted_period_parallelogram_avoid[OF countable]
obtain orig' where orig': "path_image (parallelogram_path orig' ω1 ω2) ∩ avoid = {}"
by blast
define d where "d = ω12_coords (orig - orig')"
have "compact (closure (period_parallelogram orig))" for orig
by (rule compact_closure_period_parallelogram)
hence fin: "finite (closure (period_parallelogram orig) ∩ avoid)" for orig
using assms by (intro finite_not_islimpt_in_compact) auto
from orig' have "P orig'"
by (intro assms fin)
have "P (orig' + (orig - orig'))"
by (rule assms(2)) fact+
thus ?thesis
by (simp add: algebra_simps)
qed
end
text ‹
The standard lattice is one that has been rotated and scaled such that the first generator
is 1 and the second generator ‹τ› lies in the upper half plane.
›
locale std_complex_lattice =
fixes τ :: complex (structure)
assumes Im_τ_pos: "Im τ > 0"
begin
sublocale complex_lattice 1 τ
by standard (use Im_τ_pos in ‹auto elim!: Reals_cases simp: fundpair_def›)
lemma winding_number_parallelogram_inside':
assumes "w ∈ interior (period_parallelogram z)"
shows "winding_number (parallelogram_path z 1 τ) w = 1"
using winding_number_parallelogram_inside[OF assms] Im_τ_pos by simp
end
subsection ‹Doubly-periodic functions›
text ‹
The following locale can be useful to prove that certain things respect the equivalence
relation defined by the lattice: it shows that a doubly periodic function gives the same
value for all equivalent points. Note that this is useful even for functions ‹f› that are only
doubly quasi-periodic, since one might then still be able to prove that the function
\<^term>‹λz. f z = 0› or \<^term>‹zorder f› or \<^term>‹is_pole f› are doubly periodic, so the zeros
and poles of ‹f› are distributed according to the lattice symmetry.
›
locale pre_complex_lattice_periodic = pre_complex_lattice +
fixes f :: "complex ⇒ 'a"
assumes f_periodic: "f (z + ω1) = f z" "f (z + ω2) = f z"
begin
lemma lattice_cong:
assumes "rel x y"
shows "f x = f y"
proof -
define z where "z = y - x"
from assms have z: "z ∈ Λ"
using pre_complex_lattice.rel_def pre_complex_lattice.rel_sym z_def by blast
have "f (x + z) = f x"
using z
proof (induction arbitrary: x rule: lattice_induct)
case (uminus w x)
show ?case
using uminus[of "x - w"] by simp
qed (auto simp: f_periodic simp flip: add.assoc)
thus ?thesis
by (simp add: z_def)
qed
end
locale complex_lattice_periodic =
complex_lattice ω1 ω2 + pre_complex_lattice_periodic ω1 ω2 f
for ω1 ω2 :: complex and f :: "complex ⇒ 'a"
begin
lemma eval_to_fund_parallelogram: "f (to_fund_parallelogram z) = f z"
by (rule lattice_cong) auto
end
locale complex_lattice_periodic_compose =
complex_lattice_periodic ω1 ω2 f for ω1 ω2 :: complex and f :: "complex ⇒ 'a" +
fixes h :: "'a ⇒ 'b"
begin
sublocale compose: complex_lattice_periodic ω1 ω2 "λz. h (f z)"
by standard (auto intro!: arg_cong[of _ _ h] lattice_cong simp: rel_def)
end
end