pith. machine review for the scientific record. sign in
theorem proved term proof

tree_level_partial_width_match

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 156theorem tree_level_partial_width_match
 157    (amp_RS amp_SM phaseSpace_RS phaseSpace_SM : ℝ)
 158    (hamp : amp_RS = amp_SM)
 159    (hps : phaseSpace_RS = phaseSpace_SM) :
 160    partialWidth amp_RS phaseSpace_RS = partialWidth amp_SM phaseSpace_SM :=

proof body

Term-mode proof.

 161  partialWidth_match amp_RS amp_SM phaseSpace_RS phaseSpace_SM hamp hps
 162
 163/-- If every channel's RS amplitude and phase space match the SM
 164    counterparts, then the total widths are equal channel by channel and
 165    therefore equal in sum. -/

depends on (9)

Lean names referenced from this declaration's body.