mem_L1_inner — Mathlib

English

The pointwise inner product of two L2 functions is integrable in L1, i.e., lies in L1(μ).

Русский

Пусть f,g — функции из L2; их покоординатное скалярное произведение принадлежит L1(μ).

LaTeX

$$$⟪f,g⟫ \\in L^1(μ)\\quad\\text{(as a function } a \\mapsto ⟪f(a), g(a)⟫\\text{)}$$$

Lean4

theorem mem_L1_inner (f g : α →₂[μ] E) :
    AEEqFun.mk (fun x => ⟪f x, g x⟫) ((Lp.aestronglyMeasurable f).inner (Lp.aestronglyMeasurable g)) ∈ Lp 𝕜 1 μ := by
  simp_rw [mem_Lp_iff_eLpNorm_lt_top, eLpNorm_aeeqFun]; exact eLpNorm_inner_lt_top f g

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