Theorems · Theorem · functional analysis

OrthonormalBasis.norm_dual

∀ {ι : Type u_1} {E : Type u_2} [inst : Fintype ι] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace ℝ E]
  (b : OrthonormalBasis ι ℝ E) (L : StrongDual ℝ E), ‖L‖ ^ 2 = ∑ i, L (b i) ^ 2

Defined in

Mathlib.Analysis.InnerProductSpace.Dual

Cited by

1 results in Mathlib

Foundations

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

Assumes

FintypeNormedAddCommGroupInnerProductSpace