theorem proved term proof

`kernel_correction_positive`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  55theorem kernel_correction_positive (C α ratio : ℝ)
  56    (hC : 0 < C) (hα : 0 < α) (hratio : 0 < ratio) :
  57    0 < C * ratio ^ α := by

Term-mode proof.

  58  exact mul_pos hC (Real.rpow_pos_of_pos hratio α)
  59
  60end
  61end CausalClosure
  62end DIF
  63end Papers
  64end IndisputableMonolith