← Mathematical handbook

noncomputable def Verification.claytonNegativePartial (θ u v : ℝ) : ℝ

Equations

• Verification.claytonNegativePartial θ u v = u ^ (-θ - 1) * max 0 (u ^ (-θ) + v ^ (-θ) - 1) ^ (-1 / θ - 1)

theorem Verification.claytonNegative_cdf_pos {θ : ℝ} (hmin : -1 ≤ θ) (hmax : θ < 0) (u v : ↑unitInterval) (hu : 0 < ↑u) (hv : 0 < ↑v) : (ProbabilityTheory.Copula.claytonNegative θ hmin hmax).cdf ![u, v] = max 0 (↑u ^ (-θ) + ↑v ^ (-θ) - 1) ^ (-1 / θ)

theorem Verification.claytonNegative_cdfSection_deriv {θ : ℝ} (hmin : -1 < θ) (hmax : θ < 0) (v : ↑unitInterval) (hv : 0 < ↑v) (u : ℝ) (hu : u ∈ Set.Ioo 0 1) : HasDerivAt ((ProbabilityTheory.Copula.claytonNegative θ ⋯ hmax).cdfSection v) (claytonNegativePartial θ u ↑v) u

theorem Verification.claytonNegative_conditionalCDF {θ : ℝ} (hmin : -1 < θ) (hmax : θ < 0) (v : ↑unitInterval) (hv : 0 < ↑v) : (fun (u : ↑unitInterval) => (ProbabilityTheory.Copula.claytonNegative θ ⋯ hmax).conditionalCDF u v) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => claytonNegativePartial θ ↑u ↑v

theorem Verification.claytonNegative_product_primitive {θ : ℝ} (hmin : -1 < θ) (hmax : θ < 0) (v : ↑unitInterval) (hv : 0 < ↑v) (u : ℝ) (hu : u ∈ Set.Ioo 0 1) : HasDerivAt (fun (x : ℝ) => ↑v ^ (-θ - 1) / (θ + 2) * (ProbabilityTheory.Copula.claytonNegative θ ⋯ hmax).cdfSection v x ^ (θ + 2)) (claytonNegativePartial θ u ↑v * claytonNegativePartial θ (↑v) u) u

theorem Verification.integral_claytonNegativePartial_product {θ : ℝ} (hmin : -1 < θ) (hmax : θ < 0) (v : ↑unitInterval) (hv : 0 < ↑v) : ∫ (u : ↑unitInterval), claytonNegativePartial θ ↑u ↑v * claytonNegativePartial θ ↑v ↑u = ↑v / (θ + 2)

theorem Verification.claytonNegative_kendallTau {θ : ℝ} (hmin : -1 < θ) (hmax : θ < 0) : (ProbabilityTheory.Copula.claytonNegative θ ⋯ hmax).kendallTau = θ / (θ + 2)