pith. machine review for the scientific record. sign in
def definition def or abbrev

rsKernelParams

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)

  54noncomputable def rsKernelParams (tau0 : ℝ) (h : 0 < tau0) : KernelParams := {

proof body

Definition body.

  55  alpha := alphaLock,
  56  C := phi ^ (-(3 : ℝ) / 2),
  57  tau0 := tau0,
  58  tau0_pos := h,
  59  alpha_nonneg := le_of_lt alphaLock_pos,
  60  C_nonneg := le_of_lt (Real.rpow_pos_of_pos phi_pos _)
  61}
  62
  63/-- Eight-tick aligned kernel parameters with c = 49/162. -/

used by (3)

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

depends on (15)

Lean names referenced from this declaration's body.