theorem Matrix.PosSemidef.nonneg_apply_self {n : Type u_1} {R : Type u_2} [Fintype n] [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_norm_sq_eq {n : Type u_1} [Fintype n] (x : EuclideanSpace ℝ n) : ‖x‖ ^ 2 = ∑ i : n, x i ^ 2

theorem basisFun_inner {ι : Type u_1} {𝕜 : Type u_2} [Fintype ι] [RCLike 𝕜] (x : EuclideanSpace 𝕜 ι) (i : ι) : inner 𝕜 ((EuclideanSpace.basisFun ι 𝕜) i) x = x i

theorem inner_basisFun_real {ι : Type u_1} [Fintype ι] (x : EuclideanSpace ℝ ι) (i : ι) : inner ℝ x ((EuclideanSpace.basisFun ι ℝ) i) = x i

noncomputable def OrthonormalBasis.equiv {ι : Type u_1} {ι' : Type u_2} {𝕜 : Type u_3} {E : Type u_4} {E' : Type u_5} [Fintype ι] [Fintype ι'] [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] (b : OrthonormalBasis ι 𝕜 E) (b' : OrthonormalBasis ι' 𝕜 E') (e : ι ≃ ι') : E ≃ₗᵢ[𝕜] E'

The LinearIsometryEquiv which maps an orthonormal basis to another. This is a convenience wrapper around Orthonormal.equiv.

Equations

• b.equiv b' e = ⋯.equiv ⋯ e

theorem OrthonormalBasis.equiv_apply_basis {ι : Type u_1} {ι' : Type u_2} {𝕜 : Type u_3} {E : Type u_4} {E' : Type u_5} [Fintype ι] [Fintype ι'] [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] (b : OrthonormalBasis ι 𝕜 E) (b' : OrthonormalBasis ι' 𝕜 E') (e : ι ≃ ι') (i : ι) : (b.equiv b' e) (b i) = b' (e i)

theorem OrthonormalBasis.equiv_apply {ι : Type u_1} {ι' : Type u_2} {𝕜 : Type u_3} {E : Type u_4} {E' : Type u_5} [Fintype ι] [Fintype ι'] [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] (b : OrthonormalBasis ι 𝕜 E) (b' : OrthonormalBasis ι' 𝕜 E') (e : ι ≃ ι') (x : E) : (b.equiv b' e) x = ∑ i : ι, b.repr x i • b' (e i)

theorem OrthonormalBasis.equiv_apply_euclideanSpace {ι : Type u_1} {𝕜 : Type u_3} {E : Type u_4} [Fintype ι] [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (b : OrthonormalBasis ι 𝕜 E) (x : EuclideanSpace 𝕜 ι) : ((EuclideanSpace.basisFun ι 𝕜).equiv b (Equiv.refl ι)) x = ∑ i : ι, x i • b i

@[simp]

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

theorem OrthonormalBasis.norm_dual {ι : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fintype ι] (b : OrthonormalBasis ι ℝ E) (L : NormedSpace.Dual ℝ E) : ‖L‖ ^ 2 = ∑ i : ι, L (b i) ^ 2

@[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