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

row_weak_ref_cross_section_band

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)

  54theorem row_weak_ref_cross_section_band :
  55    5.2e-38 < sigma_nu_weak_ref_cm2 ∧ sigma_nu_weak_ref_cm2 < 5.4e-38 := by

proof body

Tactic-mode proof.

  56  unfold sigma_nu_weak_ref_cm2 E_ref_GeV gev2_to_cm2
  57  have hgf := row_fermi_pred_bracket
  58  have hgf_pos : 0 < row_fermi_pred := by linarith [hgf.1]
  59  constructor
  60  · nlinarith [hgf.1, hgf_pos]
  61  · nlinarith [hgf.2, hgf_pos]
  62

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (5)

Lean names referenced from this declaration's body.