English
When transferring to power-series, under appropriate conditions, gaussNorm commutes with the coefficient-map: gaussNorm_coe_powerSeries equates these two ways of computing the norm.
Русский
При переводе в степенной ряд, при надлежащих условиях, gaussNorm и отображение коэффициентов согласованы.
LaTeX
$$gaussNorm_coe_powerSeries v c p = gaussNorm v c p$$
Lean4
@[simp]
theorem gaussNorm_coe_powerSeries [ZeroHomClass F R ℝ] [NonnegHomClass F R ℝ] (hc : 0 ≤ c) :
(p.toPowerSeries).gaussNorm v c = p.gaussNorm v c :=
by
by_cases hp : p = 0
· simp [hp]
· simp only [PowerSeries.gaussNorm, coeff_coe, gaussNorm, support_nonempty, ne_eq, hp, not_false_eq_true, ↓reduceDIte]
apply le_antisymm
· apply ciSup_le
intro n
by_cases h : n ∈ p.support
· exact Finset.le_sup' (fun j ↦ v (p.coeff j) * c ^ j) h
· simp_all [sup'_nonneg_of_ne_zero v (support_nonempty.mpr hp) hc]
· obtain ⟨i, hi⟩ := exists_eq_gaussNorm v c p
simp only [gaussNorm, support_nonempty.mpr hp, ↓reduceDIte] at hi
rw [hi]
exact le_ciSup (aux_bdd v p) i
