nnnorm_changeOriginSeries_le_tsum

English

For all k,l, the NN-norm of the k,l-entry of the origin-changed series is bounded by the ordinary sum of the same bound over all index sets of cardinality l, i.e., the length of the index set does not exceed the contributing bound.

Русский

Для всех k,l НН-норма элемента k,l-части ряда после переноса начала ограничена обычной суммой по всем индексным множествам размером l: размер индекса не влияет на величину верхней границы

LaTeX

$$$\\|p.changeOriginSeries\\; k\\; l\\|_{+} \\le \\sum_{\\{s: s.card = l\\}}' \\; \\|p(k+l)\\|_{+}$$$

Lean4

theorem nnnorm_changeOriginSeries_le_tsum (k l : ℕ) :
    ‖p.changeOriginSeries k l‖₊ ≤ ∑' _ : { s : Finset (Fin (k + l)) // s.card = l }, ‖p (k + l)‖₊ :=
  (nnnorm_sum_le _ (fun t => changeOriginSeriesTerm p k l (Subtype.val t) t.prop)).trans_eq <| by
    simp_rw [tsum_fintype, nnnorm_changeOriginSeriesTerm (p := p) (k := k) (l := l)]

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