English
For a function f: ι → ℤ with finite support in b.support and whose weighted roots sum lies in the root set, the sum cannot be zero; in particular, 0 < f or f < 0.
Русский
Для функции f: ι → ℤ с конечной поддержкой в b.support и суммой f(j)•P.root(j) лежащей в корне-диапазоне, сумма не равна нулю; верно 0 < f или f < 0.
LaTeX
$$$0 < f \quad \text{или} \quad f < 0$$$
Lean4
theorem pos_or_neg_of_sum_smul_root_mem (f : ι → ℤ) (hf : ∑ j ∈ b.support, f j • P.root j ∈ range P.root)
(hf₀ : f.support ⊆ b.support) : 0 < f ∨ f < 0 :=
by
suffices
∀ (f : ι → ℤ) (hf : ∑ j ∈ b.support, f j • P.root j ∈ AddSubmonoid.closure (P.root '' b.support))
(hf₀ : f.support ⊆ b.support) (hf' : f ≠ 0), 0 < f
by
obtain ⟨k, hk⟩ := hf
have hf' : f ≠ 0 := by rintro rfl; exact P.ne_zero k <| by simp [hk]
rcases b.root_mem_or_neg_mem k with hk' | hk' <;> rw [hk] at hk'
· left; exact this f hk' hf₀ hf'
· right; simpa using this (-f) (by convert hk'; simp) (by simpa only [support_neg]) (by simpa)
intro f hf hf₀ hf'
let f' : b.support → ℤ := fun i ↦ f i
replace hf : ∑ j, f' j • P.root j ∈ AddSubmonoid.closure (P.root '' b.support) :=
by
suffices ∑ j, f' j • P.root j = ∑ j ∈ b.support, f j • P.root j by rwa [this]
rw [← b.support.sum_finset_coe]; rfl
rw [← span_nat_eq_addSubmonoidClosure, mem_toAddSubmonoid, Fintype.mem_span_image_iff_exists_fun] at hf
obtain ⟨c, hc⟩ := hf
replace hc (i : b.support) : c i = f' i :=
Fintype.linearIndependent_iffₛ.mp (b.linearIndepOn_root.restrict_scalars' ℤ) (Int.ofNat ∘ c) f' (by simpa) i
have aux : 0 ≤ f := by
intro i
by_cases hi : i ∈ b.support
· change 0 ≤ f' ⟨i, hi⟩
simp [← hc]
· replace hi : i ∉ f.support := by contrapose! hi; exact hf₀ hi
simp_all
refine Pi.lt_def.mpr ⟨aux, ?_⟩
by_contra! contra
replace contra : f = 0 := le_antisymm contra aux
contradiction
