2.2 Chebyshev series: coefficients and completeness
Orthogonality gives coefficients by integration. Finite expansions are recovered exactly; completeness explains what happens for infinite expansions.
2.2.1 Coefficients and finite expansions
The coefficient at index \(n\) requires integrability of \(fT_n\). We keep the full constant term: \(f=a_0+\sum _{n\ge 1}a_nT_n\).
For \(n\in \mathbb {N}\), define
Functions in this domain retain their pointwise values. Addition and real scalar multiplication are pointwise. The defining condition concerns \(fT_n\), not \(f\) alone. Reference: [ATAP, Chapter 3].
Lean Formalisation
def Polynomial.Chebyshev.CoefficientInput (n : ℕ) : TypeLean definition
/-- Pointwise inputs with an integrable nth coefficient integrand (ATAP Ch. 3). -/
abbrev CoefficientInput (n : ℕ) :=
{f : ℝ → ℝ // Integrable (fun x ↦ f x * (T ℝ n).eval x) classicalMeasureT}For \(f\in \mathcal I_n\), the product \(fT_n\) is \(\mu _T\)-integrable. Every \(\mu _T\)-integrable real function, and every \(f:\mathbb {R}\to \mathbb {R}\) continuous on \([-1,1]\), belongs to \(\mathcal I_n\) for every \(n\), with unchanged pointwise values. The domain \(\mathcal I_0\) consists exactly of the \(\mu _T\)-integrable real functions. Membership of \(\mathcal I_n\) is unchanged by \(\mu _T\)-almost-everywhere equality.
Lean Formalisation
theorem Polynomial.Chebyshev.CoefficientInput.integrable {n : ℕ} (f : Polynomial.Chebyshev.CoefficientInput n) :
MeasureTheory.Integrable (fun x => ↑f x * Polynomial.eval x (Polynomial.Chebyshev.T ℝ ↑n))
Polynomial.Chebyshev.classicalMeasureTLean proof
/-- The defining coefficient integrand is integrable. -/
theorem CoefficientInput.integrable {n : ℕ} (f : CoefficientInput n) :
Integrable (fun x ↦ f.val x * (T ℝ n).eval x) classicalMeasureT := f.propertyAt each index \(n\), for \(f\in \mathcal I_n\), set
The expansion convention is \(a_0+\sum _{n\geq 1}a_nT_n\).
Reference: [ATAP, Chapters 3 and 8], with the constant-term convention made explicit here.
Lean Formalisation
def Polynomial.Chebyshev.coefficient {n : ℕ} (f : Polynomial.Chebyshev.CoefficientInput n) : ℝLean definition
/-- Chebyshev coefficient in the full constant term convention (ATAP, Chapters 3 and 8).
The input carries integrability at the selected index. -/
@[expose] noncomputable def coefficient {n : ℕ} (f : CoefficientInput n) : ℝ :=
(if n = 0 then 1 else 2) / π * ∫ x, f.val x * (T ℝ n).eval x ∂classicalMeasureTFor \(n\in \mathbb {N}\) and \(f\in \mathcal I_n\), the cosine integrand is integrable and
Reference: [ATAP, Chapters 3 and 8].
Lean Formalisation
theorem Polynomial.Chebyshev.coefficient_eq_integral_cos {n : ℕ} (f : Polynomial.Chebyshev.CoefficientInput n) :
Polynomial.Chebyshev.coefficient f =
(if n = 0 then 1 else 2) / Real.pi * ∫ (θ : ℝ) in 0..Real.pi, ↑f (Real.cos θ) * Real.cos (↑n * θ)Lean proof
/-- Cosine representation for an integrable coefficient integrand (ATAP Ch. 3). -/
theorem coefficient_eq_integral_cos {n : ℕ} (f : CoefficientInput n) :
coefficient f = (if n = 0 then 1 else 2) / π *
∫ θ in 0..π, f.val (cos θ) * cos (n * θ) := by
simp only [coefficient_eq_integral, integral_measureT_eq_integral_cos,
T_real_cos, Int.cast_natCast]For a finite set \(S\subset \mathbb {N}\) and real coefficients \(b_k\), let \(p(x)=\sum _{k\in S}b_kT_k(x)\). Then \(a_n(p)=b_n\) if \(n\in S\), and \(a_n(p)=0\) otherwise.
Reference: [ATAP, Chapter 3].
Lean Formalisation
theorem Polynomial.Chebyshev.coefficient_sum_eval_T (s : Finset ℕ) (c : ℕ → ℝ) (n : ℕ) :
Polynomial.Chebyshev.coefficient
(Polynomial.Chebyshev.CoefficientInput.ofContinuousOn
(fun x => ∑ k ∈ s, c k * Polynomial.eval x (Polynomial.Chebyshev.T ℝ ↑k)) ⋯ n) =
if n ∈ s then c n else 0Lean proof
/-- Coefficients recover finite Chebyshev expansions (ATAP Ch. 3). -/
theorem coefficient_sum_eval_T (s : Finset ℕ) (c : ℕ → ℝ) (n : ℕ) :
coefficient (CoefficientInput.ofContinuousOn
(fun x ↦ ∑ k ∈ s, c k * (T ℝ k).eval x) (by fun_prop) n) =
if n ∈ s then c n else 0 := by
simp only [coefficient, CoefficientInput.ofContinuousOn_val, Finset.sum_mul]
rw [integral_finsetSum s (fun k hk ↦ integrable_classicalMeasureT (by fun_prop)),
Finset.mul_sum]
simp only [mul_assoc, integral_const_mul]
have hc (k : ℕ) : (if n = 0 then 1 else 2) / π *
(c k * ∫ x, (T ℝ k).eval x * (T ℝ n).eval x ∂classicalMeasureT) =
c k * (if k = n then 1 else 0) := by
rw [← coefficient_eval_T k n]
simp only [coefficient, CoefficientInput.ofContinuousOn, CoefficientInput.ofL1]
ring
simp_rw [hc]
simpFor \(f\in \mathcal I_n\), if \(M\ge 0\) and \(|f(x)|\le M\) on \([-1,1]\), then \(|a_n(f)|\le M\) at \(n=0\) and \(|a_n(f)|\le 2M\) at \(n{\gt}0\).
Reference: the coefficient formula in [ATAP, Chapters 3 and 8].
Lean Formalisation
theorem Polynomial.Chebyshev.abs_coefficient_le {n : ℕ} (f : Polynomial.Chebyshev.CoefficientInput n) {M : ℝ} (hM : 0 ≤ M)
(hf : ∀ x ∈ Set.Icc (-1) 1, |↑f x| ≤ M) : |Polynomial.Chebyshev.coefficient f| ≤ (if n = 0 then 1 else 2) * MLean proof
/-- The sharp uniform bound, on the classical fixed-index domain (ATAP Ch. 3). -/
theorem abs_coefficient_le {n : ℕ} (f : CoefficientInput n) {M : ℝ} (hM : 0 ≤ M)
(hf : ∀ x ∈ Set.Icc (-1) 1, |f.val x| ≤ M) :
|coefficient f| ≤ (if n = 0 then 1 else 2) * M := by
have hi : |∫ θ in 0..π, f.val (cos θ) * cos (n * θ)| ≤ M * π := by
have h := intervalIntegral.norm_integral_le_of_norm_le_const
(a := 0) (b := π) (C := M) (f := fun θ ↦ f.val (cos θ) * cos (n * θ)) (by
intro θ hθ
rw [Real.norm_eq_abs, abs_mul]
calc
_ ≤ M * 1 := mul_le_mul (hf _ ⟨neg_one_le_cos θ, cos_le_one θ⟩)
(abs_cos_le_one _) (abs_nonneg _) hM
_ = M := mul_one _)
simpa only [Real.norm_eq_abs, sub_zero, abs_of_pos pi_pos] using h
have hn : 0 ≤ (if n = 0 then 1 else 2 : ℝ) / π := by positivity
rw [coefficient_eq_integral_cos, abs_mul, abs_of_nonneg hn]
calc
_ ≤ ((if n = 0 then 1 else 2) / π) * (M * π) := mul_le_mul_of_nonneg_left hi hn
_ = _ := by field_simpCoefficient identities and interval dependence
For \(f\in \mathcal I_n\),
The product \(fT_n\) is integrable, so this integral is finite.
Lean Formalisation
theorem Polynomial.Chebyshev.coefficient_apply {n : ℕ} (f : Polynomial.Chebyshev.CoefficientInput n) :
Polynomial.Chebyshev.coefficient f =
(if n = 0 then 1 else 2) / Real.pi *
∫ (x : ℝ), ↑f x * Polynomial.eval x (Polynomial.Chebyshev.T ℝ ↑n) ∂Polynomial.Chebyshev.classicalMeasureTLean proof
/-- The classical coefficient formula on its exact fixed-index domain (ATAP Ch. 3). -/
theorem coefficient_apply {n : ℕ} (f : CoefficientInput n) :
coefficient f = (if n = 0 then 1 else 2) / π *
∫ x, f.val x * (T ℝ n).eval x ∂classicalMeasureT := rflFor \(m,n\in \mathbb {N}\), \(a_n(T_m)\) is \(1\) when \(m=n\) and \(0\) otherwise.
Lean Formalisation
theorem Polynomial.Chebyshev.coefficient_eval_T (m n : ℕ) :
Polynomial.Chebyshev.coefficient
(Polynomial.Chebyshev.CoefficientInput.ofContinuousOn (fun x => Polynomial.eval x (Polynomial.Chebyshev.T ℝ ↑m)) ⋯
n) =
if m = n then 1 else 0Lean proof
/-- A basis polynomial's coefficients form the Kronecker delta (DLMF 18.3). -/
@[simp] theorem coefficient_eval_T (m n : ℕ) :
coefficient (CoefficientInput.ofContinuousOn (fun x ↦ (T ℝ m).eval x)
(by fun_prop) n) = if m = n then 1 else 0 := by
rw [coefficient]
change (if n = 0 then 1 else 2) / π *
(∫ x, (T ℝ m).eval x * (T ℝ n).eval x ∂classicalMeasureT) = _
rw [(classicalMeasureT_orthogonality m n).2]
by_cases h : m = n
· subst m; simp only [ite_true]; split_ifs <;> field_simp
· simp [h]For \(f,g\in \mathcal I_n\) agreeing on \([-1,1]\), or agreeing \(\mu _T\)-almost everywhere, \(a_n(f)=a_n(g)\).
Reference: [ATAP, Chapter 3].
Lean Formalisation
theorem Polynomial.Chebyshev.coefficient_congr {n : ℕ} {f g : Polynomial.Chebyshev.CoefficientInput n}
(h : Set.EqOn (↑f) (↑g) (Set.Icc (-1) 1)) : Polynomial.Chebyshev.coefficient f = Polynomial.Chebyshev.coefficient gLean proof
/-- Only values on the approximation interval affect coefficients (ATAP Ch. 3). -/
theorem coefficient_congr {n : ℕ} {f g : CoefficientInput n}
(h : Set.EqOn f.val g.val (Set.Icc (-1) 1)) : coefficient f = coefficient g := by
rw [coefficient_eq_integral_cos, coefficient_eq_integral_cos]
congr 1
apply intervalIntegral.integral_congr
intro θ hθ
dsimp only
rw [h ⟨neg_one_le_cos θ, cos_le_one θ⟩]2.2.2 Completeness in the weighted space
In \(L^2(\mu _T)\), functions that agree almost everywhere represent the same element. A Hilbert basis is an orthonormal family with dense span; its expansions converge in the norm of this space.
Let \(\mathcal P:\mathbb {R}[X]\to L^2(\mathbb {R},\mu _T;\mathbb {R})\) send a polynomial \(p\) to the class of \(x\mapsto p(x)\).
Reference: [DLMF, Table 18.3.1].
Lean Formalisation
theorem Polynomial.Chebyshev.memLp_eval_measureT (p : Polynomial ℝ) :
MeasureTheory.MemLp (fun x => Polynomial.eval x p) 2 Polynomial.Chebyshev.classicalMeasureTLean proof
/-- Polynomials belong to the weighted L² space (DLMF Table 18.3.1). -/
theorem memLp_eval_measureT (p : ℝ[X]) : MemLp (fun x ↦ p.eval x) 2 classicalMeasureT := by
apply (memLp_two_iff_integrable_sq (by fun_prop)).mpr
exact integrable_classicalMeasureT (by fun_prop)The classes of \(T_0/\sqrt\pi \) and \(T_n\sqrt{2/\pi }\) for \(n{\gt}0\) form a Hilbert basis of \(L^2(\mathbb {R},\mu _T;\mathbb {R})\).
Reference: [DLMF, Table 18.3.1], with polynomial density from the Weierstrass theorem.
Lean Formalisation
theorem Polynomial.Chebyshev.hilbertBasisT_apply (n : ℕ) :
Polynomial.Chebyshev.hilbertBasisT n = Polynomial.Chebyshev.normalizedT nLean proof
/-- The Hilbert basis vectors are the normalised Chebyshev classes (DLMF Table 18.3.1). -/
@[simp] theorem hilbertBasisT_apply (n : ℕ) : hilbertBasisT n = normalizedT n := by
exact congrFun (HilbertBasis.coe_mk _ _) nFor every \(f\in L^2(\mathbb {R},\mu _T;\mathbb {R})\),
This asserts convergence in the weighted \(L^2\) norm, not pointwise or uniform convergence.
Lean Formalisation
theorem Polynomial.Chebyshev.hasSum_coefficient_polynomialToL2
(f : ↥(MeasureTheory.Lp ℝ 2 Polynomial.Chebyshev.classicalMeasureT)) :
HasSum
(fun n =>
Polynomial.Chebyshev.coefficient ⟨↑↑f, ⋯⟩ • Polynomial.Chebyshev.polynomialToL2 (Polynomial.Chebyshev.T ℝ ↑n))
fLean proof
/-- Every weighted L² function is the sum of its Chebyshev expansion in L²
(DLMF 18.2(viii); ATAP, Chapter 3). -/
theorem hasSum_coefficient_polynomialToL2 (f : Lp ℝ 2 classicalMeasureT) :
HasSum (fun n : ℕ ↦ (coefficient (n := n) ⟨f, coefficientInput_integrable_L2 f n⟩) • polynomialToL2 (T ℝ n)) f := by
simpa only [hilbertBasisT_repr_smul] using hilbertBasisT.hasSum_repr fFor real \(f\in L^2(\mu _T)\) with full-constant coefficients \(a_n\),
The weighted energy series converges to the integral.
Reference: the Hilbert-space Parseval identity applied to the Chebyshev basis.
Lean Formalisation
theorem Polynomial.Chebyshev.hasSum_coefficient_energy (f : ↥(MeasureTheory.Lp ℝ 2 Polynomial.Chebyshev.classicalMeasureT)) :
HasSum (fun n => (if n = 0 then Real.pi else Real.pi / 2) * Polynomial.Chebyshev.coefficient ⟨↑↑f, ⋯⟩ ^ 2)
(∫ (x : ℝ), ↑↑f x ^ 2 ∂Polynomial.Chebyshev.classicalMeasureT)Lean proof
/-- Parseval as a convergent series, not merely an equality of total tsums. -/
theorem hasSum_coefficient_energy (f : Lp ℝ 2 classicalMeasureT) :
HasSum (fun n ↦ (if n = 0 then π else π / 2) * (coefficient (n := n) ⟨f, coefficientInput_integrable_L2 f _⟩) ^ 2)
(∫ x, f x ^ 2 ∂classicalMeasureT) := by
have h := hilbertBasisT.hasSum_inner_mul_inner f f
simp_rw [inner_hilbertBasisT_mul] at h
simpa only [L2.inner_def, real_inner_self_eq_norm_sq, Real.norm_eq_abs, sq_abs] using hPolynomial classes, density and normalization
Every real polynomial \(p\) is square integrable for \(\mu _T\). The class \(\mathcal P(p)\) agrees \(\mu _T\)-almost everywhere with \(x\mapsto p(x)\), and \(\langle \mathcal P(p),\mathcal P(q)\rangle =\int pq\, d\mu _T\) for all \(p,q\).
Reference: [DLMF, Table 18.3.1]. The map is real linear.
Lean Formalisation
theorem Polynomial.Chebyshev.coe_polynomialToL2 (p : Polynomial ℝ) :
↑↑(Polynomial.Chebyshev.polynomialToL2 p) =ᵐ[Polynomial.Chebyshev.classicalMeasureT] fun x => Polynomial.eval x pLean proof
/-- An almost-everywhere representative of polynomial evaluation (ATAP, Chapter 3). -/
theorem coe_polynomialToL2 (p : ℝ[X]) : polynomialToL2 p =ᵐ[classicalMeasureT] fun x ↦ p.eval x :=
(memLp_eval_measureT p).coeFn_toLpFor \(f\in L^2(\mathbb {R},\mu _T;\mathbb {R})\) and \(n\in \mathbb {N}\),
Coefficients are evaluated on any almost-everywhere representative and are independent of that choice.
Lean Formalisation
theorem Polynomial.Chebyshev.inner_polynomialToL2_left (p : Polynomial ℝ)
(f : ↥(MeasureTheory.Lp ℝ 2 Polynomial.Chebyshev.classicalMeasureT)) :
inner ℝ (Polynomial.Chebyshev.polynomialToL2 p) f =
∫ (x : ℝ), ↑↑f x * Polynomial.eval x p ∂Polynomial.Chebyshev.classicalMeasureTLean proof
/-- Polynomial inner products with arbitrary L² classes (DLMF Table 18.3.1). -/
theorem inner_polynomialToL2_left (p : ℝ[X]) (f : Lp ℝ 2 classicalMeasureT) :
⟪polynomialToL2 p, f⟫_ℝ = ∫ x, f x * p.eval x ∂classicalMeasureT := by
rw [L2.inner_def]
apply integral_congr_ae
filter_upwards [coe_polynomialToL2 p] with x hp
simp [hp]The measure \(\mu _T\) is finite and almost every point belongs to \([-1,1]\).
Reference: [DLMF, Table 18.3.1].
Lean Formalisation
theorem Polynomial.Chebyshev.isFiniteMeasure_measureT : MeasureTheory.IsFiniteMeasure Polynomial.Chebyshev.classicalMeasureTLean proof
/-- The first-kind weight is finite (DLMF Table 18.3.1). -/
instance isFiniteMeasure_measureT : IsFiniteMeasure classicalMeasureT :=
(integrable_const_iff_isFiniteMeasure (by norm_num : (1 : ℝ) ≠ 0)).mp
(integrable_classicalMeasureT (f := fun _ ↦ 1) (by fun_prop))The range of \(\mathcal P\) is dense in \(L^2(\mathbb {R},\mu _T;\mathbb {R})\).
Reference: Weierstrass approximation, as in [ATAP, Chapter 1].
Lean Formalisation
theorem Polynomial.Chebyshev.polynomialToL2_denseRange : DenseRange ⇑Polynomial.Chebyshev.polynomialToL2Lean proof
/-- Weierstrass approximation gives dense polynomial classes in weighted L² (ATAP, Chapter 1). -/
theorem polynomialToL2_denseRange : DenseRange polynomialToL2 := by
have hd := BoundedContinuousFunction.toLp_denseRange ℝ classicalMeasureT ℝ
(by norm_num : (2 : ℝ≥0∞) ≠ ∞)
apply Dense.of_closure (hd.mono ?_)
rintro _ ⟨f, rfl⟩
rw [Metric.mem_closure_iff]
intro ε hε
let K : ℝ := (measureUnivNNReal classicalMeasureT : ℝ) ^ (2 : ℝ≥0∞).toReal⁻¹
have hK : 0 ≤ K := by positivity
let δ := ε / (K + 1)
have hδ : 0 < δ := div_pos hε (by positivity)
obtain ⟨p, hp⟩ := exists_polynomial_near_of_continuousOn (-1) 1 f
f.continuous.continuousOn δ hδ
refine ⟨polynomialToL2 p, ⟨p, rfl⟩, ?_⟩
rw [dist_eq_norm, norm_sub_rev]
have hb : ‖polynomialToL2 p - BoundedContinuousFunction.toLp 2 classicalMeasureT ℝ f‖ ≤ K * δ := by
apply Lp.norm_le_of_ae_bound hδ.le
filter_upwards [ae_mem_Icc_measureT, coe_polynomialToL2 p,
f.coeFn_toLp 2 classicalMeasureT ℝ,
Lp.coeFn_sub (polynomialToL2 p) (BoundedContinuousFunction.toLp 2 classicalMeasureT ℝ f)]
with x hx hpx hfx hsub
rw [hsub]
simp only [Pi.sub_apply, hpx, hfx, Real.norm_eq_abs]
exact (hp x hx).le
apply hb.trans_lt
dsimp [δ]
rw [← mul_div_assoc]
apply (div_lt_iff₀ (by positivity : 0 < K + 1)).mpr
nlinarithWrite \(h_0=\pi \) and \(h_n=\pi /2\) for \(n{\gt}0\), and set \(e_n=h_n^{-1/2}\mathcal P(T_n)\). This is \(T_0/\sqrt\pi \) at index zero and \(T_n\sqrt{2/\pi }\) otherwise.
Reference: [DLMF, Table 18.3.1].
Lean Formalisation
def Polynomial.Chebyshev.normalizedT (n : ℕ) : ↥(MeasureTheory.Lp ℝ 2 Polynomial.Chebyshev.classicalMeasureT)Lean definition
/-- Normalised first-kind Chebyshev classes (DLMF Table 18.3.1). -/
noncomputable def normalizedT (n : ℕ) : Lp ℝ 2 classicalMeasureT :=
(√(if n = 0 then π else π / 2))⁻¹ • polynomialToL2 (T ℝ n)The family \((e_n)_{n\in \mathbb {N}}\) is orthonormal.
Reference: [DLMF, Table 18.3.1].
Lean Formalisation
theorem Polynomial.Chebyshev.inner_polynomialToL2_T (n m : ℕ) :
inner ℝ (Polynomial.Chebyshev.polynomialToL2 (Polynomial.Chebyshev.T ℝ ↑n))
(Polynomial.Chebyshev.polynomialToL2 (Polynomial.Chebyshev.T ℝ ↑m)) =
if n = m then if n = 0 then Real.pi else Real.pi / 2 else 0Lean proof
/-- First-kind squared norms as L² inner products (DLMF Table 18.3.1). -/
theorem inner_polynomialToL2_T (n m : ℕ) :
⟪polynomialToL2 (T ℝ n), polynomialToL2 (T ℝ m)⟫_ℝ =
if n = m then (if n = 0 then π else π / 2) else 0 := by
rw [inner_polynomialToL2]
exact (classicalMeasureT_orthogonality n m).2The closed real linear span of \((e_n)_{n\in \mathbb {N}}\) is the whole weighted \(L^2\) space.
Reference: [ATAP, Chapters 1 and 3].
Lean Formalisation
theorem Polynomial.Chebyshev.span_polynomialToL2_T :
Submodule.span ℝ (Set.range fun n => Polynomial.Chebyshev.polynomialToL2 (Polynomial.Chebyshev.T ℝ ↑n)) =
Polynomial.Chebyshev.polynomialToL2.rangeLean proof
/-- Chebyshev polynomial classes span the polynomial image in L² (ATAP, Chapter 3). -/
theorem span_polynomialToL2_T :
Submodule.span ℝ (Set.range (fun n : ℕ ↦ polynomialToL2 (T ℝ n))) =
LinearMap.range polynomialToL2 := by
have hs : Submodule.span ℝ (Set.range (fun n : ℕ ↦ T ℝ n)) = ⊤ := by
apply (chebyshevTsequence ℝ).span
intro n
apply isUnit_iff_ne_zero.mpr
exact leadingCoeff_ne_zero.mpr ((chebyshevTsequence ℝ).ne_zero n)
simpa only [Submodule.map_span, ← Set.range_comp, Function.comp_def, Submodule.map_top]
using congrArg (Submodule.map polynomialToL2) hsIf \(fT_n\) and \(gT_n\) are integrable for \(\mu _T\), then \(a_n(f+g)=a_n(f)+a_n(g)\). For every real \(c\) and \(f\in \mathcal I_n\), \(a_n(cf)=c\, a_n(f)\). For every finite family \((f_j)_{j\in J}\) in \(\mathcal I_n\), \(a_n(\sum _{j\in J}f_j)=\sum _{j\in J}a_n(f_j)\). In particular, additivity holds for real-valued functions continuous on \([-1,1]\).
Reference: the weighted-integral convention in [ATAP, Chapter 3].
Lean Formalisation
theorem Polynomial.Chebyshev.coefficient_add {n : ℕ} (f g : Polynomial.Chebyshev.CoefficientInput n) :
Polynomial.Chebyshev.coefficient (f.add g) = Polynomial.Chebyshev.coefficient f + Polynomial.Chebyshev.coefficient gLean proof
/-- Additivity on the full integrable-product domain (ATAP Ch. 3). -/
theorem coefficient_add {n : ℕ} (f g : CoefficientInput n) :
coefficient (f.add g) = coefficient f + coefficient g := by
simp only [coefficient, CoefficientInput.add, add_mul,
integral_add f.property g.property, mul_add]