← Copula mathematical handbook

Radical moments underlying the hyperbolic coefficient branch

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.hasDerivAt_arcosh_scaled {r x : ℝ} (hr : 0 < r) (hx : r < x) : HasDerivAt (fun (t : ℝ) => Real.arcosh (t / r)) (1 / √(x ^ 2 - r ^ 2)) x

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.hasDerivAt_sqrt_square_sub {r x : ℝ} (hr : 0 < r) (hx : r < x) : HasDerivAt (fun (t : ℝ) => √(t ^ 2 - r ^ 2)) (x / √(x ^ 2 - r ^ 2)) x

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.hasDerivAt_hyperbolic_primitive {r x : ℝ} (hr : 0 < r) (hx : r < x) : HasDerivAt (fun (t : ℝ) => (t * √(t ^ 2 - r ^ 2) - r ^ 2 * Real.arcosh (t / r)) / 2) (√(x ^ 2 - r ^ 2)) x

noncomputable def ProbabilityTheory.Copula.RankRegion.XiBlest.Support.radicalMoment (r : ℝ) (k : ℕ) : ℝ

Equations

• ProbabilityTheory.Copula.RankRegion.XiBlest.Support.radicalMoment r k = ∫ (x : ℝ) in r..1, x ^ (2 * k) * √(x ^ 2 - r ^ 2)

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.radicalMoment_zero (r : ℝ) (hr : r ∈ Set.Ioo 0 1) : radicalMoment r 0 = (√(1 - r ^ 2) - r ^ 2 * Real.arcosh (1 / r)) / 2

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.hasDerivAt_radical_recurrence {r x : ℝ} (hr : 0 < r) (hx : r < x) (n : ℕ) : HasDerivAt (fun (t : ℝ) => t ^ (2 * n + 1) * √(t ^ 2 - r ^ 2) ^ 3) ((2 * ↑n + 4) * x ^ (2 * (n + 1)) * √(x ^ 2 - r ^ 2) - (2 * ↑n + 1) * r ^ 2 * x ^ (2 * n) * √(x ^ 2 - r ^ 2)) x

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.radicalMoment_recurrence (r : ℝ) (hr : r ∈ Set.Ioo 0 1) (n : ℕ) : (2 * ↑n + 4) * radicalMoment r (n + 1) - (2 * ↑n + 1) * r ^ 2 * radicalMoment r n = √(1 - r ^ 2) ^ 3