← Copula mathematical handbook

Diagonal-band copulas at every nonnegative slope

The intercept is chosen by the uniform marginal constraint. Its existence uses the intermediate value theorem, and the ordering of its means proves monotonicity in the response threshold. No asserted copula or optimizer is passed as a hypothesis.

noncomputable def ProbabilityTheory.Copula.RankRegion.Common.clampedMean (b a : ℝ) : ℝ

Equations

• ProbabilityTheory.Copula.RankRegion.Common.clampedMean b a = ∫ (u : ↑unitInterval), ProbabilityTheory.Copula.RankRegion.Common.unitClamp (a - b * ↑u)

theorem ProbabilityTheory.Copula.RankRegion.Common.continuous_clampedMean (b : ℝ) : Continuous (clampedMean b)

theorem ProbabilityTheory.Copula.RankRegion.Common.clampedMean_monotone (b : ℝ) : Monotone (clampedMean b)

theorem ProbabilityTheory.Copula.RankRegion.Common.clampedMean_zero (b : ℝ) (hb : 0 ≤ b) : clampedMean b 0 = 0

theorem ProbabilityTheory.Copula.RankRegion.Common.clampedMean_top (b : ℝ) (hb : 0 ≤ b) : clampedMean b (b + 1) = 1

theorem ProbabilityTheory.Copula.RankRegion.Common.exists_clamped_intercept (b : ℝ) (hb : 0 ≤ b) (v : ↑unitInterval) : ∃ a ∈ Set.Icc 0 (b + 1), clampedMean b a = ↑v

noncomputable def ProbabilityTheory.Copula.RankRegion.Common.bandIntercept (b : ℝ) (hb : 0 ≤ b) (v : ↑unitInterval) : ℝ

Equations

• ProbabilityTheory.Copula.RankRegion.Common.bandIntercept b hb v = if v = 0 then 0 else if v = 1 then b + 1 else ⋯.choose

theorem ProbabilityTheory.Copula.RankRegion.Common.bandIntercept_mean (b : ℝ) (hb : 0 ≤ b) (v : ↑unitInterval) : clampedMean b (bandIntercept b hb v) = ↑v

theorem ProbabilityTheory.Copula.RankRegion.Common.bandIntercept_monotone (b : ℝ) (hb : 0 ≤ b) : Monotone (bandIntercept b hb)

noncomputable def ProbabilityTheory.Copula.RankRegion.Common.bandKernel (b : ℝ) (hb : 0 ≤ b) (v u : ↑unitInterval) : ℝ

Equations

• ProbabilityTheory.Copula.RankRegion.Common.bandKernel b hb v u = ProbabilityTheory.Copula.RankRegion.Common.unitClamp (ProbabilityTheory.Copula.RankRegion.Common.bandIntercept b hb v - b * ↑u)

theorem ProbabilityTheory.Copula.RankRegion.Common.bandKernel_integrable (b : ℝ) (hb : 0 ≤ b) (v : ↑unitInterval) : MeasureTheory.Integrable (bandKernel b hb v) MeasureTheory.volume

theorem ProbabilityTheory.Copula.RankRegion.Common.bandKernel_monotone (b : ℝ) (hb : 0 ≤ b) (u : ↑unitInterval) : Monotone fun (v : ↑unitInterval) => bandKernel b hb v u

theorem ProbabilityTheory.Copula.RankRegion.Common.bandKernel_zero (b : ℝ) (hb : 0 ≤ b) (u : ↑unitInterval) : bandKernel b hb 0 u = 0

theorem ProbabilityTheory.Copula.RankRegion.Common.bandKernel_one (b : ℝ) (hb : 0 ≤ b) (u : ↑unitInterval) : bandKernel b hb 1 u = 1

noncomputable def ProbabilityTheory.Copula.RankRegion.Common.diagonalBand (b : ℝ) (hb : 0 ≤ b) : Copula 2

Actual diagonal-band copula at slope b; normalization is solved internally.

Equations

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

theorem ProbabilityTheory.Copula.RankRegion.Common.diagonalBand_cdf (b : ℝ) (hb : 0 ≤ b) (u v : ↑unitInterval) : (diagonalBand b hb).cdf ![u, v] = ∫ (t : ↑unitInterval) in Set.Iic u, unitClamp (bandIntercept b hb v - b * ↑t)

theorem ProbabilityTheory.Copula.RankRegion.Common.diagonalBand_conditionalCDF (b : ℝ) (hb : 0 ≤ b) (v : ↑unitInterval) : (fun (u : ↑unitInterval) => (diagonalBand b hb).conditionalCDF u v) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => unitClamp (bandIntercept b hb v - b * ↑u)

theorem ProbabilityTheory.Copula.RankRegion.Common.diagonalBand_isSI (b : ℝ) (hb : 0 ≤ b) : (diagonalBand b hb).IsSI

theorem ProbabilityTheory.Copula.RankRegion.Common.diagonalBand_support (C : Copula 2) (b : ℝ) (hb : 0 ≤ b) : b * C.spearmanRho - C.chatterjeeXi ≤ b * (diagonalBand b hb).spearmanRho - (diagonalBand b hb).chatterjeeXi

theorem ProbabilityTheory.Copula.RankRegion.Common.diagonalBand_support_eq_iff (C : Copula 2) (b : ℝ) (hb : 0 ≤ b) : b * C.spearmanRho - C.chatterjeeXi = b * (diagonalBand b hb).spearmanRho - (diagonalBand b hb).chatterjeeXi ↔ C = diagonalBand b hb

theorem ProbabilityTheory.Copula.RankRegion.Common.diagonalBand_maximal_rho (C : Copula 2) (b : ℝ) (hb : 0 < b) (hx : C.chatterjeeXi ≤ (diagonalBand b ⋯).chatterjeeXi) : C.spearmanRho ≤ (diagonalBand b ⋯).spearmanRho

Every constructed positive-slope band is the unique maximizer of rho at its xi.

theorem ProbabilityTheory.Copula.RankRegion.Common.diagonalBand_maximal_rho_eq_iff (C : Copula 2) (b : ℝ) (hb : 0 < b) (hx : C.chatterjeeXi = (diagonalBand b ⋯).chatterjeeXi) : C.spearmanRho = (diagonalBand b ⋯).spearmanRho ↔ C = diagonalBand b ⋯