Documentation

Papers.AnsariRockel2024.Laplace

← Mathematical handbook
source
noncomputable def Verification.laplaceBivariate (r : ℝ) (hr : r ∈ Set.Icc (-1) 1) :
ProbabilityTheory.Copula 2
Equations
Instances For
    source
    theorem Verification.laplace_scale_pos :
    ∀ᵐ (t : ℝ) ∂↑(ProbabilityTheory.gammaProbability 1 1 ⋯ ⋯), 0 < √t
    source
    theorem Papers.AnsariRockel2024.laplace_isSklarCopula (r : ℝ) (hr : r ∈ Set.Icc (-1) 1) :
    ProbabilityTheory.Copula.IsSklarCopula (ProbabilityTheory.Copula.gaussianScaleMixtureLaw (Verification.bivariateCorrelation r) (ProbabilityTheory.gammaProbability 1 1 ⋯ ⋯) Real.sqrt) (Verification.laplaceBivariate r hr)
    source
    theorem Papers.AnsariRockel2024.laplace_one :
    Verification.laplaceBivariate 1 ⋯ = ProbabilityTheory.Copula.comonotonic 2
    source
    theorem Papers.AnsariRockel2024.laplace_negative_one :
    Verification.laplaceBivariate (-1) ⋯ = ProbabilityTheory.Copula.countermonotonic
    source
    theorem Papers.AnsariRockel2024.laplace_kendallTau (r : ℝ) (hr : r ∈ Set.Icc (-1) 1) :
    (Verification.laplaceBivariate r hr).kendallTau = 2 / Real.pi * Real.arcsin r
    source
    theorem Papers.AnsariRockel2024.laplace_lowerOrthant_monotone {r q : ℝ} (hr : r ∈ Set.Icc (-1) 1) (hq : q ∈ Set.Icc (-1) 1) (hrq : r ≤ q) :
    (Verification.laplaceBivariate r hr).LowerOrthantLE (Verification.laplaceBivariate q hq)
    source
    theorem Papers.AnsariRockel2024.laplace_lowerOrthant_iff {r q : ℝ} (hr : r ∈ Set.Icc (-1) 1) (hq : q ∈ Set.Icc (-1) 1) :
    (Verification.laplaceBivariate r hr).LowerOrthantLE (Verification.laplaceBivariate q hq) ↔ r ≤ q
    source
    theorem Papers.AnsariRockel2024.laplace_reflect_second {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) :
    Verification.laplaceBivariate (-r) ⋯ = (Verification.laplaceBivariate r hr).reflect {1}
    source
    theorem Papers.AnsariRockel2024.laplace_rho_neg {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) :
    (Verification.laplaceBivariate (-r) ⋯).spearmanRho = -(Verification.laplaceBivariate r hr).spearmanRho
    source
    theorem Papers.AnsariRockel2024.laplace_tau_neg {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) :
    (Verification.laplaceBivariate (-r) ⋯).kendallTau = -(Verification.laplaceBivariate r hr).kendallTau
    source
    theorem Papers.AnsariRockel2024.laplace_xi_neg {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) :
    (Verification.laplaceBivariate (-r) ⋯).chatterjeeXi = (Verification.laplaceBivariate r hr).chatterjeeXi
    source
    theorem Papers.AnsariRockel2024.laplace_transpose {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) :
    (Verification.laplaceBivariate r hr).transpose = Verification.laplaceBivariate r hr
    source
    theorem Papers.AnsariRockel2024.laplace_radiallySymmetric {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) :
    (Verification.laplaceBivariate r hr).IsRadiallySymmetric
    source
    theorem Papers.AnsariRockel2024.laplace_upperTail_iff_lowerTail {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (ℓ : ℝ) :
    (Verification.laplaceBivariate r hr).HasUpperTailDependence ℓ ↔ (Verification.laplaceBivariate r hr).HasLowerTailDependence ℓ