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

row_fermi_pred_lower

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)

  65theorem row_fermi_pred_lower :
  66    (1.16e-5 : ℝ) < row_fermi_pred := by

proof body

Tactic-mode proof.

  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

used by (1)

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.