theorem Matrix.PosSemidef.nonneg_apply_self {n : Type u_1} {R : Type u_2} [CommRing R] [PartialOrder R] [StarRing R] {M : Matrix n n R} (hM : M.PosSemidef) (i : n) : 0 ≤ M i i

def LinearMap.mkContinuous₂OfFiniteDimensional {E : Type u_1} {F : Type u_2} {G : Type u_3} {𝕜 : Type u_4} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] [NormedSpace 𝕜 G] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (f : E →ₗ[𝕜] F →ₗ[𝕜] G) : E →L[𝕜] F →L[𝕜] G

Given a bilinear map whose codomains are finite dimensional, outputs the continuous version.

Equations

• f.mkContinuous₂OfFiniteDimensional = LinearMap.toContinuousLinearMap { toFun := fun (x : E) => LinearMap.toContinuousLinearMap (f x), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem LinearMap.mkContinuous₂OfFiniteDimensional_apply {E : Type u_1} {F : Type u_2} {G : Type u_3} {𝕜 : Type u_4} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] [NormedSpace 𝕜 G] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (f : E →ₗ[𝕜] F →ₗ[𝕜] G) (x : E) (y : F) : (f.mkContinuous₂OfFiniteDimensional x) y = (f x) y

theorem OrthonormalBasis.inner_eq {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [NormedAddCommGroup E] [RCLike 𝕜] [InnerProductSpace 𝕜 E] [Fintype ι] [DecidableEq ι] (b : OrthonormalBasis ι 𝕜 E) {i j : ι} : inner 𝕜 (b i) (b j) = if i = j then 1 else 0

theorem OrthonormalBasis.norm_sq_eq_sum_sq_inner_right {ι : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fintype ι] (b : OrthonormalBasis ι ℝ E) (x : E) : ‖x‖ ^ 2 = ∑ i : ι, inner ℝ (b i) x ^ 2

theorem OrthonormalBasis.norm_sq_eq_sum_sq_inner_left {ι : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fintype ι] (b : OrthonormalBasis ι ℝ E) (x : E) : ‖x‖ ^ 2 = ∑ i : ι, inner ℝ x (b i) ^ 2

theorem EuclideanSpace.real_inner_eq {ι : Type u_1} [Fintype ι] (x y : EuclideanSpace ℝ ι) : inner ℝ x y = ∑ i : ι, x.ofLp i * y.ofLp i

@[simp]

theorem inner_toDual_symm_eq_self {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (L : StrongDual 𝕜 E) : inner 𝕜 ((InnerProductSpace.toDual 𝕜 E).symm L) = ⇑L

@[simp]

theorem LinearIsometryEquiv.coe_coe_eq_coe {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] (f : E ≃ₗᵢ[𝕜] F) : ⇑f.toLinearIsometry.toContinuousLinearMap = ⇑f