Fock · section of the QIQT-H book

QIQTH.Fock.OneParticle

← all sections · ← Localization · OneParticleBW →

Fock · entries 270–285 of 1000

Lemma 270 (MPFlow).  source ↗

A measure-preserving one-parameter flow on (X, μ): a one-parameter group χ of μ-measure-preserving maps. The continuum analogue of a one-parameter group of permutations of the (finite) mode set in FreeFieldTypicality.

{X:Typeu_2}→[inst:MeasurableSpace X]→Measure X→Typeu_2\{X : Type\mathrm{u\_2}\} \to [\mathrm{inst} : \mathrm{MeasurableSpace}\,X] \to \mathrm{Measure}\,X \to Type\mathrm{u\_2}

Proof. Immediate from the definitions. □\square

Used by mk, flow, mp, flow_zero, flow_add, comp_chain, unitary, unitary_apply, and 4 more.

Lemma 271 (mk).  source ↗

{X:Typeu_2}→[inst:MeasurableSpace X]→{μ:Measure X}→(flow:R→X→X)→(∀(t:R),MeasurePreserving (flow t) μ μ)→flow 0=id→(∀(st:R),flow (s+t)=flow s∘flow t)→MPFlow μ\{X : Type\mathrm{u\_2}\} \to [\mathrm{inst} : \mathrm{MeasurableSpace}\,X] \to \{\mu : \mathrm{Measure}\,X\} \to (\mathrm{flow} : \mathbb{R} \to X \to X) \to (\forall (t : \mathbb{R}), \mathrm{MeasurePreserving}\,(\mathrm{flow}\,t)\,\mu\,\mu) \to \mathrm{flow}\,0 = \mathrm{id} \to (\forall (s t : \mathbb{R}), \mathrm{flow}\,(s + t) = \mathrm{flow}\,s \circ \mathrm{flow}\,t) \to \href{/browser/qiqth-fock-oneparticle#d-qiqth-fock-oneparticle-mpflow}{\mathrm{MPFlow}}\,\mu

Proof. Immediate from the definitions. □\square

Used by translationFlow.

Definition 272 (flow).  source ↗

The flow map at time t.

flow X μ self  :=  self.1\mathrm{flow}\,X\,\mu\,\mathrm{self} \;:=\; \mathrm{self}.1

Used by mp, flow_zero, flow_add, comp_chain, unitary, unitary_apply, unitary_add_apply, unitary_zero_apply, and 3 more.

Lemma 273 (mp).  source ↗

Each time-slice preserves μ.

MeasurePreserving (self.flow t) μ μ\mathrm{MeasurePreserving}\,(\mathrm{self}.\mathrm{flow}\,t)\,\mu\,\mu

Proof. Immediate from the definitions. □\square

Used by comp_chain, unitary_apply, unitary_add_apply, unitary_zero_apply, boostUnitary_KrepL2, coeFn_boostUnitary, boostUnitary_eq_vadd.

Lemma 274 (flow_zero).  source ↗

The flow at time 0 is the identity.

self.flow 0=id\mathrm{self}.\mathrm{flow}\,0 = \mathrm{id}

Proof. Immediate from the definitions. □\square

Used by unitary_zero_apply.

Lemma 275 (flow_add).  source ↗

One-parameter group law.

self.flow (s+t)=self.flow s∘self.flow t\mathrm{self}.\mathrm{flow}\,(s + t) = \mathrm{self}.\mathrm{flow}\,s \circ \mathrm{self}.\mathrm{flow}\,t

Proof. Immediate from the definitions. □\square

Used by comp_chain.

Lemma 276 (comp_chain).  source ↗

Composing twice along the flow chains the times: ψ ∘ χ_b ∘ χ_a = ψ ∘ χ_{b+a} at the level of L².

(cmp (Φ.flow a) ⋯ ) ((cmp (Φ.flow b) ⋯ ) g)=(cmp (Φ.flow (b+a)) ⋯ ) g(\mathrm{cmp}\,(\Phi.\mathrm{flow}\,a)\,\cdots )\,((\mathrm{cmp}\,(\Phi.\mathrm{flow}\,b)\,\cdots )\,g) = (\mathrm{cmp}\,(\Phi.\mathrm{flow}\,(b + a))\,\cdots )\,g

Proof. By flow_add. □\square

Used by unitary_add_apply.

Definition 277 (unitary).  source ↗

The boost unitary at flow-time t: the unitary ψ ↦ ψ ∘ χ_{-t} on L²(μ). A genuine unitary (surjective linear isometry); unitarity is automatic from measure-preservation.

Used by unitary_apply, unitary_add_apply, unitary_zero_apply, boostUnitary.

Lemma 278 (unitary_apply).  source ↗

The boost unitary acts by precomposition with the inverse-time flow.

(Φ.U t) g=(cmp (Φ.flow (−t)) ⋯ ) g(\Phi.\mathrm{U}\,t)\,g = (\mathrm{cmp}\,(\Phi.\mathrm{flow}\,(-t))\,\cdots )\,g

Proof. Immediate from the definitions. □\square

Used by unitary_add_apply, unitary_zero_apply, boostUnitary_KrepL2, coeFn_boostUnitary, boostUnitary_eq_vadd.

Lemma 279 (unitary_add_apply).  source ↗

One-parameter group law: U(s+t) = U(s) ∘ U(t).

(Φ.U (s+t)) g=(Φ.U s) ((Φ.U t) g)(\Phi.\mathrm{U}\,(s + t))\,g = (\Phi.\mathrm{U}\,s)\,((\Phi.\mathrm{U}\,t)\,g)

Proof. By flow, mp, comp_chain, unitary_apply. □\square

Used by boostUnitary_add_apply.

Lemma 280 (unitary_zero_apply).  source ↗

U(0) = id.

(Φ.U 0) g=g(\Phi.\mathrm{U}\,0)\,g = g

Proof. By flow, mp, flow_zero, unitary_apply. □\square

Used by boostUnitary_zero_apply.

Definition 281 (translationFlow).  source ↗

The translation flow on (ℝ, volume): χ_t = (· + t), measure-preserving since Lebesgue measure is translation-invariant.

translationFlow  :=  {flow:=λtx↦x+t,mp:=_proof_1,flow_zero:=_proof_2,flow_add:=_proof_3}\mathrm{translationFlow} \;:=\; \{\mathrm{flow} :=\lambda t x \mapsto x + t , \mathrm{mp} :=\mathrm{\_proof\_1} , \mathrm{flow\_zero} :=\mathrm{\_proof\_2} , \mathrm{flow\_add} :=\mathrm{\_proof\_3}\}

Used by boostFlow.

Definition 282 (boostFlow).  source ↗

The 1+1D massive Lorentz boost flow. In rapidity coordinates θ (where p = m·sinh θ), the Lorentz-invariant one-particle measure dΩ_m = dp/2ω_p is ½·volume (∝ Lebesgue) and the boost of rapidity t is the translation θ ↦ θ + t. So the genuine continuum mass-m boost flow IS the translation flow (read in rapidity coordinates).

boostFlow  :=  translationFlow\mathrm{boostFlow} \;:=\; \href{/browser/qiqth-fock-oneparticle#d-qiqth-fock-oneparticle-translationflow}{\mathrm{translationFlow}}

Used by boostUnitary, boostUnitary_add_apply, boostUnitary_zero_apply, boostUnitary_KrepL2, coeFn_boostUnitary, boostUnitary_eq_vadd.

Definition 283 (boostUnitary).  source ↗

The 1+1D continuum boost unitary group on the one-particle space L²(ℝ) = L²(mass shell, dΩ_m) (in rapidity coordinates). This is the genuine continuum replacement for FreeFieldTypicality’s finite mode-permutation boost: a one-parameter group of unitaries (boostUnitary_add_apply, boostUnitary_zero_apply) implementing a real Lorentz symmetry.

U t  :=  boostFlow.U tU\,t \;:=\; \href{/browser/qiqth-fock-oneparticle#d-qiqth-fock-oneparticle-boostflow}{\mathrm{boostFlow}}.\mathrm{U}\,t

Used by inner_boostUnitary_KrepL2, symm_edge_eq_inner, kmsFun_ofReal_eq_inner, bcf_apply_eq_top, bcf_apply_eq_bot, vec_boost, boostUnitary_mapsTo_niceWedgeGenSet, stripKMSrvd_closure, and 35 more.

Lemma 284 (boostUnitary_add_apply).  source ↗

The boost unitaries form a one-parameter group.

(U (s+t)) g=(U s) ((U t) g)(\href{/browser/qiqth-fock-oneparticle#d-qiqth-fock-oneparticle-boostunitary}{U}\,(s + t))\,g = (\href{/browser/qiqth-fock-oneparticle#d-qiqth-fock-oneparticle-boostunitary}{U}\,s)\,((\href{/browser/qiqth-fock-oneparticle#d-qiqth-fock-oneparticle-boostunitary}{U}\,t)\,g)

Proof. By unitary_add_apply, boostFlow. □\square

Used by oneParticleBW_niceWedge, oneParticleBW_wedge_complete.

Lemma 285 (boostUnitary_zero_apply).  source ↗

The boost at rapidity 0 is the identity.

(U 0) g=g(\href{/browser/qiqth-fock-oneparticle#d-qiqth-fock-oneparticle-boostunitary}{U}\,0)\,g = g

Proof. By unitary_zero_apply, boostFlow. □\square

Used by oneParticleBW_niceWedge, niceWedgeSeparating_pos_mass, hasDerivAt_inner_boostUnitary_imaginary, oneParticleBW_wedge_complete.

← all sections · ← Localization · OneParticleBW →