summable_inner — Mathlib

English

In the lp-direct sum space lp G 2, for any f,g, the scalar sequence i ↦ ⟪f(i), g(i)⟫ is summable.

Русский

В пространстве прямой суммы lp G 2 для любых f,g последовательность i ↦ ⟪f(i), g(i)⟫ суммируема.

LaTeX

$$$ \\mathrm{Summable}\\big(i \\mapsto \\langle f(i), g(i)\\rangle\\big)$$$

Lean4

theorem summable_inner (f g : lp G 2) : Summable fun i => ⟪f i, g i⟫ := by
  -- Apply the Direct Comparison Test, comparing with ∑' i, ‖f i‖ * ‖g i‖ (summable by Hölder)

  refine .of_norm_bounded (lp.summable_mul ?_ f g) ?_
  · rw [Real.holderConjugate_iff]; norm_num
  intro i
  exact norm_inner_le_norm (𝕜 := 𝕜) _ _

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