def cauchyProductCoeff (c d : ℕ → ℝ) (n : ℕ) : ℝ

The Cauchy-product coefficient sequence attached to c, d : ℕ → ℝ.

Equations

• cauchyProductCoeff c d n = ∑ m ∈ Finset.range (n + 1), c m * d (n - m)

theorem helperForTheorem_4_4_1_absSummable_seriesTerm_at_point {a r x : ℝ} (c : ℕ → ℝ) (hc : ∀ y ∈ Set.Ioo (a - r) (a + r), Summable fun (n : ℕ) => c n * (y - a) ^ n) (hx : x ∈ Set.Ioo (a - r) (a + r)) : Summable fun (n : ℕ) => |c n * (x - a) ^ n|

Helper for Theorem 4.4.1: at any point of (a-r, a+r), the corresponding power-series terms are absolutely summable.

theorem helperForTheorem_4_4_1_cauchyInnerSum_rewrite (c d : ℕ → ℝ) (t : ℝ) (n : ℕ) : ∑ k ∈ Finset.range (n + 1), c k * t ^ k * (d (n - k) * t ^ (n - k)) = cauchyProductCoeff c d n * t ^ n

Helper for Theorem 4.4.1: rewrite the inner Cauchy-product finite sum into cauchyProductCoeff c d n * t^n.

theorem helperForTheorem_4_4_1_pointwise_product_eq_tsum {a r x : ℝ} (hr : 0 < r) (f g : ↑(Set.Ioo (a - r) (a + r)) → ℝ) (c d : ℕ → ℝ) (hf_series : ∀ (y : ℝ) (hy : y ∈ Set.Ioo (a - r) (a + r)), (Summable fun (n : ℕ) => c n * (y - a) ^ n) ∧ f ⟨y, hy⟩ = ∑' (n : ℕ), c n * (y - a) ^ n) (hg_series : ∀ (y : ℝ) (hy : y ∈ Set.Ioo (a - r) (a + r)), (Summable fun (n : ℕ) => d n * (y - a) ^ n) ∧ g ⟨y, hy⟩ = ∑' (n : ℕ), d n * (y - a) ^ n) (hx : x ∈ Set.Ioo (a - r) (a + r)) : f ⟨x, hx⟩ * g ⟨x, hx⟩ = ∑' (n : ℕ), cauchyProductCoeff c d n * (x - a) ^ n

Helper for Theorem 4.4.1: at each point in (a-r,a+r), the pointwise product equals the Cauchy-product power-series sum.

theorem realAnalyticOnInterval_mul_eq_cauchyProduct {a r : ℝ} (hr : 0 < r) (f g : ↑(Set.Ioo (a - r) (a + r)) → ℝ) (hf_analytic : IsRealAnalyticOn (Set.Ioo (a - r) (a + r)) f) (hg_analytic : IsRealAnalyticOn (Set.Ioo (a - r) (a + r)) g) (c d : ℕ → ℝ) (hf_series : ∀ (x : ℝ) (hx : x ∈ Set.Ioo (a - r) (a + r)), (Summable fun (n : ℕ) => c n * (x - a) ^ n) ∧ f ⟨x, hx⟩ = ∑' (n : ℕ), c n * (x - a) ^ n) (hg_series : ∀ (x : ℝ) (hx : x ∈ Set.Ioo (a - r) (a + r)), (Summable fun (n : ℕ) => d n * (x - a) ^ n) ∧ g ⟨x, hx⟩ = ∑' (n : ℕ), d n * (x - a) ^ n) : (IsRealAnalyticOn (Set.Ioo (a - r) (a + r)) fun (x : ↑(Set.Ioo (a - r) (a + r))) => f x * g x) ∧ ∀ (x : ℝ) (hx : x ∈ Set.Ioo (a - r) (a + r)), f ⟨x, hx⟩ * g ⟨x, hx⟩ = ∑' (n : ℕ), cauchyProductCoeff c d n * (x - a) ^ n

Theorem 4.4.1: if f, g : (a-r, a+r) → ℝ are analytic and have power-series expansions around a with coefficients c_n and d_n on (a-r, a+r), then fg is analytic on (a-r, a+r), and for every x in that interval, f(x)g(x) = ∑' n, e_n (x-a)^n where e_n = ∑_{m=0}^n c_m d_{n-m}.