← Mathematical handbook

noncomputable def Verification.rafteryL (a u v : ℝ) : ℝ

Equations

• Verification.rafteryL a u v = u + u ^ a * (v ^ a - v ^ (1 - a)) / (2 * a - 1)

noncomputable def Verification.rafteryPL (a u v : ℝ) : ℝ

Equations

• Verification.rafteryPL a u v = 1 + a * u ^ (a - 1) * (v ^ a - v ^ (1 - a)) / (2 * a - 1)

noncomputable def Verification.rafteryPR (a u v : ℝ) : ℝ

Equations

• Verification.rafteryPR a u v = v ^ a * (a * u ^ (a - 1) + (a - 1) * u ^ (-a)) / (2 * a - 1)

noncomputable def Verification.rafteryF (a u v : ℝ) : ℝ

Equations

• Verification.rafteryF a u v = if u ≤ v then Verification.rafteryL a u v else Verification.rafteryL a v u

noncomputable def Verification.rafteryP (a u v : ℝ) : ℝ

Equations

• Verification.rafteryP a u v = if u ≤ v then Verification.rafteryPL a u v else Verification.rafteryPR a u v

noncomputable def Verification.rafteryDensity (a u v : ℝ) : ℝ

Equations

• Verification.rafteryDensity a u v = a / (2 * a - 1) * min u v ^ (a - 1) * (a * max u v ^ (a - 1) + (a - 1) * max u v ^ (-a))

theorem Verification.rafteryL_deriv_first {a u v : ℝ} (hu : 0 < u) : HasDerivAt (fun (x : ℝ) => rafteryL a x v) (rafteryPL a u v) u

theorem Verification.rafteryL_deriv_second {a u v : ℝ} (hv : 0 < v) : HasDerivAt (rafteryL a u) (rafteryPR a v u) v

theorem Verification.rafteryP_diagonal {a t : ℝ} (ha : 1 < a) (ht : 0 < t) : rafteryPL a t t = rafteryPR a t t

theorem Verification.rafteryPL_deriv_second {a u v : ℝ} (hv : 0 < v) : HasDerivAt (rafteryPL a u) (a / (2 * a - 1) * u ^ (a - 1) * (a * v ^ (a - 1) + (a - 1) * v ^ (-a))) v

theorem Verification.rafteryPR_deriv_second {a u v : ℝ} (hv : 0 < v) : HasDerivAt (rafteryPR a u) (a / (2 * a - 1) * v ^ (a - 1) * (a * u ^ (a - 1) + (a - 1) * u ^ (-a))) v

theorem Verification.rafteryF_deriv_first {a u v : ℝ} (ha : 1 < a) (hu : 0 < u) : HasDerivAt (fun (x : ℝ) => rafteryF a x v) (rafteryP a u v) u

theorem Verification.rafteryP_deriv_second {a u v : ℝ} (ha : 1 < a) (hu : 0 < u) (hv : 0 < v) : HasDerivAt (rafteryP a u) (rafteryDensity a u v) v

theorem Verification.rafteryP_continuous_first {a u v : ℝ} (ha : 1 < a) (hu : 0 < u) : ContinuousAt (fun (x : ℝ) => rafteryP a x v) u