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

lambda_rec_over_ell_P

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)

 223theorem lambda_rec_over_ell_P :
 224    lambda_rec_SI / ell_P = 1 / sqrt Real.pi := by

proof body

Term-mode proof.

 225  unfold lambda_rec_SI ell_P
 226  have hpic3_pos : Real.pi * c^3 > 0 := mul_pos Real.pi_pos (pow_pos c_pos 3)
 227  have hc3_pos : c^3 > 0 := pow_pos c_pos 3
 228  have hhG_pos : hbar * G > 0 := mul_pos hbar_pos G_pos
 229  have hhG_nonneg : hbar * G ≥ 0 := le_of_lt hhG_pos
 230  have hpi_nonneg : (0 : ℝ) ≤ Real.pi := le_of_lt Real.pi_pos
 231  rw [sqrt_div hhG_nonneg, sqrt_div hhG_nonneg]
 232  have h_c3_eq : sqrt (Real.pi * c^3) = sqrt Real.pi * sqrt (c^3) :=
 233    sqrt_mul hpi_nonneg (c^3)
 234  rw [h_c3_eq]
 235  have h_sqrt_c3_ne : sqrt (c^3) ≠ 0 := (sqrt_pos.mpr hc3_pos).ne'
 236  have h_sqrt_pi_ne : sqrt Real.pi ≠ 0 := (sqrt_pos.mpr Real.pi_pos).ne'
 237  have h_sqrt_hG_ne : sqrt (hbar * G) ≠ 0 := (sqrt_pos.mpr hhG_pos).ne'
 238  field_simp [h_sqrt_c3_ne, h_sqrt_pi_ne, h_sqrt_hG_ne]
 239
 240/-- **Numerical Value**: 1/√π ≈ 0.564. -/

used by (1)

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

depends on (18)

Lean names referenced from this declaration's body.