← Mathematical handbook

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

Equations

• Verification.claytonPartial θ u v = u ^ (-θ - 1) * (u ^ (-θ) + v ^ (-θ) - 1) ^ (-1 / θ - 1)

theorem Verification.clayton_base_pos {θ u v : ℝ} (hθ : 0 < θ) (hu : u ∈ Set.Ioc 0 1) (hv : v ∈ Set.Ioc 0 1) : 0 < u ^ (-θ) + v ^ (-θ) - 1

theorem Verification.clayton_cdfSection_deriv {θ : ℝ} (hθ : 0 < θ) (v : ↑unitInterval) (hv : 0 < ↑v) (u : ℝ) (hu : u ∈ Set.Ioo 0 1) : HasDerivAt ((ProbabilityTheory.Copula.clayton 2 θ hθ).cdfSection v) (claytonPartial θ u ↑v) u

theorem Verification.clayton_conditionalCDF {θ : ℝ} (hθ : 0 < θ) (v : ↑unitInterval) (hv : 0 < ↑v) : (fun (u : ↑unitInterval) => (ProbabilityTheory.Copula.clayton 2 θ hθ).conditionalCDF u v) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => claytonPartial θ ↑u ↑v

theorem Verification.clayton_product_primitive {θ : ℝ} (hθ : 0 < θ) (v : ↑unitInterval) (hv : 0 < ↑v) (u : ℝ) (hu : u ∈ Set.Ioo 0 1) : HasDerivAt (fun (x : ℝ) => ↑v ^ (-θ - 1) / (θ + 2) * (ProbabilityTheory.Copula.clayton 2 θ hθ).cdfSection v x ^ (θ + 2)) (claytonPartial θ u ↑v * claytonPartial θ (↑v) u) u

theorem Verification.integral_claytonPartial_product {θ : ℝ} (hθ : 0 < θ) (v : ↑unitInterval) (hv : 0 < ↑v) : ∫ (u : ↑unitInterval), claytonPartial θ ↑u ↑v * claytonPartial θ ↑v ↑u = ↑v / (θ + 2)

theorem Verification.clayton_kendallTau {θ : ℝ} (hθ : 0 < θ) : (ProbabilityTheory.Copula.clayton 2 θ hθ).kendallTau = θ / (θ + 2)