← Mathematical handbook

noncomputable def Verification.n17Ratio (a u : ℝ) : ℝ

Equations

• Verification.n17Ratio a u = ((1 + u) ^ a - 1) / Verification.n17A a

theorem Verification.n17Ratio_pos {a u : ℝ} (ha : a ≠ 0) (hu : 0 < u) : 0 < n17Ratio a u

theorem Verification.n17Ratio_le_one {a u : ℝ} (ha : a ≠ 0) (hu : 0 < u) (hu1 : u ≤ 1) : n17Ratio a u ≤ 1

theorem Verification.n17Ratio_mono {a u v : ℝ} (ha : a ≠ 0) (hu : 0 < u) (huv : u ≤ v) : n17Ratio a u ≤ n17Ratio a v

noncomputable def Verification.n17Generator (a : ℝ) (ha : a ≠ 0) : ProbabilityTheory.Copula.BivariateGenerator

Equations

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

noncomputable def Verification.nelsen17 (θ : ℝ) (hθ : θ ≠ 0) : ProbabilityTheory.Copula 2

Equations

• Verification.nelsen17 θ hθ = (Verification.n17Generator (-θ) ⋯).copula

theorem Verification.nelsen17_cdf (θ : ℝ) (hθ : θ ≠ 0) (u v : ↑unitInterval) : (nelsen17 θ hθ).cdf ![u, v] = if u = 0 ∨ v = 0 then 0 else (1 + ((1 + ↑u) ^ (-θ) - 1) * ((1 + ↑v) ^ (-θ) - 1) / (2 ^ (-θ) - 1)) ^ (-θ⁻¹) - 1

theorem Verification.nelsen17_neg_one : nelsen17 (-1) ⋯ = ProbabilityTheory.Copula.independence 2

theorem Verification.nelsen17_cdf_full (θ : ℝ) (hθ : θ ≠ 0) (u v : ↑unitInterval) : (nelsen17 θ hθ).cdf ![u, v] = (1 + ((1 + ↑u) ^ (-θ) - 1) * ((1 + ↑v) ^ (-θ) - 1) / (2 ^ (-θ) - 1)) ^ (-θ⁻¹) - 1