English
Under assumptions (injectivity-like condition on v and growth with c>0 and boundedness), gaussNorm(v,c,f) = 0 if and only if f = 0.
Русский
При предположениях (инъективность по v и положительная степень c>0 и ограниченность роста), gaussNorm(v,c,f) = 0 тогда и только тогда f = 0.
LaTeX
$$$ f.gaussNorm v c = 0 \iff f = 0, \quad \text{under appropriate hypotheses (injectivity of } v, c>0,\text{ boundedness)} $$$
Lean4
@[simp]
theorem gaussNorm_eq_zero_iff [ZeroHomClass F R ℝ] [NonnegHomClass F R ℝ] {v : F} (h_eq_zero : ∀ x : R, v x = 0 → x = 0)
{f : R⟦X⟧} {c : ℝ} (hc : 0 < c) (hbd : BddAbove (Set.range fun i ↦ v (f.coeff i) * c ^ i)) :
f.gaussNorm v c = 0 ↔ f = 0 := by
refine ⟨?_, fun hf ↦ by simp [hf]⟩
contrapose!
intro hf
apply ne_of_gt
obtain ⟨n, hn⟩ := exists_coeff_ne_zero_iff_ne_zero.mpr hf
calc
0 < v (f.coeff n) * c ^ n := by
have := fun h ↦ hn (h_eq_zero (coeff n f) h)
positivity
_ ≤ gaussNorm v c f := le_ciSup hbd n
