English
Two sums count lattice points in two triangles formed by the diagonal of a rectangle; their sum counts all lattice points in the rectangle, giving p/2 · q/2 on the right-hand side.
Русский
Две суммы считают число точек с целочисленными координатами в двух треугольниках, образованных диагональю прямоугольника; сумма даёт число точек в самом прямоугольнике, равное (p/2)·(q/2).
LaTeX
$$$\sum_{a ∈ Ico 1 (p / 2).succ} a \; q / p + \sum_{a ∈ Ico 1 (q / 2).succ} a \; p / q = p / 2 \cdot (q / 2)$$$
Lean4
/-- Each of the sums in this lemma is the cardinality of the set of integer points in each of the
two triangles formed by the diagonal of the rectangle `(0, p/2) × (0, q/2)`. Adding them
gives the number of points in the rectangle. -/
theorem sum_mul_div_add_sum_mul_div_eq_mul (p q : ℕ) [hp : Fact p.Prime] (hq0 : (q : ZMod p) ≠ 0) :
∑ a ∈ Ico 1 (p / 2).succ, a * q / p + ∑ a ∈ Ico 1 (q / 2).succ, a * p / q = p / 2 * (q / 2) :=
by
have hswap :
#({x ∈ Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ | x.2 * q ≤ x.1 * p}) =
#({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p}) :=
card_equiv (Equiv.prodComm _ _)
(fun ⟨_, _⟩ => by
simp +contextual only [mem_filter, Prod.swap_prod_mk, mem_product, Equiv.prodComm_apply, and_assoc,
and_left_comm])
have hdisj :
Disjoint ({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.2 * p ≤ x.1 * q})
({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p}) :=
by
apply disjoint_filter.2 fun x hx hpq hqp => ?_
have hxp : x.1 < p :=
lt_of_le_of_lt (show x.1 ≤ p / 2 by simp_all only [Nat.lt_succ_iff, mem_Ico, mem_product])
(Nat.div_lt_self hp.1.pos (by decide))
have : (x.1 : ZMod p) = 0 := by simpa [hq0] using congr_arg ((↑) : ℕ → ZMod p) (le_antisymm hpq hqp)
apply_fun ZMod.val at this
rw [val_cast_of_lt hxp, val_zero] at this
simp only [this, nonpos_iff_eq_zero, mem_Ico, one_ne_zero, false_and, mem_product] at hx
have hunion :
{x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.2 * p ≤ x.1 * q} ∪
{x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p} =
Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ :=
Finset.ext fun x => by
have := le_total (x.2 * p) (x.1 * q)
simp only [mem_union, mem_filter, mem_Ico, mem_product]
tauto
rw [sum_Ico_eq_card_lt, sum_Ico_eq_card_lt, hswap, ← card_union_of_disjoint hdisj, hunion, card_product]
simp only [card_Ico, tsub_zero, succ_sub_succ_eq_sub]
