totalWidth

formal source

  76
  77/-- The total Higgs width is the sum of partial widths over all channels.
  78    We model "all channels" as a finite list of `(amp, phaseSpace)` pairs. -/
  79def totalWidth (channels : List (ℝ × ℝ)) : ℝ :=
  80  (channels.map (fun p => partialWidth p.fst p.snd)).sum
  81
  82/-- The total width is non-negative when each channel's phase space is. -/
  83theorem totalWidth_nonneg (channels : List (ℝ × ℝ))
  84    (hps : ∀ p ∈ channels, 0 ≤ p.snd) :
  85    0 ≤ totalWidth channels := by
  86  unfold totalWidth
  87  induction channels with
  88  | nil => simp
  89  | cons head tail ih =>
  90      simp only [List.map_cons, List.sum_cons]
  91      have hhead_mem : head ∈ head :: tail := by simp
  92      have hhead : 0 ≤ partialWidth head.fst head.snd :=
  93        partialWidth_nonneg head.fst head.snd (hps head hhead_mem)
  94      have htail : 0 ≤ (tail.map (fun p => partialWidth p.fst p.snd)).sum := by
  95        apply ih
  96        intro p hp
  97        exact hps p (by simp [hp])
  98      linarith
  99
 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 (ℝ × ℝ))