FenchelNielsenZomorrodian/Discrete/Arithmetic/FinsetLcm.lean
1import FenchelNielsenZomorrodian.Discrete.Arithmetic.FamilyLcm
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FenchelNielsenZomorrodian/Discrete/Arithmetic/FinsetLcm.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Arithmetic of period families
14GCD, LCM, prime-divisor, replicated-family, and abelian-period numerical lemmas used in compact zero-genus reductions.
15-/
17open scoped BigOperators
19namespace Finset
22 {ι : Type*} {periods : ι → ℕ} {s : Finset ι}
23 (hge : ∀ i ∈ s, 2 ≤ periods i)
24 {i j : ι} (hi : i ∈ s) (hj : j ∈ s)
25 (hji : j ≠ i) (hjEq : periods j = periods i) :
26 2 * s.lcm periods ≤ s.prod periods := by
27 classical
28 have hjmem : j ∈ s.erase i := by
29 exact Finset.mem_erase.mpr ⟨hji, hj⟩
30 have hlcmDivProdErase :
31 s.lcm periods ∣ (s.erase i).prod periods := by
32 apply Finset.lcm_dvd
33 intro k hk
34 by_cases hki : k = i
35 · subst hki
36 rw [← hjEq]
37 exact Finset.dvd_prod_of_mem periods hjmem
38 · have hkmem : k ∈ s.erase i := by
39 exact Finset.mem_erase.mpr ⟨hki, hk⟩
40 exact Finset.dvd_prod_of_mem periods hkmem
41 have hProdErasePos : 0 < (s.erase i).prod periods := by
42 exact Finset.prod_pos
43 (fun k hk => lt_of_lt_of_le (by decide : 0 < 2)
44 (hge k (Finset.mem_of_mem_erase hk)))
45 have hlcmLeProdErase : s.lcm periods ≤ (s.erase i).prod periods :=
46 Nat.le_of_dvd hProdErasePos hlcmDivProdErase
47 calc
48 2 * s.lcm periods
49 ≤ periods i * (s.erase i).prod periods :=
50 Nat.mul_le_mul (hge i hi) hlcmLeProdErase
51 _ = s.prod periods := by
52 rw [mul_comm]
53 exact Finset.prod_erase_mul (s := s) (f := periods) (a := i) hi
55end Finset