nevanlinna/Nevanlinna/bilinear.lean

79 lines
2.6 KiB
Plaintext
Raw Permalink Normal View History

2024-06-29 17:17:19 +02:00
/-
Copyright (c) 2024 Stefan Kebekus. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Stefan Kebekus
-/
2024-06-26 12:28:39 +02:00
import Mathlib.Analysis.InnerProductSpace.PiL2
2024-06-29 17:17:19 +02:00
/-!
# 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)`.
-/
2024-06-29 09:17:43 +02:00
open TensorProduct
2024-06-26 12:28:39 +02:00
2024-06-29 17:17:19 +02:00
noncomputable def InnerProductSpace.canonicalContravariantTensor
{E : Type*} [NormedAddCommGroup E] [InnerProductSpace E]
: E ⊗[] E →ₗ[] := TensorProduct.lift bilinFormOfRealInner
2024-06-28 07:53:20 +02:00
2024-06-29 17:17:19 +02:00
noncomputable def InnerProductSpace.canonicalCovariantTensor
2024-07-25 15:52:16 +02:00
(E : Type*) [NormedAddCommGroup E] [InnerProductSpace E] [FiniteDimensional E]
2024-06-29 17:17:19 +02:00
: E ⊗[] E := ∑ i, ((stdOrthonormalBasis E) i) ⊗ₜ[] ((stdOrthonormalBasis E) i)
2024-06-28 07:53:20 +02:00
2024-06-29 17:17:19 +02:00
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
2024-06-28 07:53:20 +02:00
conv =>
right
arg 2
intro i
2024-07-25 15:52:16 +02:00
rw [← w.sum_repr' (v i)]
2024-06-29 09:01:53 +02:00
simp_rw [TensorProduct.sum_tmul, TensorProduct.tmul_sum, TensorProduct.smul_tmul_smul]
2024-07-25 15:52:16 +02:00
2024-06-28 07:53:20 +02:00
conv =>
right
rw [Finset.sum_comm]
arg 2
intro y
2024-06-29 09:01:53 +02:00
rw [Finset.sum_comm]
arg 2
intro x
2024-06-28 07:53:20 +02:00
rw [← Finset.sum_smul]
2024-06-29 09:01:53 +02:00
arg 1
arg 2
intro i
2024-06-29 17:17:19 +02:00
rw [← real_inner_comm (w x)]
2024-06-29 09:17:43 +02:00
simp_rw [OrthonormalBasis.sum_inner_mul_inner v]
2024-06-28 07:53:20 +02:00
2024-06-29 17:17:19 +02:00
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
2024-06-29 09:17:43 +02:00
simp_rw [this]
2024-06-29 17:17:19 +02:00
rfl