English
A power-series-convolution type result: the support of the coefficient of (a*b) is contained in the image of sums of supports of a and b.
Русский
Результат свертки коэффициентов (a*b) имеет опору внутри образа сумм опор a и b.
LaTeX
$$((powerSeriesFamily x (a * b)).coeff g).support ⊆ (((powerSeriesFamily x a).mul (powerSeriesFamily x b)).coeff g).support.image (⋯ + ⋯)$$
Lean4
theorem support_powerSeriesFamily_subset {x : HahnSeries Γ V} (a b : PowerSeries R) (g : Γ) :
((powerSeriesFamily x (a * b)).coeff g).support ⊆
(((powerSeriesFamily x a).mul (powerSeriesFamily x b)).coeff g).support.image fun i => i.1 + i.2 :=
by
by_cases h : 0 < x.orderTop
· simp only [coeff_support, Set.Finite.toFinset_subset, support_subset_iff]
intro n hn
have he :
∃ c ∈ antidiagonal n, (PowerSeries.coeff c.1) a • (PowerSeries.coeff c.2) b • ((powers x) n).coeff g ≠ 0 :=
by
refine exists_ne_zero_of_sum_ne_zero ?_
simpa [PowerSeries.coeff_mul, sum_smul, mul_smul, h] using hn
simp only [powers_of_orderTop_pos h, mem_antidiagonal] at he
obtain ⟨c, hcn, hc⟩ := he
simp only [coe_image, Set.Finite.coe_toFinset, Set.mem_image]
use c
simp only [mul_toFun, smulFamily_toFun, Function.mem_support, hcn, and_true]
rw [powers_of_orderTop_pos h c.1, powers_of_orderTop_pos h c.2, Algebra.smul_mul_assoc, Algebra.mul_smul_comm, ←
pow_add, hcn]
simp [hc]
· simp only [coeff_support, Set.Finite.toFinset_subset, support_subset_iff]
intro n hn
by_cases hz : n = 0
· have : g = 0 ∧ (a.constantCoeff * b.constantCoeff) • (1 : V) ≠ 0 := by simpa [hz, h] using hn
simp only [coe_image, Set.mem_image]
use (0, 0)
simp [this.2, this.1, h, hz, smul_smul, mul_comm]
· simp [h, hz] at hn
