← Mathematical handbook

The corrected equation (19) and the journal's missing boundary term

noncomputable def Papers.AnsariRockel2026XiRho.sourceBandRoot (b : ℝ) (v : ↑unitInterval) : ℝ

The source dependence curves s_v and a_v.

Equations

• Papers.AnsariRockel2026XiRho.sourceBandRoot b v = Papers.AnsariRockel2026XiRho.sourceBandIntercept b v / b

noncomputable def Papers.AnsariRockel2026XiRho.sourceBandLower (b : ℝ) (v : ↑unitInterval) : ℝ

Equations

• Papers.AnsariRockel2026XiRho.sourceBandLower b v = (Papers.AnsariRockel2026XiRho.sourceBandIntercept b v - 1) / b

theorem Papers.AnsariRockel2026XiRho.sourceBand_cdf_positive_parts (b : ℝ) (hb : 0 < b) (u v : ↑unitInterval) : (sourceBand b hb).cdf ![u, v] = (sourceBandIntercept b v ^ 2 - max 0 (sourceBandIntercept b v - b * ↑u) ^ 2 - max 0 (sourceBandIntercept b v - 1) ^ 2 + max 0 (sourceBandIntercept b v - 1 - b * ↑u) ^ 2) / (2 * b)

A formula valid at every point, without case restrictions.

theorem Papers.AnsariRockel2026XiRho.sourceBand_cdf_piecewise (b : ℝ) (hb : 0 < b) (u v : ↑unitInterval) : (sourceBand b hb).cdf ![u, v] = if sourceBandLower b v < ↑u ∧ ↑u ≤ sourceBandRoot b v then ↑u - b / 2 * (↑u - sourceBandLower b v) ^ 2 + b / 2 * min (sourceBandLower b v) 0 ^ 2 else min ↑u ↑v

Equation (19) in arXiv v3, including the correction at the left boundary.

noncomputable def Papers.AnsariRockel2026XiRho.journalBandExpression (b : ℝ) (u v : ↑unitInterval) : ℝ

Literal journal equation (19), before arXiv v3 added the boundary term.

Equations

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

theorem Papers.AnsariRockel2026XiRho.journalBandExpression_negative : journalBandExpression 1 0 ⟨1 / 8, ⋯⟩ = -(1 / 8)

A negative boundary value certifies the omitted term is mathematically necessary.

theorem Papers.AnsariRockel2026XiRho.journalBandExpression_not_copula : ¬∃ (C : ProbabilityTheory.Copula 2), ∀ (u v : ↑unitInterval), C.cdf ![u, v] = journalBandExpression 1 u v

The literal uncorrected journal expression cannot be any copula CDF.