← Copula mathematical handbook

Equations (19)--(22): the explicit diagonal-band family at every positive slope

noncomputable def ProbabilityTheory.Copula.RankRegion.XiRho.bandCut (b : ℝ) : ℝ

Equations

• ProbabilityTheory.Copula.RankRegion.XiRho.bandCut b = min (b / 2) (1 / (2 * b))

noncomputable def ProbabilityTheory.Copula.RankRegion.XiRho.sourceBandIntercept (b : ℝ) (v : ↑unitInterval) : ℝ

The source's bs(v), so the conditional section is clamp(a(v)-bu,0,1).

Equations

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

theorem ProbabilityTheory.Copula.RankRegion.XiRho.bandCut_small {b : ℝ} (hb : 0 < b) (hb1 : b ≤ 1) : bandCut b = b / 2

theorem ProbabilityTheory.Copula.RankRegion.XiRho.bandCut_large {b : ℝ} (hb : 0 < b) (hb1 : 1 ≤ b) : bandCut b = 1 / (2 * b)

theorem ProbabilityTheory.Copula.RankRegion.XiRho.bandCut_mem {b : ℝ} (hb : 0 < b) : bandCut b ∈ Set.Icc 0 (1 / 2)

theorem ProbabilityTheory.Copula.RankRegion.XiRho.sourceBandIntercept_mean {b : ℝ} (hb : 0 < b) (v : ↑unitInterval) : Common.clampedMean b (sourceBandIntercept b v) = ↑v

The complete source formula satisfies the uniform marginal equation.

theorem ProbabilityTheory.Copula.RankRegion.XiRho.sourceBandIntercept_monotone {b : ℝ} (hb : 0 < b) : Monotone (sourceBandIntercept b)

Ordering is forced by the exact marginal means, including the two transition points.

noncomputable def ProbabilityTheory.Copula.RankRegion.XiRho.sourceBand (b : ℝ) (hb : 0 < b) : Copula 2

The source C_b, constructed from its explicit conditional sections.

Equations

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

theorem ProbabilityTheory.Copula.RankRegion.XiRho.sourceBand_cdf (b : ℝ) (hb : 0 < b) (u v : ↑unitInterval) : (sourceBand b hb).cdf ![u, v] = ∫ (t : ↑unitInterval) in Set.Iic u, Common.unitClamp (sourceBandIntercept b v - b * ↑t)

Equation (19), as the integral of its explicit clamped section.

theorem ProbabilityTheory.Copula.RankRegion.XiRho.sourceBand_conditionalCDF (b : ℝ) (hb : 0 < b) (v : ↑unitInterval) : (fun (u : ↑unitInterval) => (sourceBand b hb).conditionalCDF u v) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => Common.unitClamp (sourceBandIntercept b v - b * ↑u)

theorem ProbabilityTheory.Copula.RankRegion.XiRho.sourceBand_derivative (b : ℝ) (hb : 0 < b) (v : ↑unitInterval) : (fun (u : ↑unitInterval) => deriv ((sourceBand b hb).cdfSection v) ↑u) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => Common.unitClamp (sourceBandIntercept b v - b * ↑u)

theorem ProbabilityTheory.Copula.RankRegion.XiRho.sourceBand_eq_normalizedBand (b : ℝ) (hb : 0 < b) : sourceBand b hb = normalizedBand b ⋯

The explicit source family is the previously proved normalization-defined optimizer.