Documentation

Verification.Nelsen11

← Mathematical handbook

noncomputable def Verification.n11Square (t : ℝ) :

Equations

Verification.n11Square t = (2 - Real.exp t) ^ 2

Instances For

noncomputable def Verification.n11Psi (t : ℝ) :

Equations

Verification.n11Psi t = max 0 (2 - Real.exp t) ^ 2

Instances For

theorem Verification.n11Square_deriv (t : ℝ) :

HasDerivAt n11Square (-2 * Real.exp t * (2 - Real.exp t)) t

theorem Verification.n11Square_deriv2 (t : ℝ) :

HasDerivAt (fun (x : ℝ) => -2 * Real.exp x * (2 - Real.exp x)) (4 * Real.exp t * (Real.exp t - 1)) t

theorem Verification.n11Square_convex :

ConvexOn ℝ (Set.Ici 0) n11Square

theorem Verification.n11Psi_clip (t : ℝ) :

n11Psi t = n11Square (min t (Real.log 2))

theorem Verification.n11Psi_convex :

ConvexOn ℝ (Set.Ici 0) n11Psi

noncomputable def Verification.nelsen11BaseGenerator :

ProbabilityTheory.Copula.BivariateGenerator

Equations

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

Instances For

noncomputable def Verification.nelsen11Positive (θ : ℝ) (hθ : 0 < θ) (hθ1 : θ ≤ 1 / 2) :

ProbabilityTheory.Copula 2

Equations

Verification.nelsen11Positive θ hθ hθ1 = (Verification.nelsen11BaseGenerator.innerPower (2 * θ)⁻¹ ⋯).copula

Instances For

noncomputable def Verification.nelsen11 (θ : ℝ) (hθ0 : 0 ≤ θ) (hθ1 : θ ≤ 1 / 2) :

ProbabilityTheory.Copula 2

Equations

Verification.nelsen11 θ hθ0 hθ1 = if h : θ = 0 then ProbabilityTheory.Copula.independence 2 else Verification.nelsen11Positive θ ⋯ hθ1

Instances For

theorem Verification.nelsen11_zero :

nelsen11 0 ⋯ ⋯ = ProbabilityTheory.Copula.independence 2

theorem Verification.nelsen11Base_cdf (u v : ↑unitInterval) :

nelsen11BaseGenerator.copula.cdf ![u, v] = max 0 (2 - (2 - √↑u) * (2 - √↑v)) ^ 2

theorem Verification.nelsen11_positive_cdf (θ : ℝ) (hθ : 0 < θ) (hθ1 : θ ≤ 1 / 2) (u v : ↑unitInterval) :

(nelsen11Positive θ hθ hθ1).cdf ![u, v] = max 0 (↑u ^ θ * ↑v ^ θ - 2 * (1 - ↑u ^ θ) * (1 - ↑v ^ θ)) ^ θ⁻¹

theorem Verification.nelsen11_cdf (θ : ℝ) (hθ : 0 < θ) (hθ1 : θ ≤ 1 / 2) (u v : ↑unitInterval) :

(nelsen11 θ ⋯ hθ1).cdf ![u, v] = max 0 (↑u ^ θ * ↑v ^ θ - 2 * (1 - ↑u ^ θ) * (1 - ↑v ^ θ)) ^ θ⁻¹

theorem Verification.nelsen11_isNQD (θ : ℝ) (hθ0 : 0 ≤ θ) (hθ1 : θ ≤ 1 / 2) :

(nelsen11 θ hθ0 hθ1).IsNQD

theorem Verification.nelsen11_isPQD_iff (θ : ℝ) (hθ0 : 0 ≤ θ) (hθ1 : θ ≤ 1 / 2) :

(nelsen11 θ hθ0 hθ1).IsPQD ↔ θ = 0

theorem Verification.nelsen11_isCI_iff (θ : ℝ) (hθ0 : 0 ≤ θ) (hθ1 : θ ≤ 1 / 2) :

(nelsen11 θ hθ0 hθ1).IsCI ↔ θ = 0

theorem Verification.nelsen11_density_tp2_iff (θ : ℝ) (hθ0 : 0 ≤ θ) (hθ1 : θ ≤ 1 / 2) :

(nelsen11 θ hθ0 hθ1).HasMTP2Density ↔ θ = 0

theorem Verification.nelsen11_tails (θ : ℝ) (hθ0 : 0 ≤ θ) (hθ1 : θ ≤ 1 / 2) :

(nelsen11 θ hθ0 hθ1).HasLowerTailDependence 0 ∧ (nelsen11 θ hθ0 hθ1).HasUpperTailDependence 0