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

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

  93theorem lambda_at_rung_pos {lam : ℝ} (h : 0 < lam) (k : ℕ) :
  94    0 < lambda_at_rung lam k := by

proof body

Term-mode proof.

  95  unfold lambda_at_rung lambda_0
  96  exact mul_pos h (pow_pos Constants.phi_pos k)
  97
  98/-- The McMillan exponent at rung `k`: `1.04 (1 + λ_k) / (λ_k − μ*)`,
  99defined for `λ_k > μ*`. -/

used by (1)

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

depends on (10)

Lean names referenced from this declaration's body.