Skip to content

Commit

Permalink
wip tensor inner product
Browse files Browse the repository at this point in the history
  • Loading branch information
eric-wieser committed Jul 19, 2023
1 parent 8ffd8dd commit 959b8bb
Show file tree
Hide file tree
Showing 2 changed files with 81 additions and 0 deletions.
33 changes: 33 additions & 0 deletions src/for_mathlib/linear_algebra/bilinear_form/tensor_product.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,33 @@
/-
Copyright (c) 2023 Eric Wieser. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Eric Wieser
-/
import linear_algebra.bilinear_form.tensor_product

universes u v w
variables {ι : Type*} {R : Type*} {M₁ M₂ : Type*}

open_locale tensor_product

namespace bilin_form

section comm_semiring
variables [comm_semiring R]
variables [add_comm_monoid M₁] [add_comm_monoid M₂]
variables [module R M₁] [module R M₂]

lemma is_symm.tmul {B₁ : bilin_form R M₁} {B₂ : bilin_form R M₂}
(hB₁ : B₁.is_symm) (hB₂ : B₂.is_symm) : (B₁.tmul B₂).is_symm :=
suffices (B₁.tmul B₂).to_lin = (B₁.tmul B₂).to_lin.flip,
begin
intros x y,
have := fun_like.congr_fun (fun_like.congr_fun this x) y,
exact this
end,
tensor_product.ext' $ λ x₁ x₂, tensor_product.ext' $ λ y₁ y₂,
(congr_arg2 (*) (hB₁ x₁ y₁) (hB₂ x₂ y₂) : _)

end comm_semiring

end bilin_form
Original file line number Diff line number Diff line change
@@ -0,0 +1,48 @@
import for_mathlib.linear_algebra.bilinear_form.tensor_product

import analysis.inner_product_space.basic

variables {V W : Type*} [normed_add_comm_group V] [normed_add_comm_group W]
variables [inner_product_space ℝ V] [inner_product_space ℝ W]

open_locale tensor_product

noncomputable instance : inner_product_space.core ℝ (V ⊗[ℝ] W) :=

Check warning on line 10 in src/for_mathlib/linear_algebra/tensor_product/inner_product_space.lean

View workflow job for this annotation

GitHub Actions / Build project

/home/runner/work/lean-ga/lean-ga/src/for_mathlib/linear_algebra/tensor_product/inner_product_space.lean:10:14: declaration 'tensor_product.inner_product_space.core' uses sorry
{ inner := λ x y, bilin_form_of_real_inner.tmul bilin_form_of_real_inner x y,
conj_symm := λ x y,
bilin_form.is_symm.tmul (λ x y, real_inner_comm _ _) (λ x y, real_inner_comm _ _) y x,
nonneg_re := λ x, begin
simp only [is_R_or_C.re_to_real],
induction x using tensor_product.induction_on with v w x y hx hy,
{ simp only [bilin_form.zero_right] },
{ simp only [bilin_form.tmul.equations._eqn_1, bilin_form_of_real_inner_apply,
bilin_form.tensor_distrib_tmul],
exact mul_nonneg real_inner_self_nonneg real_inner_self_nonneg, },
{ simp only [bilin_form.add_left, bilin_form.add_right],
sorry },
end,
definite := sorry,
add_left := bilin_form.add_left,
smul_left := λ _ _ _, bilin_form.bilin_smul_left _ _ _ _ }

noncomputable instance : normed_add_comm_group (V ⊗[ℝ] W) :=
@inner_product_space.core.to_normed_add_comm_group ℝ _ _ _ _ _

noncomputable instance : inner_product_space ℝ (V ⊗[ℝ] W) :=
inner_product_space.of_core _

@[simp] lemma tmul_inner_tmul (v₁ : V) (w₁ : W) (v₂ : V) (w₂ : W) :
@inner ℝ _ _ (v₁ ⊗ₜ[ℝ] w₁) (v₂ ⊗ₜ[ℝ] w₂) = inner v₁ v₂ * inner w₁ w₂ :=
bilin_form.tensor_distrib_tmul _ _ _ _ _ _

@[simp] lemma norm_tmul (v : V) (w : W) : ‖v ⊗ₜ[ℝ] w‖ = ‖v‖ * ‖w‖ :=
begin
have := congr_arg real.sqrt (tmul_inner_tmul v w v w),
simp_rw real_inner_self_eq_norm_sq at this,
rw [← mul_pow, real.sqrt_sq (norm_nonneg _),
real.sqrt_sq (mul_nonneg (norm_nonneg _) (norm_nonneg _))] at this,
exact this,
end

@[simp] lemma nnnorm_tmul (v : V) (w : W) : ‖v ⊗ₜ[ℝ] w‖₊ = ‖v‖₊ * ‖w‖₊ :=
nnreal.eq $ norm_tmul _ _

0 comments on commit 959b8bb

Please sign in to comment.