theorem
proved
row_fermi_pred_eq
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Constants.FermiConstantScoreCard on GitHub at line 56.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
53/-- CODATA/PDG Fermi constant in GeV^-2. -/
54def row_fermi_codata : ℝ := 1.1663787e-5
55
56theorem row_fermi_pred_eq :
57 row_fermi_pred = 1 / (Real.sqrt 2 * vev_canonical ^ 2) := rfl
58
59private theorem sqrt2_pos : 0 < Real.sqrt 2 := Real.sqrt_pos.mpr (by norm_num)
60
61private theorem fermi_den_pos : 0 < Real.sqrt 2 * vev_canonical ^ 2 := by
62 have hv : 0 < vev_canonical ^ 2 := sq_pos_of_ne_zero (ne_of_gt vev_canonical_pos)
63 nlinarith [sqrt2_pos, hv]
64
65theorem row_fermi_pred_lower :
66 (1.16e-5 : ℝ) < row_fermi_pred := by
67 unfold row_fermi_pred
68 rw [lt_div_iff₀ fermi_den_pos]
69 have hs : Real.sqrt 2 < (1.4143 : ℝ) := sqrt2_lt_14143
70 have hden :
71 Real.sqrt 2 * vev_canonical ^ 2 < (1.4143 : ℝ) * (246 : ℝ) ^ 2 := by
72 have hv : vev_canonical = (246 : ℝ) := rfl
73 have hvpos : 0 < vev_canonical ^ 2 := sq_pos_of_ne_zero (ne_of_gt vev_canonical_pos)
74 rw [hv]
75 nlinarith
76 have hnum : (1.16e-5 : ℝ) * ((1.4143 : ℝ) * (246 : ℝ) ^ 2) < 1 := by
77 norm_num
78 nlinarith
79
80theorem row_fermi_pred_upper :
81 row_fermi_pred < (1.17e-5 : ℝ) := by
82 unfold row_fermi_pred
83 rw [div_lt_iff₀ fermi_den_pos]
84 have hs : (1.4142 : ℝ) < Real.sqrt 2 := sqrt2_gt_14142
85 have hden :
86 (1.4142 : ℝ) * (246 : ℝ) ^ 2 < Real.sqrt 2 * vev_canonical ^ 2 := by