← Mathematical handbook

Clayton's Archimedean generator and the BB1 family

noncomputable def ProbabilityTheory.Copula.claytonGenerator (θ : ℝ) (hθ : 0 < θ) : BivariateGenerator

Clayton's inverse generator (1+t)^(-1/θ), for θ > 0.

Equations

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

theorem ProbabilityTheory.Copula.claytonGenerator_copula (θ : ℝ) (hθ : 0 < θ) : (claytonGenerator θ hθ).copula = clayton 2 θ hθ

theorem ProbabilityTheory.Copula.hasArchimedeanGenerator_clayton (d : ℕ) (θ : ℝ) (hθ : 0 < θ) : (clayton d θ hθ).HasArchimedeanGenerator (claytonGenerator θ hθ)

theorem ProbabilityTheory.Copula.isArchimedean_clayton (d : ℕ) (θ : ℝ) (hθ : 0 < θ) : (clayton d θ hθ).IsArchimedean

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

BB1 (Clayton–Gumbel), with θ > 0 and outer-power parameter δ ≥ 1.

Equations

• ProbabilityTheory.Copula.bb1 θ hθ δ hδ = ((ProbabilityTheory.Copula.claytonGenerator θ hθ).outerPower δ hδ).copula

theorem ProbabilityTheory.Copula.isArchimedean_bb1 (θ : ℝ) (hθ : 0 < θ) (δ : ℝ) (hδ : 1 ≤ δ) : (bb1 θ hθ δ hδ).IsArchimedean

@[simp]

theorem ProbabilityTheory.Copula.bb1_one (θ : ℝ) (hθ : 0 < θ) : bb1 θ hθ 1 ⋯ = clayton 2 θ hθ

theorem ProbabilityTheory.Copula.cdf_bb1 (θ : ℝ) (hθ : 0 < θ) (δ : ℝ) (hδ : 1 ≤ δ) (u : Fin 2 → ↑unitInterval) (hu : ∀ (i : Fin 2), u i ≠ 0) : (bb1 θ hθ δ hδ).cdf u = (1 + ((↑(u 0) ^ (-θ) - 1) ^ δ + (↑(u 1) ^ (-θ) - 1) ^ δ) ^ δ⁻¹) ^ (-θ⁻¹)

theorem ProbabilityTheory.Copula.bb1_cdf_full (θ : ℝ) (hθ : 0 < θ) (δ : ℝ) (hδ : 1 ≤ δ) (u v : ↑unitInterval) : (bb1 θ hθ δ hδ).cdf ![u, v] = if u = 0 ∨ v = 0 then 0 else (1 + ((↑u ^ (-θ) - 1) ^ δ + (↑v ^ (-θ) - 1) ^ δ) ^ δ⁻¹) ^ (-θ⁻¹)

The BB1 CDF on the closed square for positive Clayton parameter and outer power at least one. The analytic formula is asserted only when both coordinates are positive.