Unsafe observables

The safety conditions of EpsilonEridani.QFT.Jets.Observable.Basic are only meaningful together with observables that fail them. This file records the two standard ones.

• The particle multiplicity particleMultiplicity s = (Multiset.card s : ℝ) is neither collinear safe (not_isCollinearSafe_particleMultiplicity) nor infrared safe (not_isInfraredSafe_particleMultiplicity): a collinear splitting and a soft addition each add exactly one particle.
• The leading-particle energy leadingEnergy E, the least upper bound of 0 and the values of an energy function E on the particles of a final state, is infrared safe whenever E p → 0 as p → 0 (isInfraredSafe_leadingEnergy), but for a nonzero linear energy functional it is not collinear safe (not_isCollinearSafe_leadingEnergy): splitting a particle of energy E p ≥ 0 with fraction z replaces its contribution E p by max z (1 - z) * E p (leadingEnergy_splitCollinear), which for z ∈ [0, 1] is at most E p, so already z = 1 / 2 on a single particle of positive energy witnesses the failure.

References

• G. Sterman and S. Weinberg, Jets from Quantum Chromodynamics, Phys. Rev. Lett. 39 (1977) 1436.
• G. P. Salam, Towards jetography, Eur. Phys. J. C 67 (2010) 637, §2.

Particle multiplicity

def EpsilonEridani.QFT.Jets.particleMultiplicity {V : Type u_1} : Observable V

The particle multiplicity of a final state: its number of particles, as a real number.

Equations

• EpsilonEridani.QFT.Jets.particleMultiplicity s = ↑s.card

theorem EpsilonEridani.QFT.Jets.particleMultiplicity_def {V : Type u_1} (s : Multiset V) : particleMultiplicity s = ↑s.card

@[simp]

theorem EpsilonEridani.QFT.Jets.particleMultiplicity_zero {V : Type u_1} : particleMultiplicity 0 = 0

@[simp]

theorem EpsilonEridani.QFT.Jets.particleMultiplicity_cons {V : Type u_1} (p : V) (s : Multiset V) : particleMultiplicity (p ::ₘ s) = particleMultiplicity s + 1

@[simp]

theorem EpsilonEridani.QFT.Jets.particleMultiplicity_add {V : Type u_1} (s t : Multiset V) : particleMultiplicity (s + t) = particleMultiplicity s + particleMultiplicity t

The particle multiplicity of the union of two final states is the sum of their multiplicities.

theorem EpsilonEridani.QFT.Jets.not_isCollinearSafe_particleMultiplicity {V : Type u_1} [AddCommGroup V] [Module ℝ V] : ¬IsCollinearSafe particleMultiplicity

The particle multiplicity is not collinear safe: splitting a particle adds one.

theorem EpsilonEridani.QFT.Jets.not_isInfraredSafe_particleMultiplicity {V : Type u_1} [Zero V] [TopologicalSpace V] : ¬IsInfraredSafe particleMultiplicity

The particle multiplicity is not infrared safe: adding a momentum, however soft, adds one particle.

The leading-particle energy

noncomputable def EpsilonEridani.QFT.Jets.leadingEnergy {V : Type u_1} (E : V → ℝ) : Observable V

The leading-particle energy of a final state: the least upper bound of 0 and the values of the energy function E on its particles. For a nonnegative E on a nonempty final state this is the energy of the most energetic particle; on the empty final state it is 0.

Equations

• EpsilonEridani.QFT.Jets.leadingEnergy E s = Multiset.fold max 0 (Multiset.map E s)

@[simp]

theorem EpsilonEridani.QFT.Jets.leadingEnergy_zero {V : Type u_1} (E : V → ℝ) : leadingEnergy E 0 = 0

@[simp]

theorem EpsilonEridani.QFT.Jets.leadingEnergy_cons {V : Type u_1} (E : V → ℝ) (p : V) (s : Multiset V) : leadingEnergy E (p ::ₘ s) = max (E p) (leadingEnergy E s)

@[simp]

theorem EpsilonEridani.QFT.Jets.leadingEnergy_singleton {V : Type u_1} (E : V → ℝ) (p : V) : leadingEnergy E {p} = max (E p) 0

@[simp]

theorem EpsilonEridani.QFT.Jets.leadingEnergy_le_iff {V : Type u_1} {E : V → ℝ} {s : Multiset V} {c : ℝ} : leadingEnergy E s ≤ c ↔ 0 ≤ c ∧ ∀ p ∈ s, E p ≤ c

The leading-particle energy is the least upper bound of 0 and the particle energies.

theorem EpsilonEridani.QFT.Jets.leadingEnergy_nonneg {V : Type u_1} (E : V → ℝ) (s : Multiset V) : 0 ≤ leadingEnergy E s

theorem EpsilonEridani.QFT.Jets.le_leadingEnergy {V : Type u_1} {E : V → ℝ} {s : Multiset V} {p : V} (hp : p ∈ s) : E p ≤ leadingEnergy E s

@[simp]

theorem EpsilonEridani.QFT.Jets.leadingEnergy_add {V : Type u_1} (E : V → ℝ) (s t : Multiset V) : leadingEnergy E (s + t) = max (leadingEnergy E s) (leadingEnergy E t)

The leading-particle energy of the union of two final states is the larger of the two.

theorem EpsilonEridani.QFT.Jets.isInfraredSafe_leadingEnergy {V : Type u_1} [Zero V] [TopologicalSpace V] {E : V → ℝ} (hE : Filter.Tendsto E (nhds 0) (nhds 0)) : IsInfraredSafe (leadingEnergy E)

The leading-particle energy is infrared safe for an energy function that vanishes in the limit of vanishing momentum.

theorem EpsilonEridani.QFT.Jets.leadingEnergy_splitCollinear {V : Type u_1} [AddCommGroup V] [Module ℝ V] [DecidableEq V] (E : V →ₗ[ℝ] ℝ) {p : V} (hp : 0 ≤ E p) {z : ℝ} (s : Multiset V) : leadingEnergy (⇑E) (splitCollinear p z s) = max (max z (1 - z) * E p) (leadingEnergy (⇑E) (s.erase p))

The leading-particle energy after a collinear splitting of p in any final state s, for a nonnegative energy E p: the pair z • p, (1 - z) • p contributes max z (1 - z) * E p, and s.erase p is the rest of the state. When p ∈ s this replaces the contribution E p of p; for z ∈ [0, 1] the new contribution is at most E p.

theorem EpsilonEridani.QFT.Jets.not_isCollinearSafe_leadingEnergy {V : Type u_1} [AddCommGroup V] [Module ℝ V] {E : V →ₗ[ℝ] ℝ} (hE : E ≠ 0) : ¬IsCollinearSafe (leadingEnergy ⇑E)

The leading-particle energy of a nonzero linear energy functional is not collinear safe: splitting a single particle of positive energy into two halves halves the leading energy.