English
If g and f have finite formal power series q and p at f x and x respectively, then g ∘ f has finite formal power series q.comp p at x with index m * n.
Русский
Если у g и f имеются конечные формальные рядовые q и p в точках f(x) и x соответственно, тогда у g∘f есть конечный формальный ряд q.comp p в x с индексом m·n.
LaTeX
$$$HasFiniteFPowerSeriesAt g q (f x) m \\to HasFiniteFPowerSeriesAt f p x n \\to 0 < n \\to HasFiniteFPowerSeriesAt (g \\circ f) (q.comp p) x (m \\cdot n)$$$
Lean4
/-- If two functions `g` and `f` have finite power series `q` and `p` respectively at `f x` and `x`,
then `g ∘ f` admits the finite power series `q.comp p` at `x`. -/
theorem comp {m n : ℕ} {g : F → G} {f : E → F} {q : FormalMultilinearSeries 𝕜 F G} {p : FormalMultilinearSeries 𝕜 E F}
{x : E} (hg : HasFiniteFPowerSeriesAt g q (f x) m) (hf : HasFiniteFPowerSeriesAt f p x n) (hn : 0 < n) :
HasFiniteFPowerSeriesAt (g ∘ f) (q.comp p) x (m * n) :=
by
rcases hg.hasFPowerSeriesAt.comp hf.hasFPowerSeriesAt with ⟨r, hr⟩
refine ⟨r, hr, fun i hi ↦ ?_⟩
apply Finset.sum_eq_zero
rintro c -
ext v
simp only [compAlongComposition_apply, ContinuousMultilinearMap.zero_apply]
rcases le_or_gt m c.length with hc | hc
· simp [hg.finite _ hc]
obtain ⟨j, hj⟩ : ∃ j, n ≤ c.blocksFun j := by
contrapose! hi
rw [← c.sum_blocksFun]
rcases eq_zero_or_pos c.length with h'c | h'c
· have : ∑ j : Fin c.length, c.blocksFun j = 0 :=
by
apply Finset.sum_eq_zero (fun j hj ↦ ?_)
have := j.2
grind
rw [this]
exact mul_pos (by grind) hn
·
calc
∑ j : Fin c.length, c.blocksFun j
_ < ∑ j : Fin c.length, n := by
apply Finset.sum_lt_sum (fun j hj ↦ (hi j).le)
exact ⟨⟨0, h'c⟩, Finset.mem_univ _, hi _⟩
_ = c.length * n := by simp
_ ≤ m * n := by gcongr
apply ContinuousMultilinearMap.map_coord_zero _ j
simp [applyComposition, hf.finite _ hj]
