partialWidth_match

formal source

  66
  67/-- Two partial widths matched when both amplitudes and phase-space factors
  68    agree. -/
  69theorem partialWidth_match
  70    (amp1 amp2 phaseSpace1 phaseSpace2 : ℝ)
  71    (hamp : amp1 = amp2) (hps : phaseSpace1 = phaseSpace2) :
  72    partialWidth amp1 phaseSpace1 = partialWidth amp2 phaseSpace2 := by
  73  rw [hamp, hps]
  74
  75/-! ## §2. Total Width and Branching Ratios -/
  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