`kernel_correction_positive`

proved

show as: view math explainer →

module: IndisputableMonolith.Papers.DIF.CausalClosure
domain: Papers
line: 55 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Papers.DIF.CausalClosure on GitHub at line 55.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

formal source

  52
  53    This formalizes the Solar System tension identified in the paper:
  54    the power-law kernel does not have a built-in UV suppression mechanism. -/
  55theorem kernel_correction_positive (C α ratio : ℝ)
  56    (hC : 0 < C) (hα : 0 < α) (hratio : 0 < ratio) :
  57    0 < C * ratio ^ α := by
  58  exact mul_pos hC (Real.rpow_pos_of_pos hratio α)
  59
  60end
  61end CausalClosure
  62end DIF
  63end Papers
  64end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.