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

inv_4pi_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)

 186lemma inv_4pi_lower : (0.0795 : ℝ) < 1 / (4 * Real.pi) := by

proof body

Tactic-mode proof.

 187  have h_pi_lt : Real.pi < (3.141593 : ℝ) := pi_lt_d6_local
 188  have h_pi_pos : (0 : ℝ) < Real.pi := Real.pi_pos
 189  have h_4pi_pos : (0 : ℝ) < 4 * Real.pi := by positivity
 190  -- 1/(4π) > 1/(4 * 3.141593) because π < 3.141593
 191  calc (0.0795 : ℝ) < 1 / (4 * 3.141593) := by norm_num
 192    _ < 1 / (4 * Real.pi) := by
 193        apply one_div_lt_one_div_of_lt h_4pi_pos
 194        apply mul_lt_mul_of_pos_left h_pi_lt
 195        norm_num
 196
 197/-- Upper bound: 1/(4π) < 1/(4 * 3.141592) ≈ 0.079578 < 0.0796 ✓ -/

used by (3)

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

depends on (3)

Lean names referenced from this declaration's body.