Theorems · Definition · functional analysis

RCLike.wInner

{ι : Type u_1} →
  {𝕜 : Type u_3} →
    {E : ι → Type u_4} →
      [Fintype ι] →
        [inst : RCLike 𝕜] →
          [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] →
            [(i : ι) → InnerProductSpace 𝕜 (E i)] → (ι → ℝ) → ((i : ι) → E i) → ((i : ι) → E i) → 𝕜

Weighted inner product giving rise to the L2 norm, denoted as ⟪g, f⟫_[𝕜, w].

Defined in

Mathlib.Analysis.RCLike.Inner

Cited by

33 results in Mathlib

Foundations

Depth 158 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeRCLikeSeminormedAddCommGroupInnerProductSpace