Normed-space tensor insertion and Hilbert-space contraction

Pointwise tensoring of a normed-space vector with a finite complex spin vector, as a continuous bilinear map.

Insert a finite-spin L² function into a normed-space-valued L² space.

noncomputable def LiebThirring.tensorInsertionBilinear {ι : Type u_1} {H : Type u_3} [Fintype ι] [NormedAddCommGroup H] [NormedSpace ℂ H] : H →L[ℂ] EuclideanSpace ℂ ι →L[ℂ] PiLp 2 fun (x : ι) => H

Pointwise tensoring of a normed-space vector with a finite complex spin vector, as a continuous bilinear map.

Equations

• LiebThirring.tensorInsertionBilinear = (LinearMap.mk₂ ℂ (fun (v : H) (a : EuclideanSpace ℂ ι) => WithLp.toLp 2 fun (s : ι) => a.ofLp s • v) ⋯ ⋯ ⋯ ⋯).mkContinuous₂ 1 ⋯

noncomputable def LiebThirring.tensorInsertion {ι : Type u_1} {α : Type u_2} {H : Type u_3} [Fintype ι] [MeasurableSpace α] [NormedAddCommGroup H] {μ : MeasureTheory.Measure α} [NormedSpace ℂ H] (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ ι) 2 μ)) : H →L[ℂ] ↥(MeasureTheory.Lp (PiLp 2 fun (x : ι) => H) 2 μ)

Insert a finite-spin L² function into a normed-space-valued L² space.

Equations

• LiebThirring.tensorInsertion f = (ContinuousLinearMap.compLpL₂ 2 μ LiebThirring.tensorInsertionBilinear).flip f

theorem LiebThirring.tensorInsertion_apply_ae {ι : Type u_1} {α : Type u_2} {H : Type u_3} [Fintype ι] [MeasurableSpace α] [NormedAddCommGroup H] {μ : MeasureTheory.Measure α} [NormedSpace ℂ H] (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ ι) 2 μ)) (v : H) : ∀ᵐ (x : α) ∂μ, ∀ (s : ι), (↑↑((tensorInsertion f) v) x).ofLp s = (↑↑f x).ofLp s • v

The inserted L² class has the expected pointwise representative.

theorem LiebThirring.tensorInsertion_norm {ι : Type u_1} {α : Type u_2} {H : Type u_3} [Fintype ι] [MeasurableSpace α] [NormedAddCommGroup H] {μ : MeasureTheory.Measure α} [NormedSpace ℂ H] (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ ι) 2 μ)) (v : H) : ‖(tensorInsertion f) v‖ = ‖f‖ * ‖v‖

Exact norm of tensor insertion at a vector.

theorem LiebThirring.tensorInsertion_opNorm_le {ι : Type u_1} {α : Type u_2} {H : Type u_3} [Fintype ι] [MeasurableSpace α] [NormedAddCommGroup H] {μ : MeasureTheory.Measure α} [NormedSpace ℂ H] (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ ι) 2 μ)) : ‖tensorInsertion f‖ ≤ ‖f‖

The operator norm of insertion is bounded by the norm of the inserted finite-spin function.

theorem LiebThirring.tensorInsertion_smul {ι : Type u_1} {α : Type u_2} {H : Type u_3} [Fintype ι] [MeasurableSpace α] [NormedAddCommGroup H] {μ : MeasureTheory.Measure α} [NormedSpace ℂ H] (a : ℂ) (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ ι) 2 μ)) : tensorInsertion (a • f) = a • tensorInsertion f

Tensor insertion is complex-linear in the inserted finite-spin function.

noncomputable def LiebThirring.tensorContraction {ι : Type u_1} {α : Type u_2} {H : Type u_3} [Fintype ι] [MeasurableSpace α] [NormedAddCommGroup H] {μ : MeasureTheory.Measure α} [InnerProductSpace ℂ H] [CompleteSpace H] (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ ι) 2 μ)) : ↥(MeasureTheory.Lp (PiLp 2 fun (x : ι) => H) 2 μ) →L[ℂ] H

The abstract contraction against f, defined as the adjoint of tensor insertion.

Equations

• LiebThirring.tensorContraction f = ContinuousLinearMap.adjoint (LiebThirring.tensorInsertion f)

theorem LiebThirring.tensorContraction_smul {ι : Type u_1} {α : Type u_2} {H : Type u_3} [Fintype ι] [MeasurableSpace α] [NormedAddCommGroup H] {μ : MeasureTheory.Measure α} [InnerProductSpace ℂ H] [CompleteSpace H] (a : ℂ) (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ ι) 2 μ)) : tensorContraction (a • f) = star a • tensorContraction f

Contraction is conjugate-linear in the contracted finite-spin function.

theorem LiebThirring.tensorContraction_norm_le {ι : Type u_1} {α : Type u_2} {H : Type u_3} [Fintype ι] [MeasurableSpace α] [NormedAddCommGroup H] {μ : MeasureTheory.Measure α} [InnerProductSpace ℂ H] [CompleteSpace H] (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ ι) 2 μ)) (ψ : ↥(MeasureTheory.Lp (PiLp 2 fun (x : ι) => H) 2 μ)) : ‖(tensorContraction f) ψ‖ ≤ ‖f‖ * ‖ψ‖

Contraction has the expected Hilbert-space norm bound.