← Mathematical handbook

theorem Verification.innerPower_cdf (g : ProbabilityTheory.Copula.BivariateGenerator) (p : ℝ) (hp : 1 ≤ p) (u v : ↑unitInterval) : (g.innerPower p hp).copula.cdf ![u, v] = g.copula.cdf ![ProbabilityTheory.Copula.unitPower u p⁻¹ ⋯, ProbabilityTheory.Copula.unitPower v p⁻¹ ⋯] ^ p

noncomputable def Verification.nelsen10Positive (θ : ℝ) (hθ : 0 < θ) (hθ1 : θ ≤ 1) : ProbabilityTheory.Copula 2

Nelsen 10 is the inner-power transform of AMH at parameter minus one.

Equations

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

noncomputable def Verification.nelsen10 (θ : ↑unitInterval) : ProbabilityTheory.Copula 2

Equations

• Verification.nelsen10 θ = if h : ↑θ = 0 then ProbabilityTheory.Copula.independence 2 else Verification.nelsen10Positive ↑θ ⋯ ⋯

theorem Verification.nelsen10_zero : nelsen10 0 = ProbabilityTheory.Copula.independence 2

theorem Verification.nelsen10_positive_cdf (θ : ℝ) (hθ : 0 < θ) (hθ1 : θ ≤ 1) (u v : ↑unitInterval) : (nelsen10Positive θ hθ hθ1).cdf ![u, v] = ↑u * ↑v / (1 + (1 - ↑u ^ θ) * (1 - ↑v ^ θ)) ^ θ⁻¹

theorem Verification.nelsen10_one : nelsen10 1 = ProbabilityTheory.Copula.amh (-1) ⋯ ⋯

theorem Verification.nelsen10_cdf (θ u v : ↑unitInterval) (hθ : 0 < ↑θ) : (nelsen10 θ).cdf ![u, v] = ↑u * ↑v / (1 + (1 - ↑u ^ ↑θ) * (1 - ↑v ^ ↑θ)) ^ (↑θ)⁻¹

theorem Verification.nelsen10_isNQD (θ : ↑unitInterval) : (nelsen10 θ).IsNQD

theorem Verification.nelsen10_isPQD_iff (θ : ↑unitInterval) : (nelsen10 θ).IsPQD ↔ θ = 0

theorem Verification.nelsen10_isCI_iff (θ : ↑unitInterval) : (nelsen10 θ).IsCI ↔ θ = 0

theorem Verification.nelsen10_density_tp2_iff (θ : ↑unitInterval) : (nelsen10 θ).HasMTP2Density ↔ θ = 0

theorem Verification.nelsen10_tails (θ : ↑unitInterval) : (nelsen10 θ).HasLowerTailDependence 0 ∧ (nelsen10 θ).HasUpperTailDependence 0