English
Composing a formal multilinear series with the identity yields the same series: p ∘ id 𝕜 E x = p; equivalently, p.comp (id 𝕜 E x) = p.
Русский
Скомпоновка формальной многочленовой серии с идентичностью даёт ту же серию: p ∘ id 𝕜 E x = p; эквивалентно, p.comp (id 𝕜 E x) = p.
LaTeX
$$$p \\circ (id\\; 𝕜\\; E\\ x) = p,$ i.e. $p.comp (FormalMultilinearSeries.id\\ 𝕜 E x) = p$.$$
Lean4
@[simp]
theorem comp_id (p : FormalMultilinearSeries 𝕜 E F) (x : E) : p.comp (id 𝕜 E x) = p :=
by
ext1 n
dsimp [FormalMultilinearSeries.comp]
rw [Finset.sum_eq_single (Composition.ones n)]
· show compAlongComposition p (id 𝕜 E x) (Composition.ones n) = p n
ext v
rw [compAlongComposition_apply]
apply p.congr (Composition.ones_length n)
intros
rw [applyComposition_ones]
refine congr_arg v ?_
rw [Fin.ext_iff, Fin.coe_castLE, Fin.val_mk]
· change ∀ b : Composition n, b ∈ Finset.univ → b ≠ Composition.ones n → compAlongComposition p (id 𝕜 E x) b = 0
intro b _ hb
obtain ⟨k, hk, lt_k⟩ : ∃ (k : ℕ), k ∈ Composition.blocks b ∧ 1 < k := Composition.ne_ones_iff.1 hb
obtain ⟨i, hi⟩ : ∃ (i : Fin b.blocks.length), b.blocks[i] = k := List.get_of_mem hk
let j : Fin b.length := ⟨i.val, b.blocks_length ▸ i.prop⟩
have A : 1 < b.blocksFun j := by convert lt_k
ext v
rw [compAlongComposition_apply, ContinuousMultilinearMap.zero_apply]
apply ContinuousMultilinearMap.map_coord_zero _ j
dsimp [applyComposition]
rw [id_apply_of_one_lt _ _ _ A, ContinuousMultilinearMap.zero_apply]
· simp
