← Copula mathematical handbook

The double integral behind Spearman's rho of Frank's copula

With L θ x y = -log (1 - w x w y / w θ) (see Copula.Archimedean.SpearmanRhoFrankCalculus) we prove ∫₀^θ ∫₀^θ L θ x y dy dx = θ³/3 - θ ∫₀^θ t/(e^t-1) dt + 2 ∫₀^θ t²/(e^t-1) dt (FrankRho.H_eq). The proof writes L θ x y = min x y + ∫_{max x y}^θ f x y s ds (L_eq_min_add_integral), exchanges the order of integration (Fubini over the cube (0, θ]³) and evaluates the resulting inner double integrals with K_eq.

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

The kernel f x y s restricted to max x y ≤ s.

Equations

• ProbabilityTheory.Copula.FrankRho.G x y s = if max x y ≤ s then ProbabilityTheory.Copula.FrankRho.f x y s else 0

theorem ProbabilityTheory.Copula.FrankRho.measurable_G : Measurable fun (p : ℝ × ℝ × ℝ) => G p.1 p.2.1 p.2.2

theorem ProbabilityTheory.Copula.FrankRho.abs_G_le {x y : ℝ} (hx : 0 < x) (hy : 0 < y) (s : ℝ) : |G x y s| ≤ 1

theorem ProbabilityTheory.Copula.FrankRho.G_nested (x y s : ℝ) : G x y s = if x ≤ s then if y ≤ s then f x y s else 0 else 0

theorem ProbabilityTheory.Copula.FrankRho.integral_ite_le {θ s : ℝ} (hs : s ≤ θ) (Q : ℝ → ℝ) : (∫ (x : ℝ) in Set.Ioc 0 θ, if x ≤ s then Q x else 0) = ∫ (x : ℝ) in Set.Ioc 0 s, Q x

Integral of a truncated function over (0, θ], upper truncation.

theorem ProbabilityTheory.Copula.FrankRho.integral_ite_ge {θ m : ℝ} (hm : 0 < m) (g : ℝ → ℝ) : (∫ (s : ℝ) in Set.Ioc 0 θ, if m ≤ s then g s else 0) = ∫ (s : ℝ) in Set.Ioc m θ, g s

Integral of a truncated function over (0, θ], lower truncation.

theorem ProbabilityTheory.Copula.FrankRho.integral_G_s {θ x y : ℝ} (hx : 0 < x) (hxθ : x ≤ θ) (hyθ : y ≤ θ) : ∫ (s : ℝ) in Set.Ioc 0 θ, G x y s = ∫ (s : ℝ) in max x y..θ, f x y s

theorem ProbabilityTheory.Copula.FrankRho.L_eq_min_add_G {θ x y : ℝ} (hx : 0 < x) (hy : 0 < y) (hxθ : x ≤ θ) (hyθ : y ≤ θ) : L θ x y = min x y + ∫ (s : ℝ) in Set.Ioc 0 θ, G x y s

theorem ProbabilityTheory.Copula.FrankRho.integrable_prod_of_bdd {θ : ℝ} {g : ℝ × ℝ → ℝ} (hg : Measurable g) {M : ℝ} (hb : ∀ p ∈ Set.Ioc 0 θ ×ˢ Set.Ioc 0 θ, |g p| ≤ M) : MeasureTheory.Integrable g ((MeasureTheory.volume.restrict (Set.Ioc 0 θ)).prod (MeasureTheory.volume.restrict (Set.Ioc 0 θ)))

Bounded measurable functions are integrable for the product of restricted Lebesgue measures.

theorem ProbabilityTheory.Copula.FrankRho.integral_min {θ x : ℝ} (hx : 0 ≤ x) (hxθ : x ≤ θ) : ∫ (y : ℝ) in Set.Ioc 0 θ, min x y = x * θ - x ^ 2 / 2

The mean of min x y over y ∈ (0, θ].

theorem ProbabilityTheory.Copula.FrankRho.integral_min_min {θ : ℝ} (hθ : 0 ≤ θ) : ∫ (x : ℝ) in Set.Ioc 0 θ, x * θ - x ^ 2 / 2 = θ ^ 3 / 3

noncomputable def ProbabilityTheory.Copula.FrankRho.h (θ x s : ℝ) : ℝ

The y-integral of the truncated kernel.

Equations

• ProbabilityTheory.Copula.FrankRho.h θ x s = ∫ (y : ℝ) in Set.Ioc 0 θ, ProbabilityTheory.Copula.FrankRho.G x y s

theorem ProbabilityTheory.Copula.FrankRho.integrable_G_ys {θ x : ℝ} (hx : 0 < x) : MeasureTheory.Integrable (fun (p : ℝ × ℝ) => G x p.1 p.2) ((MeasureTheory.volume.restrict (Set.Ioc 0 θ)).prod (MeasureTheory.volume.restrict (Set.Ioc 0 θ)))

theorem ProbabilityTheory.Copula.FrankRho.integrable_h {θ : ℝ} : MeasureTheory.Integrable (fun (p : ℝ × ℝ) => h θ p.1 p.2) ((MeasureTheory.volume.restrict (Set.Ioc 0 θ)).prod (MeasureTheory.volume.restrict (Set.Ioc 0 θ)))

theorem ProbabilityTheory.Copula.FrankRho.inner_swap {θ x : ℝ} (hx : 0 < x) : ∫ (y : ℝ) (s : ℝ) in Set.Ioc 0 θ, G x y s = ∫ (s : ℝ) in Set.Ioc 0 θ, h θ x s

theorem ProbabilityTheory.Copula.FrankRho.H_triple {θ : ℝ} (hθ : 0 < θ) : ∫ (x : ℝ) (y : ℝ) in Set.Ioc 0 θ, L θ x y = θ ^ 3 / 3 + ∫ (s : ℝ) (x : ℝ) in Set.Ioc 0 θ, h θ x s

theorem ProbabilityTheory.Copula.FrankRho.integral_h {θ s : ℝ} (hsθ : s ≤ θ) : ∫ (x : ℝ) in Set.Ioc 0 θ, h θ x s = ∫ (x : ℝ) (y : ℝ) in Set.Ioc 0 s, f x y s

noncomputable def ProbabilityTheory.Copula.FrankRho.S (θ : ℝ) : ℝ

S θ = ∫₀^θ t/(e^t - 1) dt = θ D₁(θ).

Equations

• ProbabilityTheory.Copula.FrankRho.S θ = ∫ (t : ℝ) in 0..θ, t / (Real.exp t - 1)

noncomputable def ProbabilityTheory.Copula.FrankRho.T (θ : ℝ) : ℝ

T θ = ∫₀^θ t²/(e^t - 1) dt = (θ²/2) D₂(θ).

Equations

• ProbabilityTheory.Copula.FrankRho.T θ = ∫ (t : ℝ) in 0..θ, t ^ 2 / (Real.exp t - 1)

theorem ProbabilityTheory.Copula.FrankRho.expm1_ne {s : ℝ} (hs : 0 < s) : Real.exp s - 1 ≠ 0

theorem ProbabilityTheory.Copula.FrankRho.hasDerivAt_S {s : ℝ} (hs : 0 < s) : HasDerivAt S (s / (Real.exp s - 1)) s

theorem ProbabilityTheory.Copula.FrankRho.hasDerivAt_T {s : ℝ} (hs : 0 < s) : HasDerivAt T (s ^ 2 / (Real.exp s - 1)) s

theorem ProbabilityTheory.Copula.FrankRho.continuousOn_S {θ : ℝ} (hθ : 0 < θ) : ContinuousOn S (Set.Icc 0 θ)

theorem ProbabilityTheory.Copula.FrankRho.continuousOn_T {θ : ℝ} (hθ : 0 < θ) : ContinuousOn T (Set.Icc 0 θ)

theorem ProbabilityTheory.Copula.FrankRho.integral_S {θ : ℝ} (hθ : 0 < θ) : ∫ (s : ℝ) in 0..θ, S s = θ * S θ - T θ

theorem ProbabilityTheory.Copula.FrankRho.H_eq {θ : ℝ} (hθ : 0 < θ) : ∫ (x : ℝ) (y : ℝ) in 0..θ, L θ x y = θ ^ 3 / 3 - θ * S θ + 2 * T θ