hsum_powerSeriesFamily_mul — Mathlib

English

The sum over the powers of a Hahn series distributes over the product of power-series-sums: the hsum of powerSeries x (a*b) equals the hsum of the product of the sums of a and b.

Русский

Сумма по степенным рядам распадается на произведение сумм по степенным рядами: hsum (powerSeriesFamily x (a*b)) = hsum((powerSeriesFamily x a).mul (powerSeriesFamily x b)).

LaTeX

$$ (HahnSeries.SummableFamily.powerSeriesFamily x (a * b)).hsum = ((HahnSeries.SummableFamily.powerSeriesFamily x a).mul (HahnSeries.SummableFamily.powerSeriesFamily x b)).hsum$$

Lean4

theorem hsum_powerSeriesFamily_mul {x : HahnSeries Γ V} (a b : PowerSeries R) :
    (powerSeriesFamily x (a * b)).hsum = ((powerSeriesFamily x a).mul (powerSeriesFamily x b)).hsum :=
  by
  by_cases h : 0 < x.orderTop;
  · ext g
    simp only [coeff_hsum_eq_sum, smulFamily_toFun, h, powers_of_orderTop_pos, HahnSeries.coeff_smul, mul_toFun,
      Algebra.mul_smul_comm, Algebra.smul_mul_assoc]
    rw [sum_subset (support_powerSeriesFamily_subset a b g)
        (fun i hi his ↦ by simpa [h, PowerSeries.coeff_mul, sum_smul] using his)]
    simp only [coeff_support, mul_toFun, smulFamily_toFun, Algebra.mul_smul_comm, Algebra.smul_mul_assoc,
      HahnSeries.coeff_smul, PowerSeries.coeff_mul, sum_smul]
    rw [sum_sigma']
    refine
      (Finset.sum_of_injOn (fun x => ⟨x.1 + x.2, x⟩) (fun _ _ _ _ => by simp) ?_ ?_
          (fun _ _ => by simp [smul_smul, mul_comm, pow_add])).symm
    · intro ij hij
      simp only [coe_sigma, coe_image, Set.mem_sigma_iff, Set.mem_image, Prod.exists, mem_coe, mem_antidiagonal,
        and_true]
      use ij.1, ij.2
      simp_all
    · intro i hi his
      have hisc :
        ∀ j k : ℕ,
          ⟨j + k, (j, k)⟩ = i → (PowerSeries.coeff k) b • (PowerSeries.coeff j a • (x ^ j * x ^ k).coeff g) = 0 :=
        by
        intro m n
        contrapose!
        simp only [powers_of_orderTop_pos h, Set.Finite.coe_toFinset, Set.mem_image, Function.mem_support, ne_eq,
          Prod.exists, not_exists, not_and] at his
        exact his m n
      simp only [mem_sigma, mem_antidiagonal] at hi
      rw [mul_comm ((PowerSeries.coeff i.snd.1) a), ← hi.2, mul_smul, pow_add]
      exact hisc i.snd.1 i.snd.2 <| Sigma.eq hi.2 (by simp)
  · simp only [h, not_false_eq_true, powerSeriesFamily_of_not_orderTop_pos, powerSeriesFamily_hsum_zero, map_mul,
      hsum_mul]
    rw [smul_mul_smul_comm, mul_one]

Похожие утверждения