← 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 Verification.clampedMean (b a : ℝ) : ℝ

Equations

• Verification.clampedMean b a = ∫ (u : ↑unitInterval), Verification.unitClamp (a - b * ↑u)

theorem Verification.continuous_clampedMean (b : ℝ) : Continuous (clampedMean b)

theorem Verification.clampedMean_monotone (b : ℝ) : Monotone (clampedMean b)

theorem Verification.clampedMean_zero (b : ℝ) (hb : 0 ≤ b) : clampedMean b 0 = 0

theorem Verification.clampedMean_top (b : ℝ) (hb : 0 ≤ b) : clampedMean b (b + 1) = 1

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

noncomputable def Verification.bandIntercept (b : ℝ) (hb : 0 ≤ b) (v : ↑unitInterval) : ℝ

Equations

• Verification.bandIntercept b hb v = if v = 0 then 0 else if v = 1 then b + 1 else ⋯.choose

theorem Verification.bandIntercept_mean (b : ℝ) (hb : 0 ≤ b) (v : ↑unitInterval) : clampedMean b (bandIntercept b hb v) = ↑v

theorem Verification.bandIntercept_monotone (b : ℝ) (hb : 0 ≤ b) : Monotone (bandIntercept b hb)

noncomputable def Verification.bandKernel (b : ℝ) (hb : 0 ≤ b) (v u : ↑unitInterval) : ℝ

Equations

• Verification.bandKernel b hb v u = Verification.unitClamp (Verification.bandIntercept b hb v - b * ↑u)

theorem Verification.bandKernel_integrable (b : ℝ) (hb : 0 ≤ b) (v : ↑unitInterval) : MeasureTheory.Integrable (bandKernel b hb v) MeasureTheory.volume

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

theorem Verification.bandKernel_zero (b : ℝ) (hb : 0 ≤ b) (u : ↑unitInterval) : bandKernel b hb 0 u = 0

theorem Verification.bandKernel_one (b : ℝ) (hb : 0 ≤ b) (u : ↑unitInterval) : bandKernel b hb 1 u = 1

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

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

Equations

• Verification.diagonalBand b hb = Verification.copulaOfConditional (Verification.bandKernel b hb) ⋯ ⋯ ⋯ ⋯ ⋯

theorem Verification.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 Verification.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 Verification.diagonalBand_isSI (b : ℝ) (hb : 0 ≤ b) : (diagonalBand b hb).IsSI

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

theorem Verification.diagonalBand_support_eq_iff (C : ProbabilityTheory.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 Verification.diagonalBand_maximal_rho (C : ProbabilityTheory.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 Verification.diagonalBand_maximal_rho_eq_iff (C : ProbabilityTheory.Copula 2) (b : ℝ) (hb : 0 < b) (hx : C.chatterjeeXi = (diagonalBand b ⋯).chatterjeeXi) : C.spearmanRho = (diagonalBand b ⋯).spearmanRho ↔ C = diagonalBand b ⋯