← Copula mathematical handbook

Polynomial inner integrals on a square-gap tail

noncomputable def ProbabilityTheory.Copula.RankRegion.XiBlest.Support.innerSquareMoment (x s : ℝ) (k : ℕ) : ℝ

Equations

• ProbabilityTheory.Copula.RankRegion.XiBlest.Support.innerSquareMoment x s k = ∫ (y : ℝ) in 0..s, (x ^ 2 - y ^ 2) ^ k

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.innerSquareMoment_zero (x s : ℝ) : innerSquareMoment x s 0 = s

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.innerSquareMoment_one (x s : ℝ) : innerSquareMoment x s 1 = x ^ 2 * s - s ^ 3 / 3

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.innerSquareMoment_two (x s : ℝ) : innerSquareMoment x s 2 = x ^ 4 * s - 2 / 3 * x ^ 2 * s ^ 3 + s ^ 5 / 5

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.innerSquareMoment_three (x s : ℝ) : innerSquareMoment x s 3 = x ^ 6 * s - x ^ 4 * s ^ 3 + 3 / 5 * x ^ 2 * s ^ 5 - s ^ 7 / 7

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.innerSquareMoment_radical (r x : ℝ) (h : 0 ≤ x ^ 2 - r ^ 2) : innerSquareMoment x (√(x ^ 2 - r ^ 2)) 0 = √(x ^ 2 - r ^ 2) ∧ innerSquareMoment x (√(x ^ 2 - r ^ 2)) 1 = (2 * x ^ 2 + r ^ 2) * √(x ^ 2 - r ^ 2) / 3 ∧ innerSquareMoment x (√(x ^ 2 - r ^ 2)) 2 = (8 * x ^ 4 + 4 * r ^ 2 * x ^ 2 + 3 * r ^ 4) * √(x ^ 2 - r ^ 2) / 15 ∧ innerSquareMoment x (√(x ^ 2 - r ^ 2)) 3 = (16 * x ^ 6 + 8 * r ^ 2 * x ^ 4 + 6 * r ^ 4 * x ^ 2 + 5 * r ^ 6) * √(x ^ 2 - r ^ 2) / 35