mathlib3 documentation

lean-ga / for_mathlib.linear_algebra.tensor_product.inner_product_space

theorem is_symm_bilin_form_of_real_inner {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] :

bilin_form_of_real_inner.is_symm

theorem pos_def_bilin_form_of_real_inner {V : Type u_1} [normed_add_comm_group V] [inner_product_space ℝ V] :

bilin_form_of_real_inner.to_quadratic_form.pos_def

@[protected, instance]

noncomputable def tensor_product.inner_product_space.core {V : Type u_1} {W : Type u_2} [normed_add_comm_group V] [normed_add_comm_group W] [inner_product_space ℝ V] [inner_product_space ℝ W] :

inner_product_space.core ℝ (tensor_product ℝ V W)

Equations

tensor_product.inner_product_space.core = {to_has_inner := {inner := λ (x y : tensor_product ℝ V W), ⇑(bilin_form_of_real_inner.tmul bilin_form_of_real_inner) x y}, conj_symm := _, nonneg_re := _, definite := _, add_left := _, smul_left := _}

@[protected, instance]

noncomputable def tensor_product.normed_add_comm_group {V : Type u_1} {W : Type u_2} [normed_add_comm_group V] [normed_add_comm_group W] [inner_product_space ℝ V] [inner_product_space ℝ W] :

normed_add_comm_group (tensor_product ℝ V W)

Equations

tensor_product.normed_add_comm_group = inner_product_space.core.to_normed_add_comm_group

@[protected, instance]

noncomputable def tensor_product.inner_product_space {V : Type u_1} {W : Type u_2} [normed_add_comm_group V] [normed_add_comm_group W] [inner_product_space ℝ V] [inner_product_space ℝ W] :

inner_product_space ℝ (tensor_product ℝ V W)

Equations

tensor_product.inner_product_space = inner_product_space.of_core tensor_product.inner_product_space.core

@[simp]

theorem tmul_inner_tmul {V : Type u_1} {W : Type u_2} [normed_add_comm_group V] [normed_add_comm_group W] [inner_product_space ℝ V] [inner_product_space ℝ W] (v₁ : V) (w₁ : W) (v₂ : V) (w₂ : W) :

has_inner.inner (v₁ ⊗ₜ[ℝ ] w₁) (v₂ ⊗ₜ[ℝ ] w₂) = has_inner.inner v₁ v₂ * has_inner.inner w₁ w₂

@[simp]

theorem norm_tmul {V : Type u_1} {W : Type u_2} [normed_add_comm_group V] [normed_add_comm_group W] [inner_product_space ℝ V] [inner_product_space ℝ W] (v : V) (w : W) :

‖v ⊗ₜ[ℝ ] w‖ = ‖v‖ * ‖w‖

@[simp]

theorem nnnorm_tmul {V : Type u_1} {W : Type u_2} [normed_add_comm_group V] [normed_add_comm_group W] [inner_product_space ℝ V] [inner_product_space ℝ W] (v : V) (w : W) :

‖v ⊗ₜ[ℝ ] w‖₊ = ‖v‖₊ * ‖w‖₊