nevanlinna/Nevanlinna/bilinear.lean

/-
Copyright (c) 2024 Stefan Kebekus. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Stefan Kebekus
-/

import Mathlib.Analysis.InnerProductSpace.PiL2

/-!

# Canoncial Elements in Tensor Powers of Real Inner Product Spaces

Given an `InnerProductSpace ℝ E`, this file defines two canonical tensors, which
are relevant when for a coordinate-free definition of differential operators
such as the Laplacian.

* `InnerProductSpace.canonicalContravariantTensor E : E ⊗[ℝ] E →ₗ[ℝ] ℝ`. This is
  the element corresponding to the inner product.

* If `E` is finite-dimensional, then `E ⊗[ℝ] E` is canonically isomorphic to its
  dual. Accordingly, there exists an element
  `InnerProductSpace.canonicalCovariantTensor E : E ⊗[ℝ] E` that corresponds to
  `InnerProductSpace.canonicalContravariantTensor E` under this identification.

The theorem `InnerProductSpace.canonicalCovariantTensorRepresentation` shows
that `InnerProductSpace.canonicalCovariantTensor E` can be computed from any
orthonormal basis `v` as `∑ i, (v i) ⊗ₜ[ℝ] (v i)`.

-/


open TensorProduct


lemma OrthonormalBasis.sum_repr'
  {𝕜 : Type*} [RCLike 𝕜]
  {E : Type*} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
  [Fintype ι]
  (b : OrthonormalBasis ι 𝕜 E)
  (v : E) :
  v = ∑ i, ⟪b i, v⟫_𝕜 • (b i) := by
  nth_rw 1 [← (b.sum_repr v)]
  simp_rw [b.repr_apply_apply v]


noncomputable def InnerProductSpace.canonicalContravariantTensor
  {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  : E ⊗[ℝ] E →ₗ[ℝ] ℝ := TensorProduct.lift bilinFormOfRealInner


noncomputable def InnerProductSpace.canonicalCovariantTensor
  (E : Type*) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] 
  : E ⊗[ℝ] E := ∑ i, ((stdOrthonormalBasis ℝ E) i) ⊗ₜ[ℝ] ((stdOrthonormalBasis ℝ E) i)


theorem InnerProductSpace.canonicalCovariantTensorRepresentation
  (E : Type*) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [Fintype ι]
  (v : OrthonormalBasis ι ℝ E)
  : InnerProductSpace.canonicalCovariantTensor E = ∑ i, (v i) ⊗ₜ[ℝ] (v i) := by

  let w := stdOrthonormalBasis ℝ E
  conv =>
    right
    arg 2
    intro i
    rw [w.sum_repr' (v i)]
  simp_rw [TensorProduct.sum_tmul, TensorProduct.tmul_sum, TensorProduct.smul_tmul_smul]
  
  conv =>
    right
    rw [Finset.sum_comm]
    arg 2
    intro y
    rw [Finset.sum_comm]
    arg 2
    intro x
    rw [← Finset.sum_smul]
    arg 1
    arg 2
    intro i
    rw [← real_inner_comm (w x)]
  simp_rw [OrthonormalBasis.sum_inner_mul_inner v]

  have {i} : ∑ j, ⟪w i, w j⟫_ℝ • w i ⊗ₜ[ℝ] w j = w i ⊗ₜ[ℝ] w i := by
    rw [Fintype.sum_eq_single i, orthonormal_iff_ite.1 w.orthonormal]; simp
    intro _ _; rw [orthonormal_iff_ite.1 w.orthonormal]; simp; tauto
  simp_rw [this]
  rfl