English
Using the inverse equivalence, a term of the origin-changed series equals the original p-term evaluated at a piecewise-constructed input split by x and y.
Русский
С помощью обратной эквивалентности член измененного ряда становится равным исходному члену p, вычисленному на входе, раз Adults по разделенным x и y.
LaTeX
$$Let s := changeOriginIndexEquiv.symm ⟨n,t⟩. Then p.changeOriginSeriesTerm s.1 s.2.1 s.2.2 s.2.2.2 (fun _ => x) (fun _ => y) = p n (t.piecewise (fun _ => x) (fun _ => y))$$
Lean4
/-- An auxiliary equivalence useful in the proofs about
`FormalMultilinearSeries.changeOriginSeries`: the set of triples `(k, l, s)`, where `s` is a
`Finset (Fin (k + l))` of cardinality `l` is equivalent to the set of pairs `(n, s)`, where `s` is a
`Finset (Fin n)`.
The forward map sends `(k, l, s)` to `(k + l, s)` and the inverse map sends `(n, s)` to
`(n - Finset.card s, Finset.card s, s)`. The actual definition is less readable because of problems
with non-definitional equalities. -/
@[simps]
def changeOriginIndexEquiv : (Σ k l : ℕ, { s : Finset (Fin (k + l)) // s.card = l }) ≃ Σ n : ℕ, Finset (Fin n)
where
toFun s := ⟨s.1 + s.2.1, s.2.2⟩
invFun
s :=
⟨s.1 - s.2.card, s.2.card,
⟨s.2.map (finCongr <| (tsub_add_cancel_of_le <| card_finset_fin_le s.2).symm).toEmbedding, Finset.card_map _⟩⟩
left_inv := by
rintro ⟨k, l, ⟨s : Finset (Fin <| k + l), hs : s.card = l⟩⟩
dsimp only [Subtype.coe_mk]
-- Lean can't automatically generalize `k' = k + l - s.card`, `l' = s.card`, so we explicitly
-- formulate the generalized goal
suffices
∀ k' l',
k' = k →
l' = l →
∀ (hkl : k + l = k' + l') (hs'),
(⟨k', l', ⟨s.map (finCongr hkl).toEmbedding, hs'⟩⟩ :
Σ k l : ℕ, { s : Finset (Fin (k + l)) // s.card = l }) =
⟨k, l, ⟨s, hs⟩⟩
by apply this <;> simp only [hs, add_tsub_cancel_right]
simp
right_inv := by
rintro ⟨n, s⟩
simp [tsub_add_cancel_of_le (card_finset_fin_le s), finCongr_eq_equivCast]
