def KLN.a₁ : ℝ

(3.4). For the change in a₂, see Theorem 2.7 of FKS

noncomputable def KLN.a₂ : ℝ

def KLN.b₁ : ℝ

(3.5)

def KLN.b₂ : ℝ

def KLN.b₃ : ℝ

def KLN.b₄ : ℝ

noncomputable def KLN.m₀ : ℝ

(3.15)

noncomputable def KLN.ω₁ (σ T α : ℝ) : ℝ

(3.18)

noncomputable def KLN.C₁ (H₀ k : ℝ) : ℝ

(4.3)

noncomputable def KLN.C₂ (H₀ k : ℝ) : ℝ

(4.4)

noncomputable def KLN.a₃ : ℝ

(4.6)

noncomputable def KLN.C₃ (H₀ k : ℝ) : ℝ

(4.7)

noncomputable def KLN.C₄ (H₀ k : ℝ) : ℝ

(4.8)

noncomputable def KLN.C₅ (H₀ k δ : ℝ) : ℝ

(4.10)

noncomputable def KLN.C₆ (H₀ k δ : ℝ) : ℝ

(4.11)

noncomputable def KLN.I (α β A : ℝ) (n : ℕ) : ℝ

(4.15)

noncomputable def KLN.J (H₀ α β k T : ℝ) : ℝ

(4.17)

def KLN.β : ℝ

noncomputable def KLN.U (H₀ α k T : ℝ) : ℝ

(4.18)

noncomputable def KLN.K (H₀ α k δ T : ℝ) : ℝ

(4.20)

noncomputable def KLN.σ₂ (δ X : ℝ) : ℝ

noncomputable def KLN.V (H₀ α k δ T : ℝ) : ℝ

(4.19)

noncomputable def KLN.M (H₀ k δ : ℝ) : ℝ

(4.23)

noncomputable def KLN.b₅ (η : ℝ) : ℝ

(4.44)

noncomputable def KLN.b₆ (X η : ℝ) : ℝ

(4.45)

noncomputable def KLN.b₇ (k η H₀ : ℝ) : ℝ

(4.50)

noncomputable def KLN.b₈ (η H : ℝ) : ℝ

(4.51)

noncomputable def KLN.b₉ (H₀ k η H : ℝ) : ℝ

(4.59)

noncomputable def KLN.C₇ (H₀ k η H : ℝ) : ℝ

(4.56)

noncomputable def KLN.b₁₀ (H₀ k μ : ℝ) : ℝ

(4.66)

noncomputable def KLN.b₁₁ (X τ : ℝ) : ℝ

(4.68)

noncomputable def KLN.C₈ (H₀ k μ : ℝ) : ℝ

(4.63)

noncomputable def KLN.b₁₂ (H : ℝ) : ℝ

(4.75)

noncomputable def KLN.CC₁ (H₀ α d δ k H σ : ℝ) : ℝ

(4.72)

noncomputable def KLN.CC₂ (H₀ d η k H μ σ : ℝ) : ℝ

(4.73)