source
theorem sum_single_apply {ι : Type u_1} (φ : ι → Type u_2) [(i : ι) → AddCommMonoid (φ i)] [Fintype ι] [DecidableEq ι] (v : (i : ι) → φ i) :
∑ i : ι, Pi.single i (v i) = v
source
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
source
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' := ⋯ }

Instances For

source
@[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
source
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
source
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
source
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
source
theorem EuclideanSpace.real_norm_sq_eq {n : Type u_1} [Fintype n] (x : EuclideanSpace ℝ n) :
‖x‖ ^ 2 = ∑ i : n, x.ofLp i ^ 2
source
theorem EuclideanSpace.real_inner_eq {ι : Type u_1} [Fintype ι] (x y : EuclideanSpace ℝ ι) :
inner ℝ x y = ∑ i : ι, x.ofLp i * y.ofLp i
source
@[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
source
theorem InnerProductSpace.toDual_apply_eq_toDualMap_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (x : E) :
(toDual 𝕜 E) x = (toDualMap 𝕜 E) x
source
theorem OrthonormalBasis.norm_dual {ι : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fintype ι] (b : OrthonormalBasis ι ℝ E) (L : StrongDual ℝ E) :
‖L‖ ^ 2 = ∑ i : ι, L (b i) ^ 2
source
@[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