Documentation

Copula.Rank.Region.XiRho.Paper.DiagonalBandUnit

← Copula mathematical handbook

The unit-slope diagonal-band copula #

The b = 1 member of equations (19)--(22), including both response endpoints.

source
noncomputable def ProbabilityTheory.Copula.RankRegion.XiRho.unitBandIntercept (v : ↑unitInterval) :
ℝ
Equations
Instances For
    source
    noncomputable def ProbabilityTheory.Copula.RankRegion.XiRho.unitBandKernel (v u : ↑unitInterval) :
    ℝ
    Equations
    Instances For
      source
      theorem ProbabilityTheory.Copula.RankRegion.XiRho.sqrt_two_mem {v : ↑unitInterval} (hv : ↑v ≤ 1 / 2) :
      √(2 * ↑v) ∈ Set.Icc 0 1
      source
      theorem ProbabilityTheory.Copula.RankRegion.XiRho.unitBandIntercept_monotone :
      Monotone unitBandIntercept
      source
      theorem ProbabilityTheory.Copula.RankRegion.XiRho.unitBandKernel_monotone (u : ↑unitInterval) :
      Monotone fun (v : ↑unitInterval) => unitBandKernel v u
      source
      theorem ProbabilityTheory.Copula.RankRegion.XiRho.unitBandKernel_integrable (v : ↑unitInterval) :
      MeasureTheory.Integrable (unitBandKernel v) MeasureTheory.volume
      source
      theorem ProbabilityTheory.Copula.RankRegion.XiRho.unitBandKernel_lower (v u : ↑unitInterval) (hv : ↑v ≤ 1 / 2) :
      unitBandKernel v u = Common.ramp ⟨√(2 * ↑v), ⋯⟩ u
      source
      theorem ProbabilityTheory.Copula.RankRegion.XiRho.unitBandKernel_upper (v u : ↑unitInterval) (hv : 1 / 2 ≤ ↑v) :
      unitBandKernel v u = 1 - Common.ramp ⟨√(2 * (1 - ↑v)), ⋯⟩ (unitInterval.symm u)
      source
      theorem ProbabilityTheory.Copula.RankRegion.XiRho.unitBandKernel_zero (u : ↑unitInterval) :
      unitBandKernel 0 u = 0
      source
      theorem ProbabilityTheory.Copula.RankRegion.XiRho.unitBandKernel_one (u : ↑unitInterval) :
      unitBandKernel 1 u = 1
      source
      theorem ProbabilityTheory.Copula.RankRegion.XiRho.unitBandKernel_mean (v : ↑unitInterval) :
      ∫ (u : ↑unitInterval), unitBandKernel v u = ↑v
      source
      noncomputable def ProbabilityTheory.Copula.RankRegion.XiRho.unitDiagonalBand :
      Copula 2

      The actual copula C₁ from the article, constructed from its conditional law.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem ProbabilityTheory.Copula.RankRegion.XiRho.unitDiagonalBand_cdf (u v : ↑unitInterval) :
        unitDiagonalBand.cdf ![u, v] = ∫ (t : ↑unitInterval) in Set.Iic u, unitBandKernel v t
        source
        theorem ProbabilityTheory.Copula.RankRegion.XiRho.unitDiagonalBand_conditionalCDF (v : ↑unitInterval) :
        (fun (u : ↑unitInterval) => unitDiagonalBand.conditionalCDF u v) =ᵐ[MeasureTheory.volume] unitBandKernel v
        source
        theorem ProbabilityTheory.Copula.RankRegion.XiRho.unitDiagonalBand_derivative (v : ↑unitInterval) :
        (fun (u : ↑unitInterval) => deriv (unitDiagonalBand.cdfSection v) ↑u) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => Common.unitClamp (unitBandIntercept v - ↑u)
        source
        theorem ProbabilityTheory.Copula.RankRegion.XiRho.unitDiagonalBand_isSI :
        unitDiagonalBand.IsSI
        source
        theorem ProbabilityTheory.Copula.RankRegion.XiRho.unitDiagonalBand_support (C : Copula 2) :
        C.spearmanRho - C.chatterjeeXi ≤ unitDiagonalBand.spearmanRho - unitDiagonalBand.chatterjeeXi
        source
        theorem ProbabilityTheory.Copula.RankRegion.XiRho.unitDiagonalBand_support_eq_iff (C : Copula 2) :
        C.spearmanRho - C.chatterjeeXi = unitDiagonalBand.spearmanRho - unitDiagonalBand.chatterjeeXi ↔ C = unitDiagonalBand