partialWidth_nonneg

formal source

  58def partialWidth (amp phaseSpace : ℝ) : ℝ := phaseSpace * amp ^ 2
  59
  60/-- Partial widths are non-negative for non-negative phase space. -/
  61theorem partialWidth_nonneg (amp phaseSpace : ℝ) (hps : 0 ≤ phaseSpace) :
  62    0 ≤ partialWidth amp phaseSpace := by
  63  unfold partialWidth
  64  have hamp2 : 0 ≤ amp ^ 2 := sq_nonneg _
  65  exact mul_nonneg hps hamp2
  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