Two-particle currying

An ordered two-coordinate version of the state currying equivalence. Its parenthesization exposes the first one-particle factor and then the second.

instance LiebThirring.pairProductVolumeIsSeparable {N : ℕ} (i j : Fin N) : MeasureTheory.IsSeparable MeasureTheory.volume

@[reducible, inline]

noncomputable abbrev LiebThirring.PairRestState {N : ℕ} (i j : Fin N) (q : ℕ) : Type

The Hilbert space of spatial and spin coordinates remaining after two distinct particles are removed.

Equations

• LiebThirring.PairRestState i j q = ↥(MeasureTheory.Lp (EuclideanSpace ℂ (LiebThirring.OtherPairSpinLabels i j q)) 2 MeasureTheory.volume)

@[reducible, inline]

noncomputable abbrev LiebThirring.PairCurriedState {N : ℕ} (i j : Fin N) (q : ℕ) : Type

The ordered two-coordinate curried state carrier.

Equations

• One or more equations did not get rendered due to their size.

instance LiebThirring.pairSpinRestSecondCountableTopology {N : ℕ} (i j : Fin N) (q : ℕ) : SecondCountableTopology ↥(MeasureTheory.Lp (PiLp 2 fun (x : Fin q) => EuclideanSpace ℂ (OtherPairSpinLabels i j q)) 2 MeasureTheory.volume)

instance LiebThirring.pairNestedSpinSecondCountableTopology {N : ℕ} (i j : Fin N) (q : ℕ) : SecondCountableTopology ↥(MeasureTheory.Lp (PiLp 2 fun (x : Fin q) => PiLp 2 fun (x : Fin q) => EuclideanSpace ℂ (OtherPairSpinLabels i j q)) 2 MeasureTheory.volume)

noncomputable def LiebThirring.innerPairCurryingEquiv {N q : ℕ} (i j : Fin N) : ↥(MeasureTheory.Lp (PiLp 2 fun (x : Fin q) => PiLp 2 fun (x : Fin q) => EuclideanSpace ℂ (OtherPairSpinLabels i j q)) 2 MeasureTheory.volume) ≃ₗᵢ[ℂ] PiLp 2 fun (x : Fin q) => ↥(MeasureTheory.Lp (PiLp 2 fun (x : Fin q) => PairRestState i j q) 2 MeasureTheory.volume)

Curry the inner position and distribute both finite spin coordinates.

Equations

• One or more equations did not get rendered due to their size.

theorem LiebThirring.innerPairCurryingEquiv_ae {N q : ℕ} (i j : Fin N) (h : ↥(MeasureTheory.Lp (PiLp 2 fun (x : Fin q) => PiLp 2 fun (x : Fin q) => EuclideanSpace ℂ (OtherPairSpinLabels i j q)) 2 MeasureTheory.volume)) (s : Fin q) : ∀ᵐ (z : Position), ∀ (r : Fin q), ∀ᵐ (y : OtherPairConfiguration i j), ∀ (t : OtherPairSpinLabels i j q), (↑↑((↑↑(((innerPairCurryingEquiv i j) h).ofLp s) z).ofLp r) y).ofLp t = (((↑↑h (z, y)).ofLp s).ofLp r).ofLp t

Representative formula for the inner half of ordered pair currying.

@[reducible, inline]

noncomputable abbrev LiebThirring.PairRawState {N q : ℕ} (i j : Fin N) : Type

The state carrier after separating two spatial coordinates, before spin regrouping.

Equations

• LiebThirring.PairRawState i j = ↥(MeasureTheory.Lp (LiebThirring.SpinAmplitudes N q) 2 MeasureTheory.volume)

@[reducible, inline]

noncomputable abbrev LiebThirring.PairSpinState {N q : ℕ} (i j : Fin N) : Type

The state carrier after separating and regrouping the two selected spins.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev LiebThirring.PairOuterState {N q : ℕ} (i j : Fin N) : Type

The state carrier after currying the first selected spatial coordinate.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LiebThirring.pairPullbackEquiv {N q : ℕ} (i j : Fin N) (hij : i ≠ j) : State N q ≃ₗᵢ[ℂ] PairRawState i j

Pull states back along the measure-preserving two-particle coordinate insertion.

Equations

• LiebThirring.pairPullbackEquiv i j hij = LiebThirring.l2PullbackEquiv (LiebThirring.pairInsertionMeasurableEquiv i j hij) ⋯

theorem LiebThirring.pairPullbackEquiv_apply_ae {N q : ℕ} (i j : Fin N) (hij : i ≠ j) (ψ : State N q) : ↑↑((pairPullbackEquiv i j hij) ψ) =ᵐ[MeasureTheory.volume] fun (w : Position × Position × OtherPairConfiguration i j) => ↑↑ψ ((pairInsertionMeasurableEquiv i j hij) w)

noncomputable def LiebThirring.pairSpinTargetEquiv {N q : ℕ} (i j : Fin N) (hij : i ≠ j) : PairRawState i j ≃ₗᵢ[ℂ] PairSpinState i j

Regroup the two selected spin coordinates in the pulled-back state.

Equations

• LiebThirring.pairSpinTargetEquiv i j hij = LiebThirring.l2TargetEquiv MeasureTheory.volume (LiebThirring.spinPairCurryingLinearIsometryEquiv i j hij)

theorem LiebThirring.pairSpinTargetEquiv_apply_ae {N q : ℕ} (i j : Fin N) (hij : i ≠ j) (a : PairRawState i j) : ↑↑((pairSpinTargetEquiv i j hij) a) =ᵐ[MeasureTheory.volume] fun (w : Position × Position × OtherPairConfiguration i j) => (spinPairCurryingLinearIsometryEquiv i j hij) (↑↑a w)

noncomputable def LiebThirring.pairOuterCurryEquiv {N q : ℕ} (i j : Fin N) : PairSpinState i j ≃ₗᵢ[ℂ] PairOuterState i j

Curry the first selected spatial coordinate in the spin-regrouped state.

Equations

• LiebThirring.pairOuterCurryEquiv i j = LiebThirring.l2CurryLinearIsometryEquiv

theorem LiebThirring.pairOuterCurryEquiv_apply_ae {N q : ℕ} (i j : Fin N) (h : PairSpinState i j) : ∀ᵐ (x : Position) (w : Position × OtherPairConfiguration i j), ↑↑(↑↑((pairOuterCurryEquiv i j) h) x) w = ↑↑h (x, w)

noncomputable def LiebThirring.pairInnerTargetEquiv {N q : ℕ} (i j : Fin N) : ↥(MeasureTheory.Lp (↥(MeasureTheory.Lp (PiLp 2 fun (x : Fin q) => PiLp 2 fun (x : Fin q) => EuclideanSpace ℂ (OtherPairSpinLabels i j q)) 2 MeasureTheory.volume)) 2 MeasureTheory.volume) ≃ₗᵢ[ℂ] ↥(MeasureTheory.Lp (PiLp 2 fun (x : Fin q) => ↥(MeasureTheory.Lp (PiLp 2 fun (x : Fin q) => PairRestState i j q) 2 MeasureTheory.volume)) 2 MeasureTheory.volume)

Curry the inner spatial coordinate and distribute its finite-spin factors.

Equations

• LiebThirring.pairInnerTargetEquiv i j = LiebThirring.l2TargetEquiv MeasureTheory.volume (LiebThirring.innerPairCurryingEquiv i j)

theorem LiebThirring.pairInnerTargetEquiv_apply_ae {N q : ℕ} (i j : Fin N) (c : PairOuterState i j) : ↑↑((pairInnerTargetEquiv i j) c) =ᵐ[MeasureTheory.volume] fun (x : Position) => (innerPairCurryingEquiv i j) (↑↑c x)

noncomputable def LiebThirring.pairCurryingLinearIsometryEquiv {N q : ℕ} (i j : Fin N) (hij : i ≠ j) : State N q ≃ₗᵢ[ℂ] PairCurriedState i j q

The ordered two-particle currying equivalence on the state carrier.

Equations

• One or more equations did not get rendered due to their size.

theorem LiebThirring.pairCurryingLinearIsometryEquiv_apply_ae {N q : ℕ} (i j : Fin N) (hij : i ≠ j) (ψ : State N q) : ∀ᵐ (x : Position), ∀ (s : Fin q), ∀ᵐ (z : Position), ∀ (r : Fin q), ∀ᵐ (y : OtherPairConfiguration i j), ∀ (t : OtherPairSpinLabels i j q), (↑↑((↑↑((↑↑((pairCurryingLinearIsometryEquiv i j hij) ψ) x).ofLp s) z).ofLp r) y).ofLp t = (↑↑ψ (insertParticlePair i j x z y)).ofLp (insertSpinPair i j s r t)

The ordered pair currying has the literal two-particle representative.