← Copula mathematical handbook

Elementary calculus for Spearman's rho of Frank's copula

Put w x = 1 - e^{-x} and, for θ > 0 and x, y ∈ (0, θ], L θ x y = -log (1 - w x * w y / w θ), so that θ * C_θ(u, v) = L θ (θ u) (θ v) for Frank's copula. This file collects the one-variable computations behind Copula.Archimedean.SpearmanRhoFrankCore:

• hasDerivAt_L: the derivative of θ ↦ L θ x y is f x y θ = e^{-θ} (1/w θ - 1/(w θ - w x w y));
• L_eq_min_add_integral: L θ x y = min x y + ∫_{max x y}^θ f x y s ds;
• K_eq: ∫₀^s ∫₀^s f x y s dy dx = s²/(e^s - 1) - ∫₀^s t/(e^t - 1) dt.

noncomputable def ProbabilityTheory.Copula.FrankRho.w (x : ℝ) : ℝ

w x = 1 - e^{-x}.

Equations

• ProbabilityTheory.Copula.FrankRho.w x = 1 - Real.exp (-x)

noncomputable def ProbabilityTheory.Copula.FrankRho.L (θ x y : ℝ) : ℝ

L θ x y = -log (1 - w x * w y / w θ), i.e. θ times Frank's cdf at (x/θ, y/θ).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ProbabilityTheory.Copula.FrankRho.f (x y s : ℝ) : ℝ

The θ-derivative of L θ x y.

Equations

• One or more equations did not get rendered due to their size.

theorem ProbabilityTheory.Copula.FrankRho.w_pos {x : ℝ} (hx : 0 < x) : 0 < w x

theorem ProbabilityTheory.Copula.FrankRho.w_nonneg {x : ℝ} (hx : 0 ≤ x) : 0 ≤ w x

theorem ProbabilityTheory.Copula.FrankRho.w_lt_one (x : ℝ) : w x < 1

theorem ProbabilityTheory.Copula.FrankRho.w_mono {x y : ℝ} (h : x ≤ y) : w x ≤ w y

theorem ProbabilityTheory.Copula.FrankRho.sub_pos' {θ x y : ℝ} (hθ : 0 < θ) (hxθ : x ≤ θ) (hy : 0 ≤ y) : 0 < w θ - w x * w y

theorem ProbabilityTheory.Copula.FrankRho.hasDerivAt_w (s : ℝ) : HasDerivAt w (Real.exp (-s)) s

theorem ProbabilityTheory.Copula.FrankRho.hasDerivAt_L {x y s : ℝ} (hs : 0 < s) (hxs : x ≤ s) (hy : 0 ≤ y) : HasDerivAt (fun (t : ℝ) => L t x y) (f x y s) s

theorem ProbabilityTheory.Copula.FrankRho.L_left {x y : ℝ} (hx : 0 < x) : L x x y = y

theorem ProbabilityTheory.Copula.FrankRho.L_right {x y : ℝ} (hy : 0 < y) : L y x y = x

theorem ProbabilityTheory.Copula.FrankRho.L_max {x y : ℝ} (hx : 0 < x) (hy : 0 < y) : L (max x y) x y = min x y

theorem ProbabilityTheory.Copula.FrankRho.continuousOn_f {x y a b : ℝ} (ha : 0 < a) (hxa : x ≤ a) (hy : 0 ≤ y) : ContinuousOn (f x y) (Set.Icc a b)

theorem ProbabilityTheory.Copula.FrankRho.L_eq_min_add_integral {θ x y : ℝ} (hx : 0 < x) (hy : 0 < y) (hxθ : x ≤ θ) (hyθ : y ≤ θ) : L θ x y = min x y + ∫ (s : ℝ) in max x y..θ, f x y s

theorem ProbabilityTheory.Copula.FrankRho.f_bounds {x y s : ℝ} (hs : 0 < s) (hx0 : 0 ≤ x) (hxs : x ≤ s) (hy0 : 0 ≤ y) (hys : y ≤ s) : -1 ≤ f x y s ∧ f x y s ≤ 0

theorem ProbabilityTheory.Copula.FrankRho.inner_integral {x s : ℝ} (hx : 0 ≤ x) (hxs : x < s) : ∫ (y : ℝ) in 0..s, 1 / (w s - w x * w y) = (s - x) / (Real.exp (-x) - Real.exp (-s))

The inner integral: ∫₀^s dy / (w s - w x w y) = (s - x)/(e^{-x} - e^{-s}) for 0 ≤ x < s.

theorem ProbabilityTheory.Copula.FrankRho.F_eq (s : ℝ) : (fun (z : ℝ) => z / (Real.exp (-(s - z)) - Real.exp (-s))) = fun (z : ℝ) => Real.exp s * (z / (Real.exp z - 1))

theorem ProbabilityTheory.Copula.FrankRho.J_integral {s : ℝ} : ∫ (x : ℝ) in 0..s, (s - x) / (Real.exp (-x) - Real.exp (-s)) = Real.exp s * ∫ (z : ℝ) in 0..s, z / (Real.exp z - 1)

Substitution z = s - x in the outer integral.

theorem ProbabilityTheory.Copula.FrankRho.intervalIntegrable_G {s : ℝ} (hs : 0 < s) : IntervalIntegrable (fun (x : ℝ) => (s - x) / (Real.exp (-x) - Real.exp (-s))) MeasureTheory.volume 0 s

theorem ProbabilityTheory.Copula.FrankRho.intervalIntegrable_inv {x s : ℝ} (hs : 0 < s) (hxs : x ≤ s) : IntervalIntegrable (fun (y : ℝ) => 1 / (w s - w x * w y)) MeasureTheory.volume 0 s

theorem ProbabilityTheory.Copula.FrankRho.K_eq {s : ℝ} (hs : 0 < s) : ∫ (x : ℝ) (y : ℝ) in 0..s, f x y s = s ^ 2 / (Real.exp s - 1) - ∫ (t : ℝ) in 0..s, t / (Real.exp t - 1)

The key computation: ∫₀^s ∫₀^s f x y s dy dx = s²/(e^s - 1) - ∫₀^s t/(e^t - 1) dt.