English
No-wrap Freiman isomorphism: under no wrap-around, the first k elements of Fin(n+1) are m-Freiman isomorphic to the first k elements of ℕ, provided hm ≠ 0 and hkmn ≤ n.
Русский
Без обхода границ: первые k элементов Fin(n+1) изоморфны по Фриману m первым k элементам ℕ при условии hm ≠ 0 и m*k ≤ n.
LaTeX
$$$\\text{isAddFreimanIso}_Iic(m,(k:Fin(n+1)),k) val$$$
Lean4
/-- **No wrap-around principle**.
The first `k + 1` elements of `Fin (n + 1)` are `m`-Freiman isomorphic to the first `k + 1` elements
of `ℕ` assuming there is no wrap-around. -/
theorem isAddFreimanIso_Iic (hm : m ≠ 0) (hkmn : m * k ≤ n) : IsAddFreimanIso m (Iic (k : Fin (n + 1))) (Iic k) val
where
bijOn.left := by simp [MapsTo, Fin.le_iff_val_le_val, Nat.mod_eq_of_lt, aux hm hkmn]
bijOn.right.left := val_injective.injOn
bijOn.right.right x
(hx : x ≤ _) := ⟨x, by simpa [le_iff_val_le_val, -val_fin_le, Nat.mod_eq_of_lt, aux hm hkmn, hx.trans_lt]⟩
map_sum_eq_map_sum s t hsA htA hs
ht := by
have (u : Multiset (Fin (n + 1))) : Nat.castRingHom _ (u.map val).sum = u.sum := by simp
rw [← this, ← this]
have {u : Multiset (Fin (n + 1))} (huk : ∀ x ∈ u, x ≤ k) (hu : card u = m) : (u.map val).sum < (n + 1) :=
Nat.lt_succ_iff.2 <|
hkmn.trans' <| by
rw [← hu, ← card_map]
refine sum_le_card_nsmul (u.map val) k ?_
simpa [le_iff_val_le_val, -val_fin_le, Nat.mod_eq_of_lt, aux hm hkmn] using huk
exact ⟨congr_arg _, CharP.natCast_injOn_Iio _ (n + 1) (this hsA hs) (this htA ht)⟩
