lemma proved tactic proof

`inv_4pi_lower_v2`

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

formal statement (Lean)

 863lemma inv_4pi_lower_v2 : (0.07957 : ℝ) < 1 / (4 * Real.pi) := by

proof body

Tactic-mode proof.

 864  have h_pi_lt : Real.pi < (3.141593 : ℝ) := pi_lt_d6_local
 865  have h_4pi_pos : (0 : ℝ) < 4 * Real.pi := by positivity
 866  calc (0.07957 : ℝ) < 1 / (4 * 3.141593) := by norm_num
 867    _ < 1 / (4 * Real.pi) := by
 868        apply one_div_lt_one_div_of_lt h_4pi_pos
 869        apply mul_lt_mul_of_pos_left h_pi_lt; norm_num
 870

used by (1)

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

step_e_mu_bounds_v2 in IndisputableMonolith.Physics.LeptonGenerations.Necessity decl_use

depends on (2)

Lean names referenced from this declaration's body.

pi_lt_d6_local in IndisputableMonolith.Physics.LeptonGenerations.Necessity decl_use
pi_lt_d6_local in IndisputableMonolith.RRF.Physics.LeptonGenerations.Necessity decl_use