← Mathematical handbook

Equations (16)-(17): the two source branches in their original distance variables

noncomputable def Papers.AnsariRockelSteinmassl2026RhoGamma.sourceMean (N : ℕ) (ell delta : ℝ) : ℝ

Equation (17), first distance moment.

Equations

• Papers.AnsariRockelSteinmassl2026RhoGamma.sourceMean N ell delta = ell + ↑N * (↑N + 1) * delta * |delta|

noncomputable def Papers.AnsariRockelSteinmassl2026RhoGamma.sourceSquare (N : ℕ) (ell delta : ℝ) : ℝ

Equation (17), second distance moment.

Equations

• Papers.AnsariRockelSteinmassl2026RhoGamma.sourceSquare N ell delta = ell * (2 * Papers.AnsariRockelSteinmassl2026RhoGamma.sourceMean N ell delta - ell) + 2 / 3 * ↑N * (↑N + 1) * |delta| ^ 3

noncomputable def Papers.AnsariRockelSteinmassl2026RhoGamma.sourceOffset (N : ℕ) (ell delta : ℝ) : ℝ

Equation (17), endpoint value of the auxiliary potential.

Equations

• Papers.AnsariRockelSteinmassl2026RhoGamma.sourceOffset N ell delta = (ell ^ 2 - (2 * ell + delta) * ell - ell * (1 - 2 * ↑N * (↑N + 1) * |delta|) * delta) / 2

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.right_source_data (S : ProbabilityTheory.Copula.RankRegion.RhoFootrule.RightData) : have ell := 1 / (2 * (↑S.N + 1)); ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperSpline.period (↑S.N) S.v S.w = 2 * ell + S.v ∧ ∫ (x : Fin 2 → ↑unitInterval), |↑(x 0) - ↑(x 1)| ∂S.copula.toMeasure = sourceMean S.N ell S.v ∧ ∫ (x : Fin 2 → ↑unitInterval), (↑(x 0) - ↑(x 1)) ^ 2 ∂S.copula.toMeasure = sourceSquare S.N ell S.v ∧ ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperSpline.offset (↑S.N) S.v S.w = sourceOffset S.N ell S.v

On the right branch, the source delta is the library's nonnegative v.

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.left_source_data (S : ProbabilityTheory.Copula.RankRegion.RhoFootrule.LeftData) : have ell := 1 / (2 * ↑S.N); ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperSpline.period (↑S.N) S.v S.w = 2 * ell - S.v ∧ ∫ (x : Fin 2 → ↑unitInterval), |↑(x 0) - ↑(x 1)| ∂S.copula.toMeasure = sourceMean S.N ell (-S.v) ∧ ∫ (x : Fin 2 → ↑unitInterval), (↑(x 0) - ↑(x 1)) ^ 2 ∂S.copula.toMeasure = sourceSquare S.N ell (-S.v) ∧ ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperSpline.offset (↑S.N) S.v S.w + S.v * S.w = sourceOffset S.N ell (-S.v)

On the left branch, the source delta is minus the library's v.

noncomputable def Papers.AnsariRockelSteinmassl2026RhoGamma.sourceRight (N : ℕ) (hN : 0 < N) (s : ℝ) (hlo : 1 / (↑N + 1) ≤ s) (hhi : s ≤ 1 / (2 * ↑N) + 1 / (2 * (↑N + 1))) : ProbabilityTheory.Copula.RankRegion.RhoFootrule.RightData

Construct the source's right branch at its auxiliary multiplier s.

Equations

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

noncomputable def Papers.AnsariRockelSteinmassl2026RhoGamma.sourceLeft (N : ℕ) (hN : 0 < N) (s : ℝ) (hlo : 1 / (2 * ↑N) + 1 / (2 * (↑N + 1)) ≤ s) (hhi : s ≤ 1 / ↑N) : ProbabilityTheory.Copula.RankRegion.RhoFootrule.LeftData

Construct the source's left branch at its auxiliary multiplier s.

Equations

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