← Mathematical handbook

The revised manuscript's positive-parameter MTP2 assertion

theorem Papers.Rockel2026XiBlest.extremal_standardized_density (b : ℝ) (hb : 0 ≤ b) : (extremalCopula b hb).toMeasure = MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑unitInterval) => ENNReal.ofReal ((Verification.quadraticRawBand b hb).standardizedDensity (x 0, x 1))

A concrete Lebesgue density for the extremal copula, obtained by standardizing the second marginal of the increasing band law. The revision's formula in terms of the derivative of q remains a separate identification obligation.

theorem Papers.Rockel2026XiBlest.extremal_hasMTP2Density (b : ℝ) (hb : 0 ≤ b) : (extremalCopula b hb).HasMTP2Density

Every finite nonnegative member has an actual Lebesgue MTP2 density.

theorem Papers.Rockel2026XiBlest.signed_extremal_hasMTP2Density (b : ℝ) (hb : 0 < b) : (signedExtremalCopula b).HasMTP2Density

Positive signed parameters give the same density-certified copulas.

noncomputable def Papers.Rockel2026XiBlest.extremalLowerSwitch (b : ℝ) (hb : 0 < b) (v : ↑unitInterval) : ℝ

The two switch points in the revised manuscript, expressed using the unclamped band endpoints.

Equations

• Papers.Rockel2026XiBlest.extremalLowerSwitch b hb v = 1 - Verification.quadraticUpper b (Papers.Rockel2026XiBlest.extremalQ b hb v)

noncomputable def Papers.Rockel2026XiBlest.extremalUpperSwitch (b : ℝ) (hb : 0 < b) (v : ↑unitInterval) : ℝ

Equations

• Papers.Rockel2026XiBlest.extremalUpperSwitch b hb v = 1 - Verification.quadraticLower (Papers.Rockel2026XiBlest.extremalQ b hb v)

theorem Papers.Rockel2026XiBlest.extremalLowerSwitch_source (b : ℝ) (hb : 0 < b) (v : ↑unitInterval) : extremalLowerSwitch b hb v = max 0 (1 - √(extremalQ b hb v + 1 / b))

theorem Papers.Rockel2026XiBlest.extremalUpperSwitch_source (b : ℝ) (hb : 0 < b) (v : ↑unitInterval) : extremalUpperSwitch b hb v = if 0 < extremalQ b hb v then 1 - √(extremalQ b hb v) else 1

theorem Papers.Rockel2026XiBlest.extremal_switch_support (b : ℝ) (hb : 0 < b) (v u : ↑unitInterval) : extremalLowerSwitch b hb v < ↑u ∧ ↑u < extremalUpperSwitch b hb v ↔ Verification.quadraticLower (extremalQ b hb v) < 1 - ↑u ∧ 1 - ↑u < Verification.quadraticUpper b (extremalQ b hb v)

The manuscript's open support band is exactly the reflection of the active interval in the clamped-square normalization integral.

theorem Papers.Rockel2026XiBlest.extremal_raw_quantile_parameter (b : ℝ) (hb : 0 < b) (v : ↑unitInterval) : (b + 1) * ↑(ProbabilityTheory.unitQuantile (Verification.quadraticRawBand b ⋯).marginal v) - b = -b * extremalQ b hb v

The quantile used by the already verified standardized-band density has exactly the manuscript's normalization parameter.

theorem Papers.Rockel2026XiBlest.extremal_raw_band_condition (b : ℝ) (hb : 0 < b) (v u : ↑unitInterval) : have B := Verification.quadraticRawBand b ⋯; have t := ProbabilityTheory.unitQuantile B.marginal v; B.lower u ≤ ↑t ∧ ↑t ≤ B.lower u + B.width ↔ 0 ≤ b * ((1 - ↑u) ^ 2 - extremalQ b hb v) ∧ b * ((1 - ↑u) ^ 2 - extremalQ b hb v) ≤ 1

The raw band's closed-strip condition is the clamped quadratic's active interval, before switching to the manuscript's open-band version.

theorem Papers.Rockel2026XiBlest.extremal_raw_columnDensity (b : ℝ) (hb : 0 < b) (v : ↑unitInterval) : have B := Verification.quadraticRawBand b ⋯; B.columnDensity (ProbabilityTheory.unitQuantile B.marginal v) = (b + 1) * (Verification.quadraticUpper b (extremalQ b hb v) - Verification.quadraticLower (extremalQ b hb v))

At the marginal quantile for v, the raw band's column density is (b+1) times the length of the manuscript's active interval.

theorem Papers.Rockel2026XiBlest.extremal_raw_support_ae (b : ℝ) (hb : 0 < b) (v : ↑unitInterval) (hv : ↑v ∈ Set.Ioo 0 1) : have B := Verification.quadraticRawBand b ⋯; have t := ProbabilityTheory.unitQuantile B.marginal v; ∀ᵐ (u : ↑unitInterval), B.lower u ≤ ↑t ∧ ↑t ≤ B.lower u + B.width ↔ extremalLowerSwitch b hb v < ↑u ∧ ↑u < extremalUpperSwitch b hb v

For interior v, the raw band's closed-strip predicate agrees almost everywhere in u with the manuscript's open switching band.

noncomputable def Papers.Rockel2026XiBlest.extremalWidthDensity (b : ℝ) (hb : 0 < b) (x : Fin 2 → ↑unitInterval) : ℝ

The nonnegative reciprocal-width form of the density printed in the revision. Its equality with the copula measure is proved below.

Equations

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

theorem Papers.Rockel2026XiBlest.extremal_standardized_eq_width_of_support (b : ℝ) (hb : 0 < b) (v u : ↑unitInterval) (hv : ↑v ∈ Set.Ioo 0 1) (hs : have B := Verification.quadraticRawBand b ⋯; have t := ProbabilityTheory.unitQuantile B.marginal v; B.lower u ≤ ↑t ∧ ↑t ≤ B.lower u + B.width ↔ extremalLowerSwitch b hb v < ↑u ∧ ↑u < extremalUpperSwitch b hb v) : (Verification.quadraticRawBand b ⋯).standardizedDensity (u, v) = extremalWidthDensity b hb ![u, v]

Once their support predicates agree, the standardized density and the reciprocal-width source candidate agree pointwise.

noncomputable def Papers.Rockel2026XiBlest.extremalDerivativeDensity (b : ℝ) (hb : 0 < b) (x : Fin 2 → ↑unitInterval) : ℝ

The exact derivative-based expression appearing in the revised lemma.

Equations

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

theorem Papers.Rockel2026XiBlest.extremalDerivativeDensity_eq_width_of_interior (b : ℝ) (hb : 0 < b) (x : Fin 2 → ↑unitInterval) (hv : ↑(x 1) ∈ Set.Ioo 0 1) : extremalDerivativeDensity b hb x = extremalWidthDensity b hb x

theorem Papers.Rockel2026XiBlest.extremalDerivativeDensity_ae_eq_width (b : ℝ) (hb : 0 < b) : extremalDerivativeDensity b hb =ᵐ[MeasureTheory.volume] extremalWidthDensity b hb

The derivative-based formula and reciprocal-width candidate agree almost everywhere on the square; only the second-coordinate endpoints are excluded.

theorem Papers.Rockel2026XiBlest.extremalWidthDensity_nonneg (b : ℝ) (hb : 0 < b) (x : Fin 2 → ↑unitInterval) : 0 ≤ extremalWidthDensity b hb x

theorem Papers.Rockel2026XiBlest.extremalWidthDensity_measurable (b : ℝ) (hb : 0 < b) : Measurable (extremalWidthDensity b hb)

theorem Papers.Rockel2026XiBlest.extremalWidthDensity_ae_standardized (b : ℝ) (hb : 0 < b) : extremalWidthDensity b hb =ᵐ[MeasureTheory.volume] fun (x : Fin 2 → ↑unitInterval) => (Verification.quadraticRawBand b ⋯).standardizedDensity (x 0, x 1)

The source's reciprocal-width density candidate is the same Lebesgue density as the verified standardized-band witness, up to a null set of switching curves and response endpoints.

theorem Papers.Rockel2026XiBlest.extremal_toMeasure_widthDensity (b : ℝ) (hb : 0 < b) : (extremalCopula b ⋯).toMeasure = MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑unitInterval) => ENNReal.ofReal (extremalWidthDensity b hb x)

The revised manuscript's reciprocal-width expression is the density of the Xi–Blest copula measure, with equality of measures rather than merely a formal candidate formula.

theorem Papers.Rockel2026XiBlest.extremal_toMeasure_derivativeDensity (b : ℝ) (hb : 0 < b) : (extremalCopula b ⋯).toMeasure = MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑unitInterval) => ENNReal.ofReal (extremalDerivativeDensity b hb x)

The revised manuscript's derivative form of the density is the actual Xi–Blest copula density almost everywhere.