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

alpha_match_pos

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)

  64theorem alpha_match_pos (alpha_above : ℝ)
  65    (h_pos : 0 < alpha_above) (h_lt : alpha_above < 1) :
  66    0 < alpha_match alpha_above := by

proof body

Tactic-mode proof.

  67  unfold alpha_match
  68  apply mul_pos h_pos
  69  have h_a_over_pi_pos : 0 < alpha_above / Real.pi :=
  70    div_pos h_pos Real.pi_pos
  71  have h_a_over_pi_sq_pos : 0 < (alpha_above / Real.pi) ^ 2 :=
  72    pow_pos h_a_over_pi_pos 2
  73  have h_c_pos : 0 < c_2_alpha := by unfold c_2_alpha; norm_num
  74  positivity
  75

used by (1)

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

depends on (2)

Lean names referenced from this declaration's body.