← Mathematical handbook

Equation (5.3): 1 - ξ(Q_A) = (3/2) J(w)

The conditional distribution of V given U = u under Q_A puts mass p(u) at A(u) and 1 - p(u) at B(u); by (2.2) 1 - ξ = 6 ∬ h (1 - h), and integrating out the response first gives p (1 - p) (B - A) = p (1 - p) w. With w' = 1 - 2p this is (3/2) J(w).

noncomputable def Papers.OrendayLaresRockel2026XiBeta.MedianSection.slopeData (s : MedianSection) : SlopeData

The slope data d = 1 - 2p = w' of the gap function of a median section.

Equations

• s.slopeData = { d := fun (u : ℝ) => 1 - 2 * s.p u, mono := ⋯, bdd := ⋯, integral_zero := ⋯ }

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.slopeData_d (s : MedianSection) (u : ℝ) : s.slopeData.d u = 1 - 2 * s.p u

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.slopeData_w (s : MedianSection) (u : ℝ) : s.slopeData.w u = s.gap u

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.slopeData_q (s : MedianSection) : s.slopeData.q = s.gap (1 / 2)

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.slopeData_abs_le (s : MedianSection) (u : ℝ) : u ∈ Set.Icc 0 1 → |u - 1 / 2| ≤ s.slopeData.w u

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.slopeData_J (s : MedianSection) : s.slopeData.J = 4 * ∫ (u : ℝ) in 0..1, s.p u * (1 - s.p u) * s.gap u

J(w) = ∫₀¹ w (1 - w'²) for the gap function of a median section.

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.measurable_kerR_uncurry (s : MedianSection) : Measurable fun (z : ↑unitInterval × ↑unitInterval) => s.kerR ↑z.1 ↑z.2

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.kerR_mul_one_sub (s : MedianSection) {v t : ℝ} (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : s.kerR v t * (1 - s.kerR v t) = s.p t * (1 - s.p t) * if s.A t ≤ v ∧ v < s.B t then 1 else 0

The product form of the kernel: k (1 - k) = p (1 - p) 1{A ≤ v < B}.

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.integral_indicator_AB (s : MedianSection) {u : ℝ} (hu0 : 0 ≤ u) (hu1 : u ≤ 1) : (∫ (v : ↑unitInterval), if s.A u ≤ ↑v ∧ ↑v < s.B u then 1 else 0) = s.B u - s.A u

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.integral_condCDF_sq_completion (s : MedianSection) (t : ↑unitInterval) : ∫ (u : ↑unitInterval), s.completion.conditionalCDF u t ^ 2 = ∫ (u : ↑unitInterval), s.kernelCDF t u ^ 2

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.integrable_integral_kernelCDF_sq (s : MedianSection) : MeasureTheory.Integrable (fun (t : ↑unitInterval) => ∫ (u : ↑unitInterval), s.kernelCDF t u ^ 2) MeasureTheory.volume

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.xi_completion_eq (s : MedianSection) : s.completion.chatterjeeXi = (6 * ∫ (t : ↑unitInterval) (u : ↑unitInterval), s.kernelCDF t u ^ 2) - 2

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.xi_completion (s : MedianSection) : s.completion.chatterjeeXi = 1 - 6 * ∫ (u : ℝ) in 0..1, s.p u * (1 - s.p u) * s.gap u

Equation (5.3), first form: 1 - ξ(Q_A) = 6 ∫₀¹ p (1 - p) w.

theorem Papers.OrendayLaresRockel2026XiBeta.MedianSection.one_sub_xi_completion (s : MedianSection) : 1 - s.completion.chatterjeeXi = 3 / 2 * s.slopeData.J

Equation (5.3): 1 - ξ(Q_A) = (3/2) J(w).