changeOriginSeriesTerm_changeOriginIndexEquiv_symm

English

There is a summability bound for the family of terms of the origin-changed series, controlled by the radius and the growth of p.

Русский

Существуют границы суммируемости семейств членов ряда изменения начала, зависящие от радиуса и роста p.

LaTeX

$$$\\text{changeOriginSeries_summable_aux₁}:\\; \\text{Summable } f(S) \\,\\Rightarrow\\; \\text{Summable } g(S)\\text{ with bound }\\dots$$$

Lean4

theorem changeOriginSeriesTerm_changeOriginIndexEquiv_symm (n t) :
    let s := changeOriginIndexEquiv.symm ⟨n, t⟩
    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) :=
  by
  have :
    ∀ (m) (hm : n = m),
      p n (t.piecewise (fun _ ↦ x) fun _ ↦ y) =
        p m ((t.map (finCongr hm).toEmbedding).piecewise (fun _ ↦ x) fun _ ↦ y) :=
    by
    rintro m rfl
    simp +unfoldPartialApp [Finset.piecewise]
  simp_rw [changeOriginSeriesTerm_apply, eq_comm]; apply this

Похожие утверждения