branchingRatio

formal source

 100/-- The branching ratio of a single channel is its partial width over the
 101    total width.  Defined to be zero if the total width is zero (a
 102    degenerate, unphysical case). -/
 103def branchingRatio (amp phaseSpace : ℝ) (channels : List (ℝ × ℝ)) : ℝ :=
 104  if totalWidth channels = 0 then 0
 105  else partialWidth amp phaseSpace / totalWidth channels
 106
 107/-- Branching ratios are non-negative when phase spaces are. -/
 108theorem branchingRatio_nonneg
 109    (amp phaseSpace : ℝ) (channels : List (ℝ × ℝ))
 110    (hps_amp : 0 ≤ phaseSpace)
 111    (hps : ∀ p ∈ channels, 0 ≤ p.snd) :
 112    0 ≤ branchingRatio amp phaseSpace channels := by
 113  unfold branchingRatio
 114  by_cases h : totalWidth channels = 0
 115  · simp [h]
 116  · simp [h]
 117    have hpw : 0 ≤ partialWidth amp phaseSpace := partialWidth_nonneg amp phaseSpace hps_amp
 118    have htot : 0 ≤ totalWidth channels := totalWidth_nonneg channels hps
 119    exact div_nonneg hpw htot
 120
 121/-! ## §3. Signal-Strength Modifier -/
 122
 123/-- The signal strength `μ_i = (σ · BR)_RS / (σ · BR)_SM` for a channel.
 124
 125    By construction, `μ = 1` when both the cross-section and the branching
 126    ratio match the SM. -/
 127def signalStrength (sigma_BR_RS sigma_BR_SM : ℝ) : ℝ :=
 128  if sigma_BR_SM = 0 then 0 else sigma_BR_RS / sigma_BR_SM
 129
 130/-- The signal-strength modifier equals 1 when both numerator and
 131    denominator agree. -/
 132theorem signalStrength_one_of_match
 133    (x : ℝ) (hx : x ≠ 0) :