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

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

  68theorem exp_kernel_pos (z z0 : ℝ) :
  69    0 < kernel KernelFamily.exponential z z0 := by

proof body

Term-mode proof.

  70  unfold kernel
  71  exact Real.exp_pos _
  72
  73/-- The maximum BIT amplitude is `J(φ) = φ - 3/2 ≈ 0.118`. -/

depends on (9)

Lean names referenced from this declaration's body.