Operators acting on two finite-spin L² factors

This module lifts a bounded operator pointwise through a finite-spin L² factor. It uses that lift to construct the two tensor insertions and proves that their projection products commute and equal the projection generated by double insertion.

noncomputable def LiebThirring.piLpMap {ι : Type u_1} {E : Type u_3} {F : Type u_4} [Fintype ι] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℂ E] [NormedSpace ℂ F] (T : E →L[ℂ] F) : (PiLp 2 fun (x : ι) => E) →L[ℂ] PiLp 2 fun (x : ι) => F

Apply a bounded complex linear operator to each finite-spin amplitude.

Equations

• LiebThirring.piLpMap T = { toFun := fun (u : PiLp 2 fun (x : ι) => E) => WithLp.toLp 2 fun (s : ι) => T (u.ofLp s), map_add' := ⋯, map_smul' := ⋯ }.mkContinuous ‖T‖ ⋯

noncomputable def LiebThirring.tensorTargetLift {ι : Type u_1} {α : Type u_2} {E : Type u_3} {F : Type u_4} [Fintype ι] [MeasurableSpace α] [NormedAddCommGroup E] [NormedAddCommGroup F] {μ : MeasureTheory.Measure α} [NormedSpace ℂ E] [NormedSpace ℂ F] (T : E →L[ℂ] F) : ↥(MeasureTheory.Lp (PiLp 2 fun (x : ι) => E) 2 μ) →L[ℂ] ↥(MeasureTheory.Lp (PiLp 2 fun (x : ι) => F) 2 μ)

Lift a bounded operator through the finite-spin L² space pointwise.

Equations

• LiebThirring.tensorTargetLift T = ContinuousLinearMap.compLpL 2 μ (LiebThirring.piLpMap T)

theorem LiebThirring.tensorTargetLift_apply_ae {ι : Type u_1} {α : Type u_2} {E : Type u_3} {F : Type u_4} [Fintype ι] [MeasurableSpace α] [NormedAddCommGroup E] [NormedAddCommGroup F] {μ : MeasureTheory.Measure α} [NormedSpace ℂ E] [NormedSpace ℂ F] (T : E →L[ℂ] F) (u : ↥(MeasureTheory.Lp (PiLp 2 fun (x : ι) => E) 2 μ)) : ∀ᵐ (x : α) ∂μ, ∀ (s : ι), (↑↑((tensorTargetLift T) u) x).ofLp s = T ((↑↑u x).ofLp s)

theorem LiebThirring.tensorTargetLift_comp_tensorInsertion {ι : Type u_1} {α : Type u_2} {E : Type u_3} {F : Type u_4} [Fintype ι] [MeasurableSpace α] [NormedAddCommGroup E] [NormedAddCommGroup F] {μ : MeasureTheory.Measure α} [NormedSpace ℂ E] [NormedSpace ℂ F] (T : E →L[ℂ] F) (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ ι) 2 μ)) : tensorTargetLift T ∘SL tensorInsertion f = tensorInsertion f ∘SL T

theorem LiebThirring.piLpMap_adjoint {ι : Type u_1} {E : Type u_3} {F : Type u_4} [Fintype ι] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℂ E] [InnerProductSpace ℂ F] [CompleteSpace E] [CompleteSpace F] (T : E →L[ℂ] F) : ContinuousLinearMap.adjoint (piLpMap T) = piLpMap (ContinuousLinearMap.adjoint T)

theorem LiebThirring.tensorTargetLift_adjoint {ι : Type u_1} {α : Type u_2} {E : Type u_3} {F : Type u_4} [Fintype ι] [MeasurableSpace α] [NormedAddCommGroup E] [NormedAddCommGroup F] {μ : MeasureTheory.Measure α} [InnerProductSpace ℂ E] [InnerProductSpace ℂ F] [CompleteSpace E] [CompleteSpace F] (T : E →L[ℂ] F) : ContinuousLinearMap.adjoint (tensorTargetLift T) = tensorTargetLift (ContinuousLinearMap.adjoint T)

@[reducible, inline]

noncomputable abbrev LiebThirring.FirstFactorSpace (ι : Type u_6) (α : Type u_7) (H : Type u_8) [Fintype ι] [MeasurableSpace α] [NormedAddCommGroup H] (μ : MeasureTheory.Measure α) : Type (max (max u_6 u_7) u_8)

The L² carrier of one finite-spin factor over the residual measure.

Equations

• LiebThirring.FirstFactorSpace ι α H μ = ↥(MeasureTheory.Lp (PiLp 2 fun (x : ι) => H) 2 μ)

@[reducible, inline]

noncomputable abbrev LiebThirring.SecondFactorSpace (ι : Type u_6) (α : Type u_7) (H : Type u_8) [Fintype ι] [MeasurableSpace α] [NormedAddCommGroup H] (μ : MeasureTheory.Measure α) : Type (max (max u_6 u_7) u_8)

The nested L² carrier of two finite-spin factors over the residual measure.

Equations

• LiebThirring.SecondFactorSpace ι α H μ = ↥(MeasureTheory.Lp (PiLp 2 fun (x : ι) => LiebThirring.FirstFactorSpace ι α H μ) 2 μ)

noncomputable def LiebThirring.firstFactorInsertion {ι : Type u_1} {α : Type u_2} [Fintype ι] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {H : Type u_5} [NormedAddCommGroup H] [NormedSpace ℂ H] (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ ι) 2 μ)) : FirstFactorSpace ι α H μ →L[ℂ] SecondFactorSpace ι α H μ

Insert a wavefunction into the outer finite-spin L² factor.

Equations

• LiebThirring.firstFactorInsertion f = LiebThirring.tensorInsertion f

noncomputable def LiebThirring.secondFactorInsertion {ι : Type u_1} {α : Type u_2} [Fintype ι] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {H : Type u_5} [NormedAddCommGroup H] [NormedSpace ℂ H] (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ ι) 2 μ)) : FirstFactorSpace ι α H μ →L[ℂ] SecondFactorSpace ι α H μ

Insert a wavefunction into the inner finite-spin L² factor.

Equations

• LiebThirring.secondFactorInsertion f = LiebThirring.tensorTargetLift (LiebThirring.tensorInsertion f)

noncomputable def LiebThirring.doubleFactorInsertion {ι : Type u_1} {α : Type u_2} [Fintype ι] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {H : Type u_5} [NormedAddCommGroup H] [NormedSpace ℂ H] (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ ι) 2 μ)) : H →L[ℂ] SecondFactorSpace ι α H μ

Insert the same wavefunction into both finite-spin L² factors.

Equations

• LiebThirring.doubleFactorInsertion f = LiebThirring.firstFactorInsertion f ∘SL LiebThirring.tensorInsertion f

theorem LiebThirring.secondFactorInsertion_comp_tensorInsertion {ι : Type u_1} {α : Type u_2} [Fintype ι] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {H : Type u_5} [NormedAddCommGroup H] [NormedSpace ℂ H] (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ ι) 2 μ)) : secondFactorInsertion f ∘SL tensorInsertion f = doubleFactorInsertion f

noncomputable def LiebThirring.firstFactorProjection {ι : Type u_1} {α : Type u_2} [Fintype ι] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ ι) 2 μ)) : SecondFactorSpace ι α H μ →L[ℂ] SecondFactorSpace ι α H μ

The operator obtained by composing outer insertion with its adjoint.

Equations

• LiebThirring.firstFactorProjection f = LiebThirring.firstFactorInsertion f ∘SL ContinuousLinearMap.adjoint (LiebThirring.firstFactorInsertion f)

noncomputable def LiebThirring.secondFactorProjection {ι : Type u_1} {α : Type u_2} [Fintype ι] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ ι) 2 μ)) : SecondFactorSpace ι α H μ →L[ℂ] SecondFactorSpace ι α H μ

The operator obtained by composing inner insertion with its adjoint.

Equations

• LiebThirring.secondFactorProjection f = LiebThirring.secondFactorInsertion f ∘SL ContinuousLinearMap.adjoint (LiebThirring.secondFactorInsertion f)

theorem LiebThirring.secondFactorInsertion_adjoint {ι : Type u_1} {α : Type u_2} [Fintype ι] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ ι) 2 μ)) : ContinuousLinearMap.adjoint (secondFactorInsertion f) = tensorTargetLift (ContinuousLinearMap.adjoint (tensorInsertion f))

theorem LiebThirring.secondFactorInsertion_adjoint_comp_firstFactorInsertion {ι : Type u_1} {α : Type u_2} [Fintype ι] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ ι) 2 μ)) : ContinuousLinearMap.adjoint (secondFactorInsertion f) ∘SL firstFactorInsertion f = tensorInsertion f ∘SL ContinuousLinearMap.adjoint (tensorInsertion f)

theorem LiebThirring.firstFactorInsertion_adjoint_comp_secondFactorInsertion {ι : Type u_1} {α : Type u_2} [Fintype ι] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ ι) 2 μ)) : ContinuousLinearMap.adjoint (firstFactorInsertion f) ∘SL secondFactorInsertion f = tensorInsertion f ∘SL ContinuousLinearMap.adjoint (tensorInsertion f)

theorem LiebThirring.operator_projection_product_first {H : Type u_6} {X : Type u_7} {Y : Type u_8} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [NormedAddCommGroup X] [InnerProductSpace ℂ X] [CompleteSpace X] [NormedAddCommGroup Y] [InnerProductSpace ℂ Y] [CompleteSpace Y] (A : X →L[ℂ] Y) (B : H →L[ℂ] X) (J : X →L[ℂ] Y) (hcross : ContinuousLinearMap.adjoint A ∘SL J = B ∘SL ContinuousLinearMap.adjoint B) (hcomm : J ∘SL B = A ∘SL B) : (A ∘SL ContinuousLinearMap.adjoint A) ∘SL J ∘SL ContinuousLinearMap.adjoint J = (A ∘SL B) ∘SL ContinuousLinearMap.adjoint (A ∘SL B)

theorem LiebThirring.firstFactorProjection_secondFactorProjection {ι : Type u_1} {α : Type u_2} [Fintype ι] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ ι) 2 μ)) : firstFactorProjection f ∘SL secondFactorProjection f = doubleFactorInsertion f ∘SL ContinuousLinearMap.adjoint (doubleFactorInsertion f)

theorem LiebThirring.operator_projection_comp_eq_of_comp_eq {H : Type u_6} {Y : Type u_7} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [NormedAddCommGroup Y] [InnerProductSpace ℂ Y] [CompleteSpace Y] (D : H →L[ℂ] Y) (U : Y ≃ₗᵢ[ℂ] Y) (hU : ↑↑U ∘SL D = D) : (D ∘SL ContinuousLinearMap.adjoint D) ∘SL ↑↑U = D ∘SL ContinuousLinearMap.adjoint D